+
+passOccursCheck :: InertSet -> TcTyVar -> TcType -> TcS (Maybe (TcType,CoercionI))
+-- passOccursCheck inerts tv ty
+-- Traverse the type and 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 to see if you can
+-- find a different flatten skolem to use, which does not mention the
+-- variable.
+-- Postcondition: Just (ty',coi) <- passOccursCheck tv ty
+-- coi :: ty' ~ ty
+-- NB: I believe there is no need to do the tcView thing here
+passOccursCheck is tv (TyConApp tc tys)
+ = do { tys_mbs <- mapM (passOccursCheck is tv) tys
+ ; case allMaybes tys_mbs of
+ Nothing -> return Nothing
+ Just tys_cois ->
+ let (tys',cois') = unzip tys_cois
+ in return $
+ Just (TyConApp tc tys', mkTyConAppCoI tc cois')
+ }
+passOccursCheck is tv (PredTy sty)
+ = do { sty_mb <- passOccursCheckPred tv sty
+ ; case sty_mb of
+ Nothing -> return Nothing
+ Just (sty',coi) -> return (Just (PredTy sty', coi))
+ }
+ where passOccursCheckPred tv (ClassP cn tys)
+ = do { tys_mbs <- mapM (passOccursCheck is tv) tys
+ ; case allMaybes tys_mbs of
+ Nothing -> return Nothing
+ Just tys_cois ->
+ let (tys', cois') = unzip tys_cois
+ in return $
+ Just (ClassP cn tys', mkClassPPredCoI cn cois')
+ }
+ passOccursCheckPred tv (IParam nm ty)
+ = do { mty <- passOccursCheck is tv ty
+ ; case mty of
+ Nothing -> return Nothing
+ Just (ty',co')
+ -> return (Just (IParam nm ty',
+ mkIParamPredCoI nm co'))
+ }
+ passOccursCheckPred tv (EqPred ty1 ty2)
+ = do { mty1 <- passOccursCheck is tv ty1
+ ; mty2 <- passOccursCheck is tv ty2
+ ; case (mty1,mty2) of
+ (Just (ty1',coi1), Just (ty2',coi2))
+ -> return $
+ Just (EqPred ty1' ty2', mkEqPredCoI coi1 coi2)
+ _ -> return Nothing
+ }
+
+passOccursCheck is tv (FunTy arg res)
+ = do { arg_mb <- passOccursCheck is tv arg
+ ; res_mb <- passOccursCheck is tv res
+ ; case (arg_mb,res_mb) of
+ (Just (arg',coiarg), Just (res',coires))
+ -> return $
+ Just (FunTy arg' res', mkFunTyCoI coiarg coires)
+ _ -> return Nothing
+ }
+
+passOccursCheck is tv (AppTy fun arg)
+ = do { fun_mb <- passOccursCheck is tv fun
+ ; arg_mb <- passOccursCheck is tv arg
+ ; case (fun_mb,arg_mb) of
+ (Just (fun',coifun), Just (arg',coiarg))
+ -> return $
+ Just (AppTy fun' arg', mkAppTyCoI coifun coiarg)
+ _ -> return Nothing
+ }
+
+passOccursCheck is tv (ForAllTy tv1 ty1)
+ = do { ty1_mb <- passOccursCheck is tv ty1
+ ; case ty1_mb of
+ Nothing -> return Nothing
+ Just (ty1',coi)
+ -> return $
+ Just (ForAllTy tv1 ty1', mkForAllTyCoI tv1 coi)
+ }
+
+passOccursCheck _is tv (TyVarTy tv')
+ | tv == tv'
+ = return Nothing
+
+passOccursCheck is tv (TyVarTy fsk)
+ | FlatSkol ty <- tcTyVarDetails fsk
+ = do { zty <- zonkFlattenedType ty -- Must zonk as it contains unif. vars
+ ; occ <- passOccursCheck is tv zty
+ ; case occ of
+ Nothing -> go_down_eq_class $ getFskEqClass is fsk
+ Just (zty',ico) -> return $ Just (zty',ico)
+ }
+ where go_down_eq_class [] = return Nothing
+ go_down_eq_class ((fsk1,co1):rest)
+ = do { occ1 <- passOccursCheck is tv (TyVarTy fsk1)
+ ; case occ1 of
+ Nothing -> go_down_eq_class rest
+ Just (ty1,co1i')
+ -> return $ Just (ty1, mkTransCoI co1i' (ACo co1)) }
+passOccursCheck _is _tv ty
+ = return (Just (ty,IdCo ty))
+
+{--
+Problematic situation:
+~~~~~~~~~~~~~~~~~~~~~~
+ Suppose we have a flatten skolem f1 := F f6
+ Suppose we are chasing for 'alpha', and:
+ f6 := G alpha with eq.class f7,f8
+
+ Then we will return F f7 potentially.
+--}
+
+
+