[commit: ghc] master: Fix the the pure unifier so that it unifies kinds (6c3045b)

[Simon Peyton Jones]

Repository : ssh://darcs.haskell.org//srv/darcs/ghc

On branch  : master

http://hackage.haskell.org/trac/ghc/changeset/6c3045b90fb28861fae826c8bbd53135d3f2a6ce

>---------------------------------------------------------------

commit 6c3045b90fb28861fae826c8bbd53135d3f2a6ce
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Mon May 14 14:05:48 2012 +0100

    Fix the the pure unifier so that it unifies kinds
    
    When unifying two type variables we must unify their kinds.
    The pure *matcher* was doing so, but the pure *unifier* was not.
    This patch fixes Trac #6015, where an instance lookup was failing
    when it should have succeeded.
    
    I removed a bunch of code aimed at support sub-kinding. It's
    tricky, ad-hoc, and I don't think its necessary any more.
    Anything we can do to simplify the sub-kinding story is welcome!

>---------------------------------------------------------------

 compiler/types/FunDeps.lhs |    4 +++
 compiler/types/Unify.lhs   |   50 +++++++++++++++----------------------------
 2 files changed, 22 insertions(+), 32 deletions(-)

diff --git a/compiler/types/FunDeps.lhs b/compiler/types/FunDeps.lhs
index 8a15813..31ef9cc 100644
--- a/compiler/types/FunDeps.lhs
+++ b/compiler/types/FunDeps.lhs
@@ -216,6 +216,10 @@ data Equation
 data FDEq = FDEq { fd_pos      :: Int -- We use '0' for the first position
                  , fd_ty_left  :: Type
                  , fd_ty_right :: Type }
+
+instance Outputable FDEq where
+  ppr (FDEq { fd_pos = p, fd_ty_left = tyl, fd_ty_right = tyr })
+    = parens (int p <> comma <+> ppr tyl <> comma <+> ppr tyr)
 \end{code}
 
 Given a bunch of predicates that must hold, such as
diff --git a/compiler/types/Unify.lhs b/compiler/types/Unify.lhs
index 50a0fcf..de4f3fe 100644
--- a/compiler/types/Unify.lhs
+++ b/compiler/types/Unify.lhs
@@ -516,36 +516,29 @@ uUnrefined subst tv1 ty2 (TyVarTy tv2)
   = uUnrefined subst tv1 ty' ty'
 
   | otherwise
-  -- So both are unrefined; next, see if the kinds force the direction
-  = case (k1_sub_k2, k2_sub_k1) of
-        (True,  True)  -> choose subst
-        (True,  False) -> bindTv subst tv2 ty1
-        (False, True)  -> bindTv subst tv1 ty2
-        (False, False) -> do
-            { subst' <- unify subst k1 k2
-            ; choose subst' }
-  where subst_kind = mkTvSubst (mkInScopeSet (tyVarsOfTypes [k1,k2])) subst
-        k1 = substTy subst_kind (tyVarKind tv1)
-        k2 = substTy subst_kind (tyVarKind tv2)
-        k1_sub_k2 = k1 `isSubKind` k2
-        k2_sub_k1 = k2 `isSubKind` k1
-        ty1 = TyVarTy tv1
-        bind subst tv ty = return $ extendVarEnv subst tv ty
-        choose subst = do
-             { b1 <- tvBindFlag tv1
-             ; b2 <- tvBindFlag tv2
-             ; case (b1, b2) of
-                 (BindMe, _)         -> bind subst tv1 ty2
-                 (Skolem, Skolem)    -> failWith (misMatch ty1 ty2)
-                 (Skolem, _)         -> bind subst tv2 ty1 }
+
+  = do {   -- So both are unrefined; unify the kinds
+       ; subst' <- unify subst (tyVarKind tv1) (tyVarKind tv2)
+
+           -- And then bind one or the other, 
+           -- depending on which is bindable
+	   -- NB: unlike TcUnify we do not have an elaborate sub-kinding 
+	   --     story.  That is relevant only during type inference, and
+           --     (I very much hope) is not relevant here.
+       ; b1 <- tvBindFlag tv1
+       ; b2 <- tvBindFlag tv2
+       ; let ty1 = TyVarTy tv1
+       ; case (b1, b2) of
+           (Skolem, Skolem) -> failWith (misMatch ty1 ty2)
+           (BindMe, _)      -> return (extendVarEnv subst' tv1 ty2)
+           (_, BindMe)      -> return (extendVarEnv subst' tv2 ty1) }
 
 uUnrefined subst tv1 ty2 ty2'	-- ty2 is not a type variable
   | tv1 `elemVarSet` niSubstTvSet subst (tyVarsOfType ty2')
   = failWith (occursCheck tv1 ty2)	-- Occurs check
-  | not (k2 `isSubKind` k1)
-  = failWith (kindMisMatch tv1 ty2)	-- Kind check
   | otherwise
-  = bindTv subst tv1 ty2		-- Bind tyvar to the synonym if poss
+  = do { subst' <- unify subst k1 k2
+       ; bindTv subst' tv1 ty2 }	-- Bind tyvar to the synonym if poss
   where
     k1 = tyVarKind tv1
     k2 = typeKind ty2'
@@ -626,13 +619,6 @@ lengthMisMatch tys1 tys2
   = sep [ptext (sLit "Can't match unequal length lists"), 
 	 nest 2 (ppr tys1), nest 2 (ppr tys2) ]
 
-kindMisMatch :: TyVar -> Type -> SDoc
-kindMisMatch tv1 t2
-  = vcat [ptext (sLit "Can't match kinds") <+> quotes (ppr (tyVarKind tv1)) <+> 
-	    ptext (sLit "and") <+> quotes (ppr (typeKind t2)),
-	  ptext (sLit "when matching") <+> quotes (ppr tv1) <+> 
-		ptext (sLit "with") <+> quotes (ppr t2)]
-
 occursCheck :: TyVar -> Type -> SDoc
 occursCheck tv ty
   = hang (ptext (sLit "Can't construct the infinite type"))