--- ; 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 { cv_given <- newGivOrDerCoVar (mkTyVarTy tv) xi_unflat xi_unflat
- ; setWantedTyBind tv xi_unflat
- ; can_eqs <- case or_flag of
- OrientThisWay -> canEq flav cv_given (mkTyVarTy tv) xi_unflat
- OrientOtherWay -> canEq flav cv_given xi_unflat (mkTyVarTy tv)
- ; return (can_eqs, co) }
- IdCo co -> do { cv_given <- newGivOrDerCoVar (mkTyVarTy tv) xi xi
- ; setWantedTyBind tv xi
- ; can_eqs <- case or_flag of
- OrientThisWay -> canEq flav cv_given (mkTyVarTy tv) xi
- OrientOtherWay -> canEq flav cv_given xi (mkTyVarTy tv)
- ; return (can_eqs, 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)