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