module GHC.Tc.Zonk.TcType
(
module GHC.Tc.Zonk.Monad
, zonkTcType, zonkTcTypes, zonkScaledTcType
, zonkTcTyVar, zonkTcTyVars
, zonkTcTyVarToTcTyVar, zonkTcTyVarsToTcTyVars
, zonkInvisTVBinder
, zonkCo
, zonkTcTyCon
, zonkTcTypeAndFV, zonkTyCoVarsAndFV, zonkTyCoVarsAndFVList
, zonkDTyCoVarSetAndFV
, zonkId, zonkCoVar, zonkTyCoVar, zonkTyCoVarKind, zonkTyCoVarBndrKind
, zonkSkolemInfo, zonkSkolemInfoAnon
, zonkCt, zonkWC, zonkSimples, zonkImplication
, tcInitTidyEnv, tcInitOpenTidyEnv
, tidyCt, tidyEvVar, tidyDelayedError
, zonkTidyTcType, zonkTidyTcTypes
, zonkTidyOrigin, zonkTidyOrigins
, zonkTidyFRRInfos
, writeMetaTyVar, writeMetaTyVarRef
, checkCoercionHole
)
where
import GHC.Prelude
import GHC.Types.Name
import GHC.Types.Var
import GHC.Types.Var.Env
import GHC.Types.Var.Set
import GHC.Types.Unique.Set
import GHC.Tc.Errors.Types
import GHC.Tc.Errors.Ppr
import GHC.Tc.Types.Constraint
import GHC.Tc.Types.Origin
import GHC.Tc.Types.TcRef
import GHC.Tc.Types.Evidence
import GHC.Tc.Types.BasicTypes
import GHC.Tc.Utils.TcType
import GHC.Tc.Zonk.Monad
import GHC.Core.InstEnv (ClsInst(is_tys))
import GHC.Core.TyCo.Rep
import GHC.Core.TyCon
import GHC.Core.Type
import GHC.Core.Coercion
import GHC.Core.Predicate
import GHC.Utils.Constants
import GHC.Utils.Outputable
import GHC.Utils.Misc
import GHC.Utils.Monad ( mapAccumLM )
import GHC.Utils.Panic
import GHC.Data.Bag
import GHC.Data.Pair
writeMetaTyVar :: HasDebugCallStack
=> TcTyVar
-> TcType
-> ZonkM ()
writeMetaTyVar :: HasDebugCallStack => CoVar -> Type -> ZonkM ()
writeMetaTyVar CoVar
tyvar Type
ty
| Bool -> Bool
not Bool
debugIsOn
= HasDebugCallStack => CoVar -> TcRef MetaDetails -> Type -> ZonkM ()
CoVar -> TcRef MetaDetails -> Type -> ZonkM ()
writeMetaTyVarRef CoVar
tyvar (CoVar -> TcRef MetaDetails
metaTyVarRef CoVar
tyvar) Type
ty
| Bool -> Bool
not (CoVar -> Bool
isTcTyVar CoVar
tyvar)
= Bool -> SDoc -> ZonkM ()
forall (m :: * -> *).
(HasCallStack, Applicative m) =>
Bool -> SDoc -> m ()
massertPpr Bool
False (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Writing to non-tc tyvar" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> CoVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoVar
tyvar)
| MetaTv { mtv_ref :: TcTyVarDetails -> TcRef MetaDetails
mtv_ref = TcRef MetaDetails
ref } <- CoVar -> TcTyVarDetails
tcTyVarDetails CoVar
tyvar
= HasDebugCallStack => CoVar -> TcRef MetaDetails -> Type -> ZonkM ()
CoVar -> TcRef MetaDetails -> Type -> ZonkM ()
writeMetaTyVarRef CoVar
tyvar TcRef MetaDetails
ref Type
ty
| Bool
otherwise
= Bool -> SDoc -> ZonkM ()
forall (m :: * -> *).
(HasCallStack, Applicative m) =>
Bool -> SDoc -> m ()
massertPpr Bool
False (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Writing to non-meta tyvar" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> CoVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoVar
tyvar)
{-# INLINE writeMetaTyVar #-}
writeMetaTyVarRef :: HasDebugCallStack
=> TcTyVar
-> TcRef MetaDetails
-> TcType
-> ZonkM ()
writeMetaTyVarRef :: HasDebugCallStack => CoVar -> TcRef MetaDetails -> Type -> ZonkM ()
writeMetaTyVarRef CoVar
tyvar TcRef MetaDetails
ref Type
ty
| Bool -> Bool
not Bool
debugIsOn
= do { String -> SDoc -> ZonkM ()
traceZonk String
"writeMetaTyVar" (CoVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoVar
tyvar SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (CoVar -> Type
tyVarKind CoVar
tyvar)
SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
":=" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)
; TcRef MetaDetails -> MetaDetails -> ZonkM ()
forall (m :: * -> *) a. MonadIO m => TcRef a -> a -> m ()
writeTcRef TcRef MetaDetails
ref (Type -> MetaDetails
Indirect Type
ty) }
| Bool
otherwise
= do { meta_details <- TcRef MetaDetails -> ZonkM MetaDetails
forall (m :: * -> *) a. MonadIO m => TcRef a -> m a
readTcRef TcRef MetaDetails
ref;
; zonked_tv_kind <- zonkTcType tv_kind
; zonked_ty <- zonkTcType ty
; let zonked_ty_kind = HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
zonked_ty
zonked_ty_lvl = Type -> TcLevel
tcTypeLevel Type
zonked_ty
level_check_ok = Bool -> Bool
not (TcLevel
zonked_ty_lvl TcLevel -> TcLevel -> Bool
`strictlyDeeperThan` TcLevel
tv_lvl)
level_check_msg = TcLevel -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcLevel
zonked_ty_lvl SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ TcLevel -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcLevel
tv_lvl SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ CoVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoVar
tyvar SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
zonked_ty
kind_check_ok = Type
zonked_ty_kind HasCallStack => Type -> Type -> Bool
Type -> Type -> Bool
`eqType` Type
zonked_tv_kind
kind_msg = SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Ill-kinded update to meta tyvar")
Int
2 ( CoVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoVar
tyvar SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"::" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
tv_kind SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
zonked_tv_kind)
SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
":="
SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"::" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
zonked_ty_kind) )
; traceZonk "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
; massertPpr (isFlexi meta_details) (double_upd_msg meta_details)
; massertPpr level_check_ok level_check_msg
; massertPpr kind_check_ok kind_msg
; writeTcRef ref (Indirect ty) }
where
tv_kind :: Type
tv_kind = CoVar -> Type
tyVarKind CoVar
tyvar
tv_lvl :: TcLevel
tv_lvl = CoVar -> TcLevel
tcTyVarLevel CoVar
tyvar
double_upd_msg :: MetaDetails -> SDoc
double_upd_msg MetaDetails
details = SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Double update of meta tyvar")
Int
2 (CoVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoVar
tyvar SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ MetaDetails -> SDoc
forall a. Outputable a => a -> SDoc
ppr MetaDetails
details)
{-# INLINE writeMetaTyVarRef #-}
zonkScaledTcType :: Scaled TcType -> ZonkM (Scaled TcType)
zonkScaledTcType :: Scaled Type -> ZonkM (Scaled Type)
zonkScaledTcType (Scaled Type
m Type
ty)
= Type -> Type -> Scaled Type
forall a. Type -> a -> Scaled a
Scaled (Type -> Type -> Scaled Type)
-> ZonkM Type -> ZonkM (Type -> Scaled Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> ZonkM Type
zonkTcType Type
m ZonkM (Type -> Scaled Type) -> ZonkM Type -> ZonkM (Scaled Type)
forall a b. ZonkM (a -> b) -> ZonkM a -> ZonkM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> ZonkM Type
zonkTcType Type
ty
zonkTcType :: TcType -> ZonkM TcType
zonkTcTypes :: [TcType] -> ZonkM [TcType]
zonkCo :: Coercion -> ZonkM Coercion
(Type -> ZonkM Type
zonkTcType, [Type] -> ZonkM [Type]
zonkTcTypes, Coercion -> ZonkM Coercion
zonkCo, [Coercion] -> ZonkM [Coercion]
_)
= TyCoMapper () ZonkM
-> (Type -> ZonkM Type, [Type] -> ZonkM [Type],
Coercion -> ZonkM Coercion, [Coercion] -> ZonkM [Coercion])
forall (m :: * -> *).
Monad m =>
TyCoMapper () m
-> (Type -> m Type, [Type] -> m [Type], Coercion -> m Coercion,
[Coercion] -> m [Coercion])
mapTyCo TyCoMapper () ZonkM
zonkTcTypeMapper
where
zonkTcTypeMapper :: TyCoMapper () ZonkM
zonkTcTypeMapper :: TyCoMapper () ZonkM
zonkTcTypeMapper = TyCoMapper
{ tcm_tyvar :: () -> CoVar -> ZonkM Type
tcm_tyvar = (CoVar -> ZonkM Type) -> () -> CoVar -> ZonkM Type
forall a b. a -> b -> a
const CoVar -> ZonkM Type
zonkTcTyVar
, tcm_covar :: () -> CoVar -> ZonkM Coercion
tcm_covar = (CoVar -> ZonkM Coercion) -> () -> CoVar -> ZonkM Coercion
forall a b. a -> b -> a
const (\CoVar
cv -> CoVar -> Coercion
mkCoVarCo (CoVar -> Coercion) -> ZonkM CoVar -> ZonkM Coercion
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CoVar -> ZonkM CoVar
zonkTyCoVarKind CoVar
cv)
, tcm_hole :: () -> CoercionHole -> ZonkM Coercion
tcm_hole = () -> CoercionHole -> ZonkM Coercion
hole
, tcm_tycobinder :: forall r.
() -> CoVar -> ForAllTyFlag -> (() -> CoVar -> ZonkM r) -> ZonkM r
tcm_tycobinder = \ ()
_env CoVar
tcv ForAllTyFlag
_vis () -> CoVar -> ZonkM r
k -> CoVar -> ZonkM CoVar
zonkTyCoVarKind CoVar
tcv ZonkM CoVar -> (CoVar -> ZonkM r) -> ZonkM r
forall a b. ZonkM a -> (a -> ZonkM b) -> ZonkM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= () -> CoVar -> ZonkM r
k ()
, tcm_tycon :: TyCon -> ZonkM TyCon
tcm_tycon = TyCon -> ZonkM TyCon
zonkTcTyCon }
where
hole :: () -> CoercionHole -> ZonkM Coercion
hole :: () -> CoercionHole -> ZonkM Coercion
hole ()
_ hole :: CoercionHole
hole@(CoercionHole { ch_ref :: CoercionHole -> IORef (Maybe Coercion)
ch_ref = IORef (Maybe Coercion)
ref, ch_co_var :: CoercionHole -> CoVar
ch_co_var = CoVar
cv })
= do { contents <- IORef (Maybe Coercion) -> ZonkM (Maybe Coercion)
forall (m :: * -> *) a. MonadIO m => TcRef a -> m a
readTcRef IORef (Maybe Coercion)
ref
; case contents of
Just Coercion
co -> do { co' <- Coercion -> ZonkM Coercion
zonkCo Coercion
co
; checkCoercionHole cv co' }
Maybe Coercion
Nothing -> do { cv' <- CoVar -> ZonkM CoVar
zonkCoVar CoVar
cv
; return $ HoleCo (hole { ch_co_var = cv' }) } }
zonkTcTyCon :: TcTyCon -> ZonkM TcTyCon
zonkTcTyCon :: TyCon -> ZonkM TyCon
zonkTcTyCon TyCon
tc
| TyCon -> Bool
isMonoTcTyCon TyCon
tc = do { tck' <- Type -> ZonkM Type
zonkTcType (TyCon -> Type
tyConKind TyCon
tc)
; return (setTcTyConKind tc tck') }
| Bool
otherwise = TyCon -> ZonkM TyCon
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return TyCon
tc
zonkTcTyVar :: TcTyVar -> ZonkM TcType
zonkTcTyVar :: CoVar -> ZonkM Type
zonkTcTyVar CoVar
tv
| CoVar -> Bool
isTcTyVar CoVar
tv
= case CoVar -> TcTyVarDetails
tcTyVarDetails CoVar
tv of
SkolemTv {} -> ZonkM Type
zonk_kind_and_return
RuntimeUnk {} -> ZonkM Type
zonk_kind_and_return
MetaTv { mtv_ref :: TcTyVarDetails -> TcRef MetaDetails
mtv_ref = TcRef MetaDetails
ref }
-> do { cts <- TcRef MetaDetails -> ZonkM MetaDetails
forall (m :: * -> *) a. MonadIO m => TcRef a -> m a
readTcRef TcRef MetaDetails
ref
; case cts of
MetaDetails
Flexi -> ZonkM Type
zonk_kind_and_return
Indirect Type
ty -> do { zty <- Type -> ZonkM Type
zonkTcType Type
ty
; writeTcRef ref (Indirect zty)
; return zty } }
| Bool
otherwise
= ZonkM Type
zonk_kind_and_return
where
zonk_kind_and_return :: ZonkM Type
zonk_kind_and_return = do { z_tv <- CoVar -> ZonkM CoVar
zonkTyCoVarKind CoVar
tv
; return (mkTyVarTy z_tv) }
zonkTcTyVarsToTcTyVars :: HasDebugCallStack => [TcTyVar] -> ZonkM [TcTyVar]
zonkTcTyVarsToTcTyVars :: HasDebugCallStack => [CoVar] -> ZonkM [CoVar]
zonkTcTyVarsToTcTyVars = (CoVar -> ZonkM CoVar) -> [CoVar] -> ZonkM [CoVar]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM HasDebugCallStack => CoVar -> ZonkM CoVar
CoVar -> ZonkM CoVar
zonkTcTyVarToTcTyVar
zonkTcTyVarToTcTyVar :: HasDebugCallStack => TcTyVar -> ZonkM TcTyVar
zonkTcTyVarToTcTyVar :: HasDebugCallStack => CoVar -> ZonkM CoVar
zonkTcTyVarToTcTyVar CoVar
tv
= do { ty <- CoVar -> ZonkM Type
zonkTcTyVar CoVar
tv
; let tv' = case Type -> Maybe CoVar
getTyVar_maybe Type
ty of
Just CoVar
tv' -> CoVar
tv'
Maybe CoVar
Nothing -> String -> SDoc -> CoVar
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"zonkTcTyVarToTcTyVar"
(CoVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoVar
tv SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)
; return tv' }
zonkInvisTVBinder :: VarBndr TcTyVar spec -> ZonkM (VarBndr TcTyVar spec)
zonkInvisTVBinder :: forall spec. VarBndr CoVar spec -> ZonkM (VarBndr CoVar spec)
zonkInvisTVBinder (Bndr CoVar
tv spec
spec) = do { tv' <- HasDebugCallStack => CoVar -> ZonkM CoVar
CoVar -> ZonkM CoVar
zonkTcTyVarToTcTyVar CoVar
tv
; return (Bndr tv' spec) }
zonkTcTypeAndFV :: TcType -> ZonkM DTyCoVarSet
zonkTcTypeAndFV :: Type -> ZonkM DTyCoVarSet
zonkTcTypeAndFV Type
ty
= Type -> DTyCoVarSet
tyCoVarsOfTypeDSet (Type -> DTyCoVarSet) -> ZonkM Type -> ZonkM DTyCoVarSet
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> ZonkM Type
zonkTcType Type
ty
zonkTyCoVar :: TyCoVar -> ZonkM TcType
zonkTyCoVar :: CoVar -> ZonkM Type
zonkTyCoVar CoVar
tv | CoVar -> Bool
isTcTyVar CoVar
tv = CoVar -> ZonkM Type
zonkTcTyVar CoVar
tv
| CoVar -> Bool
isTyVar CoVar
tv = CoVar -> Type
mkTyVarTy (CoVar -> Type) -> ZonkM CoVar -> ZonkM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CoVar -> ZonkM CoVar
zonkTyCoVarKind CoVar
tv
| Bool
otherwise = Bool -> SDoc -> ZonkM Type -> ZonkM Type
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (CoVar -> Bool
isCoVar CoVar
tv) (CoVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoVar
tv) (ZonkM Type -> ZonkM Type) -> ZonkM Type -> ZonkM Type
forall a b. (a -> b) -> a -> b
$
Coercion -> Type
mkCoercionTy (Coercion -> Type) -> (CoVar -> Coercion) -> CoVar -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoVar -> Coercion
mkCoVarCo (CoVar -> Type) -> ZonkM CoVar -> ZonkM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CoVar -> ZonkM CoVar
zonkTyCoVarKind CoVar
tv
zonkTyCoVarsAndFV :: TyCoVarSet -> ZonkM TyCoVarSet
zonkTyCoVarsAndFV :: TyCoVarSet -> ZonkM TyCoVarSet
zonkTyCoVarsAndFV TyCoVarSet
tycovars
= [Type] -> TyCoVarSet
tyCoVarsOfTypes ([Type] -> TyCoVarSet) -> ZonkM [Type] -> ZonkM TyCoVarSet
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CoVar -> ZonkM Type) -> [CoVar] -> ZonkM [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM CoVar -> ZonkM Type
zonkTyCoVar (TyCoVarSet -> [CoVar]
forall elt. UniqSet elt -> [elt]
nonDetEltsUniqSet TyCoVarSet
tycovars)
zonkDTyCoVarSetAndFV :: DTyCoVarSet -> ZonkM DTyCoVarSet
zonkDTyCoVarSetAndFV :: DTyCoVarSet -> ZonkM DTyCoVarSet
zonkDTyCoVarSetAndFV DTyCoVarSet
tycovars
= [CoVar] -> DTyCoVarSet
mkDVarSet ([CoVar] -> DTyCoVarSet) -> ZonkM [CoVar] -> ZonkM DTyCoVarSet
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([CoVar] -> ZonkM [CoVar]
zonkTyCoVarsAndFVList ([CoVar] -> ZonkM [CoVar]) -> [CoVar] -> ZonkM [CoVar]
forall a b. (a -> b) -> a -> b
$ DTyCoVarSet -> [CoVar]
dVarSetElems DTyCoVarSet
tycovars)
zonkTyCoVarsAndFVList :: [TyCoVar] -> ZonkM [TyCoVar]
zonkTyCoVarsAndFVList :: [CoVar] -> ZonkM [CoVar]
zonkTyCoVarsAndFVList [CoVar]
tycovars
= [Type] -> [CoVar]
tyCoVarsOfTypesList ([Type] -> [CoVar]) -> ZonkM [Type] -> ZonkM [CoVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CoVar -> ZonkM Type) -> [CoVar] -> ZonkM [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM CoVar -> ZonkM Type
zonkTyCoVar [CoVar]
tycovars
zonkTcTyVars :: [TcTyVar] -> ZonkM [TcType]
zonkTcTyVars :: [CoVar] -> ZonkM [Type]
zonkTcTyVars [CoVar]
tyvars = (CoVar -> ZonkM Type) -> [CoVar] -> ZonkM [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM CoVar -> ZonkM Type
zonkTcTyVar [CoVar]
tyvars
zonkTyCoVarKind :: TyCoVar -> ZonkM TyCoVar
zonkTyCoVarKind :: CoVar -> ZonkM CoVar
zonkTyCoVarKind CoVar
tv = do { kind' <- Type -> ZonkM Type
zonkTcType (CoVar -> Type
tyVarKind CoVar
tv)
; return (setTyVarKind tv kind') }
zonkTyCoVarBndrKind :: VarBndr TyCoVar flag -> ZonkM (VarBndr TyCoVar flag)
zonkTyCoVarBndrKind :: forall spec. VarBndr CoVar spec -> ZonkM (VarBndr CoVar spec)
zonkTyCoVarBndrKind (Bndr CoVar
tv flag
flag) =
do { tv' <- CoVar -> ZonkM CoVar
zonkTyCoVarKind CoVar
tv
; return (Bndr tv' flag) }
zonkId :: TcId -> ZonkM TcId
zonkId :: CoVar -> ZonkM CoVar
zonkId CoVar
id = (Type -> ZonkM Type) -> CoVar -> ZonkM CoVar
forall (m :: * -> *).
Monad m =>
(Type -> m Type) -> CoVar -> m CoVar
updateIdTypeAndMultM Type -> ZonkM Type
zonkTcType CoVar
id
zonkCoVar :: CoVar -> ZonkM CoVar
zonkCoVar :: CoVar -> ZonkM CoVar
zonkCoVar = CoVar -> ZonkM CoVar
zonkId
checkCoercionHole :: CoVar -> Coercion -> ZonkM Coercion
checkCoercionHole :: CoVar -> Coercion -> ZonkM Coercion
checkCoercionHole CoVar
cv Coercion
co
| Bool
debugIsOn
= do { cv_ty <- Type -> ZonkM Type
zonkTcType (CoVar -> Type
varType CoVar
cv)
; return $
assertPpr (ok cv_ty)
(text "Bad coercion hole" <+>
ppr cv <> colon <+> vcat [ ppr t1, ppr t2, ppr role
, ppr cv_ty ])
co }
| Bool
otherwise
= Coercion -> ZonkM Coercion
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return Coercion
co
where
(Pair Type
t1 Type
t2, Role
role) = Coercion -> (Pair Type, Role)
coercionKindRole Coercion
co
ok :: Type -> Bool
ok Type
cv_ty | EqPred EqRel
cv_rel Type
cv_t1 Type
cv_t2 <- Type -> Pred
classifyPredType Type
cv_ty
= Type
t1 HasCallStack => Type -> Type -> Bool
Type -> Type -> Bool
`eqType` Type
cv_t1
Bool -> Bool -> Bool
&& Type
t2 HasCallStack => Type -> Type -> Bool
Type -> Type -> Bool
`eqType` Type
cv_t2
Bool -> Bool -> Bool
&& Role
role Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== EqRel -> Role
eqRelRole EqRel
cv_rel
| Bool
otherwise
= Bool
False
zonkImplication :: Implication -> ZonkM Implication
zonkImplication :: Implication -> ZonkM Implication
zonkImplication implic :: Implication
implic@(Implic { ic_skols :: Implication -> [CoVar]
ic_skols = [CoVar]
skols
, ic_given :: Implication -> [CoVar]
ic_given = [CoVar]
given
, ic_wanted :: Implication -> WantedConstraints
ic_wanted = WantedConstraints
wanted
, ic_info :: Implication -> SkolemInfoAnon
ic_info = SkolemInfoAnon
info })
= do { skols' <- (CoVar -> ZonkM CoVar) -> [CoVar] -> ZonkM [CoVar]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM CoVar -> ZonkM CoVar
zonkTyCoVarKind [CoVar]
skols
; given' <- mapM zonkEvVar given
; info' <- zonkSkolemInfoAnon info
; wanted' <- zonkWCRec wanted
; return (implic { ic_skols = skols'
, ic_given = given'
, ic_wanted = wanted'
, ic_info = info' }) }
zonkEvVar :: EvVar -> ZonkM EvVar
zonkEvVar :: CoVar -> ZonkM CoVar
zonkEvVar CoVar
var = (Type -> ZonkM Type) -> CoVar -> ZonkM CoVar
forall (m :: * -> *).
Monad m =>
(Type -> m Type) -> CoVar -> m CoVar
updateIdTypeAndMultM Type -> ZonkM Type
zonkTcType CoVar
var
zonkWC :: WantedConstraints -> ZonkM WantedConstraints
zonkWC :: WantedConstraints -> ZonkM WantedConstraints
zonkWC WantedConstraints
wc = WantedConstraints -> ZonkM WantedConstraints
zonkWCRec WantedConstraints
wc
zonkWCRec :: WantedConstraints -> ZonkM WantedConstraints
zonkWCRec :: WantedConstraints -> ZonkM WantedConstraints
zonkWCRec (WC { wc_simple :: WantedConstraints -> Bag Ct
wc_simple = Bag Ct
simple, wc_impl :: WantedConstraints -> Bag Implication
wc_impl = Bag Implication
implic, wc_errors :: WantedConstraints -> Bag DelayedError
wc_errors = Bag DelayedError
errs })
= do { simple' <- Bag Ct -> ZonkM (Bag Ct)
zonkSimples Bag Ct
simple
; implic' <- mapBagM zonkImplication implic
; errs' <- mapBagM zonkDelayedError errs
; return (WC { wc_simple = simple', wc_impl = implic', wc_errors = errs' }) }
zonkSimples :: Cts -> ZonkM Cts
zonkSimples :: Bag Ct -> ZonkM (Bag Ct)
zonkSimples Bag Ct
cts = do { cts' <- (Ct -> ZonkM Ct) -> Bag Ct -> ZonkM (Bag Ct)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Bag a -> m (Bag b)
mapBagM Ct -> ZonkM Ct
zonkCt Bag Ct
cts
; traceZonk "zonkSimples done:" (ppr cts')
; return cts' }
zonkDelayedError :: DelayedError -> ZonkM DelayedError
zonkDelayedError :: DelayedError -> ZonkM DelayedError
zonkDelayedError (DE_Hole Hole
hole)
= Hole -> DelayedError
DE_Hole (Hole -> DelayedError) -> ZonkM Hole -> ZonkM DelayedError
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Hole -> ZonkM Hole
zonkHole Hole
hole
zonkDelayedError (DE_NotConcrete NotConcreteError
err)
= NotConcreteError -> DelayedError
DE_NotConcrete (NotConcreteError -> DelayedError)
-> ZonkM NotConcreteError -> ZonkM DelayedError
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NotConcreteError -> ZonkM NotConcreteError
zonkNotConcreteError NotConcreteError
err
zonkDelayedError (DE_Multiplicity Coercion
mult_co CtLoc
loc)
= Coercion -> CtLoc -> DelayedError
DE_Multiplicity (Coercion -> CtLoc -> DelayedError)
-> ZonkM Coercion -> ZonkM (CtLoc -> DelayedError)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Coercion -> ZonkM Coercion
zonkCo Coercion
mult_co ZonkM (CtLoc -> DelayedError) -> ZonkM CtLoc -> ZonkM DelayedError
forall a b. ZonkM (a -> b) -> ZonkM a -> ZonkM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> CtLoc -> ZonkM CtLoc
forall a. a -> ZonkM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CtLoc
loc
zonkHole :: Hole -> ZonkM Hole
zonkHole :: Hole -> ZonkM Hole
zonkHole hole :: Hole
hole@(Hole { hole_ty :: Hole -> Type
hole_ty = Type
ty })
= do { ty' <- Type -> ZonkM Type
zonkTcType Type
ty
; return (hole { hole_ty = ty' }) }
zonkNotConcreteError :: NotConcreteError -> ZonkM NotConcreteError
zonkNotConcreteError :: NotConcreteError -> ZonkM NotConcreteError
zonkNotConcreteError err :: NotConcreteError
err@(NCE_FRR { nce_frr_origin :: NotConcreteError -> FixedRuntimeRepOrigin
nce_frr_origin = FixedRuntimeRepOrigin
frr_orig })
= do { frr_orig <- FixedRuntimeRepOrigin -> ZonkM FixedRuntimeRepOrigin
zonkFRROrigin FixedRuntimeRepOrigin
frr_orig
; return $ err { nce_frr_origin = frr_orig } }
zonkFRROrigin :: FixedRuntimeRepOrigin -> ZonkM FixedRuntimeRepOrigin
zonkFRROrigin :: FixedRuntimeRepOrigin -> ZonkM FixedRuntimeRepOrigin
zonkFRROrigin (FixedRuntimeRepOrigin Type
ty FixedRuntimeRepContext
orig)
= do { ty' <- Type -> ZonkM Type
zonkTcType Type
ty
; return $ FixedRuntimeRepOrigin ty' orig }
zonkCt :: Ct -> ZonkM Ct
zonkCt :: Ct -> ZonkM Ct
zonkCt (CDictCan dict :: DictCt
dict@(DictCt { di_ev :: DictCt -> CtEvidence
di_ev = CtEvidence
ev, di_tys :: DictCt -> [Type]
di_tys = [Type]
args }))
= do { ev' <- CtEvidence -> ZonkM CtEvidence
zonkCtEvidence CtEvidence
ev
; args' <- mapM zonkTcType args
; return (CDictCan (dict { di_ev = ev', di_tys = args' })) }
zonkCt (CEqCan (EqCt { eq_ev :: EqCt -> CtEvidence
eq_ev = CtEvidence
ev }))
= CtEvidence -> Ct
mkNonCanonical (CtEvidence -> Ct) -> ZonkM CtEvidence -> ZonkM Ct
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CtEvidence -> ZonkM CtEvidence
zonkCtEvidence CtEvidence
ev
zonkCt (CIrredCan ir :: IrredCt
ir@(IrredCt { ir_ev :: IrredCt -> CtEvidence
ir_ev = CtEvidence
ev }))
= do { ev' <- CtEvidence -> ZonkM CtEvidence
zonkCtEvidence CtEvidence
ev
; return (CIrredCan (ir { ir_ev = ev' })) }
zonkCt Ct
ct
= do { fl' <- CtEvidence -> ZonkM CtEvidence
zonkCtEvidence (Ct -> CtEvidence
ctEvidence Ct
ct)
; return (mkNonCanonical fl') }
zonkCtEvidence :: CtEvidence -> ZonkM CtEvidence
zonkCtEvidence :: CtEvidence -> ZonkM CtEvidence
zonkCtEvidence CtEvidence
ctev
= do { let pred :: Type
pred = CtEvidence -> Type
ctev_pred CtEvidence
ctev
; pred' <- Type -> ZonkM Type
zonkTcType Type
pred
; return (setCtEvPredType ctev pred') }
zonkSkolemInfo :: SkolemInfo -> ZonkM SkolemInfo
zonkSkolemInfo :: SkolemInfo -> ZonkM SkolemInfo
zonkSkolemInfo (SkolemInfo Unique
u SkolemInfoAnon
sk) = Unique -> SkolemInfoAnon -> SkolemInfo
SkolemInfo Unique
u (SkolemInfoAnon -> SkolemInfo)
-> ZonkM SkolemInfoAnon -> ZonkM SkolemInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SkolemInfoAnon -> ZonkM SkolemInfoAnon
zonkSkolemInfoAnon SkolemInfoAnon
sk
zonkSkolemInfoAnon :: SkolemInfoAnon -> ZonkM SkolemInfoAnon
zonkSkolemInfoAnon :: SkolemInfoAnon -> ZonkM SkolemInfoAnon
zonkSkolemInfoAnon (SigSkol UserTypeCtxt
cx Type
ty [(Name, CoVar)]
tv_prs) = do { ty' <- Type -> ZonkM Type
zonkTcType Type
ty
; return (SigSkol cx ty' tv_prs) }
zonkSkolemInfoAnon (InferSkol [(Name, Type)]
ntys) = do { ntys' <- ((Name, Type) -> ZonkM (Name, Type))
-> [(Name, Type)] -> ZonkM [(Name, Type)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Name, Type) -> ZonkM (Name, Type)
forall {a}. (a, Type) -> ZonkM (a, Type)
do_one [(Name, Type)]
ntys
; return (InferSkol ntys') }
where
do_one :: (a, Type) -> ZonkM (a, Type)
do_one (a
n, Type
ty) = do { ty' <- Type -> ZonkM Type
zonkTcType Type
ty; return (n, ty') }
zonkSkolemInfoAnon SkolemInfoAnon
skol_info = SkolemInfoAnon -> ZonkM SkolemInfoAnon
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return SkolemInfoAnon
skol_info
tcInitTidyEnv :: ZonkM TidyEnv
tcInitTidyEnv :: ZonkM TidyEnv
tcInitTidyEnv
= do { ZonkGblEnv { zge_binder_stack = bndrs } <- ZonkM ZonkGblEnv
getZonkGblEnv
; go emptyTidyEnv bndrs }
where
go :: TidyEnv -> TcBinderStack -> ZonkM TidyEnv
go (TidyOccEnv
env, VarEnv CoVar
subst) []
= TidyEnv -> ZonkM TidyEnv
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyOccEnv
env, VarEnv CoVar
subst)
go (TidyOccEnv
env, VarEnv CoVar
subst) (TcBinder
b : TcBinderStack
bs)
| TcTvBndr Name
name CoVar
tyvar <- TcBinder
b
= do { let (TidyOccEnv
env', OccName
occ') = TidyOccEnv -> OccName -> (TidyOccEnv, OccName)
tidyOccName TidyOccEnv
env (Name -> OccName
nameOccName Name
name)
name' :: Name
name' = Name -> OccName -> Name
tidyNameOcc Name
name OccName
occ'
tyvar1 :: CoVar
tyvar1 = CoVar -> Name -> CoVar
setTyVarName CoVar
tyvar Name
name'
; tyvar2 <- HasDebugCallStack => CoVar -> ZonkM CoVar
CoVar -> ZonkM CoVar
zonkTcTyVarToTcTyVar CoVar
tyvar1
; go (env', extendVarEnv subst tyvar tyvar2) bs }
| Bool
otherwise
= TidyEnv -> TcBinderStack -> ZonkM TidyEnv
go (TidyOccEnv
env, VarEnv CoVar
subst) TcBinderStack
bs
tcInitOpenTidyEnv :: [TyCoVar] -> ZonkM TidyEnv
tcInitOpenTidyEnv :: [CoVar] -> ZonkM TidyEnv
tcInitOpenTidyEnv [CoVar]
tvs
= do { env1 <- ZonkM TidyEnv
tcInitTidyEnv
; return (tidyFreeTyCoVars env1 tvs) }
zonkTidyTcType :: TidyEnv -> TcType -> ZonkM (TidyEnv, TcType)
zonkTidyTcType :: TidyEnv -> Type -> ZonkM (TidyEnv, Type)
zonkTidyTcType TidyEnv
env Type
ty = do { ty' <- Type -> ZonkM Type
zonkTcType Type
ty
; return (tidyOpenTypeX env ty') }
zonkTidyTcTypes :: TidyEnv -> [TcType] -> ZonkM (TidyEnv, [TcType])
zonkTidyTcTypes :: TidyEnv -> [Type] -> ZonkM (TidyEnv, [Type])
zonkTidyTcTypes = [Type] -> TidyEnv -> [Type] -> ZonkM (TidyEnv, [Type])
zonkTidyTcTypes' []
where zonkTidyTcTypes' :: [Type] -> TidyEnv -> [Type] -> ZonkM (TidyEnv, [Type])
zonkTidyTcTypes' [Type]
zs TidyEnv
env [] = (TidyEnv, [Type]) -> ZonkM (TidyEnv, [Type])
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
env, [Type] -> [Type]
forall a. [a] -> [a]
reverse [Type]
zs)
zonkTidyTcTypes' [Type]
zs TidyEnv
env (Type
ty:[Type]
tys)
= do { (env', ty') <- TidyEnv -> Type -> ZonkM (TidyEnv, Type)
zonkTidyTcType TidyEnv
env Type
ty
; zonkTidyTcTypes' (ty':zs) env' tys }
zonkTidyOrigin :: TidyEnv -> CtOrigin -> ZonkM (TidyEnv, CtOrigin)
zonkTidyOrigin :: TidyEnv -> CtOrigin -> ZonkM (TidyEnv, CtOrigin)
zonkTidyOrigin TidyEnv
env (GivenOrigin SkolemInfoAnon
skol_info)
= do { skol_info1 <- SkolemInfoAnon -> ZonkM SkolemInfoAnon
zonkSkolemInfoAnon SkolemInfoAnon
skol_info
; let skol_info2 = TidyEnv -> SkolemInfoAnon -> SkolemInfoAnon
tidySkolemInfoAnon TidyEnv
env SkolemInfoAnon
skol_info1
; return (env, GivenOrigin skol_info2) }
zonkTidyOrigin TidyEnv
env (GivenSCOrigin SkolemInfoAnon
skol_info Int
sc_depth Bool
blocked)
= do { skol_info1 <- SkolemInfoAnon -> ZonkM SkolemInfoAnon
zonkSkolemInfoAnon SkolemInfoAnon
skol_info
; let skol_info2 = TidyEnv -> SkolemInfoAnon -> SkolemInfoAnon
tidySkolemInfoAnon TidyEnv
env SkolemInfoAnon
skol_info1
; return (env, GivenSCOrigin skol_info2 sc_depth blocked) }
zonkTidyOrigin TidyEnv
env orig :: CtOrigin
orig@(TypeEqOrigin { uo_actual :: CtOrigin -> Type
uo_actual = Type
act
, uo_expected :: CtOrigin -> Type
uo_expected = Type
exp })
= do { (env1, act') <- TidyEnv -> Type -> ZonkM (TidyEnv, Type)
zonkTidyTcType TidyEnv
env Type
act
; (env2, exp') <- zonkTidyTcType env1 exp
; return ( env2, orig { uo_actual = act'
, uo_expected = exp' }) }
zonkTidyOrigin TidyEnv
env (KindEqOrigin Type
ty1 Type
ty2 CtOrigin
orig Maybe TypeOrKind
t_or_k)
= do { (env1, ty1') <- TidyEnv -> Type -> ZonkM (TidyEnv, Type)
zonkTidyTcType TidyEnv
env Type
ty1
; (env2, ty2') <- zonkTidyTcType env1 ty2
; (env3, orig') <- zonkTidyOrigin env2 orig
; return (env3, KindEqOrigin ty1' ty2' orig' t_or_k) }
zonkTidyOrigin TidyEnv
env (FunDepOrigin1 Type
p1 CtOrigin
o1 RealSrcSpan
l1 Type
p2 CtOrigin
o2 RealSrcSpan
l2)
= do { (env1, p1') <- TidyEnv -> Type -> ZonkM (TidyEnv, Type)
zonkTidyTcType TidyEnv
env Type
p1
; (env2, o1') <- zonkTidyOrigin env1 o1
; (env3, p2') <- zonkTidyTcType env2 p2
; (env4, o2') <- zonkTidyOrigin env3 o2
; return (env4, FunDepOrigin1 p1' o1' l1 p2' o2' l2) }
zonkTidyOrigin TidyEnv
env (FunDepOrigin2 Type
p1 CtOrigin
o1 Type
p2 SrcSpan
l2)
= do { (env1, p1') <- TidyEnv -> Type -> ZonkM (TidyEnv, Type)
zonkTidyTcType TidyEnv
env Type
p1
; (env2, p2') <- zonkTidyTcType env1 p2
; (env3, o1') <- zonkTidyOrigin env2 o1
; return (env3, FunDepOrigin2 p1' o1' p2' l2) }
zonkTidyOrigin TidyEnv
env (InjTFOrigin1 Type
pred1 CtOrigin
orig1 RealSrcSpan
loc1 Type
pred2 CtOrigin
orig2 RealSrcSpan
loc2)
= do { (env1, pred1') <- TidyEnv -> Type -> ZonkM (TidyEnv, Type)
zonkTidyTcType TidyEnv
env Type
pred1
; (env2, orig1') <- zonkTidyOrigin env1 orig1
; (env3, pred2') <- zonkTidyTcType env2 pred2
; (env4, orig2') <- zonkTidyOrigin env3 orig2
; return (env4, InjTFOrigin1 pred1' orig1' loc1 pred2' orig2' loc2) }
zonkTidyOrigin TidyEnv
env (CycleBreakerOrigin CtOrigin
orig)
= do { (env1, orig') <- TidyEnv -> CtOrigin -> ZonkM (TidyEnv, CtOrigin)
zonkTidyOrigin TidyEnv
env CtOrigin
orig
; return (env1, CycleBreakerOrigin orig') }
zonkTidyOrigin TidyEnv
env (InstProvidedOrigin Module
mod ClsInst
cls_inst)
= do { (env1, is_tys') <- (TidyEnv -> Type -> ZonkM (TidyEnv, Type))
-> TidyEnv -> [Type] -> ZonkM (TidyEnv, [Type])
forall (m :: * -> *) (t :: * -> *) acc x y.
(Monad m, Traversable t) =>
(acc -> x -> m (acc, y)) -> acc -> t x -> m (acc, t y)
mapAccumLM TidyEnv -> Type -> ZonkM (TidyEnv, Type)
zonkTidyTcType TidyEnv
env (ClsInst -> [Type]
is_tys ClsInst
cls_inst)
; return (env1, InstProvidedOrigin mod (cls_inst {is_tys = is_tys'})) }
zonkTidyOrigin TidyEnv
env (WantedSuperclassOrigin Type
pty CtOrigin
orig)
= do { (env1, pty') <- TidyEnv -> Type -> ZonkM (TidyEnv, Type)
zonkTidyTcType TidyEnv
env Type
pty
; (env2, orig') <- zonkTidyOrigin env1 orig
; return (env2, WantedSuperclassOrigin pty' orig') }
zonkTidyOrigin TidyEnv
env CtOrigin
orig = (TidyEnv, CtOrigin) -> ZonkM (TidyEnv, CtOrigin)
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
env, CtOrigin
orig)
zonkTidyOrigins :: TidyEnv -> [CtOrigin] -> ZonkM (TidyEnv, [CtOrigin])
zonkTidyOrigins :: TidyEnv -> [CtOrigin] -> ZonkM (TidyEnv, [CtOrigin])
zonkTidyOrigins = (TidyEnv -> CtOrigin -> ZonkM (TidyEnv, CtOrigin))
-> TidyEnv -> [CtOrigin] -> ZonkM (TidyEnv, [CtOrigin])
forall (m :: * -> *) (t :: * -> *) acc x y.
(Monad m, Traversable t) =>
(acc -> x -> m (acc, y)) -> acc -> t x -> m (acc, t y)
mapAccumLM TidyEnv -> CtOrigin -> ZonkM (TidyEnv, CtOrigin)
zonkTidyOrigin
zonkTidyFRRInfos :: TidyEnv
-> [FixedRuntimeRepErrorInfo]
-> ZonkM (TidyEnv, [FixedRuntimeRepErrorInfo])
zonkTidyFRRInfos :: TidyEnv
-> [FixedRuntimeRepErrorInfo]
-> ZonkM (TidyEnv, [FixedRuntimeRepErrorInfo])
zonkTidyFRRInfos = [FixedRuntimeRepErrorInfo]
-> TidyEnv
-> [FixedRuntimeRepErrorInfo]
-> ZonkM (TidyEnv, [FixedRuntimeRepErrorInfo])
go []
where
go :: [FixedRuntimeRepErrorInfo]
-> TidyEnv
-> [FixedRuntimeRepErrorInfo]
-> ZonkM (TidyEnv, [FixedRuntimeRepErrorInfo])
go [FixedRuntimeRepErrorInfo]
zs TidyEnv
env [] = (TidyEnv, [FixedRuntimeRepErrorInfo])
-> ZonkM (TidyEnv, [FixedRuntimeRepErrorInfo])
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
env, [FixedRuntimeRepErrorInfo] -> [FixedRuntimeRepErrorInfo]
forall a. [a] -> [a]
reverse [FixedRuntimeRepErrorInfo]
zs)
go [FixedRuntimeRepErrorInfo]
zs TidyEnv
env (FRR_Info { frr_info_origin :: FixedRuntimeRepErrorInfo -> FixedRuntimeRepOrigin
frr_info_origin = FixedRuntimeRepOrigin Type
ty FixedRuntimeRepContext
orig
, frr_info_not_concrete :: FixedRuntimeRepErrorInfo -> Maybe (CoVar, Type)
frr_info_not_concrete = Maybe (CoVar, Type)
mb_not_conc } : [FixedRuntimeRepErrorInfo]
tys)
= do { (env, ty) <- TidyEnv -> Type -> ZonkM (TidyEnv, Type)
zonkTidyTcType TidyEnv
env Type
ty
; (env, mb_not_conc) <- go_mb_not_conc env mb_not_conc
; let info = FRR_Info { frr_info_origin :: FixedRuntimeRepOrigin
frr_info_origin = Type -> FixedRuntimeRepContext -> FixedRuntimeRepOrigin
FixedRuntimeRepOrigin Type
ty FixedRuntimeRepContext
orig
, frr_info_not_concrete :: Maybe (CoVar, Type)
frr_info_not_concrete = Maybe (CoVar, Type)
mb_not_conc }
; go (info:zs) env tys }
go_mb_not_conc :: TidyEnv
-> Maybe (CoVar, Type) -> ZonkM (TidyEnv, Maybe (CoVar, Type))
go_mb_not_conc TidyEnv
env Maybe (CoVar, Type)
Nothing = (TidyEnv, Maybe (CoVar, Type))
-> ZonkM (TidyEnv, Maybe (CoVar, Type))
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
env, Maybe (CoVar, Type)
forall a. Maybe a
Nothing)
go_mb_not_conc TidyEnv
env (Just (CoVar
tv, Type
ty))
= do { (env, tv) <- (TidyEnv, CoVar) -> ZonkM (TidyEnv, CoVar)
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return ((TidyEnv, CoVar) -> ZonkM (TidyEnv, CoVar))
-> (TidyEnv, CoVar) -> ZonkM (TidyEnv, CoVar)
forall a b. (a -> b) -> a -> b
$ TidyEnv -> CoVar -> (TidyEnv, CoVar)
tidyFreeTyCoVarX TidyEnv
env CoVar
tv
; (env, ty) <- zonkTidyTcType env ty
; return (env, Just (tv, ty)) }
tidyCt :: TidyEnv -> Ct -> Ct
tidyCt :: TidyEnv -> Ct -> Ct
tidyCt TidyEnv
env = (CtEvidence -> CtEvidence) -> Ct -> Ct
updCtEvidence (TidyEnv -> CtEvidence -> CtEvidence
tidyCtEvidence TidyEnv
env)
tidyCtEvidence :: TidyEnv -> CtEvidence -> CtEvidence
tidyCtEvidence :: TidyEnv -> CtEvidence -> CtEvidence
tidyCtEvidence TidyEnv
env CtEvidence
ctev
= CtEvidence
ctev { ctev_pred = tidyOpenType env $ ctev_pred ctev }
tidyHole :: TidyEnv -> Hole -> Hole
tidyHole :: TidyEnv -> Hole -> Hole
tidyHole TidyEnv
env h :: Hole
h@(Hole { hole_ty :: Hole -> Type
hole_ty = Type
ty })
= Hole
h { hole_ty = tidyOpenType env ty }
tidyDelayedError :: TidyEnv -> DelayedError -> DelayedError
tidyDelayedError :: TidyEnv -> DelayedError -> DelayedError
tidyDelayedError TidyEnv
env (DE_Hole Hole
hole) = Hole -> DelayedError
DE_Hole (Hole -> DelayedError) -> Hole -> DelayedError
forall a b. (a -> b) -> a -> b
$ TidyEnv -> Hole -> Hole
tidyHole TidyEnv
env Hole
hole
tidyDelayedError TidyEnv
env (DE_NotConcrete NotConcreteError
err) = NotConcreteError -> DelayedError
DE_NotConcrete (NotConcreteError -> DelayedError)
-> NotConcreteError -> DelayedError
forall a b. (a -> b) -> a -> b
$ TidyEnv -> NotConcreteError -> NotConcreteError
tidyConcreteError TidyEnv
env NotConcreteError
err
tidyDelayedError TidyEnv
env (DE_Multiplicity Coercion
mult_co CtLoc
loc)
= Coercion -> CtLoc -> DelayedError
DE_Multiplicity (TidyEnv -> Coercion -> Coercion
tidyCo TidyEnv
env Coercion
mult_co) CtLoc
loc
tidyConcreteError :: TidyEnv -> NotConcreteError -> NotConcreteError
tidyConcreteError :: TidyEnv -> NotConcreteError -> NotConcreteError
tidyConcreteError TidyEnv
env err :: NotConcreteError
err@(NCE_FRR { nce_frr_origin :: NotConcreteError -> FixedRuntimeRepOrigin
nce_frr_origin = FixedRuntimeRepOrigin
frr_orig })
= NotConcreteError
err { nce_frr_origin = tidyFRROrigin env frr_orig }
tidyFRROrigin :: TidyEnv -> FixedRuntimeRepOrigin -> FixedRuntimeRepOrigin
tidyFRROrigin :: TidyEnv -> FixedRuntimeRepOrigin -> FixedRuntimeRepOrigin
tidyFRROrigin TidyEnv
env (FixedRuntimeRepOrigin Type
ty FixedRuntimeRepContext
orig)
= Type -> FixedRuntimeRepContext -> FixedRuntimeRepOrigin
FixedRuntimeRepOrigin (TidyEnv -> Type -> Type
tidyType TidyEnv
env Type
ty) FixedRuntimeRepContext
orig
tidyEvVar :: TidyEnv -> EvVar -> EvVar
tidyEvVar :: TidyEnv -> CoVar -> CoVar
tidyEvVar TidyEnv
env CoVar
var = (Type -> Type) -> CoVar -> CoVar
updateIdTypeAndMult (TidyEnv -> Type -> Type
tidyType TidyEnv
env) CoVar
var