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 <[email protected]> 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")) _______________________________________________ Cvs-ghc mailing list [email protected] http://www.haskell.org/mailman/listinfo/cvs-ghc
