X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcInteract.lhs;h=e3d71dd291200fee3e76d93cf7a9a66a4056f9ff;hb=daa3fb945909feb28d7623aa2a075663d31076f0;hp=807dd61ba54436010a2bc24f6251772fa6dd27ca;hpb=67ed735fab12c12a1d48878d7bda33588c67fb78;p=ghc-hetmet.git diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs index 807dd61..e3d71dd 100644 --- a/compiler/typecheck/TcInteract.lhs +++ b/compiler/typecheck/TcInteract.lhs @@ -15,6 +15,7 @@ import Type import TypeRep import Id +import VarEnv import Var import TcType @@ -35,7 +36,7 @@ import Outputable import TcRnTypes import TcErrors import TcSMonad -import qualified Bag as Bag +import Bag import qualified Data.Map as Map import Maybes @@ -478,17 +479,18 @@ spontaneousSolveStage workItem inerts -- * Nothing if we were not able to solve it -- * Just wi' if we solved it, wi' (now a "given") should be put in the work list. -- See Note [Touchables and givens] --- Note, just passing the inerts through for the skolem equivalence classes +-- NB: just passing the inerts through for the skolem equivalence classes trySpontaneousSolve :: WorkItem -> InertSet -> TcS (Maybe SWorkList) trySpontaneousSolve (CTyEqCan { cc_id = cv, cc_flavor = gw, cc_tyvar = tv1, cc_rhs = xi }) inerts + | isGiven gw + = return Nothing | Just tv2 <- tcGetTyVar_maybe xi = do { tch1 <- isTouchableMetaTyVar tv1 ; tch2 <- isTouchableMetaTyVar tv2 ; case (tch1, tch2) of (True, True) -> trySpontaneousEqTwoWay inerts cv gw tv1 tv2 (True, False) -> trySpontaneousEqOneWay inerts cv gw tv1 xi - (False, True) | tyVarKind tv1 `isSubKind` tyVarKind tv2 - -> trySpontaneousEqOneWay inerts cv gw tv2 (mkTyVarTy tv1) + (False, True) -> trySpontaneousEqOneWay inerts cv gw tv2 (mkTyVarTy tv1) _ -> return Nothing } | otherwise = do { tch1 <- isTouchableMetaTyVar tv1 @@ -504,9 +506,9 @@ trySpontaneousSolve _ _ = return Nothing trySpontaneousEqOneWay :: InertSet -> CoVar -> CtFlavor -> TcTyVar -> Xi -> TcS (Maybe SWorkList) -- tv is a MetaTyVar, not untouchable --- Precondition: kind(xi) is a sub-kind of kind(tv) trySpontaneousEqOneWay inerts cv gw tv xi - | not (isSigTyVar tv) || isTyVarTy xi + | not (isSigTyVar tv) || isTyVarTy xi, + typeKind xi `isSubKind` tyVarKind tv = solveWithIdentity inerts cv gw tv xi | otherwise = return Nothing @@ -517,16 +519,45 @@ trySpontaneousEqTwoWay :: InertSet -> CoVar -> CtFlavor -> TcTyVar -> TcTyVar -- Both tyvars are *touchable* MetaTyvars -- By the CTyEqCan invariant, k2 `isSubKind` k1 trySpontaneousEqTwoWay inerts cv gw tv1 tv2 - | k1 `eqKind` k2 + | k1 `isSubKind` k2 , nicer_to_update_tv2 = solveWithIdentity inerts cv gw tv2 (mkTyVarTy tv1) - | otherwise = ASSERT( k2 `isSubKind` k1 ) - solveWithIdentity inerts cv gw tv1 (mkTyVarTy tv2) + | k2 `isSubKind` k1 + = solveWithIdentity inerts cv gw tv1 (mkTyVarTy tv2) + | otherwise = return Nothing where k1 = tyVarKind tv1 k2 = tyVarKind tv2 nicer_to_update_tv2 = isSigTyVar tv1 || isSystemName (Var.varName tv2) \end{code} + +Note [Spontaneous solving and kind compatibility] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Note that our canonical constraints insist that only *given* equalities (tv ~ xi) +or (F xis ~ rhs) require the LHS and the RHS to have exactly the same kinds. + + - We have to require this because: + Given equalities can be freely used to rewrite inside + other types or constraints. + - We do not have to do the same for wanteds because: + First, wanted equations (tv ~ xi) where tv is a touchable unification variable + may have kinds that do not agree (the kind of xi must be a sub kind of the kind of tv). + Second, any potential kind mismatch will result in the constraint not being soluble, + which will be reported anyway. This is the reason that @trySpontaneousOneWay@ and + @trySpontaneousTwoWay@ will perform a kind compatibility check, and only then will + they proceed to @solveWithIdentity@. + +Caveat: + - Givens from higher-rank, such as: + type family T b :: * -> * -> * + type instance T Bool = (->) + + f :: forall a. ((T a ~ (->)) => ...) -> a -> ... + flop = f (...) True + Whereas we would be able to apply the type instance, we would not be able to + use the given (T Bool ~ (->)) in the body of 'flop' + Note [Loopy spontaneous solving] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider the original wanted: @@ -583,23 +614,17 @@ The spontaneous solver has to return a given which mentions the unified unificat variable *on the left* of the equality. Here is what happens if not: Original wanted: (a ~ alpha), (alpha ~ Int) We spontaneously solve the first wanted, without changing the order! - given : a ~ alpha [having unifice alpha := a] + given : a ~ alpha [having unified alpha := a] Now the second wanted comes along, but he cannot rewrite the given, so we simply continue. At the end we spontaneously solve that guy, *reunifying* [alpha := Int] -We avoid this problem by orienting the given so that the unification variable is on the left. -[Note that alternatively we could attempt to enforce this at canonicalization] +We avoid this problem by orienting the given so that the unification +variable is on the left. [Note that alternatively we could attempt to +enforce this at canonicalization] -Avoiding double unifications is yet another reason to disallow touchable unification variables -as RHS of type family equations: F xis ~ alpha. Consider having already spontaneously solved -a wanted (alpha ~ [b]) by setting alpha := [b]. So the inert set looks like: - given : alpha ~ [b] -And now a new wanted (F tau ~ alpha) comes along. Since it does not react with anything -we will be left with a constraint (F tau ~ alpha) that must cause a unification of -(alpha := F tau) at some point (either in spontaneous solving, or at the end). But alpha -is *already* unified so we must not do anything to it. By disallowing naked touchables in -the RHS of constraints (in favor of introduced flatten skolems) we do not have to worry at -all about unifying or spontaneously solving (F xis ~ alpha) by unification. +See also Note [No touchables as FunEq RHS] in TcSMonad; avoiding +double unifications is the main reason we disallow touchable +unification variables as RHS of type family equations: F xis ~ alpha. \begin{code} ---------------- @@ -608,117 +633,122 @@ solveWithIdentity :: InertSet -> TcS (Maybe SWorkList) -- Solve with the identity coercion -- Precondition: kind(xi) is a sub-kind of kind(tv) --- See [New Wanted Superclass Work] to see why we do this for *given* as well +-- Precondition: CtFlavor is Wanted or Derived +-- See [New Wanted Superclass Work] to see why solveWithIdentity +-- must work for Derived as well as Wanted solveWithIdentity inerts cv gw tv xi - | not (isGiven gw) - = 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:" $ + = do { tybnds <- getTcSTyBindsMap + ; case occurCheck tybnds inerts tv xi of + Nothing -> return Nothing + Just (xi_unflat,coi) -> solve_with xi_unflat coi } + where + solve_with xi_unflat coi -- coi : xi_unflat ~ xi + = do { traceTcS "Sneaky unification:" $ vcat [text "Coercion variable: " <+> ppr gw, text "Coercion: " <+> pprEq (mkTyVarTy tv) xi, text "Left Kind is : " <+> ppr (typeKind (mkTyVarTy tv)), text "Right Kind is : " <+> ppr (typeKind xi) - ] - ; setWantedTyBind tv xi_unflat -- Set tv := xi_unflat - ; cv_given <- newGivOrDerCoVar (mkTyVarTy tv) xi_unflat xi_unflat - ; let flav = mkGivenFlavor gw UnkSkol - ; (cts, co) <- case coi of - ACo co -> do { can_eqs <- canEq flav cv_given (mkTyVarTy tv) xi_unflat - ; return (can_eqs, co) } - IdCo co -> return $ - (singleCCan (CTyEqCan { cc_id = cv_given - , cc_flavor = mkGivenFlavor gw UnkSkol - , cc_tyvar = tv, cc_rhs = xi } - -- xi, *not* xi_unflat because - -- xi_unflat may require flattening! - ), co) - ; case gw of - Wanted {} -> setWantedCoBind cv co - Derived {} -> setDerivedCoBind cv co - _ -> pprPanic "Can't spontaneously solve *given*" empty - - -- See Note [Avoid double unifications] - - ; return (Just cts) } - } - | otherwise - = return Nothing - - 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 - + ] + ; setWantedTyBind tv xi_unflat -- Set tv := xi_unflat + ; cv_given <- newGivOrDerCoVar (mkTyVarTy tv) xi_unflat xi_unflat + ; let flav = mkGivenFlavor gw UnkSkol + ; (cts, co) <- case coi of + ACo co -> do { can_eqs <- canEq flav cv_given (mkTyVarTy tv) xi_unflat + ; return (can_eqs, co) } + IdCo co -> return $ + (singleCCan (CTyEqCan { cc_id = cv_given + , cc_flavor = mkGivenFlavor gw UnkSkol + , cc_tyvar = tv, cc_rhs = xi } + -- xi, *not* xi_unflat because + -- xi_unflat may require flattening! + ), co) + ; case gw of + Wanted {} -> setWantedCoBind cv co + Derived {} -> setDerivedCoBind cv co + _ -> pprPanic "Can't spontaneously solve *given*" empty + -- See Note [Avoid double unifications] + ; return (Just cts) } + +occurCheck :: VarEnv (TcTyVar, TcType) -> InertSet + -> TcTyVar -> TcType -> Maybe (TcType,CoercionI) +-- 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) = occurCheck binds inerts tv ty +-- coi :: ty' ~ ty +-- NB: The returned type ty' may not be flat! + +occurCheck ty_binds inerts the_tv the_ty + = ok emptyVarSet the_ty + where + -- If (fsk `elem` bad) then tv occurs in any rendering + -- of the type under the expansion of fsk + ok bad this_ty@(TyConApp tc tys) + | Just tys_cois <- allMaybes (map (ok bad) tys) + , (tys',cois') <- unzip tys_cois + = Just (TyConApp tc tys', mkTyConAppCoI tc cois') + | isSynTyCon tc, Just ty_expanded <- tcView this_ty + = ok bad ty_expanded -- See Note [Type synonyms and the occur check] in TcUnify + ok bad (PredTy sty) + | Just (sty',coi) <- ok_pred bad sty + = Just (PredTy sty', coi) + ok bad (FunTy arg res) + | Just (arg', coiarg) <- ok bad arg, Just (res', coires) <- ok bad res + = Just (FunTy arg' res', mkFunTyCoI coiarg coires) + ok bad (AppTy fun arg) + | Just (fun', coifun) <- ok bad fun, Just (arg', coiarg) <- ok bad arg + = Just (AppTy fun' arg', mkAppTyCoI coifun coiarg) + ok bad (ForAllTy tv1 ty1) + -- WARNING: What if it is a (t1 ~ t2) => t3? It's not handled properly at the moment. + | Just (ty1', coi) <- ok bad ty1 + = Just (ForAllTy tv1 ty1', mkForAllTyCoI tv1 coi) + + -- Variable cases + ok bad this_ty@(TyVarTy tv) + | tv == the_tv = Nothing -- Occurs check error + | not (isTcTyVar tv) = Just (this_ty, IdCo this_ty) -- Bound var + | FlatSkol zty <- tcTyVarDetails tv = ok_fsk bad tv zty + | Just (_,ty) <- lookupVarEnv ty_binds tv = ok bad ty + | otherwise = Just (this_ty, IdCo this_ty) + + -- Check if there exists a ty bind already, as a result of sneaky unification. + -- Fall through + ok _bad _ty = Nothing + + ----------- + ok_pred bad (ClassP cn tys) + | Just tys_cois <- allMaybes $ map (ok bad) tys + = let (tys', cois') = unzip tys_cois + in Just (ClassP cn tys', mkClassPPredCoI cn cois') + ok_pred bad (IParam nm ty) + | Just (ty',co') <- ok bad ty + = Just (IParam nm ty', mkIParamPredCoI nm co') + ok_pred bad (EqPred ty1 ty2) + | Just (ty1',coi1) <- ok bad ty1, Just (ty2',coi2) <- ok bad ty2 + = Just (EqPred ty1' ty2', mkEqPredCoI coi1 coi2) + ok_pred _ _ = Nothing + + ----------- + ok_fsk bad fsk zty + | fsk `elemVarSet` bad + -- We are already trying to find a rendering of fsk, + -- and to do that it seems we need a rendering, so fail + = Nothing + | otherwise + = firstJusts (ok new_bad zty : map (go_under_fsk new_bad) fsk_equivs) + where + fsk_equivs = getFskEqClass inerts fsk + new_bad = bad `extendVarSetList` (fsk : map fst fsk_equivs) + + ----------- + go_under_fsk bad_tvs (fsk,co) + | FlatSkol zty <- tcTyVarDetails fsk + = case ok bad_tvs zty of + Nothing -> Nothing + Just (ty,coi') -> Just (ty, mkTransCoI coi' (ACo co)) + | otherwise = pprPanic "go_down_equiv" (ppr fsk) \end{code} @@ -952,10 +982,10 @@ doInteractWithInert (CFunEqCan { cc_id = cv1, cc_flavor = fl1, cc_fun = tc1 , cc_tyargs = args1, cc_rhs = xi1 }) workItem@(CFunEqCan { cc_id = cv2, cc_flavor = fl2, cc_fun = tc2 , cc_tyargs = args2, cc_rhs = xi2 }) - | fl1 `canRewrite` fl2 && lhss_match + | fl1 `canSolve` fl2 && lhss_match = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2) ; mkIRStop KeepInert cans } - | fl2 `canRewrite` fl1 && lhss_match + | fl2 `canSolve` fl1 && lhss_match = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1) ; mkIRContinue workItem DropInert cans } where @@ -965,11 +995,11 @@ doInteractWithInert inert@(CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 }) workItem@(CTyEqCan { cc_id = cv2, cc_flavor = fl2, cc_tyvar = tv2, cc_rhs = xi2 }) -- Check for matching LHS - | fl1 `canRewrite` fl2 && tv1 == tv2 + | fl1 `canSolve` fl2 && tv1 == tv2 = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2) ; mkIRStop KeepInert cans } - | fl2 `canRewrite` fl1 && tv1 == tv2 + | fl2 `canSolve` fl1 && tv1 == tv2 = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1) ; mkIRContinue workItem DropInert cans } @@ -997,14 +1027,7 @@ doInteractWithInert -- Fall-through case for all other situations doInteractWithInert _ workItem = noInteraction workItem --------------------------------------------- -combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc --- Precondition: At least one of them should be wanted -combineCtLoc (Wanted loc) _ = loc -combineCtLoc _ (Wanted loc) = loc -combineCtLoc _ _ = panic "Expected one of wanted constraints (BUG)" - - +------------------------- -- Equational Rewriting rewriteDict :: (CoVar, TcTyVar, Xi) -> (DictId, CtFlavor, Class, [Xi]) -> TcS CanonicalCt rewriteDict (cv,tv,xi) (dv,gw,cl,xis) @@ -1092,7 +1115,7 @@ rewriteEqLHS :: WhichComesFromInert -> (Coercion,Xi) -> (CoVar,CtFlavor,Xi) -> T -- Used to ineratct two equalities of the following form: -- First Equality: co1: (XXX ~ xi1) -- Second Equality: cv2: (XXX ~ xi2) --- Where the cv1 `canRewrite` cv2 equality +-- Where the cv1 `canSolve` cv2 equality -- We have an option of creating new work (xi1 ~ xi2) OR (xi2 ~ xi1). This -- depends on whether the left or the right equality comes from the inert set. -- We must: @@ -1135,13 +1158,13 @@ solveOneFromTheOther (iid,ifl) workItem | isDerived ifl && isDerived wfl = noInteraction workItem - | ifl `canRewrite` wfl + | ifl `canSolve` wfl = do { unless (isGiven wfl) $ setEvBind wid (EvId iid) -- Overwrite the binding, if one exists -- For Givens, which are lambda-bound, nothing to overwrite, ; dischargeWorkItem } - | otherwise -- wfl `canRewrite` ifl + | otherwise -- wfl `canSolve` ifl = do { unless (isGiven ifl) $ setEvBind iid (EvId wid) ; mkIRContinue workItem DropInert emptyCCan } @@ -1783,19 +1806,18 @@ new given work. There are several reasons for this: Now suppose that we have: given: C a b wanted: C a beta - By interacting the given we will get that (F a ~ b) which is not + By interacting the given we will get given (F a ~ b) which is not enough by itself to make us discharge (C a beta). However, we - may create a new given equality from the super-class that we promise - to solve: (F a ~ beta). Now we may interact this with the rest of - constraint to finally get: - given : beta ~ b - + may create a new derived equality from the super-class of the + wanted constraint (C a beta), namely derived (F a ~ beta). + Now we may interact this with given (F a ~ b) to get: + derived : beta ~ b But 'beta' is a touchable unification variable, and hence OK to - unify it with 'b', replacing the given evidence with the identity. + unify it with 'b', replacing the derived evidence with the identity. - This requires trySpontaneousSolve to solve given equalities that - have a touchable in their RHS, *in addition* to solving wanted - equalities. + This requires trySpontaneousSolve to solve *derived* + equalities that have a touchable in their RHS, *in addition* + to solving wanted equalities. Here is another example where this is useful. @@ -1884,5 +1906,3 @@ matchClassInst clas tys loc } } \end{code} - -