Fix the the pure unifier so that it unifies kinds
authorSimon Peyton Jones <simonpj@microsoft.com>
Mon, 14 May 2012 13:05:48 +0000 (14:05 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Mon, 14 May 2012 13:05:48 +0000 (14:05 +0100)
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
compiler/types/Unify.lhs

index 8a15813..31ef9cc 100644 (file)
@@ -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
index 50a0fcf..de4f3fe 100644 (file)
@@ -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"))