From: dimitris@microsoft.com Date: Wed, 6 Oct 2010 15:28:54 +0000 (+0000) Subject: Major bugfixing pass through the type checker X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=commitdiff_plain;h=67ed735fab12c12a1d48878d7bda33588c67fb78 Major bugfixing pass through the type checker --- diff --git a/compiler/typecheck/TcCanonical.lhs b/compiler/typecheck/TcCanonical.lhs index 2001c1e..f834a4c 100644 --- a/compiler/typecheck/TcCanonical.lhs +++ b/compiler/typecheck/TcCanonical.lhs @@ -259,6 +259,31 @@ canEq fl cv ty1 (TyConApp fn tys) | isSynFamilyTyCon fn, length tys == tyConArity fn = canEqLeaf fl cv (classify ty1) (FunCls fn tys) +canEq fl cv s1 s2 + | Just (t1a,t1b,t1c) <- splitCoPredTy_maybe s1, + Just (t2a,t2b,t2c) <- splitCoPredTy_maybe s2 + = do { (v1,v2,v3) <- if isWanted fl then + do { v1 <- newWantedCoVar t1a t2a + ; v2 <- newWantedCoVar t1b t2b + ; v3 <- newWantedCoVar t1c t2c + ; let res_co = mkCoPredCo (mkCoVarCoercion v1) + (mkCoVarCoercion v2) (mkCoVarCoercion v3) + ; setWantedCoBind cv res_co + ; return (v1,v2,v3) } + else let co_orig = mkCoVarCoercion cv + coa = mkCsel1Coercion co_orig + cob = mkCsel2Coercion co_orig + coc = mkCselRCoercion co_orig + in do { v1 <- newGivOrDerCoVar t1a t2a coa + ; v2 <- newGivOrDerCoVar t1b t2b cob + ; v3 <- newGivOrDerCoVar t1c t2c coc + ; return (v1,v2,v3) } + ; cc1 <- canEq fl v1 t1a t2a + ; cc2 <- canEq fl v2 t1b t2b + ; cc3 <- canEq fl v3 t1c t2c + ; return (cc1 `andCCan` cc2 `andCCan` cc3) } + + -- Split up an equality between function types into two equalities. canEq fl cv (FunTy s1 t1) (FunTy s2 t2) = do { (argv, resv) <- @@ -276,6 +301,34 @@ canEq fl cv (FunTy s1 t1) (FunTy s2 t2) ; cc2 <- canEq fl resv t1 t2 ; return (cc1 `andCCan` cc2) } +canEq fl cv (PredTy p1) (PredTy p2) = canEqPred p1 p2 + where canEqPred (IParam n1 t1) (IParam n2 t2) + | n1 == n2 + = if isWanted fl then + do { v <- newWantedCoVar t1 t2 + ; setWantedCoBind cv $ mkIParamPredCo n1 (mkCoVarCoercion cv) + ; canEq fl v t1 t2 } + else return emptyCCan -- DV: How to decompose given IP coercions? + + canEqPred (ClassP c1 tys1) (ClassP c2 tys2) + | c1 == c2 + = if isWanted fl then + do { vs <- zipWithM newWantedCoVar tys1 tys2 + ; setWantedCoBind cv $ mkClassPPredCo c1 (map mkCoVarCoercion vs) + ; andCCans <$> zipWith3M (canEq fl) vs tys1 tys2 + } + else return emptyCCan + -- How to decompose given dictionary (and implicit parameter) coercions? + -- You may think that the following is right: + -- let cos = decomposeCo (length tys1) (mkCoVarCoercion cv) + -- in zipWith3M newGivOrDerCoVar tys1 tys2 cos + -- But this assumes that the coercion is a type constructor-based + -- coercion, and not a PredTy (ClassP cn cos) coercion. So we chose + -- to not decompose these coercions. We have to get back to this + -- when we clean up the Coercion API. + + canEqPred p1 p2 = misMatchErrorTcS fl (mkPredTy p1) (mkPredTy p2) + canEq fl cv (TyConApp tc1 tys1) (TyConApp tc2 tys2) | isAlgTyCon tc1 && isAlgTyCon tc2 @@ -312,9 +365,10 @@ canEq fl cv ty1 ty2 ; cc2 <- canEq fl cv2 t1 t2 ; return (cc1 `andCCan` cc2) } -canEq fl _ s1@(ForAllTy {}) s2@(ForAllTy {}) - | Wanted {} <- fl - = misMatchErrorTcS fl s1 s2 +canEq fl _ s1@(ForAllTy {}) s2@(ForAllTy {}) + | tcIsForAllTy s1, tcIsForAllTy s2, + Wanted {} <- fl + = misMatchErrorTcS fl s1 s2 | otherwise = do { traceTcS "Ommitting decomposition of given polytype equality" (pprEq s1 s2) ; return emptyCCan } @@ -322,9 +376,10 @@ canEq fl _ s1@(ForAllTy {}) s2@(ForAllTy {}) -- Finally expand any type synonym applications. canEq fl cv ty1 ty2 | Just ty1' <- tcView ty1 = canEq fl cv ty1' ty2 canEq fl cv ty1 ty2 | Just ty2' <- tcView ty2 = canEq fl cv ty1 ty2' - canEq fl _ ty1 ty2 = misMatchErrorTcS fl ty1 ty2 + + \end{code} Note [Equality between type applications] diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs index c3d7a9e..807dd61 100644 --- a/compiler/typecheck/TcInteract.lhs +++ b/compiler/typecheck/TcInteract.lhs @@ -1,7 +1,7 @@ \begin{code} module TcInteract ( solveInteract, AtomicInert, - InertSet, emptyInert, extendInertSet, extractUnsolved, solveOne, + InertSet, emptyInert, updInertSet, extractUnsolved, solveOne, listToWorkList ) where @@ -44,7 +44,7 @@ import FastString ( sLit ) import DynFlags \end{code} -Note [InsertSet invariants] +Note [InertSet invariants] ~~~~~~~~~~~~~~~~~~~~~~~~~~~ An InertSet is a bag of canonical constraints, with the following invariants: @@ -81,18 +81,39 @@ now we do not distinguish between given and solved constraints. Note that we must switch wanted inert items to given when going under an implication constraint (when in top-level inference mode). +Note [InertSet FlattenSkolemEqClass] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +The inert_fsks field of the inert set contains an "inverse map" of all the +flatten skolem equalities in the inert set. For instance, if inert_cts looks +like this: + + fsk1 ~ fsk2 + fsk3 ~ fsk2 + fsk4 ~ fsk5 + +Then, the inert_fsks fields holds the following map: + fsk2 |-> { fsk1, fsk3 } + fsk5 |-> { fsk4 } +Along with the necessary coercions to convert fsk1 and fsk3 back to fsk2 +and fsk4 back to fsk5. Hence, the invariants of the inert_fsks field are: + + (a) All TcTyVars in the domain and range of inert_fsks are flatten skolems + (b) All TcTyVars in the domain of inert_fsk occur naked as rhs in some + equalities of inert_cts + (c) For every mapping fsk1 |-> { (fsk2,co), ... } it must be: + co : fsk2 ~ fsk1 + +The role of the inert_fsks is to make it easy to maintain the equivalence +class of each flatten skolem, which is much needed to correctly do spontaneous +solving. See Note [Loopy Spontaneous Solving] \begin{code} -- See Note [InertSet invariants] data InertSet = IS { inert_cts :: Bag.Bag CanonicalCt , inert_fsks :: Map.Map TcTyVar [(TcTyVar,Coercion)] } --- inert_fsks contains the *FlattenSkolem* equivalence classes. --- inert_fsks extra invariants: --- (a) all TcTyVars in the domain and range of inert_fsks are flatten skolems --- (b) for every mapping tv1 |-> (tv2,co), co : tv2 ~ tv1 + -- See Note [InertSet FlattenSkolemEqClass] --- newtype InertSet = IS (Bag.Bag CanonicalCt) instance Outputable InertSet where ppr is = vcat [ vcat (map ppr (Bag.bagToList $ inert_cts is)) , vcat (map (\(v,rest) -> ppr v <+> text "|->" <+> hsep (map (ppr.fst) rest)) @@ -100,20 +121,9 @@ instance Outputable InertSet where ) ] - - emptyInert :: InertSet emptyInert = IS { inert_cts = Bag.emptyBag, inert_fsks = Map.empty } - -extendInertSet :: InertSet -> AtomicInert -> InertSet --- Simply extend the bag of constraints rebuilding an inert set -extendInertSet (IS { inert_cts = cts - , inert_fsks = fsks }) item - = IS { inert_cts = cts `Bag.snocBag` item - , inert_fsks = fsks } - - updInertSet :: InertSet -> AtomicInert -> InertSet -- Introduces an element in the inert set for the first time updInertSet (IS { inert_cts = cts, inert_fsks = fsks }) @@ -125,13 +135,13 @@ updInertSet (IS { inert_cts = cts, inert_fsks = fsks }) FlatSkol {} <- tcTyVarDetails tv2 = let cts' = cts `Bag.snocBag` item fsks' = Map.insertWith (++) tv2 [(tv1, mkCoVarCoercion cv)] fsks + -- See Note [InertSet FlattenSkolemEqClass] in IS { inert_cts = cts', inert_fsks = fsks' } updInertSet (IS { inert_cts = cts , inert_fsks = fsks }) item = let cts' = cts `Bag.snocBag` item in IS { inert_cts = cts', inert_fsks = fsks } - foldlInertSetM :: (Monad m) => (a -> AtomicInert -> m a) -> a -> InertSet -> m a foldlInertSetM k z (IS { inert_cts = cts }) = Bag.foldlBagM k z cts @@ -143,7 +153,7 @@ extractUnsolved is@(IS {inert_cts = cts}) getFskEqClass :: InertSet -> TcTyVar -> [(TcTyVar,Coercion)] --- Precondition: tv is a FlatSkol +-- Precondition: tv is a FlatSkol. See Note [InertSet FlattenSkolemEqClass] getFskEqClass (IS { inert_cts = cts, inert_fsks = fsks }) tv = case lkpTyEqCanByLhs of Nothing -> fromMaybe [] (Map.lookup tv fsks) @@ -427,7 +437,15 @@ spontaneousSolveStage workItem inerts , sr_inerts = inerts , sr_stop = Stop } } -{-- + +{-- This is all old code, but does not quite work now. The problem is that due to + Note [Loopy Spontaneous Solving] we may have unflattened a type, to be able to + perform a sneaky unification. This unflattening means that we may have to recanonicalize + a given (solved) equality, this is why the result of trySpontaneousSolve is now a list + of constraints (instead of an atomic solved constraint). We would have to react all of + them once again with the worklist but that is very tiresome. Instead we throw them back + in the worklist. + | isWantedCt workItem -- Original was wanted we have now made him given so -- we have to ineract him with the inerts again because @@ -522,8 +540,42 @@ where (fsk := E alpha, on the side). Now, if we spontaneously *solve* it and keep it as wanted. In inference mode we'll end up quantifying over (alpha ~ Maybe (E alpha)) Hence, 'solveWithIdentity' performs a small occurs check before -actually solving. But this occurs check *must look through* flatten -skolems. +actually solving. But this occurs check *must look through* flatten skolems. + +However, it may be the case that the flatten skolem in hand is equal to some other +flatten skolem whith *does not* mention our unification variable. Here's a typical example: + +Original wanteds: + g: F alpha ~ F beta + w: alpha ~ F alpha +After canonicalization: + g: F beta ~ f1 + g: F alpha ~ f1 + w: alpha ~ f2 + g: F alpha ~ f2 +After some reactions: + g: f1 ~ f2 + g: F beta ~ f1 + w: alpha ~ f2 + g: F alpha ~ f2 +At this point, we will try to spontaneously solve (alpha ~ f2) which remains as yet unsolved. +We will look inside f2, which immediately mentions (F alpha), so it's not good to unify! However +by looking at the equivalence class of the flatten skolems, we can see that it is fine to +unify (alpha ~ f1) which solves our goals! + +A similar problem happens because of other spontaneous solving. Suppose we have the +following wanteds, arriving in this exact order: + (first) w: beta ~ alpha + (second) w: alpha ~ fsk + (third) g: F beta ~ fsk +Then, we first spontaneously solve the first constraint, making (beta := alpha), and having +(beta ~ alpha) as given. *Then* we encounter the second wanted (alpha ~ fsk). "fsk" does not +obviously mention alpha, so naively we can also spontaneously solve (alpha := fsk). But +that is wrong since fsk mentions beta, which has already secretly been unified to alpha! + +To avoid this problem, the same occurs check must unveil rewritings that can happen because +of spontaneously having solved other constraints. + Note [Avoid double unifications] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -559,8 +611,8 @@ solveWithIdentity :: InertSet -- See [New Wanted Superclass Work] to see why we do this for *given* as well solveWithIdentity inerts cv gw tv xi | not (isGiven gw) - = do { m <- passOccursCheck inerts tv xi - ; case m of + = do { tybnds <- getTcSTyBindsBag + ; case occ_check_ok tybnds xi of Nothing -> return Nothing Just (xi_unflat,coi) -- coi : xi_unflat ~ xi -> do { traceTcS "Sneaky unification:" $ @@ -579,7 +631,8 @@ solveWithIdentity inerts cv gw tv xi (singleCCan (CTyEqCan { cc_id = cv_given , cc_flavor = mkGivenFlavor gw UnkSkol , cc_tyvar = tv, cc_rhs = xi } - -- xi, *not* xi_unflat! + -- xi, *not* xi_unflat because + -- xi_unflat may require flattening! ), co) ; case gw of Wanted {} -> setWantedCoBind cv co @@ -588,128 +641,83 @@ solveWithIdentity inerts cv gw tv xi -- See Note [Avoid double unifications] - -- The reason that we create a new given variable (cv_given) instead of reusing cv - -- is because we do not want to end up with coercion unification variables in the givens. - ; return (Just cts) } + ; return (Just cts) } } | otherwise = return Nothing - -passOccursCheck :: InertSet -> TcTyVar -> TcType -> TcS (Maybe (TcType,CoercionI)) --- passOccursCheck inerts tv ty --- Traverse the type and make sure that 'tv' does not appear under --- some flatten skolem. If it appears under some flatten skolem --- look in that flatten skolem equivalence class to see if you can --- find a different flatten skolem to use, which does not mention the --- variable. --- Postcondition: Just (ty',coi) <- passOccursCheck tv ty --- coi :: ty' ~ ty --- NB: I believe there is no need to do the tcView thing here -passOccursCheck is tv (TyConApp tc tys) - = do { tys_mbs <- mapM (passOccursCheck is tv) tys - ; case allMaybes tys_mbs of - Nothing -> return Nothing - Just tys_cois -> - let (tys',cois') = unzip tys_cois - in return $ - Just (TyConApp tc tys', mkTyConAppCoI tc cois') - } -passOccursCheck is tv (PredTy sty) - = do { sty_mb <- passOccursCheckPred tv sty - ; case sty_mb of - Nothing -> return Nothing - Just (sty',coi) -> return (Just (PredTy sty', coi)) - } - where passOccursCheckPred tv (ClassP cn tys) - = do { tys_mbs <- mapM (passOccursCheck is tv) tys - ; case allMaybes tys_mbs of - Nothing -> return Nothing - Just tys_cois -> - let (tys', cois') = unzip tys_cois - in return $ - Just (ClassP cn tys', mkClassPPredCoI cn cois') - } - passOccursCheckPred tv (IParam nm ty) - = do { mty <- passOccursCheck is tv ty - ; case mty of - Nothing -> return Nothing - Just (ty',co') - -> return (Just (IParam nm ty', - mkIParamPredCoI nm co')) - } - passOccursCheckPred tv (EqPred ty1 ty2) - = do { mty1 <- passOccursCheck is tv ty1 - ; mty2 <- passOccursCheck is tv ty2 - ; case (mty1,mty2) of - (Just (ty1',coi1), Just (ty2',coi2)) - -> return $ - Just (EqPred ty1' ty2', mkEqPredCoI coi1 coi2) - _ -> return Nothing - } - -passOccursCheck is tv (FunTy arg res) - = do { arg_mb <- passOccursCheck is tv arg - ; res_mb <- passOccursCheck is tv res - ; case (arg_mb,res_mb) of - (Just (arg',coiarg), Just (res',coires)) - -> return $ - Just (FunTy arg' res', mkFunTyCoI coiarg coires) - _ -> return Nothing - } - -passOccursCheck is tv (AppTy fun arg) - = do { fun_mb <- passOccursCheck is tv fun - ; arg_mb <- passOccursCheck is tv arg - ; case (fun_mb,arg_mb) of - (Just (fun',coifun), Just (arg',coiarg)) - -> return $ - Just (AppTy fun' arg', mkAppTyCoI coifun coiarg) - _ -> return Nothing - } - -passOccursCheck is tv (ForAllTy tv1 ty1) - = do { ty1_mb <- passOccursCheck is tv ty1 - ; case ty1_mb of - Nothing -> return Nothing - Just (ty1',coi) - -> return $ - Just (ForAllTy tv1 ty1', mkForAllTyCoI tv1 coi) - } - -passOccursCheck _is tv (TyVarTy tv') - | tv == tv' - = return Nothing - -passOccursCheck is tv (TyVarTy fsk) - | FlatSkol ty <- tcTyVarDetails fsk - = do { zty <- zonkFlattenedType ty -- Must zonk as it contains unif. vars - ; occ <- passOccursCheck is tv zty - ; case occ of - Nothing -> go_down_eq_class $ getFskEqClass is fsk - Just (zty',ico) -> return $ Just (zty',ico) - } - where go_down_eq_class [] = return Nothing - go_down_eq_class ((fsk1,co1):rest) - = do { occ1 <- passOccursCheck is tv (TyVarTy fsk1) - ; case occ1 of - Nothing -> go_down_eq_class rest - Just (ty1,co1i') - -> return $ Just (ty1, mkTransCoI co1i' (ACo co1)) } -passOccursCheck _is _tv ty - = return (Just (ty,IdCo ty)) - -{-- -Problematic situation: -~~~~~~~~~~~~~~~~~~~~~~ - Suppose we have a flatten skolem f1 := F f6 - Suppose we are chasing for 'alpha', and: - f6 := G alpha with eq.class f7,f8 - - Then we will return F f7 potentially. ---} - - + where occ_check_ok :: Bag.Bag (TcTyVar, TcType) -> TcType -> Maybe (TcType,CoercionI) + occ_check_ok ty_binds_bag ty = ok ty + where + -- @ok ty@ + -- Traverse @ty@ to make sure that @tv@ does not appear under some flatten skolem. + -- If it appears under some flatten skolem look in that flatten skolem equivalence class + -- (see Note [InertSet FlattenSkolemEqClass], [Loopy Spontaneous Solving]) to see if you + -- can find a different flatten skolem to use, that is, one that does not mention @tv@. + -- + -- Postcondition: Just (ty',coi) <- ok ty + -- coi :: ty' ~ ty + -- + -- NB: The returned type may not be flat! + -- + -- NB: There is no need to do the tcView thing here to expand synonyms, because + -- expanded synonyms have the same or fewer variables than their expanded definitions, + -- but never more. + -- See Note [Type synonyms and the occur check] in TcUnify for the handling of type synonyms. + ok this_ty@(TyConApp tc tys) + | Just tys_cois <- allMaybes (map ok tys) + = let (tys',cois') = unzip tys_cois + in Just (TyConApp tc tys', mkTyConAppCoI tc cois') + | isSynTyCon tc, Just ty_expanded <- tcView this_ty + = ok ty_expanded + ok (PredTy sty) + | Just (sty',coi) <- ok_pred sty + = Just (PredTy sty', coi) + where ok_pred (ClassP cn tys) + | Just tys_cois <- allMaybes $ map ok tys + = let (tys', cois') = unzip tys_cois + in Just (ClassP cn tys', mkClassPPredCoI cn cois') + ok_pred (IParam nm ty) + | Just (ty',co') <- ok ty + = Just (IParam nm ty', mkIParamPredCoI nm co') + ok_pred (EqPred ty1 ty2) + | Just (ty1',coi1) <- ok ty1, Just (ty2',coi2) <- ok ty2 + = Just (EqPred ty1' ty2', mkEqPredCoI coi1 coi2) + ok_pred _ = Nothing + ok (FunTy arg res) + | Just (arg', coiarg) <- ok arg, Just (res', coires) <- ok res + = Just (FunTy arg' res', mkFunTyCoI coiarg coires) + ok (AppTy fun arg) + | Just (fun', coifun) <- ok fun, Just (arg', coiarg) <- ok arg + = Just (AppTy fun' arg', mkAppTyCoI coifun coiarg) + ok (ForAllTy tv1 ty1) + -- WARNING: What if it is a (t1 ~ t2) => t3? It's not handled properly at the moment. + | Just (ty1', coi) <- ok ty1 + = Just (ForAllTy tv1 ty1', mkForAllTyCoI tv1 coi) + + -- Variable cases + ok this_ty@(TyVarTy tv') + | not $ isTcTyVar tv' = Just (this_ty, IdCo this_ty) -- Bound variable + | tv == tv' = Nothing -- Occurs check error + -- Flatten skolem + ok (TyVarTy fsk) | FlatSkol zty <- tcTyVarDetails fsk + = case ok zty of + Nothing -> go_down_eq_class $ getFskEqClass inerts fsk + Just (zty',ico) -> Just (zty',ico) + where go_down_eq_class [] = Nothing + go_down_eq_class ((fsk1,co1):rest) + = case ok (TyVarTy fsk1) of + Nothing -> go_down_eq_class rest + Just (ty1,co1i') -> Just (ty1, mkTransCoI co1i' (ACo co1)) + -- Finally, check if bound already + ok this_ty@(TyVarTy tv0) + = case Bag.foldlBag find_bind Nothing ty_binds_bag of + Nothing -> Just (this_ty, IdCo this_ty) + Just ty0 -> ok ty0 + where find_bind Nothing (tvx,tyx) | tv0 == tvx = Just tyx + find_bind m _ = m + -- Fall through + ok _ty = Nothing \end{code} @@ -972,10 +980,12 @@ doInteractWithInert | fl2 `canRewrite` fl1 && tv2 `elemVarSet` tyVarsOfType xi1 = do { rewritten_eq <- rewriteEqRHS (cv2,tv2,xi2) (cv1,fl1,tv1,xi1) ; mkIRContinue workItem DropInert rewritten_eq } --- Finally, if workitem is a flatten equivalence class constraint and the --- inert is a wanted constraints, even when the workitem cannot rewrite the --- inert, drop the inert out because you may have to reconsider solving him --- using the equivalence class you created. + +-- Finally, if workitem is a Flatten Equivalence Class constraint and the +-- inert is a wanted constraint, even when the workitem cannot rewrite the +-- inert, drop the inert out because you may have to reconsider solving the +-- inert *using* the equivalence class you created. See note [Loopy Spontaneous Solving] +-- and [InertSet FlattenSkolemEqClass] | not $ isGiven fl1, -- The inert is wanted or derived isMetaTyVar tv1, -- and has a unification variable lhs @@ -984,7 +994,7 @@ doInteractWithInert = mkIRContinue workItem DropInert (singletonWorkList inert) --- Fall-through case for all other cases +-- Fall-through case for all other situations doInteractWithInert _ workItem = noInteraction workItem -------------------------------------------- @@ -1108,15 +1118,6 @@ rewriteEqLHS which (co1,xi1) (cv2,gw,xi2) mkSymCoercion co1 `mkTransCoercion` mkCoVarCoercion cv2 ; mkCanonical gw cv2' } --- -> --- if isWanted gw then --- do { cv2' <- newWantedCoVar xi1 xi2 --- ; setWantedCoBind cv2 $ --- co1 `mkTransCoercion` mkCoVarCoercion cv2' --- ; return cv2' } --- else newGivOrDerCoVar xi1 xi2 $ --- mkSymCoercion co1 `mkTransCoercion` mkCoVarCoercion cv2 --- ; mkCanonical gw cv2' } solveOneFromTheOther :: (EvVar, CtFlavor) -> CanonicalCt -> TcS InteractResult diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs index c986811..f8b357a 100644 --- a/compiler/typecheck/TcSMonad.lhs +++ b/compiler/typecheck/TcSMonad.lhs @@ -31,11 +31,10 @@ module TcSMonad ( getInstEnvs, getFamInstEnvs, -- Getting the environments getTopEnv, getGblEnv, getTcEvBinds, getUntouchablesTcS, - getTcEvBindsBag, getTcSContext, getTcSTyBinds, + getTcEvBindsBag, getTcSContext, getTcSTyBinds, getTcSTyBindsBag, newFlattenSkolemTy, -- Flatten skolems - zonkFlattenedType, instDFunTypes, -- Instantiation @@ -434,6 +433,7 @@ runTcS context untouch tcs ; return (res, evBindMapBinds ev_binds) } where do_unification (tv,ty) = TcM.writeMetaTyVar tv ty + nestImplicTcS :: EvBindsVar -> TcTyVarSet -> TcS a -> TcS a nestImplicTcS ref untouch tcs @@ -475,6 +475,10 @@ getTcEvBinds = TcS (return . tcs_ev_binds) getTcSTyBinds :: TcS (IORef (Bag (TcTyVar, TcType))) getTcSTyBinds = TcS (return . tcs_ty_binds) +getTcSTyBindsBag :: TcS (Bag (TcTyVar, TcType)) +getTcSTyBindsBag = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef) + + getTcEvBindsBag :: TcS EvBindMap getTcEvBindsBag = do { EvBindsVar ev_ref _ <- getTcEvBinds @@ -577,26 +581,6 @@ newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty mkTcTyVar name (typeKind ty) (FlatSkol ty) } - -zonkFlattenedType :: TcType -> TcS TcType -zonkFlattenedType ty = wrapTcS (TcM.zonkTcType ty) - - -{-- -tyVarsOfUnflattenedType :: TcType -> TcTyVarSet --- A version of tyVarsOfType which looks through flatSkols -tyVarsOfUnflattenedType ty - = foldVarSet (unionVarSet . do_tv) emptyVarSet (tyVarsOfType ty) - where - do_tv :: TyVar -> TcTyVarSet - do_tv tv = ASSERT( isTcTyVar tv) - case tcTyVarDetails tv of - FlatSkol _ ty -> tyVarsOfUnflattenedType ty - _ -> unitVarSet tv ---} - - - -- Instantiations -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs index d8be2d1..48258ed 100644 --- a/compiler/typecheck/TcSimplify.lhs +++ b/compiler/typecheck/TcSimplify.lhs @@ -405,7 +405,7 @@ simplifySuperClass self wanteds ; (unsolved, ev_binds) <- runTcS SimplCheck emptyVarSet $ do { can_self <- canGivens loc [self] - ; let inert = foldlBag extendInertSet emptyInert can_self + ; let inert = foldlBag updInertSet emptyInert can_self -- No need for solveInteract; we know it's inert ; solveWanteds inert wanteds } diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs index d73869f..2b9838b 100644 --- a/compiler/typecheck/TcUnify.lhs +++ b/compiler/typecheck/TcUnify.lhs @@ -46,6 +46,8 @@ import Name import ErrUtils import BasicTypes import Bag + +import Maybes ( allMaybes ) import Util import Outputable import FastString @@ -575,7 +577,16 @@ uType_np origin orig_ty1 orig_ty2 -- Predicates go origin (PredTy p1) (PredTy p2) = uPred origin p1 p2 - -- Functions; just check the two parts + -- Coercion functions: (t1a ~ t1b) => t1c ~ (t2a ~ t2b) => t2c + go origin ty1 ty2 + | Just (t1a,t1b,t1c) <- splitCoPredTy_maybe ty1, + Just (t2a,t2b,t2c) <- splitCoPredTy_maybe ty2 + = do { co1 <- uType origin t1a t2a + ; co2 <- uType origin t1b t2b + ; co3 <- uType origin t1c t2c + ; return $ mkCoPredCoI co1 co2 co3 } + + -- Functions (or predicate functions) just check the two parts go origin (FunTy fun1 arg1) (FunTy fun2 arg2) = do { coi_l <- uType origin fun1 fun2 ; coi_r <- uType origin arg1 arg2 @@ -607,7 +618,8 @@ uType_np origin orig_ty1 orig_ty2 ; return $ mkAppTyCoI coi_s coi_t } go _ ty1 ty2 - | isSigmaTy ty1 || isSigmaTy ty2 + | tcIsForAllTy ty1 || tcIsForAllTy ty2 +{-- | isSigmaTy ty1 || isSigmaTy ty2 --} = unifySigmaTy origin ty1 ty2 -- Anything else fails @@ -909,27 +921,65 @@ checkTauTvUpdate :: TcTyVar -> TcType -> TcM (Maybe TcType) checkTauTvUpdate tv ty = do { ty' <- zonkTcType ty - ; if ok ty' && (typeKind ty' `isSubKind` tyVarKind tv) - then return (Just ty') + ; if typeKind ty' `isSubKind` tyVarKind tv then + case ok ty' of + Nothing -> return Nothing + Just ty'' -> return (Just ty'') else return Nothing } - where ok :: TcType -> Bool - -- Check that (a) tv is not among the free variables of - -- the type and that (b) the type is type-family-free. - -- Reason: Note [Type family sharing] - ok ty1 | Just ty1' <- tcView ty1 = ok ty1' - ok (TyVarTy tv') = not (tv == tv') - ok (TyConApp tc tys) = all ok tys && not (isSynFamilyTyCon tc) - ok (PredTy sty) = ok_pred sty - ok (FunTy arg res) = ok arg && ok res - ok (AppTy fun arg) = ok fun && ok arg - ok (ForAllTy _tv1 ty1) = ok ty1 - - ok_pred (IParam _ ty) = ok ty - ok_pred (ClassP _ tys) = all ok tys - ok_pred (EqPred ty1 ty2) = ok ty1 && ok ty2 + + where ok :: TcType -> Maybe TcType + 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 (PredTy sty) | Just sty' <- ok_pred sty = Just (PredTy sty') + 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 + + ok_pred (IParam nm ty) | Just ty' <- ok ty = Just (IParam nm ty') + ok_pred (ClassP cl tys) + | Just tys' <- allMaybes (map ok tys) + = Just (ClassP cl tys') + ok_pred (EqPred ty1 ty2) + | Just ty1' <- ok ty1, Just ty2' <- ok ty2 + = Just (EqPred ty1' ty2') + -- Fall-through + ok_pred _pty = Nothing \end{code} +Note [Type synonyms and the occur check] +~~~~~~~~~~~~~~~~~~~~ +Generally speaking we need to update a variable with type synonyms not expanded, which +improves later error messages, except for when looking inside a type synonym may help resolve +a spurious occurs check error. Consider: + type A a = () + + f :: (A a -> a -> ()) -> () + f = \ _ -> () + + x :: () + x = f (\ x p -> p x) + +We will eventually get a constraint of the form t ~ A t. The ok function above will +properly expand the type (A t) to just (), which is ok to be unified with t. If we had +unified with the original type A t, we would lead the type checker into an infinite loop. + +Hence, if the occurs check fails for a type synonym application, then (and *only* then), +the ok function expands the synonym to detect opportunities for occurs check success using +the underlying definition of the type synonym. + +The same applies later on in the constraint interaction code; see TcInteract, +function @occ_check_ok@. + + Note [Type family sharing] ~~~~~~~~~~~~~~ We must avoid eagerly unifying type variables to types that contain function symbols, diff --git a/compiler/types/Coercion.lhs b/compiler/types/Coercion.lhs index 8249ed9..f7c48f4 100644 --- a/compiler/types/Coercion.lhs +++ b/compiler/types/Coercion.lhs @@ -44,8 +44,9 @@ module Coercion ( mkForAllCoercion, mkInstsCoercion, mkUnsafeCoercion, mkNewTypeCoercion, mkFamInstCoercion, mkAppsCoercion, mkCsel1Coercion, mkCsel2Coercion, mkCselRCoercion, - - mkCoVarCoercion, + + mkClassPPredCo, mkIParamPredCo, + mkCoVarCoercion, mkCoPredCo, unsafeCoercionTyCon, symCoercionTyCon, @@ -68,7 +69,7 @@ module Coercion ( mkTyConAppCoI, mkAppTyCoI, mkFunTyCoI, mkForAllTyCoI, fromCoI, - mkClassPPredCoI, mkIParamPredCoI, mkEqPredCoI + mkClassPPredCoI, mkIParamPredCoI, mkEqPredCoI, mkCoPredCoI ) where @@ -282,6 +283,11 @@ mkCoPredTy s t r = ASSERT( not (co_var `elemVarSet` tyVarsOfType r) ) where co_var = mkWildCoVar (mkCoKind s t) +mkCoPredCo :: Coercion -> Coercion -> Coercion -> Coercion +-- Creates a coercion between (s1~t1) => r1 and (s2~t2) => r2 +mkCoPredCo = mkCoPredTy + + splitCoPredTy_maybe :: Type -> Maybe (Type, Type, Type) splitCoPredTy_maybe ty | Just (cv,r) <- splitForAllTy_maybe ty @@ -347,7 +353,7 @@ mkTyConCoercion con cos = mkTyConApp con cos -- | Make a function 'Coercion' between two other 'Coercion's mkFunCoercion :: Coercion -> Coercion -> Coercion -mkFunCoercion co1 co2 = mkFunTy co1 co2 +mkFunCoercion co1 co2 = mkFunTy co1 co2 -- NB: Handles correctly the forall for eqpreds! -- | Make a 'Coercion' which binds a variable within an inner 'Coercion' mkForAllCoercion :: Var -> Coercion -> Coercion @@ -444,6 +450,16 @@ mkFamInstCoercion name tvs family inst_tys rep_tycon desc = CoAxiom { co_ax_tvs = tvs , co_ax_lhs = mkTyConApp family inst_tys , co_ax_rhs = mkTyConApp rep_tycon (mkTyVarTys tvs) } + + +mkClassPPredCo :: Class -> [Coercion] -> Coercion +mkClassPPredCo cls = (PredTy . ClassP cls) + +mkIParamPredCo :: (IPName Name) -> Coercion -> Coercion +mkIParamPredCo ipn = (PredTy . IParam ipn) + + + \end{code} @@ -680,6 +696,11 @@ mkIParamPredCoI ipn = liftCoI (PredTy . IParam ipn) -- | Smart constructor for type equality 'Coercion's on 'CoercionI'. Similar to 'mkClassPPredCoI' mkEqPredCoI :: CoercionI -> CoercionI -> CoercionI mkEqPredCoI = liftCoI2 (\t1 t2 -> PredTy (EqPred t1 t2)) + +mkCoPredCoI :: CoercionI -> CoercionI -> CoercionI -> CoercionI +mkCoPredCoI coi1 coi2 coi3 = mkFunTyCoI (mkEqPredCoI coi1 coi2) coi3 + + \end{code} %************************************************************************