Commit cec7d580 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Fix the pure unifier

This patch fixes Trac #13705, by fixing a long-standing outright bug
in the pure unifier.  I'm surprised this hasn't caused more trouble
before now!
parent fea9a757
......@@ -455,7 +455,7 @@ tc_unify_tys_fg match_kis bind_fn tys1 tys2
-- | This function is actually the one to call the unifier -- a little
-- too general for outside clients, though.
tc_unify_tys :: (TyVar -> BindFlag)
-> Bool -- ^ True <=> unify; False <=> match
-> AmIUnifying -- ^ True <=> unify; False <=> match
-> Bool -- ^ True <=> doing an injectivity check
-> Bool -- ^ True <=> treat the kinds as well
-> RnEnv2
......@@ -464,12 +464,17 @@ tc_unify_tys :: (TyVar -> BindFlag)
-> [Type] -> [Type]
-> UnifyResultM (TvSubstEnv, CvSubstEnv)
tc_unify_tys bind_fn unif inj_check match_kis rn_env tv_env cv_env tys1 tys2
= initUM bind_fn unif inj_check rn_env tv_env cv_env $
= initUM tv_env cv_env $
do { when match_kis $
unify_tys kis1 kis2
; unify_tys tys1 tys2
unify_tys env kis1 kis2
; unify_tys env tys1 tys2
; (,) <$> getTvSubstEnv <*> getCvSubstEnv }
where
env = UMEnv { um_bind_fun = bind_fn
, um_unif = unif
, um_inj_tf = inj_check
, um_rn_env = rn_env }
kis1 = map typeKind tys1
kis2 = map typeKind tys2
......@@ -664,7 +669,7 @@ this, but we musn't map a to anything else!)
We thus must parameterize the algorithm over whether it's being used
for an injectivity check (refrain from looking at non-injective arguments
to type families) or not (do indeed look at those arguments). This is
implemented by the uf_int_tf field of UmEnv.
implemented by the uf_inj_tf field of UmEnv.
(It's all a question of whether or not to include equation (7) from Fig. 2
of [ITF].)
......@@ -770,151 +775,158 @@ coercions in this manner.
-------------- unify_ty: the main workhorse -----------
unify_ty :: Type -> Type -- Types to be unified and a co
type AmIUnifying = Bool -- True <=> Unifying
-- False <=> Matching
unify_ty :: UMEnv
-> Type -> Type -- Types to be unified and a co
-> Coercion -- A coercion between their kinds
-- See Note [Kind coercions in Unify]
-> UM ()
-- See Note [Specification of unification]
-- Respects newtypes, PredTypes
unify_ty ty1 ty2 kco
unify_ty env ty1 ty2 kco
-- TODO: More commentary needed here
| Just ty1' <- tcView ty1 = unify_ty ty1' ty2 kco
| Just ty2' <- tcView ty2 = unify_ty ty1 ty2' kco
| CastTy ty1' co <- ty1 = unify_ty ty1' ty2 (co `mkTransCo` kco)
| CastTy ty2' co <- ty2 = unify_ty ty1 ty2' (kco `mkTransCo` mkSymCo co)
unify_ty (TyVarTy tv1) ty2 kco = uVar tv1 ty2 kco
unify_ty ty1 (TyVarTy tv2) kco
= do { unif <- amIUnifying
; if unif
then umSwapRn $ uVar tv2 ty1 (mkSymCo kco)
else surelyApart } -- non-tv on left; tv on right: can't match.
unify_ty ty1 ty2 _kco
| Just (tc1, tys1) <- tcSplitTyConApp_maybe ty1
, Just (tc2, tys2) <- tcSplitTyConApp_maybe ty2
= if tc1 == tc2 || (tcIsStarKind ty1 && tcIsStarKind ty2)
then if isInjectiveTyCon tc1 Nominal
then unify_tys tys1 tys2
else do { let inj | isTypeFamilyTyCon tc1
= case familyTyConInjectivityInfo tc1 of
| Just ty1' <- tcView ty1 = unify_ty env ty1' ty2 kco
| Just ty2' <- tcView ty2 = unify_ty env ty1 ty2' kco
| CastTy ty1' co <- ty1 = unify_ty env ty1' ty2 (co `mkTransCo` kco)
| CastTy ty2' co <- ty2 = unify_ty env ty1 ty2' (kco `mkTransCo` mkSymCo co)
unify_ty env (TyVarTy tv1) ty2 kco
= uVar env tv1 ty2 kco
unify_ty env ty1 (TyVarTy tv2) kco
| um_unif env -- If unifying, can swap args
= uVar (umSwapRn env) tv2 ty1 (mkSymCo kco)
unify_ty env ty1 ty2 _kco
| Just (tc1, tys1) <- mb_tc_app1
, Just (tc2, tys2) <- mb_tc_app2
, tc1 == tc2 || (tcIsStarKind ty1 && tcIsStarKind ty2)
= if isInjectiveTyCon tc1 Nominal
then unify_tys env tys1 tys2
else do { let inj | isTypeFamilyTyCon tc1
= case familyTyConInjectivityInfo tc1 of
NotInjective -> repeat False
Injective bs -> bs
| otherwise
= repeat False
| otherwise
= repeat False
(inj_tys1, noninj_tys1) = partitionByList inj tys1
(inj_tys2, noninj_tys2) = partitionByList inj tys2
(inj_tys1, noninj_tys1) = partitionByList inj tys1
(inj_tys2, noninj_tys2) = partitionByList inj tys2
; unify_tys inj_tys1 inj_tys2
; inj_tf <- checkingInjectivity
; unless inj_tf $ -- See (end of) Note [Specification of unification]
don'tBeSoSure $ unify_tys noninj_tys1 noninj_tys2 }
else -- tc1 /= tc2
if isGenerativeTyCon tc1 Nominal && isGenerativeTyCon tc2 Nominal
then surelyApart
else maybeApart
; unify_tys env inj_tys1 inj_tys2
; unless (um_inj_tf env) $ -- See (end of) Note [Specification of unification]
don'tBeSoSure $ unify_tys env noninj_tys1 noninj_tys2 }
| Just (tc1, _) <- mb_tc_app1
, not (isGenerativeTyCon tc1 Nominal)
-- E.g. unify_ty (F ty1) b = MaybeApart
-- because the (F ty1) behaves like a variable
-- NB: if unifying, we have already dealt
-- with the 'ty2 = variable' case
= maybeApart
| Just (tc2, _) <- mb_tc_app2
, not (isGenerativeTyCon tc2 Nominal)
, um_unif env
-- E.g. unify_ty [a] (F ty2) = MaybeApart, when unifying (only)
-- because the (F ty2) behaves like a variable
-- NB: we have already dealt with the 'ty1 = variable' case
= maybeApart
where
mb_tc_app1 = tcSplitTyConApp_maybe ty1
mb_tc_app2 = tcSplitTyConApp_maybe ty2
-- Applications need a bit of care!
-- They can match FunTy and TyConApp, so use splitAppTy_maybe
-- NB: we've already dealt with type variables,
-- so if one type is an App the other one jolly well better be too
unify_ty (AppTy ty1a ty1b) ty2 _kco
unify_ty env (AppTy ty1a ty1b) ty2 _kco
| Just (ty2a, ty2b) <- tcRepSplitAppTy_maybe ty2
= unify_ty_app ty1a [ty1b] ty2a [ty2b]
= unify_ty_app env ty1a [ty1b] ty2a [ty2b]
unify_ty ty1 (AppTy ty2a ty2b) _kco
unify_ty env ty1 (AppTy ty2a ty2b) _kco
| Just (ty1a, ty1b) <- tcRepSplitAppTy_maybe ty1
= unify_ty_app ty1a [ty1b] ty2a [ty2b]
= unify_ty_app env ty1a [ty1b] ty2a [ty2b]
unify_ty (LitTy x) (LitTy y) _kco | x == y = return ()
unify_ty _ (LitTy x) (LitTy y) _kco | x == y = return ()
unify_ty (ForAllTy (TvBndr tv1 _) ty1) (ForAllTy (TvBndr tv2 _) ty2) kco
= do { unify_ty (tyVarKind tv1) (tyVarKind tv2) (mkNomReflCo liftedTypeKind)
; umRnBndr2 tv1 tv2 $ unify_ty ty1 ty2 kco }
unify_ty env (ForAllTy (TvBndr tv1 _) ty1) (ForAllTy (TvBndr tv2 _) ty2) kco
= do { unify_ty env (tyVarKind tv1) (tyVarKind tv2) (mkNomReflCo liftedTypeKind)
; let env' = umRnBndr2 env tv1 tv2
; unify_ty env' ty1 ty2 kco }
-- See Note [Matching coercion variables]
unify_ty (CoercionTy co1) (CoercionTy co2) kco
= do { unif <- amIUnifying
; c_subst <- getCvSubstEnv
unify_ty env (CoercionTy co1) (CoercionTy co2) kco
= do { c_subst <- getCvSubstEnv
; case co1 of
CoVarCo cv
| not unif
, not (cv `elemVarEnv` c_subst)
-> do { b <- tvBindFlagL cv
; if b == BindMe
then do { checkRnEnvRCo co2
; let (co_l, co_r) = decomposeFunCo kco
-- cv :: t1 ~ t2
-- co2 :: s1 ~ s2
-- co_l :: t1 ~ s1
-- co_r :: t2 ~ s2
; extendCvEnv cv (co_l `mkTransCo`
co2 `mkTransCo`
mkSymCo co_r) }
else return () }
| not (um_unif env)
, not (cv `elemVarEnv` c_subst)
, BindMe <- tvBindFlagL env cv
-> do { checkRnEnvRCo env co2
; let (co_l, co_r) = decomposeFunCo kco
-- cv :: t1 ~ t2
-- co2 :: s1 ~ s2
-- co_l :: t1 ~ s1
-- co_r :: t2 ~ s2
; extendCvEnv cv (co_l `mkTransCo`
co2 `mkTransCo`
mkSymCo co_r) }
_ -> return () }
unify_ty ty1 _ _
| Just (tc1, _) <- splitTyConApp_maybe ty1
, not (isGenerativeTyCon tc1 Nominal)
= maybeApart
unify_ty _ ty2 _
| Just (tc2, _) <- splitTyConApp_maybe ty2
, not (isGenerativeTyCon tc2 Nominal)
= do { unif <- amIUnifying
; if unif then maybeApart else surelyApart }
unify_ty _ _ _ = surelyApart
unify_ty _ _ _ _ = surelyApart
unify_ty_app :: Type -> [Type] -> Type -> [Type] -> UM ()
unify_ty_app ty1 ty1args ty2 ty2args
unify_ty_app :: UMEnv -> Type -> [Type] -> Type -> [Type] -> UM ()
unify_ty_app env ty1 ty1args ty2 ty2args
| Just (ty1', ty1a) <- repSplitAppTy_maybe ty1
, Just (ty2', ty2a) <- repSplitAppTy_maybe ty2
= unify_ty_app ty1' (ty1a : ty1args) ty2' (ty2a : ty2args)
= unify_ty_app env ty1' (ty1a : ty1args) ty2' (ty2a : ty2args)
| otherwise
= do { let ki1 = typeKind ty1
ki2 = typeKind ty2
-- See Note [Kind coercions in Unify]
; unify_ty ki1 ki2 (mkNomReflCo liftedTypeKind)
; unify_ty ty1 ty2 (mkNomReflCo ki1)
; unify_tys ty1args ty2args }
; unify_ty env ki1 ki2 (mkNomReflCo liftedTypeKind)
; unify_ty env ty1 ty2 (mkNomReflCo ki1)
; unify_tys env ty1args ty2args }
unify_tys :: [Type] -> [Type] -> UM ()
unify_tys orig_xs orig_ys
unify_tys :: UMEnv -> [Type] -> [Type] -> UM ()
unify_tys env orig_xs orig_ys
= go orig_xs orig_ys
where
go [] [] = return ()
go (x:xs) (y:ys)
-- See Note [Kind coercions in Unify]
= do { unify_ty x y (mkNomReflCo $ typeKind x)
= do { unify_ty env x y (mkNomReflCo $ typeKind x)
; go xs ys }
go _ _ = maybeApart -- See Note [Lists of different lengths are MaybeApart]
---------------------------------
uVar :: TyVar -- Variable to be unified
uVar :: UMEnv
-> TyVar -- Variable to be unified
-> Type -- with this Type
-> Coercion -- :: kind tv ~N kind ty
-> UM ()
uVar tv1 ty kco
uVar env tv1 ty kco
= do { -- Check to see whether tv1 is refined by the substitution
subst <- getTvSubstEnv
; case (lookupVarEnv subst tv1) of
Just ty' -> do { unif <- amIUnifying
; if unif
then unify_ty ty' ty kco -- Yes, call back into unify
else -- when *matching*, we don't want to just recur here.
-- this is because the range of the subst is the target
-- type, not the template type. So, just check for
-- normal type equality.
guard ((ty' `mkCastTy` kco) `eqType` ty) }
Nothing -> uUnrefined tv1 ty ty kco } -- No, continue
uUnrefined :: TyVar -- variable to be unified
Just ty' | um_unif env -- Unifying, so
-> unify_ty env ty' ty kco -- call back into unify
| otherwise
-> -- Matching, we don't want to just recur here.
-- this is because the range of the subst is the target
-- type, not the template type. So, just check for
-- normal type equality.
guard ((ty' `mkCastTy` kco) `eqType` ty)
Nothing -> uUnrefined env tv1 ty ty kco } -- No, continue
uUnrefined :: UMEnv
-> TyVar -- variable to be unified
-> Type -- with this Type
-> Type -- (version w/ expanded synonyms)
-> Coercion -- :: kind tv ~N kind ty
......@@ -922,36 +934,36 @@ uUnrefined :: TyVar -- variable to be unified
-- We know that tv1 isn't refined
uUnrefined tv1 ty2 ty2' kco
uUnrefined env tv1 ty2 ty2' kco
| Just ty2'' <- coreView ty2'
= uUnrefined tv1 ty2 ty2'' kco -- Unwrap synonyms
= uUnrefined env tv1 ty2 ty2'' kco -- Unwrap synonyms
-- This is essential, in case we have
-- type Foo a = a
-- and then unify a ~ Foo a
| TyVarTy tv2 <- ty2'
= do { tv1' <- umRnOccL tv1
; tv2' <- umRnOccR tv2
; unif <- amIUnifying
= do { let tv1' = umRnOccL env tv1
tv2' = umRnOccR env tv2
-- See Note [Self-substitution when matching]
; when (tv1' /= tv2' || not unif) $ do
; when (tv1' /= tv2' || not (um_unif env)) $ do
{ subst <- getTvSubstEnv
-- Check to see whether tv2 is refined
; case lookupVarEnv subst tv2 of
{ Just ty' | unif -> uUnrefined tv1 ty' ty' kco
; _ -> do
{ Just ty' | um_unif env -> uUnrefined env tv1 ty' ty' kco
; _ -> do
{ -- So both are unrefined
-- And then bind one or the other,
-- depending on which is bindable
; b1 <- tvBindFlagL tv1
; b2 <- tvBindFlagR tv2
; let ty1 = mkTyVarTy tv1
; let b1 = tvBindFlagL env tv1
b2 = tvBindFlagR env tv2
ty1 = mkTyVarTy tv1
; case (b1, b2) of
(BindMe, _) -> do { checkRnEnvR ty2 -- make sure ty2 is not a local
; extendTvEnv tv1 (ty2 `mkCastTy` mkSymCo kco) }
(_, BindMe) | unif -> do { checkRnEnvL ty1 -- ditto for ty1
; extendTvEnv tv2 (ty1 `mkCastTy` kco) }
(BindMe, _) -> do { checkRnEnvR env ty2 -- make sure ty2 is not a local
; extendTvEnv tv1 (ty2 `mkCastTy` mkSymCo kco) }
(_, BindMe) | um_unif env
-> do { checkRnEnvL env ty1 -- ditto for ty1
; extendTvEnv tv2 (ty1 `mkCastTy` kco) }
_ | tv1' == tv2' -> return ()
-- How could this happen? If we're only matching and if
......@@ -960,12 +972,11 @@ uUnrefined tv1 ty2 ty2' kco
_ -> maybeApart -- See Note [Unification with skolems]
}}}}
uUnrefined tv1 ty2 ty2' kco -- ty2 is not a type variable
uUnrefined env tv1 ty2 ty2' kco -- ty2 is not a type variable
= do { occurs <- elemNiSubstSet tv1 (tyCoVarsOfType ty2')
; unif <- amIUnifying
; if unif && occurs -- See Note [Self-substitution when matching]
; if um_unif env && occurs -- See Note [Self-substitution when matching]
then maybeApart -- Occurs check, see Note [Fine-grained unification]
else do bindTv tv1 (ty2 `mkCastTy` mkSymCo kco) }
else do bindTv env tv1 (ty2 `mkCastTy` mkSymCo kco) }
-- Bind tyvar to the synonym if poss
elemNiSubstSet :: TyVar -> TyCoVarSet -> UM Bool
......@@ -973,11 +984,10 @@ elemNiSubstSet v set
= do { tsubst <- getTvSubstEnv
; return $ v `elemVarSet` niSubstTvSet tsubst set }
bindTv :: TyVar -> Type -> UM ()
bindTv tv ty -- ty is not a variable
= do { checkRnEnvR ty -- make sure ty mentions no local variables
; b <- tvBindFlagL tv
; case b of
bindTv :: UMEnv -> TyVar -> Type -> UM ()
bindTv env tv ty -- ty is not a variable
= do { checkRnEnvR env ty -- make sure ty mentions no local variables
; case tvBindFlagL env tv of
Skolem -> maybeApart -- See Note [Unification with skolems]
BindMe -> extendTvEnv tv ty
}
......@@ -1006,147 +1016,125 @@ data BindFlag
-}
data UMEnv = UMEnv { um_bind_fun :: TyVar -> BindFlag
-- the user-supplied BindFlag function
, um_unif :: Bool -- unification (True) or matching?
, um_inj_tf :: Bool -- checking for injectivity?
-- See (end of) Note [Specification of unification]
-- User-supplied BindFlag function
, um_unif :: AmIUnifying
, um_inj_tf :: Bool -- Checking for injectivity?
-- See (end of) Note [Specification of unification]
, um_rn_env :: RnEnv2 }
data UMState = UMState
{ um_tv_env :: TvSubstEnv
, um_cv_env :: CvSubstEnv }
newtype UM a = UM { unUM :: UMEnv -> UMState
-> UnifyResultM (UMState, a) }
newtype UM a = UM { unUM :: UMState -> UnifyResultM (UMState, a) }
instance Functor UM where
fmap = liftM
instance Applicative UM where
pure a = UM (\_ s -> pure (s, a))
pure a = UM (\s -> pure (s, a))
(<*>) = ap
instance Monad UM where
fail _ = UM (\_ _ -> SurelyApart) -- failed pattern match
m >>= k = UM (\env state ->
do { (state', v) <- unUM m env state
; unUM (k v) env state' })
fail _ = UM (\_ -> SurelyApart) -- failed pattern match
m >>= k = UM (\state ->
do { (state', v) <- unUM m state
; unUM (k v) state' })
-- need this instance because of a use of 'guard' above
instance Alternative UM where
empty = UM (\_ _ -> Control.Applicative.empty)
m1 <|> m2 = UM (\env state ->
unUM m1 env state <|>
unUM m2 env state)
empty = UM (\_ -> Control.Applicative.empty)
m1 <|> m2 = UM (\state ->
unUM m1 state <|>
unUM m2 state)
instance MonadPlus UM
#if __GLASGOW_HASKELL__ > 710
instance MonadFail.MonadFail UM where
fail _ = UM (\_tvs _subst -> SurelyApart) -- failed pattern match
fail _ = UM (\_ -> SurelyApart) -- failed pattern match
#endif
initUM :: (TyVar -> BindFlag)
-> Bool -- True <=> unify; False <=> match
-> Bool -- True <=> doing an injectivity check
-> RnEnv2
-> TvSubstEnv -- subst to extend
initUM :: TvSubstEnv -- subst to extend
-> CvSubstEnv
-> UM a -> UnifyResultM a
initUM badtvs unif inj_tf rn_env subst_env cv_subst_env um
= case unUM um env state of
initUM subst_env cv_subst_env um
= case unUM um state of
Unifiable (_, subst) -> Unifiable subst
MaybeApart (_, subst) -> MaybeApart subst
SurelyApart -> SurelyApart
where
env = UMEnv { um_bind_fun = badtvs
, um_unif = unif
, um_inj_tf = inj_tf
, um_rn_env = rn_env }
state = UMState { um_tv_env = subst_env
, um_cv_env = cv_subst_env }
tvBindFlagL :: TyVar -> UM BindFlag
tvBindFlagL tv = UM $ \env state ->
Unifiable (state, if inRnEnvL (um_rn_env env) tv
then Skolem
else um_bind_fun env tv)
tvBindFlagL :: UMEnv -> TyVar -> BindFlag
tvBindFlagL env tv
| inRnEnvL (um_rn_env env) tv = Skolem
| otherwise = um_bind_fun env tv
tvBindFlagR :: TyVar -> UM BindFlag
tvBindFlagR tv = UM $ \env state ->
Unifiable (state, if inRnEnvR (um_rn_env env) tv
then Skolem
else um_bind_fun env tv)
tvBindFlagR :: UMEnv -> TyVar -> BindFlag
tvBindFlagR env tv
| inRnEnvR (um_rn_env env) tv = Skolem
| otherwise = um_bind_fun env tv
getTvSubstEnv :: UM TvSubstEnv
getTvSubstEnv = UM $ \_ state -> Unifiable (state, um_tv_env state)
getTvSubstEnv = UM $ \state -> Unifiable (state, um_tv_env state)
getCvSubstEnv :: UM CvSubstEnv
getCvSubstEnv = UM $ \_ state -> Unifiable (state, um_cv_env state)
getCvSubstEnv = UM $ \state -> Unifiable (state, um_cv_env state)
extendTvEnv :: TyVar -> Type -> UM ()
extendTvEnv tv ty = UM $ \_ state ->
extendTvEnv tv ty = UM $ \state ->
Unifiable (state { um_tv_env = extendVarEnv (um_tv_env state) tv ty }, ())
extendCvEnv :: CoVar -> Coercion -> UM ()
extendCvEnv cv co = UM $ \_ state ->
extendCvEnv cv co = UM $ \state ->
Unifiable (state { um_cv_env = extendVarEnv (um_cv_env state) cv co }, ())
umRnBndr2 :: TyCoVar -> TyCoVar -> UM a -> UM a
umRnBndr2 v1 v2 thing = UM $ \env state ->
let rn_env' = rnBndr2 (um_rn_env env) v1 v2 in
unUM thing (env { um_rn_env = rn_env' }) state
umRnBndr2 :: UMEnv -> TyCoVar -> TyCoVar -> UMEnv
umRnBndr2 env v1 v2
= env { um_rn_env = rnBndr2 (um_rn_env env) v1 v2 }
checkRnEnv :: (RnEnv2 -> VarEnv Var) -> VarSet -> UM ()
checkRnEnv get_set varset = UM $ \env state ->
checkRnEnv :: (RnEnv2 -> VarEnv Var) -> UMEnv -> VarSet -> UM ()
checkRnEnv get_set env varset = UM $ \ state ->
let env_vars = get_set (um_rn_env env) in
if isEmptyVarEnv env_vars || (getUniqSet varset `disjointVarEnv` env_vars)
-- NB: That isEmptyVarSet is a critical optimization; it
-- means we don't have to calculate the free vars of
-- the type, often saving quite a bit of allocation.
then Unifiable (state, ())
then Unifiable (state, ())
else MaybeApart (state, ())
-- | Converts any SurelyApart to a MaybeApart
don'tBeSoSure :: UM () -> UM ()
don'tBeSoSure um = UM $ \env state ->
case unUM um env state of
don'tBeSoSure um = UM $ \ state ->
case unUM um state of
SurelyApart -> MaybeApart (state, ())
other -> other
checkRnEnvR :: Type -> UM ()
checkRnEnvR ty = checkRnEnv rnEnvR (tyCoVarsOfType ty)
checkRnEnvL :: Type -> UM ()
checkRnEnvL ty = checkRnEnv rnEnvL (tyCoVarsOfType ty)
checkRnEnvRCo :: Coercion -> UM ()
checkRnEnvRCo co = checkRnEnv rnEnvR (tyCoVarsOfCo co)
checkRnEnvR :: UMEnv -> Type -> UM ()
checkRnEnvR env ty = checkRnEnv rnEnvR env (tyCoVarsOfType ty)
umRnOccL :: TyVar -> UM TyVar
umRnOccL v = UM $ \env state ->
Unifiable (state, rnOccL (um_rn_env env) v)
checkRnEnvL :: UMEnv -> Type -> UM ()
checkRnEnvL env ty = checkRnEnv rnEnvL env (tyCoVarsOfType ty)
umRnOccR :: TyVar -> UM TyVar
umRnOccR v = UM $ \env state ->
Unifiable (state, rnOccR (um_rn_env env) v)
checkRnEnvRCo :: UMEnv -> Coercion -> UM ()
checkRnEnvRCo env co = checkRnEnv rnEnvR env (tyCoVarsOfCo co)
umSwapRn :: UM a -> UM a
umSwapRn thing = UM $ \env state ->
let rn_env' = rnSwap (um_rn_env env) in
unUM thing (env { um_rn_env = rn_env' }) state
umRnOccL :: UMEnv -> TyVar -> TyVar
umRnOccL env v = rnOccL (um_rn_env env) v
amIUnifying :: UM Bool
amIUnifying = UM $ \env state -> Unifiable (state, um_unif env)
umRnOccR :: UMEnv -> TyVar -> TyVar
umRnOccR env v = rnOccR (um_rn_env env) v
checkingInjectivity :: UM Bool
checkingInjectivity = UM $ \env state -> Unifiable (state, um_inj_tf env)
umSwapRn :: UMEnv -> UMEnv
umSwapRn env = env { um_rn_env = rnSwap (um_rn_env env) }
maybeApart :: UM ()
maybeApart = UM (\_ state -> MaybeApart (state, ()))
maybeApart = UM (\state -> MaybeApart (state, ()))
surelyApart :: UM a
surelyApart = UM (\_ _ -> SurelyApart)
surelyApart = UM (\_ -> SurelyApart)
{-
%************************************************************************
......
{-# LANGUAGE TypeFamilyDependencies #-}
module T13705 where
data D x
type family F t = s | s -> t
type instance F (D t) = D (F t)
f :: F s -> ()
f _ = ()
g :: D (F t) -> ()
g x = f x
......@@ -264,3 +264,4 @@ test('T13244', normal, compile, [''])
test('T13398a', normal, compile, [''])
test('T13398b', normal, compile, [''])
test('T13662', normal, compile, [''])
test('T13705', normal, compile, [''])
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment