import TypeRep
import Id
+import VarEnv
import Var
import TcType
-> 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 }
-- 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
-- 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
= 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
= 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}
-- 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)
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.