+ 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
+