Repository : ssh://darcs.haskell.org//srv/darcs/ghc On branch : master
http://hackage.haskell.org/trac/ghc/changeset/242fc5606d5a94205949f8bd58bea348c247d863 >--------------------------------------------------------------- commit 242fc5606d5a94205949f8bd58bea348c247d863 Author: Simon Peyton Jones <simo...@microsoft.com> Date: Fri Oct 19 01:22:20 2012 +0100 Some refactoring of the occurs check in TcUnify I was experimenting with allowing unification with a type variable when there are type functions in the type; but that led to strangely worse error messages (See Note [Conservative unification check]) in TcUnify. I don't quite understand why, but the simple thing for now is to maintain the same behaviour. I tidied up the code a bit though. >--------------------------------------------------------------- compiler/typecheck/TcUnify.lhs | 107 ++++++++++++++++++++++------------------ 1 files changed, 59 insertions(+), 48 deletions(-) diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs index 18c77d7..3a13b9c 100644 --- a/compiler/typecheck/TcUnify.lhs +++ b/compiler/typecheck/TcUnify.lhs @@ -766,22 +766,19 @@ uUnfilledVar origin swapped tv1 details1 non_var_ty2 -- ty2 is not a type varia MetaTv { mtv_info = TauTv, mtv_ref = ref1 } -> do { mb_ty2' <- checkTauTvUpdate tv1 non_var_ty2 ; case mb_ty2' of - Nothing -> do { traceTc "Occ/kind defer" (ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1) - $$ ppr non_var_ty2 $$ ppr (typeKind non_var_ty2)) - ; defer } Just ty2' -> updateMeta tv1 ref1 ty2' + Nothing -> do { traceTc "Occ/kind defer" + (ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1) + $$ ppr non_var_ty2 $$ ppr (typeKind non_var_ty2)) + ; defer } } _other -> do { traceTc "Skolem defer" (ppr tv1); defer } -- Skolems of all sorts where - defer | Just ty2' <- tcView non_var_ty2 -- Note [Avoid deferring] - -- non_var_ty2 isn't expanded yet - = uUnfilledVar origin swapped tv1 details1 ty2' - | otherwise - = unSwap swapped (uType_defer origin) (mkTyVarTy tv1) non_var_ty2 - -- Occurs check or an untouchable: just defer - -- NB: occurs check isn't necessarily fatal: - -- eg tv1 occured in type family parameter + defer = unSwap swapped (uType_defer origin) (mkTyVarTy tv1) non_var_ty2 + -- Occurs check or an untouchable: just defer + -- NB: occurs check isn't necessarily fatal: + -- eg tv1 occured in type family parameter ---------------- uUnfilledVars :: CtOrigin @@ -855,51 +852,65 @@ checkTauTvUpdate :: TcTyVar -> TcType -> TcM (Maybe TcType) -- sort matters out. checkTauTvUpdate tv ty - = do { ty' <- zonkTcType ty - ; sub_k <- unifyKindX (tyVarKind tv) (typeKind ty') + = do { ty1 <- zonkTcType ty + ; sub_k <- unifyKindX (tyVarKind tv) (typeKind ty1) ; case sub_k of - Nothing -> return Nothing - Just LT -> return Nothing - _ -> return (occurCheckExpand tv ty') } - -{- + Nothing -> return Nothing + Just LT -> return Nothing + _ | defer_me ty1 -- Quick test + -> -- Failed quick test so try harder + case occurCheckExpand tv ty1 of + Nothing -> return Nothing + Just ty2 | defer_me ty2 -> return Nothing + | otherwise -> return (Just ty2) + | otherwise -> return (Just ty1) } where - ok :: TcType -> Maybe TcType - -- This version of TcType.occurCheckExpand checked that ty does - -- not contain any type families, but that's no longer necessary: - -- See Note [Type family sharing] - -- - -- Checks that tv does not occur in the arg type - -- expanding type synonyms where necessary to make this so - -- eg type Phantom a = Bool - -- ok (tv -> Int) = Nothing - -- ok (x -> Int) = Just (x -> Int) - -- ok (Phantom tv -> Int) = Just (Bool -> Int) - ok (TyVarTy tv') | not (tv == tv') = Just (TyVarTy tv') - ok this_ty@(TyConApp tc tys) - | not (isSynFamilyTyCon tc), Just tys' <- allMaybes (map ok tys) - = Just (TyConApp tc tys') - | isSynTyCon tc, Just ty_expanded <- tcView this_ty - = ok ty_expanded -- See Note [Type synonyms and the occur check] - ok ty@(LitTy {}) = Just ty - ok (FunTy arg res) | Just arg' <- ok arg, Just res' <- ok res - = Just (FunTy arg' res') - ok (AppTy fun arg) | Just fun' <- ok fun, Just arg' <- ok arg - = Just (AppTy fun' arg') - ok (ForAllTy tv1 ty1) | Just ty1' <- ok ty1 = Just (ForAllTy tv1 ty1') - -- Fall-through - ok _ty = Nothing --} + defer_me :: TcType -> Bool + -- Checks for (a) occurrence of tv + -- (b) type family applicatios + -- See Note [Conservative unification check] + defer_me (LitTy {}) = False + defer_me (TyVarTy tv') = tv == tv' + defer_me (TyConApp tc tys) = isSynFamilyTyCon tc || any defer_me tys + defer_me (FunTy arg res) = defer_me arg || defer_me res + defer_me (AppTy fun arg) = defer_me fun || defer_me arg + defer_me (ForAllTy _ ty) = defer_me ty \end{code} -Note [Avoid deferring] -~~~~~~~~~~~~~~~~~~~~~~ -We try to avoid creating deferred constraints only for efficiency. -Example (Trac #4917) +Note [Conservative unification check] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +When unifying (tv ~ rhs), w try to avoid creating deferred constraints +only for efficiency. However, we do not unify (the defer_me check) if + a) There's an occurs check (tv is in fvs(rhs)) + b) There's a type-function call in 'rhs' + +If we fail defer_me we use occurCheckExpand to try to make it pass, +(see Note [Type synonyms and the occur check]) and then use defer_me +again to check. Example: Trac #4917) a ~ Const a b where type Const a b = a. We can solve this immediately, even when 'a' is a skolem, just by expanding the synonym. +We always defer type-function calls, even if it's be perfectly safe to +unify, eg (a ~ F [b]). Reason: this ensures that the constraint +solver gets to see, and hence simplify the type-function call, which +in turn might simplify the type of an inferred function. Test ghci046 +is a case in point. + +More mysteriously, test T7010 gave a horrible error + T7010.hs:29:21: + Couldn't match type `Serial (ValueTuple Float)' with `IO Float' + Expected type: (ValueTuple Vector, ValueTuple Vector) + Actual type: (ValueTuple Vector, ValueTuple Vector) +because an insoluble type function constraint got mixed up with +a soluble one when flattening. I never fully understood this, but +deferring type-function applications made it go away :-(. +T5853 also got a less-good error message with more aggressive +unification of type functions. + +Moreover the Note [Type family sharing] gives another reason, but +again I'm not sure if it's really valid. + Note [Type synonyms and the occur check] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Generally speaking we try to update a variable with type synonyms not _______________________________________________ Cvs-ghc mailing list Cvs-ghc@haskell.org http://www.haskell.org/mailman/listinfo/cvs-ghc
