X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcInteract.lhs;h=f0edcc97f49106a1ddec382dba3271db02173e88;hb=cd2f5397bc1345fc37706168c268a8bd37af7f2f;hp=2a5350341395dd3c341fbb85f7b92e4ab95176d1;hpb=2060788524c41ae87ba87276cb59e7cab574fe68;p=ghc-hetmet.git diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs index 2a53503..f0edcc9 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 @@ -604,10 +605,11 @@ solveWithIdentity :: InertSet -> TcS (Maybe SWorkList) -- Solve with the identity coercion -- Precondition: kind(xi) is a sub-kind of kind(tv) --- Precondition: CtFlavor is not Given --- 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 - = do { tybnds <- getTcSTyBindsBag + = do { tybnds <- getTcSTyBindsMap ; case occurCheck tybnds inerts tv xi of Nothing -> return Nothing Just (xi_unflat,coi) -> solve_with xi_unflat coi } @@ -639,7 +641,7 @@ solveWithIdentity inerts cv gw tv xi -- See Note [Avoid double unifications] ; return (Just cts) } -occurCheck :: Bag (TcTyVar, TcType) -> InertSet +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 @@ -650,9 +652,11 @@ occurCheck :: Bag (TcTyVar, TcType) -> InertSet -- coi :: ty' ~ ty -- NB: The returned type ty' may not be flat! -occurCheck ty_binds_bag inerts tv ty - = ok emptyVarSet ty +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 @@ -674,32 +678,18 @@ occurCheck ty_binds_bag inerts tv ty = Just (ForAllTy tv1 ty1', mkForAllTyCoI tv1 coi) -- Variable cases - ok _bad this_ty@(TyVarTy tv') - | not $ isTcTyVar tv' = Just (this_ty, IdCo this_ty) -- Bound variable - | tv == tv' = Nothing -- Occurs check error - - ok bad (TyVarTy fsk) - | FlatSkol zty <- tcTyVarDetails fsk - = if fsk `elemVarSet` bad then - -- its type has been checked - go_down_eq_class bad $ getFskEqClass inerts fsk - else - -- its type is not yet checked - case ok bad zty of - Nothing -> go_down_eq_class (bad `extendVarSet` fsk) $ - getFskEqClass inerts fsk - Just (zty',ico) -> Just (zty',ico) + 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. - ok bad this_ty@(TyVarTy tv0) - = case Bag.foldlBag find_bind Nothing ty_binds_bag of - Nothing -> Just (this_ty, IdCo this_ty) - Just ty0 -> ok bad ty0 - where find_bind Nothing (tvx,tyx) | tv0 == tvx = Just tyx - find_bind m _ = m -- 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 @@ -712,13 +702,25 @@ occurCheck ty_binds_bag inerts tv ty = Just (EqPred ty1' ty2', mkEqPredCoI coi1 coi2) ok_pred _ _ = Nothing - go_down_eq_class _bad_tvs [] = Nothing - go_down_eq_class bad_tvs ((fsk1,co1):rest) - | fsk1 `elemVarSet` bad_tvs = go_down_eq_class bad_tvs rest - | otherwise - = case ok bad_tvs (TyVarTy fsk1) of - Nothing -> go_down_eq_class (bad_tvs `extendVarSet` fsk1) rest - Just (ty1,co1i') -> Just (ty1, mkTransCoI co1i' (ACo co1)) + ----------- + 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} @@ -1783,19 +1785,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.