- ]
- ; 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 { can_eqs <- canEq flav cv_given (mkTyVarTy tv) xi_unflat
- ; return (can_eqs, co) }
- IdCo co -> return $
- (singleCCan (CTyEqCan { cc_id = cv_given
- , cc_flavor = mkGivenFlavor gw UnkSkol
- , cc_tyvar = tv, cc_rhs = xi }
- -- xi, *not* xi_unflat!
- ), co)
- ; case gw of
- Wanted {} -> setWantedCoBind cv co
- Derived {} -> setDerivedCoBind cv co
- _ -> pprPanic "Can't spontaneously solve *given*" empty
-
- -- See Note [Avoid double unifications]
-
- -- The reason that we create a new given variable (cv_given) instead of reusing cv
- -- is because we do not want to end up with coercion unification variables in the givens.
- ; return (Just cts) }
- }
- | otherwise
- = return Nothing
-
-
-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.
---}