{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE TupleSections #-}
{-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
module GHC.Tc.Utils.TcMType (
TcTyVar, TcKind, TcType, TcTauType, TcThetaType, TcTyVarSet,
newFlexiTyVar,
newNamedFlexiTyVar,
newFlexiTyVarTy,
newFlexiTyVarTys,
newOpenFlexiTyVar, newOpenFlexiTyVarTy, newOpenTypeKind,
newOpenBoxedTypeKind,
newMetaKindVar, newMetaKindVars, newMetaTyVarTyAtLevel,
newAnonMetaTyVar, cloneMetaTyVar,
newCycleBreakerTyVar,
newMultiplicityVar,
readMetaTyVar, writeMetaTyVar, writeMetaTyVarRef,
newTauTvDetailsAtLevel, newMetaDetails, newMetaTyVarName,
isFilledMetaTyVar_maybe, isFilledMetaTyVar, isUnfilledMetaTyVar,
newEvVar, newEvVars, newDict,
newWantedWithLoc, newWanted, newWanteds, cloneWanted, cloneWC, cloneWantedCtEv,
emitWanted, emitWantedEq, emitWantedEvVar, emitWantedEvVars,
emitWantedEqs,
newTcEvBinds, newNoTcEvBinds, addTcEvBind,
emitNewExprHole,
newCoercionHole, fillCoercionHole, isFilledCoercionHole,
unpackCoercionHole, unpackCoercionHole_maybe,
checkCoercionHole,
ConcreteHole, newConcreteHole,
newImplication,
newMetaTyVars, newMetaTyVarX, newMetaTyVarsX,
newMetaTyVarTyVarX,
newTyVarTyVar, cloneTyVarTyVar,
newPatSigTyVar, newSkolemTyVar, newWildCardX,
ExpType(..), ExpSigmaType, ExpRhoType,
mkCheckExpType, newInferExpType, tcInfer,
readExpType, readExpType_maybe, readScaledExpType,
expTypeToType, scaledExpTypeToType,
checkingExpType_maybe, checkingExpType,
inferResultToType, fillInferResult, promoteTcType,
zonkTidyTcType, zonkTidyTcTypes, zonkTidyOrigin, zonkTidyOrigins,
tidyEvVar, tidyCt, tidyHole,
zonkTcTyVar, zonkTcTyVars,
zonkTcTyVarToTcTyVar, zonkTcTyVarsToTcTyVars,
zonkInvisTVBinder,
zonkTyCoVarsAndFV, zonkTcTypeAndFV, zonkDTyCoVarSetAndFV,
zonkTyCoVarsAndFVList,
zonkTcType, zonkTcTypes, zonkCo,
zonkTyCoVarKind,
zonkEvVar, zonkWC, zonkImplication, zonkSimples,
zonkId, zonkCoVar,
zonkCt, zonkSkolemInfo, zonkSkolemInfoAnon,
defaultTyVar, promoteMetaTyVarTo, promoteTyVarSet,
quantifyTyVars, isQuantifiableTv,
zonkAndSkolemise, skolemiseQuantifiedTyVar,
doNotQuantifyTyVars,
candidateQTyVarsOfType, candidateQTyVarsOfKind,
candidateQTyVarsOfTypes, candidateQTyVarsOfKinds,
candidateQTyVarsWithBinders,
CandidatesQTvs(..), delCandidates,
candidateKindVars, partitionCandidates,
checkTypeHasFixedRuntimeRep,
anyUnfilledCoercionHoles
) where
import GHC.Prelude
import GHC.Driver.Session
import qualified GHC.LanguageExtensions as LangExt
import GHC.Tc.Types.Origin
import GHC.Tc.Utils.Monad
import GHC.Tc.Types.Constraint
import GHC.Tc.Types.Evidence
import {-# SOURCE #-} GHC.Tc.Utils.Unify( unifyType )
import GHC.Tc.Utils.TcType
import GHC.Tc.Errors.Types
import GHC.Tc.Errors.Ppr
import GHC.Core.TyCo.Rep
import GHC.Core.TyCo.Ppr
import GHC.Core.Type
import GHC.Core.TyCon
import GHC.Core.Coercion
import GHC.Core.Class
import GHC.Core.Predicate
import GHC.Core.InstEnv (ClsInst(is_tys))
import GHC.Types.Var
import GHC.Types.Id as Id
import GHC.Types.Name
import GHC.Types.Var.Set
import GHC.Builtin.Types
import GHC.Types.Error
import GHC.Types.Var.Env
import GHC.Types.Unique.Set
import GHC.Types.Basic ( TypeOrKind(..)
, NonStandardDefaultingStrategy(..)
, DefaultingStrategy(..), defaultNonStandardTyVars )
import GHC.Data.FastString
import GHC.Data.Bag
import GHC.Data.Pair
import GHC.Utils.Misc
import GHC.Utils.Outputable
import GHC.Utils.Panic
import GHC.Utils.Panic.Plain
import GHC.Utils.Constants (debugIsOn)
import GHC.Utils.Trace
import Control.Monad
import GHC.Data.Maybe
import qualified Data.Semigroup as Semi
newMetaKindVar :: TcM TcKind
newMetaKindVar :: TcM TcKind
newMetaKindVar
= do { TcTyVarDetails
details <- MetaInfo -> TcM TcTyVarDetails
newMetaDetails MetaInfo
TauTv
; Name
name <- FastString -> TcM Name
newMetaTyVarName (String -> FastString
fsLit String
"k")
; let kv :: TyVar
kv = Name -> TcKind -> TcTyVarDetails -> TyVar
mkTcTyVar Name
name TcKind
liftedTypeKind TcTyVarDetails
details
; String -> SDoc -> TcRn ()
traceTc String
"newMetaKindVar" (TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
kv)
; TcKind -> TcM TcKind
forall (m :: * -> *) a. Monad m => a -> m a
return (TyVar -> TcKind
mkTyVarTy TyVar
kv) }
newMetaKindVars :: Int -> TcM [TcKind]
newMetaKindVars :: Int -> TcM [TcKind]
newMetaKindVars Int
n = Int -> TcM TcKind -> TcM [TcKind]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
n TcM TcKind
newMetaKindVar
newEvVars :: TcThetaType -> TcM [EvVar]
newEvVars :: [TcKind] -> TcM [TyVar]
newEvVars [TcKind]
theta = (TcKind -> IOEnv (Env TcGblEnv TcLclEnv) TyVar)
-> [TcKind] -> TcM [TyVar]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM TcKind -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
forall gbl lcl. TcKind -> TcRnIf gbl lcl TyVar
newEvVar [TcKind]
theta
newEvVar :: TcPredType -> TcRnIf gbl lcl EvVar
newEvVar :: TcKind -> TcRnIf gbl lcl TyVar
newEvVar TcKind
ty = do { Name
name <- OccName -> TcRnIf gbl lcl Name
forall gbl lcl. OccName -> TcRnIf gbl lcl Name
newSysName (TcKind -> OccName
predTypeOccName TcKind
ty)
; TyVar -> TcRnIf gbl lcl TyVar
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> TcKind -> TcKind -> TyVar
mkLocalIdOrCoVar Name
name TcKind
Many TcKind
ty) }
newWantedWithLoc :: CtLoc -> PredType -> TcM CtEvidence
newWantedWithLoc :: CtLoc -> TcKind -> TcM CtEvidence
newWantedWithLoc CtLoc
loc TcKind
pty
= do TcEvDest
dst <- case TcKind -> Pred
classifyPredType TcKind
pty of
EqPred {}
-> CoercionHole -> TcEvDest
HoleDest (CoercionHole -> TcEvDest)
-> IOEnv (Env TcGblEnv TcLclEnv) CoercionHole
-> IOEnv (Env TcGblEnv TcLclEnv) TcEvDest
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcKind -> IOEnv (Env TcGblEnv TcLclEnv) CoercionHole
newCoercionHole TcKind
pty
SpecialPred SpecialPred
s
-> case SpecialPred
s of
IsReflPrimPred {} -> TcEvDest -> IOEnv (Env TcGblEnv TcLclEnv) TcEvDest
forall (m :: * -> *) a. Monad m => a -> m a
return TcEvDest
NoDest
Pred
_ -> TyVar -> TcEvDest
EvVarDest (TyVar -> TcEvDest)
-> IOEnv (Env TcGblEnv TcLclEnv) TyVar
-> IOEnv (Env TcGblEnv TcLclEnv) TcEvDest
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcKind -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
forall gbl lcl. TcKind -> TcRnIf gbl lcl TyVar
newEvVar TcKind
pty
CtEvidence -> TcM CtEvidence
forall (m :: * -> *) a. Monad m => a -> m a
return (CtEvidence -> TcM CtEvidence) -> CtEvidence -> TcM CtEvidence
forall a b. (a -> b) -> a -> b
$ CtWanted :: TcKind -> TcEvDest -> CtLoc -> RewriterSet -> CtEvidence
CtWanted { ctev_dest :: TcEvDest
ctev_dest = TcEvDest
dst
, ctev_pred :: TcKind
ctev_pred = TcKind
pty
, ctev_loc :: CtLoc
ctev_loc = CtLoc
loc
, ctev_rewriters :: RewriterSet
ctev_rewriters = RewriterSet
emptyRewriterSet }
newWanted :: CtOrigin -> Maybe TypeOrKind -> PredType -> TcM CtEvidence
newWanted :: CtOrigin -> Maybe TypeOrKind -> TcKind -> TcM CtEvidence
newWanted CtOrigin
orig Maybe TypeOrKind
t_or_k TcKind
pty
= do CtLoc
loc <- CtOrigin -> Maybe TypeOrKind -> TcM CtLoc
getCtLocM CtOrigin
orig Maybe TypeOrKind
t_or_k
CtLoc -> TcKind -> TcM CtEvidence
newWantedWithLoc CtLoc
loc TcKind
pty
newWanteds :: CtOrigin -> ThetaType -> TcM [CtEvidence]
newWanteds :: CtOrigin -> [TcKind] -> TcM [CtEvidence]
newWanteds CtOrigin
orig = (TcKind -> TcM CtEvidence) -> [TcKind] -> TcM [CtEvidence]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (CtOrigin -> Maybe TypeOrKind -> TcKind -> TcM CtEvidence
newWanted CtOrigin
orig Maybe TypeOrKind
forall a. Maybe a
Nothing)
cloneWantedCtEv :: CtEvidence -> TcM CtEvidence
cloneWantedCtEv :: CtEvidence -> TcM CtEvidence
cloneWantedCtEv ctev :: CtEvidence
ctev@(CtWanted { ctev_pred :: CtEvidence -> TcKind
ctev_pred = TcKind
pty, ctev_dest :: CtEvidence -> TcEvDest
ctev_dest = HoleDest CoercionHole
_ })
| TcKind -> Bool
isEqPrimPred TcKind
pty
= do { CoercionHole
co_hole <- TcKind -> IOEnv (Env TcGblEnv TcLclEnv) CoercionHole
newCoercionHole TcKind
pty
; CtEvidence -> TcM CtEvidence
forall (m :: * -> *) a. Monad m => a -> m a
return (CtEvidence
ctev { ctev_dest :: TcEvDest
ctev_dest = CoercionHole -> TcEvDest
HoleDest CoercionHole
co_hole }) }
| Bool
otherwise
= String -> SDoc -> TcM CtEvidence
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"cloneWantedCtEv" (TcKind -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcKind
pty)
cloneWantedCtEv CtEvidence
ctev = CtEvidence -> TcM CtEvidence
forall (m :: * -> *) a. Monad m => a -> m a
return CtEvidence
ctev
cloneWanted :: Ct -> TcM Ct
cloneWanted :: Ct -> TcM Ct
cloneWanted Ct
ct = CtEvidence -> Ct
mkNonCanonical (CtEvidence -> Ct) -> TcM CtEvidence -> TcM Ct
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CtEvidence -> TcM CtEvidence
cloneWantedCtEv (Ct -> CtEvidence
ctEvidence Ct
ct)
cloneWC :: WantedConstraints -> TcM WantedConstraints
cloneWC :: WantedConstraints -> TcM WantedConstraints
cloneWC wc :: WantedConstraints
wc@(WC { wc_simple :: WantedConstraints -> Cts
wc_simple = Cts
simples, wc_impl :: WantedConstraints -> Bag Implication
wc_impl = Bag Implication
implics })
= do { Cts
simples' <- (Ct -> TcM Ct) -> Cts -> IOEnv (Env TcGblEnv TcLclEnv) Cts
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Bag a -> m (Bag b)
mapBagM Ct -> TcM Ct
cloneWanted Cts
simples
; Bag Implication
implics' <- (Implication -> IOEnv (Env TcGblEnv TcLclEnv) Implication)
-> Bag Implication
-> IOEnv (Env TcGblEnv TcLclEnv) (Bag Implication)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Bag a -> m (Bag b)
mapBagM Implication -> IOEnv (Env TcGblEnv TcLclEnv) Implication
cloneImplication Bag Implication
implics
; WantedConstraints -> TcM WantedConstraints
forall (m :: * -> *) a. Monad m => a -> m a
return (WantedConstraints
wc { wc_simple :: Cts
wc_simple = Cts
simples', wc_impl :: Bag Implication
wc_impl = Bag Implication
implics' }) }
cloneImplication :: Implication -> TcM Implication
cloneImplication :: Implication -> IOEnv (Env TcGblEnv TcLclEnv) Implication
cloneImplication implic :: Implication
implic@(Implic { ic_binds :: Implication -> EvBindsVar
ic_binds = EvBindsVar
binds, ic_wanted :: Implication -> WantedConstraints
ic_wanted = WantedConstraints
inner_wanted })
= do { EvBindsVar
binds' <- EvBindsVar -> TcM EvBindsVar
cloneEvBindsVar EvBindsVar
binds
; WantedConstraints
inner_wanted' <- WantedConstraints -> TcM WantedConstraints
cloneWC WantedConstraints
inner_wanted
; Implication -> IOEnv (Env TcGblEnv TcLclEnv) Implication
forall (m :: * -> *) a. Monad m => a -> m a
return (Implication
implic { ic_binds :: EvBindsVar
ic_binds = EvBindsVar
binds', ic_wanted :: WantedConstraints
ic_wanted = WantedConstraints
inner_wanted' }) }
emitWanted :: CtOrigin -> TcPredType -> TcM EvTerm
emitWanted :: CtOrigin -> TcKind -> TcM EvTerm
emitWanted CtOrigin
origin TcKind
pty
= do { CtEvidence
ev <- CtOrigin -> Maybe TypeOrKind -> TcKind -> TcM CtEvidence
newWanted CtOrigin
origin Maybe TypeOrKind
forall a. Maybe a
Nothing TcKind
pty
; Ct -> TcRn ()
emitSimple (Ct -> TcRn ()) -> Ct -> TcRn ()
forall a b. (a -> b) -> a -> b
$ CtEvidence -> Ct
mkNonCanonical CtEvidence
ev
; EvTerm -> TcM EvTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (EvTerm -> TcM EvTerm) -> EvTerm -> TcM EvTerm
forall a b. (a -> b) -> a -> b
$ CtEvidence -> EvTerm
ctEvTerm CtEvidence
ev }
emitWantedEqs :: CtOrigin -> [(TcType,TcType)] -> TcM ()
emitWantedEqs :: CtOrigin -> [(TcKind, TcKind)] -> TcRn ()
emitWantedEqs CtOrigin
origin [(TcKind, TcKind)]
pairs
| [(TcKind, TcKind)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(TcKind, TcKind)]
pairs
= () -> TcRn ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
| Bool
otherwise
= ((TcKind, TcKind) -> IOEnv (Env TcGblEnv TcLclEnv) Coercion)
-> [(TcKind, TcKind)] -> TcRn ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((TcKind -> TcKind -> IOEnv (Env TcGblEnv TcLclEnv) Coercion)
-> (TcKind, TcKind) -> IOEnv (Env TcGblEnv TcLclEnv) Coercion
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (CtOrigin
-> TypeOrKind
-> Role
-> TcKind
-> TcKind
-> IOEnv (Env TcGblEnv TcLclEnv) Coercion
emitWantedEq CtOrigin
origin TypeOrKind
TypeLevel Role
Nominal)) [(TcKind, TcKind)]
pairs
emitWantedEq :: CtOrigin -> TypeOrKind -> Role -> TcType -> TcType -> TcM Coercion
emitWantedEq :: CtOrigin
-> TypeOrKind
-> Role
-> TcKind
-> TcKind
-> IOEnv (Env TcGblEnv TcLclEnv) Coercion
emitWantedEq CtOrigin
origin TypeOrKind
t_or_k Role
role TcKind
ty1 TcKind
ty2
= do { CoercionHole
hole <- TcKind -> IOEnv (Env TcGblEnv TcLclEnv) CoercionHole
newCoercionHole TcKind
pty
; CtLoc
loc <- CtOrigin -> Maybe TypeOrKind -> TcM CtLoc
getCtLocM CtOrigin
origin (TypeOrKind -> Maybe TypeOrKind
forall a. a -> Maybe a
Just TypeOrKind
t_or_k)
; Ct -> TcRn ()
emitSimple (Ct -> TcRn ()) -> Ct -> TcRn ()
forall a b. (a -> b) -> a -> b
$ CtEvidence -> Ct
mkNonCanonical (CtEvidence -> Ct) -> CtEvidence -> Ct
forall a b. (a -> b) -> a -> b
$
CtWanted :: TcKind -> TcEvDest -> CtLoc -> RewriterSet -> CtEvidence
CtWanted { ctev_pred :: TcKind
ctev_pred = TcKind
pty
, ctev_dest :: TcEvDest
ctev_dest = CoercionHole -> TcEvDest
HoleDest CoercionHole
hole
, ctev_loc :: CtLoc
ctev_loc = CtLoc
loc
, ctev_rewriters :: RewriterSet
ctev_rewriters = [TcKind] -> RewriterSet
rewriterSetFromTypes [TcKind
ty1, TcKind
ty2] }
; Coercion -> IOEnv (Env TcGblEnv TcLclEnv) Coercion
forall (m :: * -> *) a. Monad m => a -> m a
return (CoercionHole -> Coercion
HoleCo CoercionHole
hole) }
where
pty :: TcKind
pty = Role -> TcKind -> TcKind -> TcKind
mkPrimEqPredRole Role
role TcKind
ty1 TcKind
ty2
emitWantedEvVar :: CtOrigin -> TcPredType -> TcM EvVar
emitWantedEvVar :: CtOrigin -> TcKind -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
emitWantedEvVar CtOrigin
origin TcKind
ty
= do { TyVar
new_cv <- TcKind -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
forall gbl lcl. TcKind -> TcRnIf gbl lcl TyVar
newEvVar TcKind
ty
; CtLoc
loc <- CtOrigin -> Maybe TypeOrKind -> TcM CtLoc
getCtLocM CtOrigin
origin Maybe TypeOrKind
forall a. Maybe a
Nothing
; let ctev :: CtEvidence
ctev = CtWanted :: TcKind -> TcEvDest -> CtLoc -> RewriterSet -> CtEvidence
CtWanted { ctev_dest :: TcEvDest
ctev_dest = TyVar -> TcEvDest
EvVarDest TyVar
new_cv
, ctev_pred :: TcKind
ctev_pred = TcKind
ty
, ctev_loc :: CtLoc
ctev_loc = CtLoc
loc
, ctev_rewriters :: RewriterSet
ctev_rewriters = RewriterSet
emptyRewriterSet }
; Ct -> TcRn ()
emitSimple (Ct -> TcRn ()) -> Ct -> TcRn ()
forall a b. (a -> b) -> a -> b
$ CtEvidence -> Ct
mkNonCanonical CtEvidence
ctev
; TyVar -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
forall (m :: * -> *) a. Monad m => a -> m a
return TyVar
new_cv }
emitWantedEvVars :: CtOrigin -> [TcPredType] -> TcM [EvVar]
emitWantedEvVars :: CtOrigin -> [TcKind] -> TcM [TyVar]
emitWantedEvVars CtOrigin
orig = (TcKind -> IOEnv (Env TcGblEnv TcLclEnv) TyVar)
-> [TcKind] -> TcM [TyVar]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (CtOrigin -> TcKind -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
emitWantedEvVar CtOrigin
orig)
emitNewExprHole :: OccName
-> Type -> TcM HoleExprRef
emitNewExprHole :: OccName -> TcKind -> TcM HoleExprRef
emitNewExprHole OccName
occ TcKind
ty
= do { Unique
u <- TcRnIf TcGblEnv TcLclEnv Unique
forall gbl lcl. TcRnIf gbl lcl Unique
newUnique
; TcRef EvTerm
ref <- EvTerm -> TcRnIf TcGblEnv TcLclEnv (TcRef EvTerm)
forall a gbl lcl. a -> TcRnIf gbl lcl (TcRef a)
newTcRef (String -> SDoc -> EvTerm
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"unfilled unbound-variable evidence" (Unique -> SDoc
forall a. Outputable a => a -> SDoc
ppr Unique
u))
; let her :: HoleExprRef
her = TcRef EvTerm -> TcKind -> Unique -> HoleExprRef
HER TcRef EvTerm
ref TcKind
ty Unique
u
; CtLoc
loc <- CtOrigin -> Maybe TypeOrKind -> TcM CtLoc
getCtLocM (Maybe OccName -> CtOrigin
ExprHoleOrigin (OccName -> Maybe OccName
forall a. a -> Maybe a
Just OccName
occ)) (TypeOrKind -> Maybe TypeOrKind
forall a. a -> Maybe a
Just TypeOrKind
TypeLevel)
; let hole :: Hole
hole = Hole :: HoleSort -> OccName -> TcKind -> CtLoc -> Hole
Hole { hole_sort :: HoleSort
hole_sort = HoleExprRef -> HoleSort
ExprHole HoleExprRef
her
, hole_occ :: OccName
hole_occ = OccName
occ
, hole_ty :: TcKind
hole_ty = TcKind
ty
, hole_loc :: CtLoc
hole_loc = CtLoc
loc }
; Hole -> TcRn ()
emitHole Hole
hole
; HoleExprRef -> TcM HoleExprRef
forall (m :: * -> *) a. Monad m => a -> m a
return HoleExprRef
her }
newDict :: Class -> [TcType] -> TcM DictId
newDict :: Class -> [TcKind] -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
newDict Class
cls [TcKind]
tys
= do { Name
name <- OccName -> TcM Name
forall gbl lcl. OccName -> TcRnIf gbl lcl Name
newSysName (OccName -> OccName
mkDictOcc (Class -> OccName
forall a. NamedThing a => a -> OccName
getOccName Class
cls))
; TyVar -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
forall (m :: * -> *) a. Monad m => a -> m a
return (HasDebugCallStack => Name -> TcKind -> TcKind -> TyVar
Name -> TcKind -> TcKind -> TyVar
mkLocalId Name
name TcKind
Many (Class -> [TcKind] -> TcKind
mkClassPred Class
cls [TcKind]
tys)) }
predTypeOccName :: PredType -> OccName
predTypeOccName :: TcKind -> OccName
predTypeOccName TcKind
ty = case TcKind -> Pred
classifyPredType TcKind
ty of
ClassPred Class
cls [TcKind]
_ -> OccName -> OccName
mkDictOcc (Class -> OccName
forall a. NamedThing a => a -> OccName
getOccName Class
cls)
EqPred {} -> FastString -> OccName
mkVarOccFS (String -> FastString
fsLit String
"co")
IrredPred {} -> FastString -> OccName
mkVarOccFS (String -> FastString
fsLit String
"irred")
ForAllPred {} -> FastString -> OccName
mkVarOccFS (String -> FastString
fsLit String
"df")
SpecialPred SpecialPred
s ->
case SpecialPred
s of
IsReflPrimPred {} -> FastString -> OccName
mkVarOccFS (String -> FastString
fsLit String
"rfl")
newImplication :: TcM Implication
newImplication :: IOEnv (Env TcGblEnv TcLclEnv) Implication
newImplication
= do TcLclEnv
env <- TcRnIf TcGblEnv TcLclEnv TcLclEnv
forall gbl lcl. TcRnIf gbl lcl lcl
getLclEnv
Bool
warn_inaccessible <- WarningFlag -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. WarningFlag -> TcRnIf gbl lcl Bool
woptM WarningFlag
Opt_WarnInaccessibleCode
Implication -> IOEnv (Env TcGblEnv TcLclEnv) Implication
forall (m :: * -> *) a. Monad m => a -> m a
return (Implication
implicationPrototype { ic_env :: TcLclEnv
ic_env = TcLclEnv
env
, ic_warn_inaccessible :: Bool
ic_warn_inaccessible = Bool
warn_inaccessible })
newCoercionHole :: TcPredType -> TcM CoercionHole
newCoercionHole :: TcKind -> IOEnv (Env TcGblEnv TcLclEnv) CoercionHole
newCoercionHole TcKind
pred_ty
= do { TyVar
co_var <- TcKind -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
forall gbl lcl. TcKind -> TcRnIf gbl lcl TyVar
newEvVar TcKind
pred_ty
; String -> SDoc -> TcRn ()
traceTc String
"New coercion hole:" (TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
co_var SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> TcKind -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcKind
pred_ty)
; IORef (Maybe Coercion)
ref <- Maybe Coercion
-> IOEnv (Env TcGblEnv TcLclEnv) (IORef (Maybe Coercion))
forall a env. a -> IOEnv env (IORef a)
newMutVar Maybe Coercion
forall a. Maybe a
Nothing
; CoercionHole -> IOEnv (Env TcGblEnv TcLclEnv) CoercionHole
forall (m :: * -> *) a. Monad m => a -> m a
return (CoercionHole -> IOEnv (Env TcGblEnv TcLclEnv) CoercionHole)
-> CoercionHole -> IOEnv (Env TcGblEnv TcLclEnv) CoercionHole
forall a b. (a -> b) -> a -> b
$ CoercionHole :: TyVar -> IORef (Maybe Coercion) -> CoercionHole
CoercionHole { ch_co_var :: TyVar
ch_co_var = TyVar
co_var, ch_ref :: IORef (Maybe Coercion)
ch_ref = IORef (Maybe Coercion)
ref } }
fillCoercionHole :: CoercionHole -> Coercion -> TcM ()
fillCoercionHole :: CoercionHole -> Coercion -> TcRn ()
fillCoercionHole (CoercionHole { ch_ref :: CoercionHole -> IORef (Maybe Coercion)
ch_ref = IORef (Maybe Coercion)
ref, ch_co_var :: CoercionHole -> TyVar
ch_co_var = TyVar
cv }) Coercion
co = do
Bool -> TcRn () -> TcRn ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
debugIsOn (TcRn () -> TcRn ()) -> TcRn () -> TcRn ()
forall a b. (a -> b) -> a -> b
$ do
Maybe Coercion
cts <- IORef (Maybe Coercion) -> TcRnIf TcGblEnv TcLclEnv (Maybe Coercion)
forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
readTcRef IORef (Maybe Coercion)
ref
Maybe Coercion -> (Coercion -> TcRn ()) -> TcRn ()
forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenIsJust Maybe Coercion
cts ((Coercion -> TcRn ()) -> TcRn ())
-> (Coercion -> TcRn ()) -> TcRn ()
forall a b. (a -> b) -> a -> b
$ \Coercion
old_co ->
String -> SDoc -> TcRn ()
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"Filling a filled coercion hole" (TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
cv SDoc -> SDoc -> SDoc
$$ Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
co SDoc -> SDoc -> SDoc
$$ Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
old_co)
String -> SDoc -> TcRn ()
traceTc String
"Filling coercion hole" (TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
cv SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
":=" SDoc -> SDoc -> SDoc
<+> Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
co)
IORef (Maybe Coercion) -> Maybe Coercion -> TcRn ()
forall a gbl lcl. TcRef a -> a -> TcRnIf gbl lcl ()
writeTcRef IORef (Maybe Coercion)
ref (Coercion -> Maybe Coercion
forall a. a -> Maybe a
Just Coercion
co)
isFilledCoercionHole :: CoercionHole -> TcM Bool
isFilledCoercionHole :: CoercionHole -> TcRnIf TcGblEnv TcLclEnv Bool
isFilledCoercionHole (CoercionHole { ch_ref :: CoercionHole -> IORef (Maybe Coercion)
ch_ref = IORef (Maybe Coercion)
ref }) = Maybe Coercion -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Coercion -> Bool)
-> TcRnIf TcGblEnv TcLclEnv (Maybe Coercion)
-> TcRnIf TcGblEnv TcLclEnv Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IORef (Maybe Coercion) -> TcRnIf TcGblEnv TcLclEnv (Maybe Coercion)
forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
readTcRef IORef (Maybe Coercion)
ref
unpackCoercionHole :: CoercionHole -> TcM Coercion
unpackCoercionHole :: CoercionHole -> IOEnv (Env TcGblEnv TcLclEnv) Coercion
unpackCoercionHole CoercionHole
hole
= do { Maybe Coercion
contents <- CoercionHole -> TcRnIf TcGblEnv TcLclEnv (Maybe Coercion)
unpackCoercionHole_maybe CoercionHole
hole
; case Maybe Coercion
contents of
Just Coercion
co -> Coercion -> IOEnv (Env TcGblEnv TcLclEnv) Coercion
forall (m :: * -> *) a. Monad m => a -> m a
return Coercion
co
Maybe Coercion
Nothing -> String -> SDoc -> IOEnv (Env TcGblEnv TcLclEnv) Coercion
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"Unfilled coercion hole" (CoercionHole -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoercionHole
hole) }
unpackCoercionHole_maybe :: CoercionHole -> TcM (Maybe Coercion)
unpackCoercionHole_maybe :: CoercionHole -> TcRnIf TcGblEnv TcLclEnv (Maybe Coercion)
unpackCoercionHole_maybe (CoercionHole { ch_ref :: CoercionHole -> IORef (Maybe Coercion)
ch_ref = IORef (Maybe Coercion)
ref }) = IORef (Maybe Coercion) -> TcRnIf TcGblEnv TcLclEnv (Maybe Coercion)
forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
readTcRef IORef (Maybe Coercion)
ref
checkCoercionHole :: CoVar -> Coercion -> TcM Coercion
checkCoercionHole :: TyVar -> Coercion -> IOEnv (Env TcGblEnv TcLclEnv) Coercion
checkCoercionHole TyVar
cv Coercion
co
| Bool
debugIsOn
= do { TcKind
cv_ty <- TcKind -> TcM TcKind
zonkTcType (TyVar -> TcKind
varType TyVar
cv)
; Coercion -> IOEnv (Env TcGblEnv TcLclEnv) Coercion
forall (m :: * -> *) a. Monad m => a -> m a
return (Coercion -> IOEnv (Env TcGblEnv TcLclEnv) Coercion)
-> Coercion -> IOEnv (Env TcGblEnv TcLclEnv) Coercion
forall a b. (a -> b) -> a -> b
$
Bool -> SDoc -> Coercion -> Coercion
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (TcKind -> Bool
ok TcKind
cv_ty)
(String -> SDoc
text String
"Bad coercion hole" SDoc -> SDoc -> SDoc
<+>
TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
cv SDoc -> SDoc -> SDoc
<> SDoc
colon SDoc -> SDoc -> SDoc
<+> [SDoc] -> SDoc
vcat [ TcKind -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcKind
t1, TcKind -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcKind
t2, Role -> SDoc
forall a. Outputable a => a -> SDoc
ppr Role
role
, TcKind -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcKind
cv_ty ])
Coercion
co }
| Bool
otherwise
= Coercion -> IOEnv (Env TcGblEnv TcLclEnv) Coercion
forall (m :: * -> *) a. Monad m => a -> m a
return Coercion
co
where
(Pair TcKind
t1 TcKind
t2, Role
role) = Coercion -> (Pair TcKind, Role)
coercionKindRole Coercion
co
ok :: TcKind -> Bool
ok TcKind
cv_ty | EqPred EqRel
cv_rel TcKind
cv_t1 TcKind
cv_t2 <- TcKind -> Pred
classifyPredType TcKind
cv_ty
= TcKind
t1 TcKind -> TcKind -> Bool
`eqType` TcKind
cv_t1
Bool -> Bool -> Bool
&& TcKind
t2 TcKind -> TcKind -> Bool
`eqType` TcKind
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
type ConcreteHole = CoercionHole
newConcreteHole :: Kind
-> Type
-> TcM (ConcreteHole, TcType)
newConcreteHole :: TcKind -> TcKind -> TcM (CoercionHole, TcKind)
newConcreteHole TcKind
ki TcKind
ty
= do { TcKind
concrete_ty <- TcKind -> TcM TcKind
newFlexiTyVarTy TcKind
ki
; let co_ty :: TcKind
co_ty = TcKind -> TcKind -> TcKind -> TcKind -> TcKind
mkHeteroPrimEqPred TcKind
ki TcKind
ki TcKind
ty TcKind
concrete_ty
; CoercionHole
hole <- TcKind -> IOEnv (Env TcGblEnv TcLclEnv) CoercionHole
newCoercionHole TcKind
co_ty
; (CoercionHole, TcKind) -> TcM (CoercionHole, TcKind)
forall (m :: * -> *) a. Monad m => a -> m a
return (CoercionHole
hole, TcKind
concrete_ty) }
newInferExpType :: TcM ExpType
newInferExpType :: TcM ExpType
newInferExpType
= do { Unique
u <- TcRnIf TcGblEnv TcLclEnv Unique
forall gbl lcl. TcRnIf gbl lcl Unique
newUnique
; TcLevel
tclvl <- TcM TcLevel
getTcLevel
; String -> SDoc -> TcRn ()
traceTc String
"newInferExpType" (Unique -> SDoc
forall a. Outputable a => a -> SDoc
ppr Unique
u SDoc -> SDoc -> SDoc
<+> TcLevel -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcLevel
tclvl)
; IORef (Maybe TcKind)
ref <- Maybe TcKind
-> IOEnv (Env TcGblEnv TcLclEnv) (IORef (Maybe TcKind))
forall a env. a -> IOEnv env (IORef a)
newMutVar Maybe TcKind
forall a. Maybe a
Nothing
; ExpType -> TcM ExpType
forall (m :: * -> *) a. Monad m => a -> m a
return (InferResult -> ExpType
Infer (IR :: Unique -> TcLevel -> IORef (Maybe TcKind) -> InferResult
IR { ir_uniq :: Unique
ir_uniq = Unique
u, ir_lvl :: TcLevel
ir_lvl = TcLevel
tclvl
, ir_ref :: IORef (Maybe TcKind)
ir_ref = IORef (Maybe TcKind)
ref })) }
readExpType_maybe :: ExpType -> TcM (Maybe TcType)
readExpType_maybe :: ExpType -> TcM (Maybe TcKind)
readExpType_maybe (Check TcKind
ty) = Maybe TcKind -> TcM (Maybe TcKind)
forall (m :: * -> *) a. Monad m => a -> m a
return (TcKind -> Maybe TcKind
forall a. a -> Maybe a
Just TcKind
ty)
readExpType_maybe (Infer (IR { ir_ref :: InferResult -> IORef (Maybe TcKind)
ir_ref = IORef (Maybe TcKind)
ref})) = IORef (Maybe TcKind) -> TcM (Maybe TcKind)
forall a env. IORef a -> IOEnv env a
readMutVar IORef (Maybe TcKind)
ref
readScaledExpType :: Scaled ExpType -> TcM (Scaled Type)
readScaledExpType :: Scaled ExpType -> TcM (Scaled TcKind)
readScaledExpType (Scaled TcKind
m ExpType
exp_ty)
= do { TcKind
ty <- ExpType -> TcM TcKind
readExpType ExpType
exp_ty
; Scaled TcKind -> TcM (Scaled TcKind)
forall (m :: * -> *) a. Monad m => a -> m a
return (TcKind -> TcKind -> Scaled TcKind
forall a. TcKind -> a -> Scaled a
Scaled TcKind
m TcKind
ty) }
readExpType :: ExpType -> TcM TcType
readExpType :: ExpType -> TcM TcKind
readExpType ExpType
exp_ty
= do { Maybe TcKind
mb_ty <- ExpType -> TcM (Maybe TcKind)
readExpType_maybe ExpType
exp_ty
; case Maybe TcKind
mb_ty of
Just TcKind
ty -> TcKind -> TcM TcKind
forall (m :: * -> *) a. Monad m => a -> m a
return TcKind
ty
Maybe TcKind
Nothing -> String -> SDoc -> TcM TcKind
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"Unknown expected type" (ExpType -> SDoc
forall a. Outputable a => a -> SDoc
ppr ExpType
exp_ty) }
checkingExpType_maybe :: ExpType -> Maybe TcType
checkingExpType_maybe :: ExpType -> Maybe TcKind
checkingExpType_maybe (Check TcKind
ty) = TcKind -> Maybe TcKind
forall a. a -> Maybe a
Just TcKind
ty
checkingExpType_maybe (Infer {}) = Maybe TcKind
forall a. Maybe a
Nothing
checkingExpType :: String -> ExpType -> TcType
checkingExpType :: String -> ExpType -> TcKind
checkingExpType String
_ (Check TcKind
ty) = TcKind
ty
checkingExpType String
err ExpType
et = String -> SDoc -> TcKind
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"checkingExpType" (String -> SDoc
text String
err SDoc -> SDoc -> SDoc
$$ ExpType -> SDoc
forall a. Outputable a => a -> SDoc
ppr ExpType
et)
scaledExpTypeToType :: Scaled ExpType -> TcM (Scaled TcType)
scaledExpTypeToType :: Scaled ExpType -> TcM (Scaled TcKind)
scaledExpTypeToType (Scaled TcKind
m ExpType
exp_ty)
= do { TcKind
ty <- ExpType -> TcM TcKind
expTypeToType ExpType
exp_ty
; Scaled TcKind -> TcM (Scaled TcKind)
forall (m :: * -> *) a. Monad m => a -> m a
return (TcKind -> TcKind -> Scaled TcKind
forall a. TcKind -> a -> Scaled a
Scaled TcKind
m TcKind
ty) }
expTypeToType :: ExpType -> TcM TcType
expTypeToType :: ExpType -> TcM TcKind
expTypeToType (Check TcKind
ty) = TcKind -> TcM TcKind
forall (m :: * -> *) a. Monad m => a -> m a
return TcKind
ty
expTypeToType (Infer InferResult
inf_res) = InferResult -> TcM TcKind
inferResultToType InferResult
inf_res
inferResultToType :: InferResult -> TcM Type
inferResultToType :: InferResult -> TcM TcKind
inferResultToType (IR { ir_uniq :: InferResult -> Unique
ir_uniq = Unique
u, ir_lvl :: InferResult -> TcLevel
ir_lvl = TcLevel
tc_lvl
, ir_ref :: InferResult -> IORef (Maybe TcKind)
ir_ref = IORef (Maybe TcKind)
ref })
= do { Maybe TcKind
mb_inferred_ty <- IORef (Maybe TcKind) -> TcM (Maybe TcKind)
forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
readTcRef IORef (Maybe TcKind)
ref
; TcKind
tau <- case Maybe TcKind
mb_inferred_ty of
Just TcKind
ty -> do { TcKind -> TcRn ()
ensureMonoType TcKind
ty
; TcKind -> TcM TcKind
forall (m :: * -> *) a. Monad m => a -> m a
return TcKind
ty }
Maybe TcKind
Nothing -> do { TcKind
rr <- TcLevel -> TcKind -> TcM TcKind
newMetaTyVarTyAtLevel TcLevel
tc_lvl TcKind
runtimeRepTy
; TcKind
tau <- TcLevel -> TcKind -> TcM TcKind
newMetaTyVarTyAtLevel TcLevel
tc_lvl (TcKind -> TcKind
mkTYPEapp TcKind
rr)
; IORef (Maybe TcKind) -> Maybe TcKind -> TcRn ()
forall a env. IORef a -> a -> IOEnv env ()
writeMutVar IORef (Maybe TcKind)
ref (TcKind -> Maybe TcKind
forall a. a -> Maybe a
Just TcKind
tau)
; TcKind -> TcM TcKind
forall (m :: * -> *) a. Monad m => a -> m a
return TcKind
tau }
; String -> SDoc -> TcRn ()
traceTc String
"Forcing ExpType to be monomorphic:"
(Unique -> SDoc
forall a. Outputable a => a -> SDoc
ppr Unique
u SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
":=" SDoc -> SDoc -> SDoc
<+> TcKind -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcKind
tau)
; TcKind -> TcM TcKind
forall (m :: * -> *) a. Monad m => a -> m a
return TcKind
tau }
tcInfer :: (ExpSigmaType -> TcM a) -> TcM (a, TcSigmaType)
tcInfer :: (ExpType -> TcM a) -> TcM (a, TcKind)
tcInfer ExpType -> TcM a
tc_check
= do { ExpType
res_ty <- TcM ExpType
newInferExpType
; a
result <- ExpType -> TcM a
tc_check ExpType
res_ty
; TcKind
res_ty <- ExpType -> TcM TcKind
readExpType ExpType
res_ty
; (a, TcKind) -> TcM (a, TcKind)
forall (m :: * -> *) a. Monad m => a -> m a
return (a
result, TcKind
res_ty) }
fillInferResult :: TcType -> InferResult -> TcM TcCoercionN
fillInferResult :: TcKind -> InferResult -> IOEnv (Env TcGblEnv TcLclEnv) Coercion
fillInferResult TcKind
act_res_ty (IR { ir_uniq :: InferResult -> Unique
ir_uniq = Unique
u, ir_lvl :: InferResult -> TcLevel
ir_lvl = TcLevel
res_lvl
, ir_ref :: InferResult -> IORef (Maybe TcKind)
ir_ref = IORef (Maybe TcKind)
ref })
= do { Maybe TcKind
mb_exp_res_ty <- IORef (Maybe TcKind) -> TcM (Maybe TcKind)
forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
readTcRef IORef (Maybe TcKind)
ref
; case Maybe TcKind
mb_exp_res_ty of
Just TcKind
exp_res_ty
-> do { String -> SDoc -> TcRn ()
traceTc String
"Joining inferred ExpType" (SDoc -> TcRn ()) -> SDoc -> TcRn ()
forall a b. (a -> b) -> a -> b
$
Unique -> SDoc
forall a. Outputable a => a -> SDoc
ppr Unique
u SDoc -> SDoc -> SDoc
<> SDoc
colon SDoc -> SDoc -> SDoc
<+> TcKind -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcKind
act_res_ty SDoc -> SDoc -> SDoc
<+> Char -> SDoc
char Char
'~' SDoc -> SDoc -> SDoc
<+> TcKind -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcKind
exp_res_ty
; TcLevel
cur_lvl <- TcM TcLevel
getTcLevel
; Bool -> TcRn () -> TcRn ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (TcLevel
cur_lvl TcLevel -> TcLevel -> Bool
`sameDepthAs` TcLevel
res_lvl) (TcRn () -> TcRn ()) -> TcRn () -> TcRn ()
forall a b. (a -> b) -> a -> b
$
TcKind -> TcRn ()
ensureMonoType TcKind
act_res_ty
; Maybe TypedThing
-> TcKind -> TcKind -> IOEnv (Env TcGblEnv TcLclEnv) Coercion
unifyType Maybe TypedThing
forall a. Maybe a
Nothing TcKind
act_res_ty TcKind
exp_res_ty }
Maybe TcKind
Nothing
-> do { String -> SDoc -> TcRn ()
traceTc String
"Filling inferred ExpType" (SDoc -> TcRn ()) -> SDoc -> TcRn ()
forall a b. (a -> b) -> a -> b
$
Unique -> SDoc
forall a. Outputable a => a -> SDoc
ppr Unique
u SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
":=" SDoc -> SDoc -> SDoc
<+> TcKind -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcKind
act_res_ty
; (Coercion
prom_co, TcKind
act_res_ty) <- TcLevel -> TcKind -> TcM (Coercion, TcKind)
promoteTcType TcLevel
res_lvl TcKind
act_res_ty
; IORef (Maybe TcKind) -> Maybe TcKind -> TcRn ()
forall a gbl lcl. TcRef a -> a -> TcRnIf gbl lcl ()
writeTcRef IORef (Maybe TcKind)
ref (TcKind -> Maybe TcKind
forall a. a -> Maybe a
Just TcKind
act_res_ty)
; Coercion -> IOEnv (Env TcGblEnv TcLclEnv) Coercion
forall (m :: * -> *) a. Monad m => a -> m a
return Coercion
prom_co }
}
ensureMonoType :: TcType -> TcM ()
ensureMonoType :: TcKind -> TcRn ()
ensureMonoType TcKind
res_ty
| TcKind -> Bool
isTauTy TcKind
res_ty
= () -> TcRn ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
| Bool
otherwise
= do { TcKind
mono_ty <- TcM TcKind
newOpenFlexiTyVarTy
; let eq_orig :: CtOrigin
eq_orig = TypeEqOrigin :: TcKind -> TcKind -> Maybe TypedThing -> Bool -> CtOrigin
TypeEqOrigin { uo_actual :: TcKind
uo_actual = TcKind
res_ty
, uo_expected :: TcKind
uo_expected = TcKind
mono_ty
, uo_thing :: Maybe TypedThing
uo_thing = Maybe TypedThing
forall a. Maybe a
Nothing
, uo_visible :: Bool
uo_visible = Bool
False }
; Coercion
_co <- CtOrigin
-> TypeOrKind
-> Role
-> TcKind
-> TcKind
-> IOEnv (Env TcGblEnv TcLclEnv) Coercion
emitWantedEq CtOrigin
eq_orig TypeOrKind
TypeLevel Role
Nominal TcKind
res_ty TcKind
mono_ty
; () -> TcRn ()
forall (m :: * -> *) a. Monad m => a -> m a
return () }
promoteTcType :: TcLevel -> TcType -> TcM (TcCoercionN, TcType)
promoteTcType :: TcLevel -> TcKind -> TcM (Coercion, TcKind)
promoteTcType TcLevel
dest_lvl TcKind
ty
= do { TcLevel
cur_lvl <- TcM TcLevel
getTcLevel
; if (TcLevel
cur_lvl TcLevel -> TcLevel -> Bool
`sameDepthAs` TcLevel
dest_lvl)
then (Coercion, TcKind) -> TcM (Coercion, TcKind)
forall (m :: * -> *) a. Monad m => a -> m a
return (TcKind -> Coercion
mkTcNomReflCo TcKind
ty, TcKind
ty)
else TcM (Coercion, TcKind)
promote_it }
where
promote_it :: TcM (TcCoercion, TcType)
promote_it :: TcM (Coercion, TcKind)
promote_it
= do { TcKind
rr <- TcLevel -> TcKind -> TcM TcKind
newMetaTyVarTyAtLevel TcLevel
dest_lvl TcKind
runtimeRepTy
; TcKind
prom_ty <- TcLevel -> TcKind -> TcM TcKind
newMetaTyVarTyAtLevel TcLevel
dest_lvl (TcKind -> TcKind
mkTYPEapp TcKind
rr)
; let eq_orig :: CtOrigin
eq_orig = TypeEqOrigin :: TcKind -> TcKind -> Maybe TypedThing -> Bool -> CtOrigin
TypeEqOrigin { uo_actual :: TcKind
uo_actual = TcKind
ty
, uo_expected :: TcKind
uo_expected = TcKind
prom_ty
, uo_thing :: Maybe TypedThing
uo_thing = Maybe TypedThing
forall a. Maybe a
Nothing
, uo_visible :: Bool
uo_visible = Bool
False }
; Coercion
co <- CtOrigin
-> TypeOrKind
-> Role
-> TcKind
-> TcKind
-> IOEnv (Env TcGblEnv TcLclEnv) Coercion
emitWantedEq CtOrigin
eq_orig TypeOrKind
TypeLevel Role
Nominal TcKind
ty TcKind
prom_ty
; (Coercion, TcKind) -> TcM (Coercion, TcKind)
forall (m :: * -> *) a. Monad m => a -> m a
return (Coercion
co, TcKind
prom_ty) }
newMetaTyVarName :: FastString -> TcM Name
newMetaTyVarName :: FastString -> TcM Name
newMetaTyVarName FastString
str
= do { Unique
uniq <- TcRnIf TcGblEnv TcLclEnv Unique
forall gbl lcl. TcRnIf gbl lcl Unique
newUnique
; Name -> TcM Name
forall (m :: * -> *) a. Monad m => a -> m a
return (Unique -> OccName -> Name
mkSystemName Unique
uniq (FastString -> OccName
mkTyVarOccFS FastString
str)) }
cloneMetaTyVarName :: Name -> TcM Name
cloneMetaTyVarName :: Name -> TcM Name
cloneMetaTyVarName Name
name
= do { Unique
uniq <- TcRnIf TcGblEnv TcLclEnv Unique
forall gbl lcl. TcRnIf gbl lcl Unique
newUnique
; Name -> TcM Name
forall (m :: * -> *) a. Monad m => a -> m a
return (Unique -> OccName -> Name
mkSystemName Unique
uniq (Name -> OccName
nameOccName Name
name)) }
metaInfoToTyVarName :: MetaInfo -> FastString
metaInfoToTyVarName :: MetaInfo -> FastString
metaInfoToTyVarName MetaInfo
meta_info =
case MetaInfo
meta_info of
MetaInfo
TauTv -> String -> FastString
fsLit String
"t"
MetaInfo
TyVarTv -> String -> FastString
fsLit String
"a"
MetaInfo
RuntimeUnkTv -> String -> FastString
fsLit String
"r"
MetaInfo
CycleBreakerTv -> String -> FastString
fsLit String
"b"
MetaInfo
ConcreteTv -> String -> FastString
fsLit String
"c"
newAnonMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
newAnonMetaTyVar :: MetaInfo -> TcKind -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
newAnonMetaTyVar MetaInfo
mi = FastString
-> MetaInfo -> TcKind -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
newNamedAnonMetaTyVar (MetaInfo -> FastString
metaInfoToTyVarName MetaInfo
mi) MetaInfo
mi
newNamedAnonMetaTyVar :: FastString -> MetaInfo -> Kind -> TcM TcTyVar
newNamedAnonMetaTyVar :: FastString
-> MetaInfo -> TcKind -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
newNamedAnonMetaTyVar FastString
tyvar_name MetaInfo
meta_info TcKind
kind
= do { Name
name <- FastString -> TcM Name
newMetaTyVarName FastString
tyvar_name
; TcTyVarDetails
details <- MetaInfo -> TcM TcTyVarDetails
newMetaDetails MetaInfo
meta_info
; let tyvar :: TyVar
tyvar = Name -> TcKind -> TcTyVarDetails -> TyVar
mkTcTyVar Name
name TcKind
kind TcTyVarDetails
details
; String -> SDoc -> TcRn ()
traceTc String
"newAnonMetaTyVar" (TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
tyvar)
; TyVar -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
forall (m :: * -> *) a. Monad m => a -> m a
return TyVar
tyvar }
newSkolemTyVar :: SkolemInfo -> Name -> Kind -> TcM TcTyVar
newSkolemTyVar :: SkolemInfo -> Name -> TcKind -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
newSkolemTyVar SkolemInfo
skol_info Name
name TcKind
kind
= do { TcLevel
lvl <- TcM TcLevel
getTcLevel
; TyVar -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> TcKind -> TcTyVarDetails -> TyVar
mkTcTyVar Name
name TcKind
kind (SkolemInfo -> TcLevel -> Bool -> TcTyVarDetails
SkolemTv SkolemInfo
skol_info TcLevel
lvl Bool
False)) }
newTyVarTyVar :: Name -> Kind -> TcM TcTyVar
newTyVarTyVar :: Name -> TcKind -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
newTyVarTyVar Name
name TcKind
kind
= do { TcTyVarDetails
details <- MetaInfo -> TcM TcTyVarDetails
newMetaDetails MetaInfo
TyVarTv
; let tyvar :: TyVar
tyvar = Name -> TcKind -> TcTyVarDetails -> TyVar
mkTcTyVar Name
name TcKind
kind TcTyVarDetails
details
; String -> SDoc -> TcRn ()
traceTc String
"newTyVarTyVar" (TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
tyvar)
; TyVar -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
forall (m :: * -> *) a. Monad m => a -> m a
return TyVar
tyvar }
cloneTyVarTyVar :: Name -> Kind -> TcM TcTyVar
cloneTyVarTyVar :: Name -> TcKind -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
cloneTyVarTyVar Name
name TcKind
kind
= do { TcTyVarDetails
details <- MetaInfo -> TcM TcTyVarDetails
newMetaDetails MetaInfo
TyVarTv
; Unique
uniq <- TcRnIf TcGblEnv TcLclEnv Unique
forall gbl lcl. TcRnIf gbl lcl Unique
newUnique
; let name' :: Name
name' = Name
name Name -> Unique -> Name
`setNameUnique` Unique
uniq
tyvar :: TyVar
tyvar = Name -> TcKind -> TcTyVarDetails -> TyVar
mkTcTyVar Name
name' TcKind
kind TcTyVarDetails
details
; String -> SDoc -> TcRn ()
traceTc String
"cloneTyVarTyVar" (TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
tyvar)
; TyVar -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
forall (m :: * -> *) a. Monad m => a -> m a
return TyVar
tyvar }
newPatSigTyVar :: Name -> Kind -> TcM TcTyVar
newPatSigTyVar :: Name -> TcKind -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
newPatSigTyVar Name
name TcKind
kind
= do { TcTyVarDetails
details <- MetaInfo -> TcM TcTyVarDetails
newMetaDetails MetaInfo
TauTv
; Unique
uniq <- TcRnIf TcGblEnv TcLclEnv Unique
forall gbl lcl. TcRnIf gbl lcl Unique
newUnique
; let name' :: Name
name' = Name
name Name -> Unique -> Name
`setNameUnique` Unique
uniq
tyvar :: TyVar
tyvar = Name -> TcKind -> TcTyVarDetails -> TyVar
mkTcTyVar Name
name' TcKind
kind TcTyVarDetails
details
; String -> SDoc -> TcRn ()
traceTc String
"newPatSigTyVar" (TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
tyvar)
; TyVar -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
forall (m :: * -> *) a. Monad m => a -> m a
return TyVar
tyvar }
cloneAnonMetaTyVar :: MetaInfo -> TyVar -> TcKind -> TcM TcTyVar
cloneAnonMetaTyVar :: MetaInfo -> TyVar -> TcKind -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
cloneAnonMetaTyVar MetaInfo
info TyVar
tv TcKind
kind
= do { TcTyVarDetails
details <- MetaInfo -> TcM TcTyVarDetails
newMetaDetails MetaInfo
info
; Name
name <- Name -> TcM Name
cloneMetaTyVarName (TyVar -> Name
tyVarName TyVar
tv)
; let tyvar :: TyVar
tyvar = Name -> TcKind -> TcTyVarDetails -> TyVar
mkTcTyVar Name
name TcKind
kind TcTyVarDetails
details
; String -> SDoc -> TcRn ()
traceTc String
"cloneAnonMetaTyVar" (TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
tyvar SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> TcKind -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TyVar -> TcKind
tyVarKind TyVar
tyvar))
; TyVar -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
forall (m :: * -> *) a. Monad m => a -> m a
return TyVar
tyvar }
newCycleBreakerTyVar :: TcKind -> TcM TcTyVar
newCycleBreakerTyVar :: TcKind -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
newCycleBreakerTyVar TcKind
kind
= do { TcTyVarDetails
details <- MetaInfo -> TcM TcTyVarDetails
newMetaDetails MetaInfo
CycleBreakerTv
; Name
name <- FastString -> TcM Name
newMetaTyVarName (String -> FastString
fsLit String
"cbv")
; TyVar -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> TcKind -> TcTyVarDetails -> TyVar
mkTcTyVar Name
name TcKind
kind TcTyVarDetails
details) }
newMetaDetails :: MetaInfo -> TcM TcTyVarDetails
newMetaDetails :: MetaInfo -> TcM TcTyVarDetails
newMetaDetails MetaInfo
info
= do { IORef MetaDetails
ref <- MetaDetails -> IOEnv (Env TcGblEnv TcLclEnv) (IORef MetaDetails)
forall a env. a -> IOEnv env (IORef a)
newMutVar MetaDetails
Flexi
; TcLevel
tclvl <- TcM TcLevel
getTcLevel
; TcTyVarDetails -> TcM TcTyVarDetails
forall (m :: * -> *) a. Monad m => a -> m a
return (MetaTv :: MetaInfo -> IORef MetaDetails -> TcLevel -> TcTyVarDetails
MetaTv { mtv_info :: MetaInfo
mtv_info = MetaInfo
info
, mtv_ref :: IORef MetaDetails
mtv_ref = IORef MetaDetails
ref
, mtv_tclvl :: TcLevel
mtv_tclvl = TcLevel
tclvl }) }
newTauTvDetailsAtLevel :: TcLevel -> TcM TcTyVarDetails
newTauTvDetailsAtLevel :: TcLevel -> TcM TcTyVarDetails
newTauTvDetailsAtLevel TcLevel
tclvl
= do { IORef MetaDetails
ref <- MetaDetails -> IOEnv (Env TcGblEnv TcLclEnv) (IORef MetaDetails)
forall a env. a -> IOEnv env (IORef a)
newMutVar MetaDetails
Flexi
; TcTyVarDetails -> TcM TcTyVarDetails
forall (m :: * -> *) a. Monad m => a -> m a
return (MetaTv :: MetaInfo -> IORef MetaDetails -> TcLevel -> TcTyVarDetails
MetaTv { mtv_info :: MetaInfo
mtv_info = MetaInfo
TauTv
, mtv_ref :: IORef MetaDetails
mtv_ref = IORef MetaDetails
ref
, mtv_tclvl :: TcLevel
mtv_tclvl = TcLevel
tclvl }) }
cloneMetaTyVar :: TcTyVar -> TcM TcTyVar
cloneMetaTyVar :: TyVar -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
cloneMetaTyVar TyVar
tv
= Bool
-> IOEnv (Env TcGblEnv TcLclEnv) TyVar
-> IOEnv (Env TcGblEnv TcLclEnv) TyVar
forall a. HasCallStack => Bool -> a -> a
assert (TyVar -> Bool
isTcTyVar TyVar
tv) (IOEnv (Env TcGblEnv TcLclEnv) TyVar
-> IOEnv (Env TcGblEnv TcLclEnv) TyVar)
-> IOEnv (Env TcGblEnv TcLclEnv) TyVar
-> IOEnv (Env TcGblEnv TcLclEnv) TyVar
forall a b. (a -> b) -> a -> b
$
do { IORef MetaDetails
ref <- MetaDetails -> IOEnv (Env TcGblEnv TcLclEnv) (IORef MetaDetails)
forall a env. a -> IOEnv env (IORef a)
newMutVar MetaDetails
Flexi
; Name
name' <- Name -> TcM Name
cloneMetaTyVarName (TyVar -> Name
tyVarName TyVar
tv)
; let details' :: TcTyVarDetails
details' = case TyVar -> TcTyVarDetails
tcTyVarDetails TyVar
tv of
details :: TcTyVarDetails
details@(MetaTv {}) -> TcTyVarDetails
details { mtv_ref :: IORef MetaDetails
mtv_ref = IORef MetaDetails
ref }
TcTyVarDetails
_ -> String -> SDoc -> TcTyVarDetails
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"cloneMetaTyVar" (TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
tv)
tyvar :: TyVar
tyvar = Name -> TcKind -> TcTyVarDetails -> TyVar
mkTcTyVar Name
name' (TyVar -> TcKind
tyVarKind TyVar
tv) TcTyVarDetails
details'
; String -> SDoc -> TcRn ()
traceTc String
"cloneMetaTyVar" (TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
tyvar)
; TyVar -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
forall (m :: * -> *) a. Monad m => a -> m a
return TyVar
tyvar }
readMetaTyVar :: TyVar -> TcM MetaDetails
readMetaTyVar :: TyVar -> TcM MetaDetails
readMetaTyVar TyVar
tyvar = Bool -> SDoc -> TcM MetaDetails -> TcM MetaDetails
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (TyVar -> Bool
isMetaTyVar TyVar
tyvar) (TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
tyvar) (TcM MetaDetails -> TcM MetaDetails)
-> TcM MetaDetails -> TcM MetaDetails
forall a b. (a -> b) -> a -> b
$
IORef MetaDetails -> TcM MetaDetails
forall a env. IORef a -> IOEnv env a
readMutVar (TyVar -> IORef MetaDetails
metaTyVarRef TyVar
tyvar)
isFilledMetaTyVar_maybe :: TcTyVar -> TcM (Maybe Type)
isFilledMetaTyVar_maybe :: TyVar -> TcM (Maybe TcKind)
isFilledMetaTyVar_maybe TyVar
tv
| TyVar -> Bool
isTcTyVar TyVar
tv
, MetaTv { mtv_ref :: TcTyVarDetails -> IORef MetaDetails
mtv_ref = IORef MetaDetails
ref } <- TyVar -> TcTyVarDetails
tcTyVarDetails TyVar
tv
= do { MetaDetails
cts <- IORef MetaDetails -> TcM MetaDetails
forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
readTcRef IORef MetaDetails
ref
; case MetaDetails
cts of
Indirect TcKind
ty -> Maybe TcKind -> TcM (Maybe TcKind)
forall (m :: * -> *) a. Monad m => a -> m a
return (TcKind -> Maybe TcKind
forall a. a -> Maybe a
Just TcKind
ty)
MetaDetails
Flexi -> Maybe TcKind -> TcM (Maybe TcKind)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe TcKind
forall a. Maybe a
Nothing }
| Bool
otherwise
= Maybe TcKind -> TcM (Maybe TcKind)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe TcKind
forall a. Maybe a
Nothing
isFilledMetaTyVar :: TyVar -> TcM Bool
isFilledMetaTyVar :: TyVar -> TcRnIf TcGblEnv TcLclEnv Bool
isFilledMetaTyVar TyVar
tv = Maybe TcKind -> Bool
forall a. Maybe a -> Bool
isJust (Maybe TcKind -> Bool)
-> TcM (Maybe TcKind) -> TcRnIf TcGblEnv TcLclEnv Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyVar -> TcM (Maybe TcKind)
isFilledMetaTyVar_maybe TyVar
tv
isUnfilledMetaTyVar :: TyVar -> TcM Bool
isUnfilledMetaTyVar :: TyVar -> TcRnIf TcGblEnv TcLclEnv Bool
isUnfilledMetaTyVar TyVar
tv
| MetaTv { mtv_ref :: TcTyVarDetails -> IORef MetaDetails
mtv_ref = IORef MetaDetails
ref } <- TyVar -> TcTyVarDetails
tcTyVarDetails TyVar
tv
= do { MetaDetails
details <- IORef MetaDetails -> TcM MetaDetails
forall a env. IORef a -> IOEnv env a
readMutVar IORef MetaDetails
ref
; Bool -> TcRnIf TcGblEnv TcLclEnv Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (MetaDetails -> Bool
isFlexi MetaDetails
details) }
| Bool
otherwise = Bool -> TcRnIf TcGblEnv TcLclEnv Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
writeMetaTyVar :: TyVar -> TcKind -> TcRn ()
writeMetaTyVar TyVar
tyvar TcKind
ty
| Bool -> Bool
not Bool
debugIsOn
= TyVar -> IORef MetaDetails -> TcKind -> TcRn ()
writeMetaTyVarRef TyVar
tyvar (TyVar -> IORef MetaDetails
metaTyVarRef TyVar
tyvar) TcKind
ty
| Bool -> Bool
not (TyVar -> Bool
isTcTyVar TyVar
tyvar)
= Bool -> SDoc -> TcRn ()
forall (m :: * -> *).
(HasCallStack, Applicative m) =>
Bool -> SDoc -> m ()
massertPpr Bool
False (String -> SDoc
text String
"Writing to non-tc tyvar" SDoc -> SDoc -> SDoc
<+> TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
tyvar)
| MetaTv { mtv_ref :: TcTyVarDetails -> IORef MetaDetails
mtv_ref = IORef MetaDetails
ref } <- TyVar -> TcTyVarDetails
tcTyVarDetails TyVar
tyvar
= TyVar -> IORef MetaDetails -> TcKind -> TcRn ()
writeMetaTyVarRef TyVar
tyvar IORef MetaDetails
ref TcKind
ty
| Bool
otherwise
= Bool -> SDoc -> TcRn ()
forall (m :: * -> *).
(HasCallStack, Applicative m) =>
Bool -> SDoc -> m ()
massertPpr Bool
False (String -> SDoc
text String
"Writing to non-meta tyvar" SDoc -> SDoc -> SDoc
<+> TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
tyvar)
writeMetaTyVarRef :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM ()
writeMetaTyVarRef :: TyVar -> IORef MetaDetails -> TcKind -> TcRn ()
writeMetaTyVarRef TyVar
tyvar IORef MetaDetails
ref TcKind
ty
| Bool -> Bool
not Bool
debugIsOn
= do { String -> SDoc -> TcRn ()
traceTc String
"writeMetaTyVar" (TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
tyvar SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> TcKind -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TyVar -> TcKind
tyVarKind TyVar
tyvar)
SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
":=" SDoc -> SDoc -> SDoc
<+> TcKind -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcKind
ty)
; IORef MetaDetails -> MetaDetails -> TcRn ()
forall a gbl lcl. TcRef a -> a -> TcRnIf gbl lcl ()
writeTcRef IORef MetaDetails
ref (TcKind -> MetaDetails
Indirect TcKind
ty) }
| Bool
otherwise
= do { MetaDetails
meta_details <- IORef MetaDetails -> TcM MetaDetails
forall a env. IORef a -> IOEnv env a
readMutVar IORef MetaDetails
ref;
; TcKind
zonked_tv_kind <- TcKind -> TcM TcKind
zonkTcType TcKind
tv_kind
; TcKind
zonked_ty <- TcKind -> TcM TcKind
zonkTcType TcKind
ty
; let zonked_ty_kind :: TcKind
zonked_ty_kind = HasDebugCallStack => TcKind -> TcKind
TcKind -> TcKind
tcTypeKind TcKind
zonked_ty
zonked_ty_lvl :: TcLevel
zonked_ty_lvl = TcKind -> TcLevel
tcTypeLevel TcKind
zonked_ty
level_check_ok :: Bool
level_check_ok = Bool -> Bool
not (TcLevel
zonked_ty_lvl TcLevel -> TcLevel -> Bool
`strictlyDeeperThan` TcLevel
tv_lvl)
level_check_msg :: SDoc
level_check_msg = TcLevel -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcLevel
zonked_ty_lvl SDoc -> SDoc -> SDoc
$$ TcLevel -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcLevel
tv_lvl SDoc -> SDoc -> SDoc
$$ TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
tyvar SDoc -> SDoc -> SDoc
$$ TcKind -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcKind
ty
kind_check_ok :: Bool
kind_check_ok = TcKind
zonked_ty_kind TcKind -> TcKind -> Bool
`eqType` TcKind
zonked_tv_kind
kind_msg :: SDoc
kind_msg = SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Ill-kinded update to meta tyvar")
Int
2 ( TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
tyvar SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"::" SDoc -> SDoc -> SDoc
<+> (TcKind -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcKind
tv_kind SDoc -> SDoc -> SDoc
$$ TcKind -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcKind
zonked_tv_kind)
SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
":="
SDoc -> SDoc -> SDoc
<+> TcKind -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcKind
ty SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"::" SDoc -> SDoc -> SDoc
<+> (TcKind -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcKind
zonked_ty_kind) )
; String -> SDoc -> TcRn ()
traceTc String
"writeMetaTyVar" (TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
tyvar SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
":=" SDoc -> SDoc -> SDoc
<+> TcKind -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcKind
ty)
; Bool -> SDoc -> TcRn ()
forall (m :: * -> *).
(HasCallStack, Applicative m) =>
Bool -> SDoc -> m ()
massertPpr (MetaDetails -> Bool
isFlexi MetaDetails
meta_details) (MetaDetails -> SDoc
double_upd_msg MetaDetails
meta_details)
; Bool -> SDoc -> TcRn ()
forall (m :: * -> *).
(HasCallStack, Applicative m) =>
Bool -> SDoc -> m ()
massertPpr Bool
level_check_ok SDoc
level_check_msg
; Bool -> SDoc -> TcRn ()
forall (m :: * -> *).
(HasCallStack, Applicative m) =>
Bool -> SDoc -> m ()
massertPpr Bool
kind_check_ok SDoc
kind_msg
; IORef MetaDetails -> MetaDetails -> TcRn ()
forall a env. IORef a -> a -> IOEnv env ()
writeMutVar IORef MetaDetails
ref (TcKind -> MetaDetails
Indirect TcKind
ty) }
where
tv_kind :: TcKind
tv_kind = TyVar -> TcKind
tyVarKind TyVar
tyvar
tv_lvl :: TcLevel
tv_lvl = TyVar -> TcLevel
tcTyVarLevel TyVar
tyvar
double_upd_msg :: MetaDetails -> SDoc
double_upd_msg MetaDetails
details = SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Double update of meta tyvar")
Int
2 (TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
tyvar SDoc -> SDoc -> SDoc
$$ MetaDetails -> SDoc
forall a. Outputable a => a -> SDoc
ppr MetaDetails
details)
newMultiplicityVar :: TcM TcType
newMultiplicityVar :: TcM TcKind
newMultiplicityVar = TcKind -> TcM TcKind
newFlexiTyVarTy TcKind
multiplicityTy
newFlexiTyVar :: Kind -> TcM TcTyVar
newFlexiTyVar :: TcKind -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
newFlexiTyVar TcKind
kind = MetaInfo -> TcKind -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
newAnonMetaTyVar MetaInfo
TauTv TcKind
kind
newNamedFlexiTyVar :: FastString -> Kind -> TcM TcTyVar
newNamedFlexiTyVar :: FastString -> TcKind -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
newNamedFlexiTyVar FastString
fs TcKind
kind = FastString
-> MetaInfo -> TcKind -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
newNamedAnonMetaTyVar FastString
fs MetaInfo
TauTv TcKind
kind
newFlexiTyVarTy :: Kind -> TcM TcType
newFlexiTyVarTy :: TcKind -> TcM TcKind
newFlexiTyVarTy TcKind
kind = do
TyVar
tc_tyvar <- TcKind -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
newFlexiTyVar TcKind
kind
TcKind -> TcM TcKind
forall (m :: * -> *) a. Monad m => a -> m a
return (TyVar -> TcKind
mkTyVarTy TyVar
tc_tyvar)
newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
newFlexiTyVarTys :: Int -> TcKind -> TcM [TcKind]
newFlexiTyVarTys Int
n TcKind
kind = Int -> TcM TcKind -> TcM [TcKind]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
n (TcKind -> TcM TcKind
newFlexiTyVarTy TcKind
kind)
newOpenTypeKind :: TcM TcKind
newOpenTypeKind :: TcM TcKind
newOpenTypeKind
= do { TcKind
rr <- TcKind -> TcM TcKind
newFlexiTyVarTy TcKind
runtimeRepTy
; TcKind -> TcM TcKind
forall (m :: * -> *) a. Monad m => a -> m a
return (TcKind -> TcKind
mkTYPEapp TcKind
rr) }
newOpenFlexiTyVarTy :: TcM TcType
newOpenFlexiTyVarTy :: TcM TcKind
newOpenFlexiTyVarTy
= do { TyVar
tv <- IOEnv (Env TcGblEnv TcLclEnv) TyVar
newOpenFlexiTyVar
; TcKind -> TcM TcKind
forall (m :: * -> *) a. Monad m => a -> m a
return (TyVar -> TcKind
mkTyVarTy TyVar
tv) }
newOpenFlexiTyVar :: TcM TcTyVar
newOpenFlexiTyVar :: IOEnv (Env TcGblEnv TcLclEnv) TyVar
newOpenFlexiTyVar
= do { TcKind
kind <- TcM TcKind
newOpenTypeKind
; TcKind -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
newFlexiTyVar TcKind
kind }
newOpenBoxedTypeKind :: TcM TcKind
newOpenBoxedTypeKind :: TcM TcKind
newOpenBoxedTypeKind
= do { TcKind
lev <- TcKind -> TcM TcKind
newFlexiTyVarTy (TyCon -> TcKind
mkTyConTy TyCon
levityTyCon)
; let rr :: TcKind
rr = TyCon -> [TcKind] -> TcKind
mkTyConApp TyCon
boxedRepDataConTyCon [TcKind
lev]
; TcKind -> TcM TcKind
forall (m :: * -> *) a. Monad m => a -> m a
return (TcKind -> TcKind
mkTYPEapp TcKind
rr) }
newMetaTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
newMetaTyVars :: [TyVar] -> TcM (TCvSubst, [TyVar])
newMetaTyVars = TCvSubst -> [TyVar] -> TcM (TCvSubst, [TyVar])
newMetaTyVarsX TCvSubst
emptyTCvSubst
newMetaTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
newMetaTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TyVar])
newMetaTyVarsX TCvSubst
subst = (TCvSubst
-> TyVar -> IOEnv (Env TcGblEnv TcLclEnv) (TCvSubst, TyVar))
-> TCvSubst -> [TyVar] -> TcM (TCvSubst, [TyVar])
forall (m :: * -> *) acc x y.
Monad m =>
(acc -> x -> m (acc, y)) -> acc -> [x] -> m (acc, [y])
mapAccumLM TCvSubst
-> TyVar -> IOEnv (Env TcGblEnv TcLclEnv) (TCvSubst, TyVar)
newMetaTyVarX TCvSubst
subst
newMetaTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
newMetaTyVarX :: TCvSubst
-> TyVar -> IOEnv (Env TcGblEnv TcLclEnv) (TCvSubst, TyVar)
newMetaTyVarX = MetaInfo
-> TCvSubst
-> TyVar
-> IOEnv (Env TcGblEnv TcLclEnv) (TCvSubst, TyVar)
new_meta_tv_x MetaInfo
TauTv
newMetaTyVarTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
newMetaTyVarTyVarX :: TCvSubst
-> TyVar -> IOEnv (Env TcGblEnv TcLclEnv) (TCvSubst, TyVar)
newMetaTyVarTyVarX = MetaInfo
-> TCvSubst
-> TyVar
-> IOEnv (Env TcGblEnv TcLclEnv) (TCvSubst, TyVar)
new_meta_tv_x MetaInfo
TyVarTv
newWildCardX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
newWildCardX :: TCvSubst
-> TyVar -> IOEnv (Env TcGblEnv TcLclEnv) (TCvSubst, TyVar)
newWildCardX TCvSubst
subst TyVar
tv
= do { TyVar
new_tv <- MetaInfo -> TcKind -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
newAnonMetaTyVar MetaInfo
TauTv (HasDebugCallStack => TCvSubst -> TcKind -> TcKind
TCvSubst -> TcKind -> TcKind
substTy TCvSubst
subst (TyVar -> TcKind
tyVarKind TyVar
tv))
; (TCvSubst, TyVar)
-> IOEnv (Env TcGblEnv TcLclEnv) (TCvSubst, TyVar)
forall (m :: * -> *) a. Monad m => a -> m a
return (TCvSubst -> TyVar -> TyVar -> TCvSubst
extendTvSubstWithClone TCvSubst
subst TyVar
tv TyVar
new_tv, TyVar
new_tv) }
new_meta_tv_x :: MetaInfo -> TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
new_meta_tv_x :: MetaInfo
-> TCvSubst
-> TyVar
-> IOEnv (Env TcGblEnv TcLclEnv) (TCvSubst, TyVar)
new_meta_tv_x MetaInfo
info TCvSubst
subst TyVar
tv
= do { TyVar
new_tv <- MetaInfo -> TyVar -> TcKind -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
cloneAnonMetaTyVar MetaInfo
info TyVar
tv TcKind
substd_kind
; let subst1 :: TCvSubst
subst1 = TCvSubst -> TyVar -> TyVar -> TCvSubst
extendTvSubstWithClone TCvSubst
subst TyVar
tv TyVar
new_tv
; (TCvSubst, TyVar)
-> IOEnv (Env TcGblEnv TcLclEnv) (TCvSubst, TyVar)
forall (m :: * -> *) a. Monad m => a -> m a
return (TCvSubst
subst1, TyVar
new_tv) }
where
substd_kind :: TcKind
substd_kind = TCvSubst -> TcKind -> TcKind
substTyUnchecked TCvSubst
subst (TyVar -> TcKind
tyVarKind TyVar
tv)
newMetaTyVarTyAtLevel :: TcLevel -> TcKind -> TcM TcType
newMetaTyVarTyAtLevel :: TcLevel -> TcKind -> TcM TcKind
newMetaTyVarTyAtLevel TcLevel
tc_lvl TcKind
kind
= do { TcTyVarDetails
details <- TcLevel -> TcM TcTyVarDetails
newTauTvDetailsAtLevel TcLevel
tc_lvl
; Name
name <- FastString -> TcM Name
newMetaTyVarName (String -> FastString
fsLit String
"p")
; TcKind -> TcM TcKind
forall (m :: * -> *) a. Monad m => a -> m a
return (TyVar -> TcKind
mkTyVarTy (Name -> TcKind -> TcTyVarDetails -> TyVar
mkTcTyVar Name
name TcKind
kind TcTyVarDetails
details)) }
data CandidatesQTvs
= DV { CandidatesQTvs -> DTyVarSet
dv_kvs :: DTyVarSet
, CandidatesQTvs -> DTyVarSet
dv_tvs :: DTyVarSet
, CandidatesQTvs -> CoVarSet
dv_cvs :: CoVarSet
}
instance Semi.Semigroup CandidatesQTvs where
(DV { dv_kvs :: CandidatesQTvs -> DTyVarSet
dv_kvs = DTyVarSet
kv1, dv_tvs :: CandidatesQTvs -> DTyVarSet
dv_tvs = DTyVarSet
tv1, dv_cvs :: CandidatesQTvs -> CoVarSet
dv_cvs = CoVarSet
cv1 })
<> :: CandidatesQTvs -> CandidatesQTvs -> CandidatesQTvs
<> (DV { dv_kvs :: CandidatesQTvs -> DTyVarSet
dv_kvs = DTyVarSet
kv2, dv_tvs :: CandidatesQTvs -> DTyVarSet
dv_tvs = DTyVarSet
tv2, dv_cvs :: CandidatesQTvs -> CoVarSet
dv_cvs = CoVarSet
cv2 })
= DV :: DTyVarSet -> DTyVarSet -> CoVarSet -> CandidatesQTvs
DV { dv_kvs :: DTyVarSet
dv_kvs = DTyVarSet
kv1 DTyVarSet -> DTyVarSet -> DTyVarSet
`unionDVarSet` DTyVarSet
kv2
, dv_tvs :: DTyVarSet
dv_tvs = DTyVarSet
tv1 DTyVarSet -> DTyVarSet -> DTyVarSet
`unionDVarSet` DTyVarSet
tv2
, dv_cvs :: CoVarSet
dv_cvs = CoVarSet
cv1 CoVarSet -> CoVarSet -> CoVarSet
`unionVarSet` CoVarSet
cv2 }
instance Monoid CandidatesQTvs where
mempty :: CandidatesQTvs
mempty = DV :: DTyVarSet -> DTyVarSet -> CoVarSet -> CandidatesQTvs
DV { dv_kvs :: DTyVarSet
dv_kvs = DTyVarSet
emptyDVarSet, dv_tvs :: DTyVarSet
dv_tvs = DTyVarSet
emptyDVarSet, dv_cvs :: CoVarSet
dv_cvs = CoVarSet
emptyVarSet }
mappend :: CandidatesQTvs -> CandidatesQTvs -> CandidatesQTvs
mappend = CandidatesQTvs -> CandidatesQTvs -> CandidatesQTvs
forall a. Semigroup a => a -> a -> a
(Semi.<>)
instance Outputable CandidatesQTvs where
ppr :: CandidatesQTvs -> SDoc
ppr (DV {dv_kvs :: CandidatesQTvs -> DTyVarSet
dv_kvs = DTyVarSet
kvs, dv_tvs :: CandidatesQTvs -> DTyVarSet
dv_tvs = DTyVarSet
tvs, dv_cvs :: CandidatesQTvs -> CoVarSet
dv_cvs = CoVarSet
cvs })
= String -> SDoc
text String
"DV" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
braces ((SDoc -> SDoc) -> [SDoc] -> SDoc
forall a. (a -> SDoc) -> [a] -> SDoc
pprWithCommas SDoc -> SDoc
forall a. a -> a
id [ String -> SDoc
text String
"dv_kvs =" SDoc -> SDoc -> SDoc
<+> DTyVarSet -> SDoc
forall a. Outputable a => a -> SDoc
ppr DTyVarSet
kvs
, String -> SDoc
text String
"dv_tvs =" SDoc -> SDoc -> SDoc
<+> DTyVarSet -> SDoc
forall a. Outputable a => a -> SDoc
ppr DTyVarSet
tvs
, String -> SDoc
text String
"dv_cvs =" SDoc -> SDoc -> SDoc
<+> CoVarSet -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoVarSet
cvs ])
isEmptyCandidates :: CandidatesQTvs -> Bool
isEmptyCandidates :: CandidatesQTvs -> Bool
isEmptyCandidates (DV { dv_kvs :: CandidatesQTvs -> DTyVarSet
dv_kvs = DTyVarSet
kvs, dv_tvs :: CandidatesQTvs -> DTyVarSet
dv_tvs = DTyVarSet
tvs })
= DTyVarSet -> Bool
isEmptyDVarSet DTyVarSet
kvs Bool -> Bool -> Bool
&& DTyVarSet -> Bool
isEmptyDVarSet DTyVarSet
tvs
candidateVars :: CandidatesQTvs -> ([TcTyVar], [TcTyVar])
candidateVars :: CandidatesQTvs -> ([TyVar], [TyVar])
candidateVars (DV { dv_kvs :: CandidatesQTvs -> DTyVarSet
dv_kvs = DTyVarSet
dep_kv_set, dv_tvs :: CandidatesQTvs -> DTyVarSet
dv_tvs = DTyVarSet
nondep_tkv_set })
= ([TyVar]
dep_kvs, [TyVar]
nondep_tvs)
where
dep_kvs :: [TyVar]
dep_kvs = [TyVar] -> [TyVar]
scopedSort ([TyVar] -> [TyVar]) -> [TyVar] -> [TyVar]
forall a b. (a -> b) -> a -> b
$ DTyVarSet -> [TyVar]
dVarSetElems DTyVarSet
dep_kv_set
nondep_tvs :: [TyVar]
nondep_tvs = DTyVarSet -> [TyVar]
dVarSetElems (DTyVarSet
nondep_tkv_set DTyVarSet -> DTyVarSet -> DTyVarSet
`minusDVarSet` DTyVarSet
dep_kv_set)
candidateKindVars :: CandidatesQTvs -> TyVarSet
candidateKindVars :: CandidatesQTvs -> CoVarSet
candidateKindVars CandidatesQTvs
dvs = DTyVarSet -> CoVarSet
dVarSetToVarSet (CandidatesQTvs -> DTyVarSet
dv_kvs CandidatesQTvs
dvs)
delCandidates :: CandidatesQTvs -> [Var] -> CandidatesQTvs
delCandidates :: CandidatesQTvs -> [TyVar] -> CandidatesQTvs
delCandidates (DV { dv_kvs :: CandidatesQTvs -> DTyVarSet
dv_kvs = DTyVarSet
kvs, dv_tvs :: CandidatesQTvs -> DTyVarSet
dv_tvs = DTyVarSet
tvs, dv_cvs :: CandidatesQTvs -> CoVarSet
dv_cvs = CoVarSet
cvs }) [TyVar]
vars
= DV :: DTyVarSet -> DTyVarSet -> CoVarSet -> CandidatesQTvs
DV { dv_kvs :: DTyVarSet
dv_kvs = DTyVarSet
kvs DTyVarSet -> [TyVar] -> DTyVarSet
`delDVarSetList` [TyVar]
vars
, dv_tvs :: DTyVarSet
dv_tvs = DTyVarSet
tvs DTyVarSet -> [TyVar] -> DTyVarSet
`delDVarSetList` [TyVar]
vars
, dv_cvs :: CoVarSet
dv_cvs = CoVarSet
cvs CoVarSet -> [TyVar] -> CoVarSet
`delVarSetList` [TyVar]
vars }
partitionCandidates :: CandidatesQTvs -> (TyVar -> Bool) -> (TyVarSet, CandidatesQTvs)
partitionCandidates :: CandidatesQTvs -> (TyVar -> Bool) -> (CoVarSet, CandidatesQTvs)
partitionCandidates dvs :: CandidatesQTvs
dvs@(DV { dv_kvs :: CandidatesQTvs -> DTyVarSet
dv_kvs = DTyVarSet
kvs, dv_tvs :: CandidatesQTvs -> DTyVarSet
dv_tvs = DTyVarSet
tvs }) TyVar -> Bool
pred
= (CoVarSet
extracted, CandidatesQTvs
dvs { dv_kvs :: DTyVarSet
dv_kvs = DTyVarSet
rest_kvs, dv_tvs :: DTyVarSet
dv_tvs = DTyVarSet
rest_tvs })
where
(DTyVarSet
extracted_kvs, DTyVarSet
rest_kvs) = (TyVar -> Bool) -> DTyVarSet -> (DTyVarSet, DTyVarSet)
partitionDVarSet TyVar -> Bool
pred DTyVarSet
kvs
(DTyVarSet
extracted_tvs, DTyVarSet
rest_tvs) = (TyVar -> Bool) -> DTyVarSet -> (DTyVarSet, DTyVarSet)
partitionDVarSet TyVar -> Bool
pred DTyVarSet
tvs
extracted :: CoVarSet
extracted = DTyVarSet -> CoVarSet
dVarSetToVarSet DTyVarSet
extracted_kvs CoVarSet -> CoVarSet -> CoVarSet
`unionVarSet` DTyVarSet -> CoVarSet
dVarSetToVarSet DTyVarSet
extracted_tvs
candidateQTyVarsWithBinders :: [TyVar] -> Type -> TcM CandidatesQTvs
candidateQTyVarsWithBinders :: [TyVar] -> TcKind -> TcM CandidatesQTvs
candidateQTyVarsWithBinders [TyVar]
bound_tvs TcKind
ty
= do { CandidatesQTvs
kvs <- [TcKind] -> TcM CandidatesQTvs
candidateQTyVarsOfKinds ((TyVar -> TcKind) -> [TyVar] -> [TcKind]
forall a b. (a -> b) -> [a] -> [b]
map TyVar -> TcKind
tyVarKind [TyVar]
bound_tvs)
; CandidatesQTvs
all_tvs <- TcKind
-> Bool
-> CoVarSet
-> CandidatesQTvs
-> TcKind
-> TcM CandidatesQTvs
collect_cand_qtvs TcKind
ty Bool
False CoVarSet
emptyVarSet CandidatesQTvs
kvs TcKind
ty
; CandidatesQTvs -> TcM CandidatesQTvs
forall (m :: * -> *) a. Monad m => a -> m a
return (CandidatesQTvs
all_tvs CandidatesQTvs -> [TyVar] -> CandidatesQTvs
`delCandidates` [TyVar]
bound_tvs) }
candidateQTyVarsOfType :: TcType
-> TcM CandidatesQTvs
candidateQTyVarsOfType :: TcKind -> TcM CandidatesQTvs
candidateQTyVarsOfType TcKind
ty = TcKind
-> Bool
-> CoVarSet
-> CandidatesQTvs
-> TcKind
-> TcM CandidatesQTvs
collect_cand_qtvs TcKind
ty Bool
False CoVarSet
emptyVarSet CandidatesQTvs
forall a. Monoid a => a
mempty TcKind
ty
candidateQTyVarsOfTypes :: [Type] -> TcM CandidatesQTvs
candidateQTyVarsOfTypes :: [TcKind] -> TcM CandidatesQTvs
candidateQTyVarsOfTypes [TcKind]
tys = (CandidatesQTvs -> TcKind -> TcM CandidatesQTvs)
-> CandidatesQTvs -> [TcKind] -> TcM CandidatesQTvs
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM (\CandidatesQTvs
acc TcKind
ty -> TcKind
-> Bool
-> CoVarSet
-> CandidatesQTvs
-> TcKind
-> TcM CandidatesQTvs
collect_cand_qtvs TcKind
ty Bool
False CoVarSet
emptyVarSet CandidatesQTvs
acc TcKind
ty)
CandidatesQTvs
forall a. Monoid a => a
mempty [TcKind]
tys
candidateQTyVarsOfKind :: TcKind
-> TcM CandidatesQTvs
candidateQTyVarsOfKind :: TcKind -> TcM CandidatesQTvs
candidateQTyVarsOfKind TcKind
ty = TcKind
-> Bool
-> CoVarSet
-> CandidatesQTvs
-> TcKind
-> TcM CandidatesQTvs
collect_cand_qtvs TcKind
ty Bool
True CoVarSet
emptyVarSet CandidatesQTvs
forall a. Monoid a => a
mempty TcKind
ty
candidateQTyVarsOfKinds :: [TcKind]
-> TcM CandidatesQTvs
candidateQTyVarsOfKinds :: [TcKind] -> TcM CandidatesQTvs
candidateQTyVarsOfKinds [TcKind]
tys = (CandidatesQTvs -> TcKind -> TcM CandidatesQTvs)
-> CandidatesQTvs -> [TcKind] -> TcM CandidatesQTvs
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\CandidatesQTvs
acc TcKind
ty -> TcKind
-> Bool
-> CoVarSet
-> CandidatesQTvs
-> TcKind
-> TcM CandidatesQTvs
collect_cand_qtvs TcKind
ty Bool
True CoVarSet
emptyVarSet CandidatesQTvs
acc TcKind
ty)
CandidatesQTvs
forall a. Monoid a => a
mempty [TcKind]
tys
collect_cand_qtvs
:: TcType
-> Bool
-> VarSet
-> CandidatesQTvs
-> Type
-> TcM CandidatesQTvs
collect_cand_qtvs :: TcKind
-> Bool
-> CoVarSet
-> CandidatesQTvs
-> TcKind
-> TcM CandidatesQTvs
collect_cand_qtvs TcKind
orig_ty Bool
is_dep CoVarSet
bound CandidatesQTvs
dvs TcKind
ty
= CandidatesQTvs -> TcKind -> TcM CandidatesQTvs
go CandidatesQTvs
dvs TcKind
ty
where
is_bound :: TyVar -> Bool
is_bound TyVar
tv = TyVar
tv TyVar -> CoVarSet -> Bool
`elemVarSet` CoVarSet
bound
go :: CandidatesQTvs -> TcType -> TcM CandidatesQTvs
go :: CandidatesQTvs -> TcKind -> TcM CandidatesQTvs
go CandidatesQTvs
dv (AppTy TcKind
t1 TcKind
t2) = (CandidatesQTvs -> TcKind -> TcM CandidatesQTvs)
-> CandidatesQTvs -> [TcKind] -> TcM CandidatesQTvs
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM CandidatesQTvs -> TcKind -> TcM CandidatesQTvs
go CandidatesQTvs
dv [TcKind
t1, TcKind
t2]
go CandidatesQTvs
dv (TyConApp TyCon
tc [TcKind]
tys) = CandidatesQTvs -> [TyConBinder] -> [TcKind] -> TcM CandidatesQTvs
go_tc_args CandidatesQTvs
dv (TyCon -> [TyConBinder]
tyConBinders TyCon
tc) [TcKind]
tys
go CandidatesQTvs
dv (FunTy AnonArgFlag
_ TcKind
w TcKind
arg TcKind
res) = (CandidatesQTvs -> TcKind -> TcM CandidatesQTvs)
-> CandidatesQTvs -> [TcKind] -> TcM CandidatesQTvs
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM CandidatesQTvs -> TcKind -> TcM CandidatesQTvs
go CandidatesQTvs
dv [TcKind
w, TcKind
arg, TcKind
res]
go CandidatesQTvs
dv (LitTy {}) = CandidatesQTvs -> TcM CandidatesQTvs
forall (m :: * -> *) a. Monad m => a -> m a
return CandidatesQTvs
dv
go CandidatesQTvs
dv (CastTy TcKind
ty Coercion
co) = do CandidatesQTvs
dv1 <- CandidatesQTvs -> TcKind -> TcM CandidatesQTvs
go CandidatesQTvs
dv TcKind
ty
TcKind
-> CoVarSet -> CandidatesQTvs -> Coercion -> TcM CandidatesQTvs
collect_cand_qtvs_co TcKind
orig_ty CoVarSet
bound CandidatesQTvs
dv1 Coercion
co
go CandidatesQTvs
dv (CoercionTy Coercion
co) = TcKind
-> CoVarSet -> CandidatesQTvs -> Coercion -> TcM CandidatesQTvs
collect_cand_qtvs_co TcKind
orig_ty CoVarSet
bound CandidatesQTvs
dv Coercion
co
go CandidatesQTvs
dv (TyVarTy TyVar
tv)
| TyVar -> Bool
is_bound TyVar
tv = CandidatesQTvs -> TcM CandidatesQTvs
forall (m :: * -> *) a. Monad m => a -> m a
return CandidatesQTvs
dv
| Bool
otherwise = do { Maybe TcKind
m_contents <- TyVar -> TcM (Maybe TcKind)
isFilledMetaTyVar_maybe TyVar
tv
; case Maybe TcKind
m_contents of
Just TcKind
ind_ty -> CandidatesQTvs -> TcKind -> TcM CandidatesQTvs
go CandidatesQTvs
dv TcKind
ind_ty
Maybe TcKind
Nothing -> CandidatesQTvs -> TyVar -> TcM CandidatesQTvs
go_tv CandidatesQTvs
dv TyVar
tv }
go CandidatesQTvs
dv (ForAllTy (Bndr TyVar
tv ArgFlag
_) TcKind
ty)
= do { CandidatesQTvs
dv1 <- TcKind
-> Bool
-> CoVarSet
-> CandidatesQTvs
-> TcKind
-> TcM CandidatesQTvs
collect_cand_qtvs TcKind
orig_ty Bool
True CoVarSet
bound CandidatesQTvs
dv (TyVar -> TcKind
tyVarKind TyVar
tv)
; TcKind
-> Bool
-> CoVarSet
-> CandidatesQTvs
-> TcKind
-> TcM CandidatesQTvs
collect_cand_qtvs TcKind
orig_ty Bool
is_dep (CoVarSet
bound CoVarSet -> TyVar -> CoVarSet
`extendVarSet` TyVar
tv) CandidatesQTvs
dv1 TcKind
ty }
go_tc_args :: CandidatesQTvs -> [TyConBinder] -> [TcKind] -> TcM CandidatesQTvs
go_tc_args CandidatesQTvs
dv (TyConBinder
tc_bndr:[TyConBinder]
tc_bndrs) (TcKind
ty:[TcKind]
tys)
= do { CandidatesQTvs
dv1 <- TcKind
-> Bool
-> CoVarSet
-> CandidatesQTvs
-> TcKind
-> TcM CandidatesQTvs
collect_cand_qtvs TcKind
orig_ty (Bool
is_dep Bool -> Bool -> Bool
|| TyConBinder -> Bool
isNamedTyConBinder TyConBinder
tc_bndr)
CoVarSet
bound CandidatesQTvs
dv TcKind
ty
; CandidatesQTvs -> [TyConBinder] -> [TcKind] -> TcM CandidatesQTvs
go_tc_args CandidatesQTvs
dv1 [TyConBinder]
tc_bndrs [TcKind]
tys }
go_tc_args CandidatesQTvs
dv [TyConBinder]
_bndrs [TcKind]
tys
= (CandidatesQTvs -> TcKind -> TcM CandidatesQTvs)
-> CandidatesQTvs -> [TcKind] -> TcM CandidatesQTvs
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM CandidatesQTvs -> TcKind -> TcM CandidatesQTvs
go CandidatesQTvs
dv [TcKind]
tys
go_tv :: CandidatesQTvs -> TyVar -> TcM CandidatesQTvs
go_tv dv :: CandidatesQTvs
dv@(DV { dv_kvs :: CandidatesQTvs -> DTyVarSet
dv_kvs = DTyVarSet
kvs, dv_tvs :: CandidatesQTvs -> DTyVarSet
dv_tvs = DTyVarSet
tvs }) TyVar
tv
| TyVar
tv TyVar -> DTyVarSet -> Bool
`elemDVarSet` DTyVarSet
kvs
= CandidatesQTvs -> TcM CandidatesQTvs
forall (m :: * -> *) a. Monad m => a -> m a
return CandidatesQTvs
dv
| Bool -> Bool
not Bool
is_dep
, TyVar
tv TyVar -> DTyVarSet -> Bool
`elemDVarSet` DTyVarSet
tvs
= CandidatesQTvs -> TcM CandidatesQTvs
forall (m :: * -> *) a. Monad m => a -> m a
return CandidatesQTvs
dv
| Bool
otherwise
= do { TcKind
tv_kind <- TcKind -> TcM TcKind
zonkTcType (TyVar -> TcKind
tyVarKind TyVar
tv)
; let tv_kind_vars :: CoVarSet
tv_kind_vars = TcKind -> CoVarSet
tyCoVarsOfType TcKind
tv_kind
; TcLevel
cur_lvl <- TcM TcLevel
getTcLevel
; if | TyVar -> TcLevel
tcTyVarLevel TyVar
tv TcLevel -> TcLevel -> Bool
forall a. Ord a => a -> a -> Bool
<= TcLevel
cur_lvl
-> CandidatesQTvs -> TcM CandidatesQTvs
forall (m :: * -> *) a. Monad m => a -> m a
return CandidatesQTvs
dv
| case TyVar -> TcTyVarDetails
tcTyVarDetails TyVar
tv of
SkolemTv SkolemInfo
_ TcLevel
lvl Bool
_ -> TcLevel
lvl TcLevel -> TcLevel -> Bool
forall a. Ord a => a -> a -> Bool
> TcLevel -> TcLevel
pushTcLevel TcLevel
cur_lvl
TcTyVarDetails
_ -> Bool
False
-> CandidatesQTvs -> TcM CandidatesQTvs
forall (m :: * -> *) a. Monad m => a -> m a
return CandidatesQTvs
dv
| CoVarSet -> CoVarSet -> Bool
intersectsVarSet CoVarSet
bound CoVarSet
tv_kind_vars
-> do { String -> SDoc -> TcRn ()
traceTc String
"Naughty quantifier" (SDoc -> TcRn ()) -> SDoc -> TcRn ()
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
vcat [ TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
tv SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> TcKind -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcKind
tv_kind
, String -> SDoc
text String
"bound:" SDoc -> SDoc -> SDoc
<+> [TyVar] -> SDoc
pprTyVars (CoVarSet -> [TyVar]
forall elt. UniqSet elt -> [elt]
nonDetEltsUniqSet CoVarSet
bound)
, String -> SDoc
text String
"fvs:" SDoc -> SDoc -> SDoc
<+> [TyVar] -> SDoc
pprTyVars (CoVarSet -> [TyVar]
forall elt. UniqSet elt -> [elt]
nonDetEltsUniqSet CoVarSet
tv_kind_vars) ]
; let escapees :: CoVarSet
escapees = CoVarSet -> CoVarSet -> CoVarSet
intersectVarSet CoVarSet
bound CoVarSet
tv_kind_vars
; TcKind -> TyVar -> CoVarSet -> TcM CandidatesQTvs
forall a. TcKind -> TyVar -> CoVarSet -> TcM a
naughtyQuantification TcKind
orig_ty TyVar
tv CoVarSet
escapees }
| Bool
otherwise
-> do { let tv' :: TyVar
tv' = TyVar
tv TyVar -> TcKind -> TyVar
`setTyVarKind` TcKind
tv_kind
dv' :: CandidatesQTvs
dv' | Bool
is_dep = CandidatesQTvs
dv { dv_kvs :: DTyVarSet
dv_kvs = DTyVarSet
kvs DTyVarSet -> TyVar -> DTyVarSet
`extendDVarSet` TyVar
tv' }
| Bool
otherwise = CandidatesQTvs
dv { dv_tvs :: DTyVarSet
dv_tvs = DTyVarSet
tvs DTyVarSet -> TyVar -> DTyVarSet
`extendDVarSet` TyVar
tv' }
; TcKind
-> Bool
-> CoVarSet
-> CandidatesQTvs
-> TcKind
-> TcM CandidatesQTvs
collect_cand_qtvs TcKind
orig_ty Bool
True CoVarSet
bound CandidatesQTvs
dv' TcKind
tv_kind } }
collect_cand_qtvs_co :: TcType
-> VarSet
-> CandidatesQTvs -> Coercion
-> TcM CandidatesQTvs
collect_cand_qtvs_co :: TcKind
-> CoVarSet -> CandidatesQTvs -> Coercion -> TcM CandidatesQTvs
collect_cand_qtvs_co TcKind
orig_ty CoVarSet
bound = CandidatesQTvs -> Coercion -> TcM CandidatesQTvs
go_co
where
go_co :: CandidatesQTvs -> Coercion -> TcM CandidatesQTvs
go_co CandidatesQTvs
dv (Refl TcKind
ty) = TcKind
-> Bool
-> CoVarSet
-> CandidatesQTvs
-> TcKind
-> TcM CandidatesQTvs
collect_cand_qtvs TcKind
orig_ty Bool
True CoVarSet
bound CandidatesQTvs
dv TcKind
ty
go_co CandidatesQTvs
dv (GRefl Role
_ TcKind
ty MCoercionN
mco) = do CandidatesQTvs
dv1 <- TcKind
-> Bool
-> CoVarSet
-> CandidatesQTvs
-> TcKind
-> TcM CandidatesQTvs
collect_cand_qtvs TcKind
orig_ty Bool
True CoVarSet
bound CandidatesQTvs
dv TcKind
ty
CandidatesQTvs -> MCoercionN -> TcM CandidatesQTvs
go_mco CandidatesQTvs
dv1 MCoercionN
mco
go_co CandidatesQTvs
dv (TyConAppCo Role
_ TyCon
_ [Coercion]
cos) = (CandidatesQTvs -> Coercion -> TcM CandidatesQTvs)
-> CandidatesQTvs -> [Coercion] -> TcM CandidatesQTvs
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM CandidatesQTvs -> Coercion -> TcM CandidatesQTvs
go_co CandidatesQTvs
dv [Coercion]
cos
go_co CandidatesQTvs
dv (AppCo Coercion
co1 Coercion
co2) = (CandidatesQTvs -> Coercion -> TcM CandidatesQTvs)
-> CandidatesQTvs -> [Coercion] -> TcM CandidatesQTvs
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM CandidatesQTvs -> Coercion -> TcM CandidatesQTvs
go_co CandidatesQTvs
dv [Coercion
co1, Coercion
co2]
go_co CandidatesQTvs
dv (FunCo Role
_ Coercion
w Coercion
co1 Coercion
co2) = (CandidatesQTvs -> Coercion -> TcM CandidatesQTvs)
-> CandidatesQTvs -> [Coercion] -> TcM CandidatesQTvs
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM CandidatesQTvs -> Coercion -> TcM CandidatesQTvs
go_co CandidatesQTvs
dv [Coercion
w, Coercion
co1, Coercion
co2]
go_co CandidatesQTvs
dv (AxiomInstCo CoAxiom Branched
_ Int
_ [Coercion]
cos) = (CandidatesQTvs -> Coercion -> TcM CandidatesQTvs)
-> CandidatesQTvs -> [Coercion] -> TcM CandidatesQTvs
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM CandidatesQTvs -> Coercion -> TcM CandidatesQTvs
go_co CandidatesQTvs
dv [Coercion]
cos
go_co CandidatesQTvs
dv (AxiomRuleCo CoAxiomRule
_ [Coercion]
cos) = (CandidatesQTvs -> Coercion -> TcM CandidatesQTvs)
-> CandidatesQTvs -> [Coercion] -> TcM CandidatesQTvs
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM CandidatesQTvs -> Coercion -> TcM CandidatesQTvs
go_co CandidatesQTvs
dv [Coercion]
cos
go_co CandidatesQTvs
dv (UnivCo UnivCoProvenance
prov Role
_ TcKind
t1 TcKind
t2) = do CandidatesQTvs
dv1 <- CandidatesQTvs -> UnivCoProvenance -> TcM CandidatesQTvs
go_prov CandidatesQTvs
dv UnivCoProvenance
prov
CandidatesQTvs
dv2 <- TcKind
-> Bool
-> CoVarSet
-> CandidatesQTvs
-> TcKind
-> TcM CandidatesQTvs
collect_cand_qtvs TcKind
orig_ty Bool
True CoVarSet
bound CandidatesQTvs
dv1 TcKind
t1
TcKind
-> Bool
-> CoVarSet
-> CandidatesQTvs
-> TcKind
-> TcM CandidatesQTvs
collect_cand_qtvs TcKind
orig_ty Bool
True CoVarSet
bound CandidatesQTvs
dv2 TcKind
t2
go_co CandidatesQTvs
dv (SymCo Coercion
co) = CandidatesQTvs -> Coercion -> TcM CandidatesQTvs
go_co CandidatesQTvs
dv Coercion
co
go_co CandidatesQTvs
dv (TransCo Coercion
co1 Coercion
co2) = (CandidatesQTvs -> Coercion -> TcM CandidatesQTvs)
-> CandidatesQTvs -> [Coercion] -> TcM CandidatesQTvs
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM CandidatesQTvs -> Coercion -> TcM CandidatesQTvs
go_co CandidatesQTvs
dv [Coercion
co1, Coercion
co2]
go_co CandidatesQTvs
dv (NthCo Role
_ Int
_ Coercion
co) = CandidatesQTvs -> Coercion -> TcM CandidatesQTvs
go_co CandidatesQTvs
dv Coercion
co
go_co CandidatesQTvs
dv (LRCo LeftOrRight
_ Coercion
co) = CandidatesQTvs -> Coercion -> TcM CandidatesQTvs
go_co CandidatesQTvs
dv Coercion
co
go_co CandidatesQTvs
dv (InstCo Coercion
co1 Coercion
co2) = (CandidatesQTvs -> Coercion -> TcM CandidatesQTvs)
-> CandidatesQTvs -> [Coercion] -> TcM CandidatesQTvs
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM CandidatesQTvs -> Coercion -> TcM CandidatesQTvs
go_co CandidatesQTvs
dv [Coercion
co1, Coercion
co2]
go_co CandidatesQTvs
dv (KindCo Coercion
co) = CandidatesQTvs -> Coercion -> TcM CandidatesQTvs
go_co CandidatesQTvs
dv Coercion
co
go_co CandidatesQTvs
dv (SubCo Coercion
co) = CandidatesQTvs -> Coercion -> TcM CandidatesQTvs
go_co CandidatesQTvs
dv Coercion
co
go_co CandidatesQTvs
dv (HoleCo CoercionHole
hole)
= do Maybe Coercion
m_co <- CoercionHole -> TcRnIf TcGblEnv TcLclEnv (Maybe Coercion)
unpackCoercionHole_maybe CoercionHole
hole
case Maybe Coercion
m_co of
Just Coercion
co -> CandidatesQTvs -> Coercion -> TcM CandidatesQTvs
go_co CandidatesQTvs
dv Coercion
co
Maybe Coercion
Nothing -> CandidatesQTvs -> TyVar -> TcM CandidatesQTvs
go_cv CandidatesQTvs
dv (CoercionHole -> TyVar
coHoleCoVar CoercionHole
hole)
go_co CandidatesQTvs
dv (CoVarCo TyVar
cv) = CandidatesQTvs -> TyVar -> TcM CandidatesQTvs
go_cv CandidatesQTvs
dv TyVar
cv
go_co CandidatesQTvs
dv (ForAllCo TyVar
tcv Coercion
kind_co Coercion
co)
= do { CandidatesQTvs
dv1 <- CandidatesQTvs -> Coercion -> TcM CandidatesQTvs
go_co CandidatesQTvs
dv Coercion
kind_co
; TcKind
-> CoVarSet -> CandidatesQTvs -> Coercion -> TcM CandidatesQTvs
collect_cand_qtvs_co TcKind
orig_ty (CoVarSet
bound CoVarSet -> TyVar -> CoVarSet
`extendVarSet` TyVar
tcv) CandidatesQTvs
dv1 Coercion
co }
go_mco :: CandidatesQTvs -> MCoercionN -> TcM CandidatesQTvs
go_mco CandidatesQTvs
dv MCoercionN
MRefl = CandidatesQTvs -> TcM CandidatesQTvs
forall (m :: * -> *) a. Monad m => a -> m a
return CandidatesQTvs
dv
go_mco CandidatesQTvs
dv (MCo Coercion
co) = CandidatesQTvs -> Coercion -> TcM CandidatesQTvs
go_co CandidatesQTvs
dv Coercion
co
go_prov :: CandidatesQTvs -> UnivCoProvenance -> TcM CandidatesQTvs
go_prov CandidatesQTvs
dv (PhantomProv Coercion
co) = CandidatesQTvs -> Coercion -> TcM CandidatesQTvs
go_co CandidatesQTvs
dv Coercion
co
go_prov CandidatesQTvs
dv (ProofIrrelProv Coercion
co) = CandidatesQTvs -> Coercion -> TcM CandidatesQTvs
go_co CandidatesQTvs
dv Coercion
co
go_prov CandidatesQTvs
dv (PluginProv String
_) = CandidatesQTvs -> TcM CandidatesQTvs
forall (m :: * -> *) a. Monad m => a -> m a
return CandidatesQTvs
dv
go_prov CandidatesQTvs
dv (CorePrepProv Bool
_) = CandidatesQTvs -> TcM CandidatesQTvs
forall (m :: * -> *) a. Monad m => a -> m a
return CandidatesQTvs
dv
go_cv :: CandidatesQTvs -> CoVar -> TcM CandidatesQTvs
go_cv :: CandidatesQTvs -> TyVar -> TcM CandidatesQTvs
go_cv dv :: CandidatesQTvs
dv@(DV { dv_cvs :: CandidatesQTvs -> CoVarSet
dv_cvs = CoVarSet
cvs }) TyVar
cv
| TyVar -> Bool
is_bound TyVar
cv = CandidatesQTvs -> TcM CandidatesQTvs
forall (m :: * -> *) a. Monad m => a -> m a
return CandidatesQTvs
dv
| TyVar
cv TyVar -> CoVarSet -> Bool
`elemVarSet` CoVarSet
cvs = CandidatesQTvs -> TcM CandidatesQTvs
forall (m :: * -> *) a. Monad m => a -> m a
return CandidatesQTvs
dv
| Bool
otherwise = TcKind
-> Bool
-> CoVarSet
-> CandidatesQTvs
-> TcKind
-> TcM CandidatesQTvs
collect_cand_qtvs TcKind
orig_ty Bool
True CoVarSet
bound
(CandidatesQTvs
dv { dv_cvs :: CoVarSet
dv_cvs = CoVarSet
cvs CoVarSet -> TyVar -> CoVarSet
`extendVarSet` TyVar
cv })
(TyVar -> TcKind
idType TyVar
cv)
is_bound :: TyVar -> Bool
is_bound TyVar
tv = TyVar
tv TyVar -> CoVarSet -> Bool
`elemVarSet` CoVarSet
bound
quantifyTyVars :: SkolemInfo
-> NonStandardDefaultingStrategy
-> CandidatesQTvs
-> TcM [TcTyVar]
quantifyTyVars :: SkolemInfo
-> NonStandardDefaultingStrategy -> CandidatesQTvs -> TcM [TyVar]
quantifyTyVars SkolemInfo
skol_info NonStandardDefaultingStrategy
ns_strat CandidatesQTvs
dvs
| CandidatesQTvs -> Bool
isEmptyCandidates CandidatesQTvs
dvs
= do { String -> SDoc -> TcRn ()
traceTc String
"quantifyTyVars has nothing to quantify" SDoc
empty
; [TyVar] -> TcM [TyVar]
forall (m :: * -> *) a. Monad m => a -> m a
return [] }
| Bool
otherwise
= do { String -> SDoc -> TcRn ()
traceTc String
"quantifyTyVars {"
( [SDoc] -> SDoc
vcat [ String -> SDoc
text String
"ns_strat =" SDoc -> SDoc -> SDoc
<+> NonStandardDefaultingStrategy -> SDoc
forall a. Outputable a => a -> SDoc
ppr NonStandardDefaultingStrategy
ns_strat
, String -> SDoc
text String
"dvs =" SDoc -> SDoc -> SDoc
<+> CandidatesQTvs -> SDoc
forall a. Outputable a => a -> SDoc
ppr CandidatesQTvs
dvs ])
; [TyVar]
undefaulted <- NonStandardDefaultingStrategy -> CandidatesQTvs -> TcM [TyVar]
defaultTyVars NonStandardDefaultingStrategy
ns_strat CandidatesQTvs
dvs
; [TyVar]
final_qtvs <- (TyVar -> IOEnv (Env TcGblEnv TcLclEnv) (Maybe TyVar))
-> [TyVar] -> TcM [TyVar]
forall (m :: * -> *) a b.
Applicative m =>
(a -> m (Maybe b)) -> [a] -> m [b]
mapMaybeM TyVar -> IOEnv (Env TcGblEnv TcLclEnv) (Maybe TyVar)
zonk_quant [TyVar]
undefaulted
; String -> SDoc -> TcRn ()
traceTc String
"quantifyTyVars }"
([SDoc] -> SDoc
vcat [ String -> SDoc
text String
"undefaulted:" SDoc -> SDoc -> SDoc
<+> [TyVar] -> SDoc
pprTyVars [TyVar]
undefaulted
, String -> SDoc
text String
"final_qtvs:" SDoc -> SDoc -> SDoc
<+> [TyVar] -> SDoc
pprTyVars [TyVar]
final_qtvs ])
; let co_vars :: [TyVar]
co_vars = (TyVar -> Bool) -> [TyVar] -> [TyVar]
forall a. (a -> Bool) -> [a] -> [a]
filter TyVar -> Bool
isCoVar [TyVar]
final_qtvs
; Bool -> SDoc -> TcRn ()
forall (m :: * -> *).
(HasCallStack, Applicative m) =>
Bool -> SDoc -> m ()
massertPpr ([TyVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TyVar]
co_vars) ([TyVar] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TyVar]
co_vars)
; [TyVar] -> TcM [TyVar]
forall (m :: * -> *) a. Monad m => a -> m a
return [TyVar]
final_qtvs }
where
zonk_quant :: TyVar -> IOEnv (Env TcGblEnv TcLclEnv) (Maybe TyVar)
zonk_quant TyVar
tkv
| Bool -> Bool
not (TyVar -> Bool
isTyVar TyVar
tkv)
= Maybe TyVar -> IOEnv (Env TcGblEnv TcLclEnv) (Maybe TyVar)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe TyVar
forall a. Maybe a
Nothing
| Bool
otherwise
= TyVar -> Maybe TyVar
forall a. a -> Maybe a
Just (TyVar -> Maybe TyVar)
-> IOEnv (Env TcGblEnv TcLclEnv) TyVar
-> IOEnv (Env TcGblEnv TcLclEnv) (Maybe TyVar)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SkolemInfo -> TyVar -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
skolemiseQuantifiedTyVar SkolemInfo
skol_info TyVar
tkv
isQuantifiableTv :: TcLevel
-> TcTyVar
-> Bool
isQuantifiableTv :: TcLevel -> TyVar -> Bool
isQuantifiableTv TcLevel
outer_tclvl TyVar
tcv
| TyVar -> Bool
isTcTyVar TyVar
tcv
= TyVar -> TcLevel
tcTyVarLevel TyVar
tcv TcLevel -> TcLevel -> Bool
forall a. Ord a => a -> a -> Bool
> TcLevel
outer_tclvl
| Bool
otherwise
= Bool
False
zonkAndSkolemise :: SkolemInfo -> TcTyCoVar -> TcM TcTyCoVar
zonkAndSkolemise :: SkolemInfo -> TyVar -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
zonkAndSkolemise SkolemInfo
skol_info TyVar
tyvar
| TyVar -> Bool
isTyVarTyVar TyVar
tyvar
= do { TyVar
zonked_tyvar <- HasDebugCallStack => TyVar -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
TyVar -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
zonkTcTyVarToTcTyVar TyVar
tyvar
; SkolemInfo -> TyVar -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
skolemiseQuantifiedTyVar SkolemInfo
skol_info TyVar
zonked_tyvar }
| Bool
otherwise
= Bool
-> SDoc
-> IOEnv (Env TcGblEnv TcLclEnv) TyVar
-> IOEnv (Env TcGblEnv TcLclEnv) TyVar
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (TyVar -> Bool
isImmutableTyVar TyVar
tyvar Bool -> Bool -> Bool
|| TyVar -> Bool
isCoVar TyVar
tyvar) (TyVar -> SDoc
pprTyVar TyVar
tyvar) (IOEnv (Env TcGblEnv TcLclEnv) TyVar
-> IOEnv (Env TcGblEnv TcLclEnv) TyVar)
-> IOEnv (Env TcGblEnv TcLclEnv) TyVar
-> IOEnv (Env TcGblEnv TcLclEnv) TyVar
forall a b. (a -> b) -> a -> b
$
TyVar -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
zonkTyCoVarKind TyVar
tyvar
skolemiseQuantifiedTyVar :: SkolemInfo -> TcTyVar -> TcM TcTyVar
skolemiseQuantifiedTyVar :: SkolemInfo -> TyVar -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
skolemiseQuantifiedTyVar SkolemInfo
skol_info TyVar
tv
= case TyVar -> TcTyVarDetails
tcTyVarDetails TyVar
tv of
SkolemTv {} -> do { TcKind
kind <- TcKind -> TcM TcKind
zonkTcType (TyVar -> TcKind
tyVarKind TyVar
tv)
; TyVar -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
forall (m :: * -> *) a. Monad m => a -> m a
return (TyVar -> TcKind -> TyVar
setTyVarKind TyVar
tv TcKind
kind) }
MetaTv {} -> SkolemInfo -> TyVar -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
skolemiseUnboundMetaTyVar SkolemInfo
skol_info TyVar
tv
TcTyVarDetails
_other -> String -> SDoc -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"skolemiseQuantifiedTyVar" (TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
tv)
defaultTyVar :: DefaultingStrategy
-> TcTyVar
-> TcM Bool
defaultTyVar :: DefaultingStrategy -> TyVar -> TcRnIf TcGblEnv TcLclEnv Bool
defaultTyVar DefaultingStrategy
def_strat TyVar
tv
| Bool -> Bool
not (TyVar -> Bool
isMetaTyVar TyVar
tv)
= Bool -> TcRnIf TcGblEnv TcLclEnv Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
| TyVar -> Bool
isTyVarTyVar TyVar
tv
= Bool -> TcRnIf TcGblEnv TcLclEnv Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
| TyVar -> Bool
isRuntimeRepVar TyVar
tv
, Bool
default_ns_vars
= do { String -> SDoc -> TcRn ()
traceTc String
"Defaulting a RuntimeRep var to LiftedRep" (TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
tv)
; TyVar -> TcKind -> TcRn ()
writeMetaTyVar TyVar
tv TcKind
liftedRepTy
; Bool -> TcRnIf TcGblEnv TcLclEnv Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True }
| TyVar -> Bool
isLevityVar TyVar
tv
, Bool
default_ns_vars
= do { String -> SDoc -> TcRn ()
traceTc String
"Defaulting a Levity var to Lifted" (TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
tv)
; TyVar -> TcKind -> TcRn ()
writeMetaTyVar TyVar
tv TcKind
liftedDataConTy
; Bool -> TcRnIf TcGblEnv TcLclEnv Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True }
| TyVar -> Bool
isMultiplicityVar TyVar
tv
, Bool
default_ns_vars
= do { String -> SDoc -> TcRn ()
traceTc String
"Defaulting a Multiplicity var to Many" (TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
tv)
; TyVar -> TcKind -> TcRn ()
writeMetaTyVar TyVar
tv TcKind
manyDataConTy
; Bool -> TcRnIf TcGblEnv TcLclEnv Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True }
| DefaultingStrategy
DefaultKindVars <- DefaultingStrategy
def_strat
= TyVar -> TcRnIf TcGblEnv TcLclEnv Bool
default_kind_var TyVar
tv
| Bool
otherwise
= Bool -> TcRnIf TcGblEnv TcLclEnv Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
where
default_ns_vars :: Bool
default_ns_vars :: Bool
default_ns_vars = DefaultingStrategy -> Bool
defaultNonStandardTyVars DefaultingStrategy
def_strat
default_kind_var :: TyVar -> TcM Bool
default_kind_var :: TyVar -> TcRnIf TcGblEnv TcLclEnv Bool
default_kind_var TyVar
kv
| TcKind -> Bool
isLiftedTypeKind (TyVar -> TcKind
tyVarKind TyVar
kv)
= do { String -> SDoc -> TcRn ()
traceTc String
"Defaulting a kind var to *" (TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
kv)
; TyVar -> TcKind -> TcRn ()
writeMetaTyVar TyVar
kv TcKind
liftedTypeKind
; Bool -> TcRnIf TcGblEnv TcLclEnv Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True }
| Bool
otherwise
= do { TcRnMessage -> TcRn ()
addErr (TcRnMessage -> TcRn ()) -> TcRnMessage -> TcRn ()
forall a b. (a -> b) -> a -> b
$ DiagnosticMessage -> TcRnMessage
forall a. (Diagnostic a, Typeable a) => a -> TcRnMessage
TcRnUnknownMessage (DiagnosticMessage -> TcRnMessage)
-> DiagnosticMessage -> TcRnMessage
forall a b. (a -> b) -> a -> b
$ [GhcHint] -> SDoc -> DiagnosticMessage
mkPlainError [GhcHint]
noHints (SDoc -> DiagnosticMessage) -> SDoc -> DiagnosticMessage
forall a b. (a -> b) -> a -> b
$
([SDoc] -> SDoc
vcat [ String -> SDoc
text String
"Cannot default kind variable" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
kv')
, String -> SDoc
text String
"of kind:" SDoc -> SDoc -> SDoc
<+> TcKind -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TyVar -> TcKind
tyVarKind TyVar
kv')
, String -> SDoc
text String
"Perhaps enable PolyKinds or add a kind signature" ])
; Bool -> TcRnIf TcGblEnv TcLclEnv Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
}
where
(TidyEnv
_, TyVar
kv') = TidyEnv -> TyVar -> (TidyEnv, TyVar)
tidyOpenTyCoVar TidyEnv
emptyTidyEnv TyVar
kv
defaultTyVars :: NonStandardDefaultingStrategy
-> CandidatesQTvs
-> TcM [TcTyVar]
defaultTyVars :: NonStandardDefaultingStrategy -> CandidatesQTvs -> TcM [TyVar]
defaultTyVars NonStandardDefaultingStrategy
ns_strat CandidatesQTvs
dvs
= do { Bool
poly_kinds <- Extension -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. Extension -> TcRnIf gbl lcl Bool
xoptM Extension
LangExt.PolyKinds
; let
def_tvs, def_kvs :: DefaultingStrategy
def_tvs :: DefaultingStrategy
def_tvs = NonStandardDefaultingStrategy -> DefaultingStrategy
NonStandardDefaulting NonStandardDefaultingStrategy
ns_strat
def_kvs :: DefaultingStrategy
def_kvs
| Bool
poly_kinds = DefaultingStrategy
def_tvs
| Bool
otherwise = DefaultingStrategy
DefaultKindVars
; [Bool]
defaulted_kvs <- (TyVar -> TcRnIf TcGblEnv TcLclEnv Bool)
-> [TyVar] -> IOEnv (Env TcGblEnv TcLclEnv) [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (DefaultingStrategy -> TyVar -> TcRnIf TcGblEnv TcLclEnv Bool
defaultTyVar DefaultingStrategy
def_kvs) [TyVar]
dep_kvs
; [Bool]
defaulted_tvs <- (TyVar -> TcRnIf TcGblEnv TcLclEnv Bool)
-> [TyVar] -> IOEnv (Env TcGblEnv TcLclEnv) [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (DefaultingStrategy -> TyVar -> TcRnIf TcGblEnv TcLclEnv Bool
defaultTyVar DefaultingStrategy
def_tvs) [TyVar]
nondep_tvs
; let undefaulted_kvs :: [TyVar]
undefaulted_kvs = [ TyVar
kv | (TyVar
kv, Bool
False) <- [TyVar]
dep_kvs [TyVar] -> [Bool] -> [(TyVar, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [Bool]
defaulted_kvs ]
undefaulted_tvs :: [TyVar]
undefaulted_tvs = [ TyVar
tv | (TyVar
tv, Bool
False) <- [TyVar]
nondep_tvs [TyVar] -> [Bool] -> [(TyVar, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [Bool]
defaulted_tvs ]
; [TyVar] -> TcM [TyVar]
forall (m :: * -> *) a. Monad m => a -> m a
return ([TyVar]
undefaulted_kvs [TyVar] -> [TyVar] -> [TyVar]
forall a. [a] -> [a] -> [a]
++ [TyVar]
undefaulted_tvs) }
where
([TyVar]
dep_kvs, [TyVar]
nondep_tvs) = CandidatesQTvs -> ([TyVar], [TyVar])
candidateVars CandidatesQTvs
dvs
skolemiseUnboundMetaTyVar :: SkolemInfo -> TcTyVar -> TcM TyVar
skolemiseUnboundMetaTyVar :: SkolemInfo -> TyVar -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
skolemiseUnboundMetaTyVar SkolemInfo
skol_info TyVar
tv
= Bool
-> SDoc
-> IOEnv (Env TcGblEnv TcLclEnv) TyVar
-> IOEnv (Env TcGblEnv TcLclEnv) TyVar
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (TyVar -> Bool
isMetaTyVar TyVar
tv) (TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
tv) (IOEnv (Env TcGblEnv TcLclEnv) TyVar
-> IOEnv (Env TcGblEnv TcLclEnv) TyVar)
-> IOEnv (Env TcGblEnv TcLclEnv) TyVar
-> IOEnv (Env TcGblEnv TcLclEnv) TyVar
forall a b. (a -> b) -> a -> b
$
do { TyVar -> TcRn ()
check_empty TyVar
tv
; TcLevel
tc_lvl <- TcM TcLevel
getTcLevel
; SrcSpan
here <- TcRn SrcSpan
getSrcSpanM
; TcKind
kind <- TcKind -> TcM TcKind
zonkTcType (TyVar -> TcKind
tyVarKind TyVar
tv)
; let tv_name :: Name
tv_name = TyVar -> Name
tyVarName TyVar
tv
final_name :: Name
final_name | Name -> Bool
isSystemName Name
tv_name
= Unique -> OccName -> SrcSpan -> Name
mkInternalName (Name -> Unique
nameUnique Name
tv_name)
(Name -> OccName
nameOccName Name
tv_name) SrcSpan
here
| Bool
otherwise
= Name
tv_name
details :: TcTyVarDetails
details = SkolemInfo -> TcLevel -> Bool -> TcTyVarDetails
SkolemTv SkolemInfo
skol_info (TcLevel -> TcLevel
pushTcLevel TcLevel
tc_lvl) Bool
False
final_tv :: TyVar
final_tv = Name -> TcKind -> TcTyVarDetails -> TyVar
mkTcTyVar Name
final_name TcKind
kind TcTyVarDetails
details
; String -> SDoc -> TcRn ()
traceTc String
"Skolemising" (TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
tv SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
":=" SDoc -> SDoc -> SDoc
<+> TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
final_tv)
; TyVar -> TcKind -> TcRn ()
writeMetaTyVar TyVar
tv (TyVar -> TcKind
mkTyVarTy TyVar
final_tv)
; TyVar -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
forall (m :: * -> *) a. Monad m => a -> m a
return TyVar
final_tv }
where
check_empty :: TyVar -> TcRn ()
check_empty TyVar
tv
= Bool -> TcRn () -> TcRn ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
debugIsOn (TcRn () -> TcRn ()) -> TcRn () -> TcRn ()
forall a b. (a -> b) -> a -> b
$
do { MetaDetails
cts <- TyVar -> TcM MetaDetails
readMetaTyVar TyVar
tv
; case MetaDetails
cts of
MetaDetails
Flexi -> () -> TcRn ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Indirect TcKind
ty -> Bool -> String -> SDoc -> TcRn () -> TcRn ()
forall a. HasCallStack => Bool -> String -> SDoc -> a -> a
warnPprTrace Bool
True String
"skolemiseUnboundMetaTyVar" (TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
tv SDoc -> SDoc -> SDoc
$$ TcKind -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcKind
ty) (TcRn () -> TcRn ()) -> TcRn () -> TcRn ()
forall a b. (a -> b) -> a -> b
$
() -> TcRn ()
forall (m :: * -> *) a. Monad m => a -> m a
return () }
doNotQuantifyTyVars :: CandidatesQTvs
-> (TidyEnv -> TcM (TidyEnv, SDoc))
-> TcM ()
doNotQuantifyTyVars :: CandidatesQTvs -> (TidyEnv -> TcM (TidyEnv, SDoc)) -> TcRn ()
doNotQuantifyTyVars CandidatesQTvs
dvs TidyEnv -> TcM (TidyEnv, SDoc)
where_found
| CandidatesQTvs -> Bool
isEmptyCandidates CandidatesQTvs
dvs
= String -> SDoc -> TcRn ()
traceTc String
"doNotQuantifyTyVars has nothing to error on" SDoc
empty
| Bool
otherwise
= do { String -> SDoc -> TcRn ()
traceTc String
"doNotQuantifyTyVars" (CandidatesQTvs -> SDoc
forall a. Outputable a => a -> SDoc
ppr CandidatesQTvs
dvs)
; [TyVar]
undefaulted <- NonStandardDefaultingStrategy -> CandidatesQTvs -> TcM [TyVar]
defaultTyVars NonStandardDefaultingStrategy
DefaultNonStandardTyVars CandidatesQTvs
dvs
; let leftover_metas :: [TyVar]
leftover_metas = (TyVar -> Bool) -> [TyVar] -> [TyVar]
forall a. (a -> Bool) -> [a] -> [a]
filter TyVar -> Bool
isMetaTyVar [TyVar]
undefaulted
; Bool -> TcRn () -> TcRn ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([TyVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TyVar]
leftover_metas) (TcRn () -> TcRn ()) -> TcRn () -> TcRn ()
forall a b. (a -> b) -> a -> b
$
do { let (TidyEnv
tidy_env1, [TyVar]
tidied_tvs) = TidyEnv -> [TyVar] -> (TidyEnv, [TyVar])
tidyOpenTyCoVars TidyEnv
emptyTidyEnv [TyVar]
leftover_metas
; (TidyEnv
tidy_env2, SDoc
where_doc) <- TidyEnv -> TcM (TidyEnv, SDoc)
where_found TidyEnv
tidy_env1
; let msg :: TcRnMessage
msg = DiagnosticMessage -> TcRnMessage
forall a. (Diagnostic a, Typeable a) => a -> TcRnMessage
TcRnUnknownMessage (DiagnosticMessage -> TcRnMessage)
-> DiagnosticMessage -> TcRnMessage
forall a b. (a -> b) -> a -> b
$ [GhcHint] -> SDoc -> DiagnosticMessage
mkPlainError [GhcHint]
noHints (SDoc -> DiagnosticMessage) -> SDoc -> DiagnosticMessage
forall a b. (a -> b) -> a -> b
$ Bool -> SDoc -> SDoc
pprWithExplicitKindsWhen Bool
True (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
vcat [ String -> SDoc
text String
"Uninferrable type variable"
SDoc -> SDoc -> SDoc
<> [TyVar] -> SDoc
forall a. [a] -> SDoc
plural [TyVar]
tidied_tvs
SDoc -> SDoc -> SDoc
<+> (TyVar -> SDoc) -> [TyVar] -> SDoc
forall a. (a -> SDoc) -> [a] -> SDoc
pprWithCommas TyVar -> SDoc
pprTyVar [TyVar]
tidied_tvs
SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"in"
, SDoc
where_doc ]
; (TidyEnv, TcRnMessage) -> TcRn ()
forall a. (TidyEnv, TcRnMessage) -> TcM a
failWithTcM (TidyEnv
tidy_env2, TcRnMessage
msg) }
; String -> SDoc -> TcRn ()
traceTc String
"doNotQuantifyTyVars success" SDoc
empty }
promoteMetaTyVarTo :: TcLevel -> TcTyVar -> TcM Bool
promoteMetaTyVarTo :: TcLevel -> TyVar -> TcRnIf TcGblEnv TcLclEnv Bool
promoteMetaTyVarTo TcLevel
tclvl TyVar
tv
| Bool -> SDoc -> Bool -> Bool
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (TyVar -> Bool
isMetaTyVar TyVar
tv) (TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
tv) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
TyVar -> TcLevel
tcTyVarLevel TyVar
tv TcLevel -> TcLevel -> Bool
`strictlyDeeperThan` TcLevel
tclvl
= do { TyVar
cloned_tv <- TyVar -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
cloneMetaTyVar TyVar
tv
; let rhs_tv :: TyVar
rhs_tv = TyVar -> TcLevel -> TyVar
setMetaTyVarTcLevel TyVar
cloned_tv TcLevel
tclvl
; TyVar -> TcKind -> TcRn ()
writeMetaTyVar TyVar
tv (TyVar -> TcKind
mkTyVarTy TyVar
rhs_tv)
; String -> SDoc -> TcRn ()
traceTc String
"promoteTyVar" (TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
tv SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"-->" SDoc -> SDoc -> SDoc
<+> TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
rhs_tv)
; Bool -> TcRnIf TcGblEnv TcLclEnv Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True }
| Bool
otherwise
= Bool -> TcRnIf TcGblEnv TcLclEnv Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
promoteTyVarSet :: TcTyVarSet -> TcM Bool
promoteTyVarSet :: CoVarSet -> TcRnIf TcGblEnv TcLclEnv Bool
promoteTyVarSet CoVarSet
tvs
= do { TcLevel
tclvl <- TcM TcLevel
getTcLevel
; [Bool]
bools <- (TyVar -> TcRnIf TcGblEnv TcLclEnv Bool)
-> [TyVar] -> IOEnv (Env TcGblEnv TcLclEnv) [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (TcLevel -> TyVar -> TcRnIf TcGblEnv TcLclEnv Bool
promoteMetaTyVarTo TcLevel
tclvl) ([TyVar] -> IOEnv (Env TcGblEnv TcLclEnv) [Bool])
-> [TyVar] -> IOEnv (Env TcGblEnv TcLclEnv) [Bool]
forall a b. (a -> b) -> a -> b
$
(TyVar -> Bool) -> [TyVar] -> [TyVar]
forall a. (a -> Bool) -> [a] -> [a]
filter TyVar -> Bool
isPromotableMetaTyVar ([TyVar] -> [TyVar]) -> [TyVar] -> [TyVar]
forall a b. (a -> b) -> a -> b
$
CoVarSet -> [TyVar]
forall elt. UniqSet elt -> [elt]
nonDetEltsUniqSet CoVarSet
tvs
; Bool -> TcRnIf TcGblEnv TcLclEnv Bool
forall (m :: * -> *) a. Monad m => a -> m a
return ([Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [Bool]
bools) }
zonkTcTypeAndFV :: TcType -> TcM DTyCoVarSet
zonkTcTypeAndFV :: TcKind -> TcM DTyVarSet
zonkTcTypeAndFV TcKind
ty
= TcKind -> DTyVarSet
tyCoVarsOfTypeDSet (TcKind -> DTyVarSet) -> TcM TcKind -> TcM DTyVarSet
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcKind -> TcM TcKind
zonkTcType TcKind
ty
zonkTyCoVar :: TyCoVar -> TcM TcType
zonkTyCoVar :: TyVar -> TcM TcKind
zonkTyCoVar TyVar
tv | TyVar -> Bool
isTcTyVar TyVar
tv = TyVar -> TcM TcKind
zonkTcTyVar TyVar
tv
| TyVar -> Bool
isTyVar TyVar
tv = TyVar -> TcKind
mkTyVarTy (TyVar -> TcKind)
-> IOEnv (Env TcGblEnv TcLclEnv) TyVar -> TcM TcKind
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyVar -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
zonkTyCoVarKind TyVar
tv
| Bool
otherwise = Bool -> SDoc -> TcM TcKind -> TcM TcKind
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (TyVar -> Bool
isCoVar TyVar
tv) (TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
tv) (TcM TcKind -> TcM TcKind) -> TcM TcKind -> TcM TcKind
forall a b. (a -> b) -> a -> b
$
Coercion -> TcKind
mkCoercionTy (Coercion -> TcKind) -> (TyVar -> Coercion) -> TyVar -> TcKind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVar -> Coercion
mkCoVarCo (TyVar -> TcKind)
-> IOEnv (Env TcGblEnv TcLclEnv) TyVar -> TcM TcKind
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyVar -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
zonkTyCoVarKind TyVar
tv
zonkTyCoVarsAndFV :: TyCoVarSet -> TcM TyCoVarSet
zonkTyCoVarsAndFV :: CoVarSet -> TcM CoVarSet
zonkTyCoVarsAndFV CoVarSet
tycovars
= [TcKind] -> CoVarSet
tyCoVarsOfTypes ([TcKind] -> CoVarSet) -> TcM [TcKind] -> TcM CoVarSet
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TyVar -> TcM TcKind) -> [TyVar] -> TcM [TcKind]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM TyVar -> TcM TcKind
zonkTyCoVar (CoVarSet -> [TyVar]
forall elt. UniqSet elt -> [elt]
nonDetEltsUniqSet CoVarSet
tycovars)
zonkDTyCoVarSetAndFV :: DTyCoVarSet -> TcM DTyCoVarSet
zonkDTyCoVarSetAndFV :: DTyVarSet -> TcM DTyVarSet
zonkDTyCoVarSetAndFV DTyVarSet
tycovars
= [TyVar] -> DTyVarSet
mkDVarSet ([TyVar] -> DTyVarSet) -> TcM [TyVar] -> TcM DTyVarSet
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([TyVar] -> TcM [TyVar]
zonkTyCoVarsAndFVList ([TyVar] -> TcM [TyVar]) -> [TyVar] -> TcM [TyVar]
forall a b. (a -> b) -> a -> b
$ DTyVarSet -> [TyVar]
dVarSetElems DTyVarSet
tycovars)
zonkTyCoVarsAndFVList :: [TyCoVar] -> TcM [TyCoVar]
zonkTyCoVarsAndFVList :: [TyVar] -> TcM [TyVar]
zonkTyCoVarsAndFVList [TyVar]
tycovars
= [TcKind] -> [TyVar]
tyCoVarsOfTypesList ([TcKind] -> [TyVar]) -> TcM [TcKind] -> TcM [TyVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TyVar -> TcM TcKind) -> [TyVar] -> TcM [TcKind]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM TyVar -> TcM TcKind
zonkTyCoVar [TyVar]
tycovars
zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
zonkTcTyVars :: [TyVar] -> TcM [TcKind]
zonkTcTyVars [TyVar]
tyvars = (TyVar -> TcM TcKind) -> [TyVar] -> TcM [TcKind]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM TyVar -> TcM TcKind
zonkTcTyVar [TyVar]
tyvars
zonkTyCoVarKind :: TyCoVar -> TcM TyCoVar
zonkTyCoVarKind :: TyVar -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
zonkTyCoVarKind TyVar
tv = do { TcKind
kind' <- TcKind -> TcM TcKind
zonkTcType (TyVar -> TcKind
tyVarKind TyVar
tv)
; TyVar -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
forall (m :: * -> *) a. Monad m => a -> m a
return (TyVar -> TcKind -> TyVar
setTyVarKind TyVar
tv TcKind
kind') }
zonkImplication :: Implication -> TcM Implication
zonkImplication :: Implication -> IOEnv (Env TcGblEnv TcLclEnv) Implication
zonkImplication implic :: Implication
implic@(Implic { ic_skols :: Implication -> [TyVar]
ic_skols = [TyVar]
skols
, ic_given :: Implication -> [TyVar]
ic_given = [TyVar]
given
, ic_wanted :: Implication -> WantedConstraints
ic_wanted = WantedConstraints
wanted
, ic_info :: Implication -> SkolemInfoAnon
ic_info = SkolemInfoAnon
info })
= do { [TyVar]
skols' <- (TyVar -> IOEnv (Env TcGblEnv TcLclEnv) TyVar)
-> [TyVar] -> TcM [TyVar]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM TyVar -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
zonkTyCoVarKind [TyVar]
skols
; [TyVar]
given' <- (TyVar -> IOEnv (Env TcGblEnv TcLclEnv) TyVar)
-> [TyVar] -> TcM [TyVar]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM TyVar -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
zonkEvVar [TyVar]
given
; SkolemInfoAnon
info' <- SkolemInfoAnon -> TcM SkolemInfoAnon
zonkSkolemInfoAnon SkolemInfoAnon
info
; WantedConstraints
wanted' <- WantedConstraints -> TcM WantedConstraints
zonkWCRec WantedConstraints
wanted
; Implication -> IOEnv (Env TcGblEnv TcLclEnv) Implication
forall (m :: * -> *) a. Monad m => a -> m a
return (Implication
implic { ic_skols :: [TyVar]
ic_skols = [TyVar]
skols'
, ic_given :: [TyVar]
ic_given = [TyVar]
given'
, ic_wanted :: WantedConstraints
ic_wanted = WantedConstraints
wanted'
, ic_info :: SkolemInfoAnon
ic_info = SkolemInfoAnon
info' }) }
zonkEvVar :: EvVar -> TcM EvVar
zonkEvVar :: TyVar -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
zonkEvVar TyVar
var = (TcKind -> TcM TcKind)
-> TyVar -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
forall (m :: * -> *).
Monad m =>
(TcKind -> m TcKind) -> TyVar -> m TyVar
updateIdTypeAndMultM TcKind -> TcM TcKind
zonkTcType TyVar
var
zonkWC :: WantedConstraints -> TcM WantedConstraints
zonkWC :: WantedConstraints -> TcM WantedConstraints
zonkWC WantedConstraints
wc = WantedConstraints -> TcM WantedConstraints
zonkWCRec WantedConstraints
wc
zonkWCRec :: WantedConstraints -> TcM WantedConstraints
zonkWCRec :: WantedConstraints -> TcM WantedConstraints
zonkWCRec (WC { wc_simple :: WantedConstraints -> Cts
wc_simple = Cts
simple, wc_impl :: WantedConstraints -> Bag Implication
wc_impl = Bag Implication
implic, wc_holes :: WantedConstraints -> Bag Hole
wc_holes = Bag Hole
holes })
= do { Cts
simple' <- Cts -> IOEnv (Env TcGblEnv TcLclEnv) Cts
zonkSimples Cts
simple
; Bag Implication
implic' <- (Implication -> IOEnv (Env TcGblEnv TcLclEnv) Implication)
-> Bag Implication
-> IOEnv (Env TcGblEnv TcLclEnv) (Bag Implication)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Bag a -> m (Bag b)
mapBagM Implication -> IOEnv (Env TcGblEnv TcLclEnv) Implication
zonkImplication Bag Implication
implic
; Bag Hole
holes' <- (Hole -> IOEnv (Env TcGblEnv TcLclEnv) Hole)
-> Bag Hole -> IOEnv (Env TcGblEnv TcLclEnv) (Bag Hole)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Bag a -> m (Bag b)
mapBagM Hole -> IOEnv (Env TcGblEnv TcLclEnv) Hole
zonkHole Bag Hole
holes
; WantedConstraints -> TcM WantedConstraints
forall (m :: * -> *) a. Monad m => a -> m a
return (WC :: Cts -> Bag Implication -> Bag Hole -> WantedConstraints
WC { wc_simple :: Cts
wc_simple = Cts
simple', wc_impl :: Bag Implication
wc_impl = Bag Implication
implic', wc_holes :: Bag Hole
wc_holes = Bag Hole
holes' }) }
zonkSimples :: Cts -> TcM Cts
zonkSimples :: Cts -> IOEnv (Env TcGblEnv TcLclEnv) Cts
zonkSimples Cts
cts = do { Cts
cts' <- (Ct -> TcM Ct) -> Cts -> IOEnv (Env TcGblEnv TcLclEnv) Cts
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Bag a -> m (Bag b)
mapBagM Ct -> TcM Ct
zonkCt Cts
cts
; String -> SDoc -> TcRn ()
traceTc String
"zonkSimples done:" (Cts -> SDoc
forall a. Outputable a => a -> SDoc
ppr Cts
cts')
; Cts -> IOEnv (Env TcGblEnv TcLclEnv) Cts
forall (m :: * -> *) a. Monad m => a -> m a
return Cts
cts' }
zonkHole :: Hole -> TcM Hole
zonkHole :: Hole -> IOEnv (Env TcGblEnv TcLclEnv) Hole
zonkHole hole :: Hole
hole@(Hole { hole_ty :: Hole -> TcKind
hole_ty = TcKind
ty })
= do { TcKind
ty' <- TcKind -> TcM TcKind
zonkTcType TcKind
ty
; Hole -> IOEnv (Env TcGblEnv TcLclEnv) Hole
forall (m :: * -> *) a. Monad m => a -> m a
return (Hole
hole { hole_ty :: TcKind
hole_ty = TcKind
ty' }) }
zonkCt :: Ct -> TcM Ct
zonkCt :: Ct -> TcM Ct
zonkCt ct :: Ct
ct@(CDictCan { cc_ev :: Ct -> CtEvidence
cc_ev = CtEvidence
ev, cc_tyargs :: Ct -> [TcKind]
cc_tyargs = [TcKind]
args })
= do { CtEvidence
ev' <- CtEvidence -> TcM CtEvidence
zonkCtEvidence CtEvidence
ev
; [TcKind]
args' <- (TcKind -> TcM TcKind) -> [TcKind] -> TcM [TcKind]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM TcKind -> TcM TcKind
zonkTcType [TcKind]
args
; Ct -> TcM Ct
forall (m :: * -> *) a. Monad m => a -> m a
return (Ct -> TcM Ct) -> Ct -> TcM Ct
forall a b. (a -> b) -> a -> b
$ Ct
ct { cc_ev :: CtEvidence
cc_ev = CtEvidence
ev', cc_tyargs :: [TcKind]
cc_tyargs = [TcKind]
args' } }
zonkCt (CEqCan { cc_ev :: Ct -> CtEvidence
cc_ev = CtEvidence
ev })
= CtEvidence -> Ct
mkNonCanonical (CtEvidence -> Ct) -> TcM CtEvidence -> TcM Ct
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CtEvidence -> TcM CtEvidence
zonkCtEvidence CtEvidence
ev
zonkCt ct :: Ct
ct@(CIrredCan { cc_ev :: Ct -> CtEvidence
cc_ev = CtEvidence
ev })
= do { CtEvidence
ev' <- CtEvidence -> TcM CtEvidence
zonkCtEvidence CtEvidence
ev
; Ct -> TcM Ct
forall (m :: * -> *) a. Monad m => a -> m a
return (Ct
ct { cc_ev :: CtEvidence
cc_ev = CtEvidence
ev' }) }
zonkCt Ct
ct
= do { CtEvidence
fl' <- CtEvidence -> TcM CtEvidence
zonkCtEvidence (Ct -> CtEvidence
ctEvidence Ct
ct)
; Ct -> TcM Ct
forall (m :: * -> *) a. Monad m => a -> m a
return (CtEvidence -> Ct
mkNonCanonical CtEvidence
fl') }
zonkCtEvidence :: CtEvidence -> TcM CtEvidence
zonkCtEvidence :: CtEvidence -> TcM CtEvidence
zonkCtEvidence CtEvidence
ctev
= do { TcKind
pred' <- TcKind -> TcM TcKind
zonkTcType (CtEvidence -> TcKind
ctev_pred CtEvidence
ctev)
; CtEvidence -> TcM CtEvidence
forall (m :: * -> *) a. Monad m => a -> m a
return (HasDebugCallStack => CtEvidence -> TcKind -> CtEvidence
CtEvidence -> TcKind -> CtEvidence
setCtEvPredType CtEvidence
ctev TcKind
pred')
}
zonkSkolemInfo :: SkolemInfo -> TcM SkolemInfo
zonkSkolemInfo :: SkolemInfo -> TcM SkolemInfo
zonkSkolemInfo (SkolemInfo Unique
u SkolemInfoAnon
sk) = Unique -> SkolemInfoAnon -> SkolemInfo
SkolemInfo Unique
u (SkolemInfoAnon -> SkolemInfo)
-> TcM SkolemInfoAnon -> TcM SkolemInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SkolemInfoAnon -> TcM SkolemInfoAnon
zonkSkolemInfoAnon SkolemInfoAnon
sk
zonkSkolemInfoAnon :: SkolemInfoAnon -> TcM SkolemInfoAnon
zonkSkolemInfoAnon :: SkolemInfoAnon -> TcM SkolemInfoAnon
zonkSkolemInfoAnon (SigSkol UserTypeCtxt
cx TcKind
ty [(Name, TyVar)]
tv_prs) = do { TcKind
ty' <- TcKind -> TcM TcKind
zonkTcType TcKind
ty
; SkolemInfoAnon -> TcM SkolemInfoAnon
forall (m :: * -> *) a. Monad m => a -> m a
return (UserTypeCtxt -> TcKind -> [(Name, TyVar)] -> SkolemInfoAnon
SigSkol UserTypeCtxt
cx TcKind
ty' [(Name, TyVar)]
tv_prs) }
zonkSkolemInfoAnon (InferSkol [(Name, TcKind)]
ntys) = do { [(Name, TcKind)]
ntys' <- ((Name, TcKind) -> IOEnv (Env TcGblEnv TcLclEnv) (Name, TcKind))
-> [(Name, TcKind)]
-> IOEnv (Env TcGblEnv TcLclEnv) [(Name, TcKind)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Name, TcKind) -> IOEnv (Env TcGblEnv TcLclEnv) (Name, TcKind)
forall a. (a, TcKind) -> IOEnv (Env TcGblEnv TcLclEnv) (a, TcKind)
do_one [(Name, TcKind)]
ntys
; SkolemInfoAnon -> TcM SkolemInfoAnon
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Name, TcKind)] -> SkolemInfoAnon
InferSkol [(Name, TcKind)]
ntys') }
where
do_one :: (a, TcKind) -> IOEnv (Env TcGblEnv TcLclEnv) (a, TcKind)
do_one (a
n, TcKind
ty) = do { TcKind
ty' <- TcKind -> TcM TcKind
zonkTcType TcKind
ty; (a, TcKind) -> IOEnv (Env TcGblEnv TcLclEnv) (a, TcKind)
forall (m :: * -> *) a. Monad m => a -> m a
return (a
n, TcKind
ty') }
zonkSkolemInfoAnon SkolemInfoAnon
skol_info = SkolemInfoAnon -> TcM SkolemInfoAnon
forall (m :: * -> *) a. Monad m => a -> m a
return SkolemInfoAnon
skol_info
zonkTcType :: TcType -> TcM TcType
zonkTcTypes :: [TcType] -> TcM [TcType]
zonkCo :: Coercion -> TcM Coercion
(TcKind -> TcM TcKind
zonkTcType, [TcKind] -> TcM [TcKind]
zonkTcTypes, Coercion -> IOEnv (Env TcGblEnv TcLclEnv) Coercion
zonkCo, [Coercion] -> TcM [Coercion]
_)
= TyCoMapper () TcM
-> (TcKind -> TcM TcKind, [TcKind] -> TcM [TcKind],
Coercion -> IOEnv (Env TcGblEnv TcLclEnv) Coercion,
[Coercion] -> TcM [Coercion])
forall (m :: * -> *).
Monad m =>
TyCoMapper () m
-> (TcKind -> m TcKind, [TcKind] -> m [TcKind],
Coercion -> m Coercion, [Coercion] -> m [Coercion])
mapTyCo TyCoMapper () TcM
zonkTcTypeMapper
zonkTcTypeMapper :: TyCoMapper () TcM
zonkTcTypeMapper :: TyCoMapper () TcM
zonkTcTypeMapper = TyCoMapper :: forall env (m :: * -> *).
(env -> TyVar -> m TcKind)
-> (env -> TyVar -> m Coercion)
-> (env -> CoercionHole -> m Coercion)
-> (env -> TyVar -> ArgFlag -> m (env, TyVar))
-> (TyCon -> m TyCon)
-> TyCoMapper env m
TyCoMapper
{ tcm_tyvar :: () -> TyVar -> TcM TcKind
tcm_tyvar = (TyVar -> TcM TcKind) -> () -> TyVar -> TcM TcKind
forall a b. a -> b -> a
const TyVar -> TcM TcKind
zonkTcTyVar
, tcm_covar :: () -> TyVar -> IOEnv (Env TcGblEnv TcLclEnv) Coercion
tcm_covar = (TyVar -> IOEnv (Env TcGblEnv TcLclEnv) Coercion)
-> () -> TyVar -> IOEnv (Env TcGblEnv TcLclEnv) Coercion
forall a b. a -> b -> a
const (\TyVar
cv -> TyVar -> Coercion
mkCoVarCo (TyVar -> Coercion)
-> IOEnv (Env TcGblEnv TcLclEnv) TyVar
-> IOEnv (Env TcGblEnv TcLclEnv) Coercion
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyVar -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
zonkTyCoVarKind TyVar
cv)
, tcm_hole :: () -> CoercionHole -> IOEnv (Env TcGblEnv TcLclEnv) Coercion
tcm_hole = () -> CoercionHole -> IOEnv (Env TcGblEnv TcLclEnv) Coercion
hole
, tcm_tycobinder :: () -> TyVar -> ArgFlag -> TcM ((), TyVar)
tcm_tycobinder = \()
_env TyVar
tv ArgFlag
_vis -> ((), ) (TyVar -> ((), TyVar))
-> IOEnv (Env TcGblEnv TcLclEnv) TyVar -> TcM ((), TyVar)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyVar -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
zonkTyCoVarKind TyVar
tv
, tcm_tycon :: TyCon -> TcM TyCon
tcm_tycon = TyCon -> TcM TyCon
zonkTcTyCon }
where
hole :: () -> CoercionHole -> TcM Coercion
hole :: () -> CoercionHole -> IOEnv (Env TcGblEnv TcLclEnv) Coercion
hole ()
_ hole :: CoercionHole
hole@(CoercionHole { ch_ref :: CoercionHole -> IORef (Maybe Coercion)
ch_ref = IORef (Maybe Coercion)
ref, ch_co_var :: CoercionHole -> TyVar
ch_co_var = TyVar
cv })
= do { Maybe Coercion
contents <- IORef (Maybe Coercion) -> TcRnIf TcGblEnv TcLclEnv (Maybe Coercion)
forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
readTcRef IORef (Maybe Coercion)
ref
; case Maybe Coercion
contents of
Just Coercion
co -> do { Coercion
co' <- Coercion -> IOEnv (Env TcGblEnv TcLclEnv) Coercion
zonkCo Coercion
co
; TyVar -> Coercion -> IOEnv (Env TcGblEnv TcLclEnv) Coercion
checkCoercionHole TyVar
cv Coercion
co' }
Maybe Coercion
Nothing -> do { TyVar
cv' <- TyVar -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
zonkCoVar TyVar
cv
; Coercion -> IOEnv (Env TcGblEnv TcLclEnv) Coercion
forall (m :: * -> *) a. Monad m => a -> m a
return (Coercion -> IOEnv (Env TcGblEnv TcLclEnv) Coercion)
-> Coercion -> IOEnv (Env TcGblEnv TcLclEnv) Coercion
forall a b. (a -> b) -> a -> b
$ CoercionHole -> Coercion
HoleCo (CoercionHole
hole { ch_co_var :: TyVar
ch_co_var = TyVar
cv' }) } }
zonkTcTyCon :: TcTyCon -> TcM TcTyCon
zonkTcTyCon :: TyCon -> TcM TyCon
zonkTcTyCon TyCon
tc
| TyCon -> Bool
tcTyConIsPoly TyCon
tc = TyCon -> TcM TyCon
forall (m :: * -> *) a. Monad m => a -> m a
return TyCon
tc
| Bool
otherwise = do { TcKind
tck' <- TcKind -> TcM TcKind
zonkTcType (TyCon -> TcKind
tyConKind TyCon
tc)
; TyCon -> TcM TyCon
forall (m :: * -> *) a. Monad m => a -> m a
return (TyCon -> TcKind -> TyCon
setTcTyConKind TyCon
tc TcKind
tck') }
zonkTcTyVar :: TcTyVar -> TcM TcType
zonkTcTyVar :: TyVar -> TcM TcKind
zonkTcTyVar TyVar
tv
| TyVar -> Bool
isTcTyVar TyVar
tv
= case TyVar -> TcTyVarDetails
tcTyVarDetails TyVar
tv of
SkolemTv {} -> TcM TcKind
zonk_kind_and_return
RuntimeUnk {} -> TcM TcKind
zonk_kind_and_return
MetaTv { mtv_ref :: TcTyVarDetails -> IORef MetaDetails
mtv_ref = IORef MetaDetails
ref }
-> do { MetaDetails
cts <- IORef MetaDetails -> TcM MetaDetails
forall a env. IORef a -> IOEnv env a
readMutVar IORef MetaDetails
ref
; case MetaDetails
cts of
MetaDetails
Flexi -> TcM TcKind
zonk_kind_and_return
Indirect TcKind
ty -> do { TcKind
zty <- TcKind -> TcM TcKind
zonkTcType TcKind
ty
; IORef MetaDetails -> MetaDetails -> TcRn ()
forall a gbl lcl. TcRef a -> a -> TcRnIf gbl lcl ()
writeTcRef IORef MetaDetails
ref (TcKind -> MetaDetails
Indirect TcKind
zty)
; TcKind -> TcM TcKind
forall (m :: * -> *) a. Monad m => a -> m a
return TcKind
zty } }
| Bool
otherwise
= TcM TcKind
zonk_kind_and_return
where
zonk_kind_and_return :: TcM TcKind
zonk_kind_and_return = do { TyVar
z_tv <- TyVar -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
zonkTyCoVarKind TyVar
tv
; TcKind -> TcM TcKind
forall (m :: * -> *) a. Monad m => a -> m a
return (TyVar -> TcKind
mkTyVarTy TyVar
z_tv) }
zonkTcTyVarsToTcTyVars :: HasDebugCallStack => [TcTyVar] -> TcM [TcTyVar]
zonkTcTyVarsToTcTyVars :: [TyVar] -> TcM [TyVar]
zonkTcTyVarsToTcTyVars = (TyVar -> IOEnv (Env TcGblEnv TcLclEnv) TyVar)
-> [TyVar] -> TcM [TyVar]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM HasDebugCallStack => TyVar -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
TyVar -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
zonkTcTyVarToTcTyVar
zonkTcTyVarToTcTyVar :: HasDebugCallStack => TcTyVar -> TcM TcTyVar
zonkTcTyVarToTcTyVar :: TyVar -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
zonkTcTyVarToTcTyVar TyVar
tv
= do { TcKind
ty <- TyVar -> TcM TcKind
zonkTcTyVar TyVar
tv
; let tv' :: TyVar
tv' = case TcKind -> Maybe TyVar
tcGetTyVar_maybe TcKind
ty of
Just TyVar
tv' -> TyVar
tv'
Maybe TyVar
Nothing -> String -> SDoc -> TyVar
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"zonkTcTyVarToTcTyVar"
(TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
tv SDoc -> SDoc -> SDoc
$$ TcKind -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcKind
ty)
; TyVar -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
forall (m :: * -> *) a. Monad m => a -> m a
return TyVar
tv' }
zonkInvisTVBinder :: VarBndr TcTyVar spec -> TcM (VarBndr TcTyVar spec)
zonkInvisTVBinder :: VarBndr TyVar spec -> TcM (VarBndr TyVar spec)
zonkInvisTVBinder (Bndr TyVar
tv spec
spec) = do { TyVar
tv' <- HasDebugCallStack => TyVar -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
TyVar -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
zonkTcTyVarToTcTyVar TyVar
tv
; VarBndr TyVar spec -> TcM (VarBndr TyVar spec)
forall (m :: * -> *) a. Monad m => a -> m a
return (TyVar -> spec -> VarBndr TyVar spec
forall var argf. var -> argf -> VarBndr var argf
Bndr TyVar
tv' spec
spec) }
zonkId :: TcId -> TcM TcId
zonkId :: TyVar -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
zonkId TyVar
id = (TcKind -> TcM TcKind)
-> TyVar -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
forall (m :: * -> *).
Monad m =>
(TcKind -> m TcKind) -> TyVar -> m TyVar
Id.updateIdTypeAndMultM TcKind -> TcM TcKind
zonkTcType TyVar
id
zonkCoVar :: CoVar -> TcM CoVar
zonkCoVar :: TyVar -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
zonkCoVar = TyVar -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
zonkId
zonkTidyTcType :: TidyEnv -> TcType -> TcM (TidyEnv, TcType)
zonkTidyTcType :: TidyEnv -> TcKind -> TcM (TidyEnv, TcKind)
zonkTidyTcType TidyEnv
env TcKind
ty = do { TcKind
ty' <- TcKind -> TcM TcKind
zonkTcType TcKind
ty
; (TidyEnv, TcKind) -> TcM (TidyEnv, TcKind)
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv -> TcKind -> (TidyEnv, TcKind)
tidyOpenType TidyEnv
env TcKind
ty') }
zonkTidyTcTypes :: TidyEnv -> [TcType] -> TcM (TidyEnv, [TcType])
zonkTidyTcTypes :: TidyEnv -> [TcKind] -> TcM (TidyEnv, [TcKind])
zonkTidyTcTypes = [TcKind] -> TidyEnv -> [TcKind] -> TcM (TidyEnv, [TcKind])
zonkTidyTcTypes' []
where zonkTidyTcTypes' :: [TcKind] -> TidyEnv -> [TcKind] -> TcM (TidyEnv, [TcKind])
zonkTidyTcTypes' [TcKind]
zs TidyEnv
env [] = (TidyEnv, [TcKind]) -> TcM (TidyEnv, [TcKind])
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
env, [TcKind] -> [TcKind]
forall a. [a] -> [a]
reverse [TcKind]
zs)
zonkTidyTcTypes' [TcKind]
zs TidyEnv
env (TcKind
ty:[TcKind]
tys)
= do { (TidyEnv
env', TcKind
ty') <- TidyEnv -> TcKind -> TcM (TidyEnv, TcKind)
zonkTidyTcType TidyEnv
env TcKind
ty
; [TcKind] -> TidyEnv -> [TcKind] -> TcM (TidyEnv, [TcKind])
zonkTidyTcTypes' (TcKind
ty'TcKind -> [TcKind] -> [TcKind]
forall a. a -> [a] -> [a]
:[TcKind]
zs) TidyEnv
env' [TcKind]
tys }
zonkTidyOrigin :: TidyEnv -> CtOrigin -> TcM (TidyEnv, CtOrigin)
zonkTidyOrigin :: TidyEnv -> CtOrigin -> TcM (TidyEnv, CtOrigin)
zonkTidyOrigin TidyEnv
env (GivenOrigin SkolemInfoAnon
skol_info)
= do { SkolemInfoAnon
skol_info1 <- SkolemInfoAnon -> TcM SkolemInfoAnon
zonkSkolemInfoAnon SkolemInfoAnon
skol_info
; let skol_info2 :: SkolemInfoAnon
skol_info2 = TidyEnv -> SkolemInfoAnon -> SkolemInfoAnon
tidySkolemInfoAnon TidyEnv
env SkolemInfoAnon
skol_info1
; (TidyEnv, CtOrigin) -> TcM (TidyEnv, CtOrigin)
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
env, SkolemInfoAnon -> CtOrigin
GivenOrigin SkolemInfoAnon
skol_info2) }
zonkTidyOrigin TidyEnv
env (OtherSCOrigin Int
sc_depth SkolemInfoAnon
skol_info)
= do { SkolemInfoAnon
skol_info1 <- SkolemInfoAnon -> TcM SkolemInfoAnon
zonkSkolemInfoAnon SkolemInfoAnon
skol_info
; let skol_info2 :: SkolemInfoAnon
skol_info2 = TidyEnv -> SkolemInfoAnon -> SkolemInfoAnon
tidySkolemInfoAnon TidyEnv
env SkolemInfoAnon
skol_info1
; (TidyEnv, CtOrigin) -> TcM (TidyEnv, CtOrigin)
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
env, Int -> SkolemInfoAnon -> CtOrigin
OtherSCOrigin Int
sc_depth SkolemInfoAnon
skol_info2) }
zonkTidyOrigin TidyEnv
env orig :: CtOrigin
orig@(TypeEqOrigin { uo_actual :: CtOrigin -> TcKind
uo_actual = TcKind
act
, uo_expected :: CtOrigin -> TcKind
uo_expected = TcKind
exp })
= do { (TidyEnv
env1, TcKind
act') <- TidyEnv -> TcKind -> TcM (TidyEnv, TcKind)
zonkTidyTcType TidyEnv
env TcKind
act
; (TidyEnv
env2, TcKind
exp') <- TidyEnv -> TcKind -> TcM (TidyEnv, TcKind)
zonkTidyTcType TidyEnv
env1 TcKind
exp
; (TidyEnv, CtOrigin) -> TcM (TidyEnv, CtOrigin)
forall (m :: * -> *) a. Monad m => a -> m a
return ( TidyEnv
env2, CtOrigin
orig { uo_actual :: TcKind
uo_actual = TcKind
act'
, uo_expected :: TcKind
uo_expected = TcKind
exp' }) }
zonkTidyOrigin TidyEnv
env (KindEqOrigin TcKind
ty1 TcKind
ty2 CtOrigin
orig Maybe TypeOrKind
t_or_k)
= do { (TidyEnv
env1, TcKind
ty1') <- TidyEnv -> TcKind -> TcM (TidyEnv, TcKind)
zonkTidyTcType TidyEnv
env TcKind
ty1
; (TidyEnv
env2, TcKind
ty2') <- TidyEnv -> TcKind -> TcM (TidyEnv, TcKind)
zonkTidyTcType TidyEnv
env1 TcKind
ty2
; (TidyEnv
env3, CtOrigin
orig') <- TidyEnv -> CtOrigin -> TcM (TidyEnv, CtOrigin)
zonkTidyOrigin TidyEnv
env2 CtOrigin
orig
; (TidyEnv, CtOrigin) -> TcM (TidyEnv, CtOrigin)
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
env3, TcKind -> TcKind -> CtOrigin -> Maybe TypeOrKind -> CtOrigin
KindEqOrigin TcKind
ty1' TcKind
ty2' CtOrigin
orig' Maybe TypeOrKind
t_or_k) }
zonkTidyOrigin TidyEnv
env (FunDepOrigin1 TcKind
p1 CtOrigin
o1 RealSrcSpan
l1 TcKind
p2 CtOrigin
o2 RealSrcSpan
l2)
= do { (TidyEnv
env1, TcKind
p1') <- TidyEnv -> TcKind -> TcM (TidyEnv, TcKind)
zonkTidyTcType TidyEnv
env TcKind
p1
; (TidyEnv
env2, CtOrigin
o1') <- TidyEnv -> CtOrigin -> TcM (TidyEnv, CtOrigin)
zonkTidyOrigin TidyEnv
env1 CtOrigin
o1
; (TidyEnv
env3, TcKind
p2') <- TidyEnv -> TcKind -> TcM (TidyEnv, TcKind)
zonkTidyTcType TidyEnv
env2 TcKind
p2
; (TidyEnv
env4, CtOrigin
o2') <- TidyEnv -> CtOrigin -> TcM (TidyEnv, CtOrigin)
zonkTidyOrigin TidyEnv
env3 CtOrigin
o2
; (TidyEnv, CtOrigin) -> TcM (TidyEnv, CtOrigin)
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
env4, TcKind
-> CtOrigin
-> RealSrcSpan
-> TcKind
-> CtOrigin
-> RealSrcSpan
-> CtOrigin
FunDepOrigin1 TcKind
p1' CtOrigin
o1' RealSrcSpan
l1 TcKind
p2' CtOrigin
o2' RealSrcSpan
l2) }
zonkTidyOrigin TidyEnv
env (FunDepOrigin2 TcKind
p1 CtOrigin
o1 TcKind
p2 SrcSpan
l2)
= do { (TidyEnv
env1, TcKind
p1') <- TidyEnv -> TcKind -> TcM (TidyEnv, TcKind)
zonkTidyTcType TidyEnv
env TcKind
p1
; (TidyEnv
env2, TcKind
p2') <- TidyEnv -> TcKind -> TcM (TidyEnv, TcKind)
zonkTidyTcType TidyEnv
env1 TcKind
p2
; (TidyEnv
env3, CtOrigin
o1') <- TidyEnv -> CtOrigin -> TcM (TidyEnv, CtOrigin)
zonkTidyOrigin TidyEnv
env2 CtOrigin
o1
; (TidyEnv, CtOrigin) -> TcM (TidyEnv, CtOrigin)
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
env3, TcKind -> CtOrigin -> TcKind -> SrcSpan -> CtOrigin
FunDepOrigin2 TcKind
p1' CtOrigin
o1' TcKind
p2' SrcSpan
l2) }
zonkTidyOrigin TidyEnv
env (InjTFOrigin1 TcKind
pred1 CtOrigin
orig1 RealSrcSpan
loc1 TcKind
pred2 CtOrigin
orig2 RealSrcSpan
loc2)
= do { (TidyEnv
env1, TcKind
pred1') <- TidyEnv -> TcKind -> TcM (TidyEnv, TcKind)
zonkTidyTcType TidyEnv
env TcKind
pred1
; (TidyEnv
env2, CtOrigin
orig1') <- TidyEnv -> CtOrigin -> TcM (TidyEnv, CtOrigin)
zonkTidyOrigin TidyEnv
env1 CtOrigin
orig1
; (TidyEnv
env3, TcKind
pred2') <- TidyEnv -> TcKind -> TcM (TidyEnv, TcKind)
zonkTidyTcType TidyEnv
env2 TcKind
pred2
; (TidyEnv
env4, CtOrigin
orig2') <- TidyEnv -> CtOrigin -> TcM (TidyEnv, CtOrigin)
zonkTidyOrigin TidyEnv
env3 CtOrigin
orig2
; (TidyEnv, CtOrigin) -> TcM (TidyEnv, CtOrigin)
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
env4, TcKind
-> CtOrigin
-> RealSrcSpan
-> TcKind
-> CtOrigin
-> RealSrcSpan
-> CtOrigin
InjTFOrigin1 TcKind
pred1' CtOrigin
orig1' RealSrcSpan
loc1 TcKind
pred2' CtOrigin
orig2' RealSrcSpan
loc2) }
zonkTidyOrigin TidyEnv
env (CycleBreakerOrigin CtOrigin
orig)
= do { (TidyEnv
env1, CtOrigin
orig') <- TidyEnv -> CtOrigin -> TcM (TidyEnv, CtOrigin)
zonkTidyOrigin TidyEnv
env CtOrigin
orig
; (TidyEnv, CtOrigin) -> TcM (TidyEnv, CtOrigin)
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
env1, CtOrigin -> CtOrigin
CycleBreakerOrigin CtOrigin
orig') }
zonkTidyOrigin TidyEnv
env (InstProvidedOrigin Module
mod ClsInst
cls_inst)
= do { (TidyEnv
env1, [TcKind]
is_tys') <- (TidyEnv -> TcKind -> TcM (TidyEnv, TcKind))
-> TidyEnv -> [TcKind] -> TcM (TidyEnv, [TcKind])
forall (m :: * -> *) acc x y.
Monad m =>
(acc -> x -> m (acc, y)) -> acc -> [x] -> m (acc, [y])
mapAccumLM TidyEnv -> TcKind -> TcM (TidyEnv, TcKind)
zonkTidyTcType TidyEnv
env (ClsInst -> [TcKind]
is_tys ClsInst
cls_inst)
; (TidyEnv, CtOrigin) -> TcM (TidyEnv, CtOrigin)
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
env1, Module -> ClsInst -> CtOrigin
InstProvidedOrigin Module
mod (ClsInst
cls_inst {is_tys :: [TcKind]
is_tys = [TcKind]
is_tys'})) }
zonkTidyOrigin TidyEnv
env (FixedRuntimeRepOrigin TcKind
ty FRROrigin
frr_orig)
= do { (TidyEnv
env1, TcKind
ty') <- TidyEnv -> TcKind -> TcM (TidyEnv, TcKind)
zonkTidyTcType TidyEnv
env TcKind
ty
; (TidyEnv, CtOrigin) -> TcM (TidyEnv, CtOrigin)
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
env1, TcKind -> FRROrigin -> CtOrigin
FixedRuntimeRepOrigin TcKind
ty' FRROrigin
frr_orig)}
zonkTidyOrigin TidyEnv
env (WantedSuperclassOrigin TcKind
pty CtOrigin
orig)
= do { (TidyEnv
env1, TcKind
pty') <- TidyEnv -> TcKind -> TcM (TidyEnv, TcKind)
zonkTidyTcType TidyEnv
env TcKind
pty
; (TidyEnv
env2, CtOrigin
orig') <- TidyEnv -> CtOrigin -> TcM (TidyEnv, CtOrigin)
zonkTidyOrigin TidyEnv
env1 CtOrigin
orig
; (TidyEnv, CtOrigin) -> TcM (TidyEnv, CtOrigin)
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
env2, TcKind -> CtOrigin -> CtOrigin
WantedSuperclassOrigin TcKind
pty' CtOrigin
orig') }
zonkTidyOrigin TidyEnv
env CtOrigin
orig = (TidyEnv, CtOrigin) -> TcM (TidyEnv, CtOrigin)
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
env, CtOrigin
orig)
zonkTidyOrigins :: TidyEnv -> [CtOrigin] -> TcM (TidyEnv, [CtOrigin])
zonkTidyOrigins :: TidyEnv -> [CtOrigin] -> TcM (TidyEnv, [CtOrigin])
zonkTidyOrigins = (TidyEnv -> CtOrigin -> TcM (TidyEnv, CtOrigin))
-> TidyEnv -> [CtOrigin] -> TcM (TidyEnv, [CtOrigin])
forall (m :: * -> *) acc x y.
Monad m =>
(acc -> x -> m (acc, y)) -> acc -> [x] -> m (acc, [y])
mapAccumLM TidyEnv -> CtOrigin -> TcM (TidyEnv, CtOrigin)
zonkTidyOrigin
tidyCt :: TidyEnv -> Ct -> Ct
tidyCt :: TidyEnv -> Ct -> Ct
tidyCt TidyEnv
env Ct
ct = Ct
ct { cc_ev :: CtEvidence
cc_ev = TidyEnv -> CtEvidence -> CtEvidence
tidyCtEvidence TidyEnv
env (Ct -> CtEvidence
ctEvidence Ct
ct) }
tidyCtEvidence :: TidyEnv -> CtEvidence -> CtEvidence
tidyCtEvidence :: TidyEnv -> CtEvidence -> CtEvidence
tidyCtEvidence TidyEnv
env CtEvidence
ctev = CtEvidence
ctev { ctev_pred :: TcKind
ctev_pred = TidyEnv -> TcKind -> TcKind
tidyType TidyEnv
env TcKind
ty }
where
ty :: TcKind
ty = CtEvidence -> TcKind
ctev_pred CtEvidence
ctev
tidyHole :: TidyEnv -> Hole -> Hole
tidyHole :: TidyEnv -> Hole -> Hole
tidyHole TidyEnv
env h :: Hole
h@(Hole { hole_ty :: Hole -> TcKind
hole_ty = TcKind
ty }) = Hole
h { hole_ty :: TcKind
hole_ty = TidyEnv -> TcKind -> TcKind
tidyType TidyEnv
env TcKind
ty }
tidyEvVar :: TidyEnv -> EvVar -> EvVar
tidyEvVar :: TidyEnv -> TyVar -> TyVar
tidyEvVar TidyEnv
env TyVar
var = (TcKind -> TcKind) -> TyVar -> TyVar
updateIdTypeAndMult (TidyEnv -> TcKind -> TcKind
tidyType TidyEnv
env) TyVar
var
checkTypeHasFixedRuntimeRep :: FixedRuntimeRepProvenance -> Type -> TcM ()
checkTypeHasFixedRuntimeRep :: FixedRuntimeRepProvenance -> TcKind -> TcRn ()
checkTypeHasFixedRuntimeRep FixedRuntimeRepProvenance
prov TcKind
ty =
Bool -> TcRn () -> TcRn ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (TcKind -> Bool
typeHasFixedRuntimeRep TcKind
ty)
((ErrInfo -> TcRnMessage) -> TcRn ()
addDetailedDiagnostic ((ErrInfo -> TcRnMessage) -> TcRn ())
-> (ErrInfo -> TcRnMessage) -> TcRn ()
forall a b. (a -> b) -> a -> b
$ TcKind -> FixedRuntimeRepProvenance -> ErrInfo -> TcRnMessage
TcRnTypeDoesNotHaveFixedRuntimeRep TcKind
ty FixedRuntimeRepProvenance
prov)
naughtyQuantification :: TcType
-> TcTyVar
-> TyVarSet
-> TcM a
naughtyQuantification :: TcKind -> TyVar -> CoVarSet -> TcM a
naughtyQuantification TcKind
orig_ty TyVar
tv CoVarSet
escapees
= do { TcKind
orig_ty1 <- TcKind -> TcM TcKind
zonkTcType TcKind
orig_ty
; [TyVar]
escapees' <- [TyVar] -> TcM [TyVar]
HasDebugCallStack => [TyVar] -> TcM [TyVar]
zonkTcTyVarsToTcTyVars ([TyVar] -> TcM [TyVar]) -> [TyVar] -> TcM [TyVar]
forall a b. (a -> b) -> a -> b
$
CoVarSet -> [TyVar]
forall elt. UniqSet elt -> [elt]
nonDetEltsUniqSet CoVarSet
escapees
; let fvs :: [TyVar]
fvs = TcKind -> [TyVar]
tyCoVarsOfTypeWellScoped TcKind
orig_ty1
env0 :: TidyEnv
env0 = TidyEnv -> [TyVar] -> TidyEnv
tidyFreeTyCoVars TidyEnv
emptyTidyEnv [TyVar]
fvs
env :: TidyEnv
env = TidyEnv
env0 TidyEnv -> [TyVar] -> TidyEnv
`delTidyEnvList` [TyVar]
escapees'
orig_ty' :: TcKind
orig_ty' = TidyEnv -> TcKind -> TcKind
tidyType TidyEnv
env TcKind
orig_ty1
ppr_tidied :: [TyVar] -> SDoc
ppr_tidied = [TyVar] -> SDoc
pprTyVars ([TyVar] -> SDoc) -> ([TyVar] -> [TyVar]) -> [TyVar] -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TyVar -> TyVar) -> [TyVar] -> [TyVar]
forall a b. (a -> b) -> [a] -> [b]
map (TidyEnv -> TyVar -> TyVar
tidyTyCoVarOcc TidyEnv
env)
msg :: TcRnMessage
msg = DiagnosticMessage -> TcRnMessage
forall a. (Diagnostic a, Typeable a) => a -> TcRnMessage
TcRnUnknownMessage (DiagnosticMessage -> TcRnMessage)
-> DiagnosticMessage -> TcRnMessage
forall a b. (a -> b) -> a -> b
$ [GhcHint] -> SDoc -> DiagnosticMessage
mkPlainError [GhcHint]
noHints (SDoc -> DiagnosticMessage) -> SDoc -> DiagnosticMessage
forall a b. (a -> b) -> a -> b
$
Bool -> SDoc -> SDoc
pprWithExplicitKindsWhen Bool
True (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
vcat [ [SDoc] -> SDoc
sep [ String -> SDoc
text String
"Cannot generalise type; skolem" SDoc -> SDoc -> SDoc
<> [TyVar] -> SDoc
forall a. [a] -> SDoc
plural [TyVar]
escapees'
, SDoc -> SDoc
quotes (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ [TyVar] -> SDoc
ppr_tidied [TyVar]
escapees'
, String -> SDoc
text String
"would escape" SDoc -> SDoc -> SDoc
<+> [TyVar] -> SDoc
forall a. [a] -> SDoc
itsOrTheir [TyVar]
escapees' SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"scope"
]
, [SDoc] -> SDoc
sep [ String -> SDoc
text String
"if I tried to quantify"
, [TyVar] -> SDoc
ppr_tidied [TyVar
tv]
, String -> SDoc
text String
"in this type:"
]
, Int -> SDoc -> SDoc
nest Int
2 (TcKind -> SDoc
pprTidiedType TcKind
orig_ty')
, String -> SDoc
text String
"(Indeed, I sometimes struggle even printing this correctly,"
, String -> SDoc
text String
" due to its ill-scoped nature.)"
]
; (TidyEnv, TcRnMessage) -> TcM a
forall a. (TidyEnv, TcRnMessage) -> TcM a
failWithTcM (TidyEnv
env, TcRnMessage
msg) }
anyUnfilledCoercionHoles :: RewriterSet -> TcM Bool
anyUnfilledCoercionHoles :: RewriterSet -> TcRnIf TcGblEnv TcLclEnv Bool
anyUnfilledCoercionHoles (RewriterSet UniqSet CoercionHole
set)
= (CoercionHole
-> TcRnIf TcGblEnv TcLclEnv Bool -> TcRnIf TcGblEnv TcLclEnv Bool)
-> TcRnIf TcGblEnv TcLclEnv Bool
-> UniqSet CoercionHole
-> TcRnIf TcGblEnv TcLclEnv Bool
forall elt a. (elt -> a -> a) -> a -> UniqSet elt -> a
nonDetStrictFoldUniqSet CoercionHole
-> TcRnIf TcGblEnv TcLclEnv Bool -> TcRnIf TcGblEnv TcLclEnv Bool
go (Bool -> TcRnIf TcGblEnv TcLclEnv Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False) UniqSet CoercionHole
set
where
go :: CoercionHole -> TcM Bool -> TcM Bool
go :: CoercionHole
-> TcRnIf TcGblEnv TcLclEnv Bool -> TcRnIf TcGblEnv TcLclEnv Bool
go CoercionHole
hole TcRnIf TcGblEnv TcLclEnv Bool
m_acc = TcRnIf TcGblEnv TcLclEnv Bool
m_acc TcRnIf TcGblEnv TcLclEnv Bool
-> TcRnIf TcGblEnv TcLclEnv Bool -> TcRnIf TcGblEnv TcLclEnv Bool
forall (f :: * -> *). Applicative f => f Bool -> f Bool -> f Bool
<||> CoercionHole -> TcRnIf TcGblEnv TcLclEnv Bool
check_hole CoercionHole
hole
check_hole :: CoercionHole -> TcM Bool
check_hole :: CoercionHole -> TcRnIf TcGblEnv TcLclEnv Bool
check_hole CoercionHole
hole = do { Maybe Coercion
m_co <- CoercionHole -> TcRnIf TcGblEnv TcLclEnv (Maybe Coercion)
unpackCoercionHole_maybe CoercionHole
hole
; case Maybe Coercion
m_co of
Maybe Coercion
Nothing -> Bool -> TcRnIf TcGblEnv TcLclEnv Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
Just Coercion
co -> UnfilledCoercionHoleMonoid -> TcRnIf TcGblEnv TcLclEnv Bool
unUCHM (Coercion -> UnfilledCoercionHoleMonoid
check_co Coercion
co) }
check_ty :: Type -> UnfilledCoercionHoleMonoid
check_co :: Coercion -> UnfilledCoercionHoleMonoid
(TcKind -> UnfilledCoercionHoleMonoid
check_ty, [TcKind] -> UnfilledCoercionHoleMonoid
_, Coercion -> UnfilledCoercionHoleMonoid
check_co, [Coercion] -> UnfilledCoercionHoleMonoid
_) = TyCoFolder () UnfilledCoercionHoleMonoid
-> ()
-> (TcKind -> UnfilledCoercionHoleMonoid,
[TcKind] -> UnfilledCoercionHoleMonoid,
Coercion -> UnfilledCoercionHoleMonoid,
[Coercion] -> UnfilledCoercionHoleMonoid)
forall a env.
Monoid a =>
TyCoFolder env a
-> env
-> (TcKind -> a, [TcKind] -> a, Coercion -> a, [Coercion] -> a)
foldTyCo TyCoFolder () UnfilledCoercionHoleMonoid
folder ()
folder :: TyCoFolder () UnfilledCoercionHoleMonoid
folder :: TyCoFolder () UnfilledCoercionHoleMonoid
folder = TyCoFolder :: forall env a.
(TcKind -> Maybe TcKind)
-> (env -> TyVar -> a)
-> (env -> TyVar -> a)
-> (env -> CoercionHole -> a)
-> (env -> TyVar -> ArgFlag -> env)
-> TyCoFolder env a
TyCoFolder { tcf_view :: TcKind -> Maybe TcKind
tcf_view = TcKind -> Maybe TcKind
noView
, tcf_tyvar :: () -> TyVar -> UnfilledCoercionHoleMonoid
tcf_tyvar = \ ()
_ TyVar
tv -> TcKind -> UnfilledCoercionHoleMonoid
check_ty (TyVar -> TcKind
tyVarKind TyVar
tv)
, tcf_covar :: () -> TyVar -> UnfilledCoercionHoleMonoid
tcf_covar = \ ()
_ TyVar
cv -> TcKind -> UnfilledCoercionHoleMonoid
check_ty (TyVar -> TcKind
varType TyVar
cv)
, tcf_hole :: () -> CoercionHole -> UnfilledCoercionHoleMonoid
tcf_hole = \ ()
_ -> TcRnIf TcGblEnv TcLclEnv Bool -> UnfilledCoercionHoleMonoid
UCHM (TcRnIf TcGblEnv TcLclEnv Bool -> UnfilledCoercionHoleMonoid)
-> (CoercionHole -> TcRnIf TcGblEnv TcLclEnv Bool)
-> CoercionHole
-> UnfilledCoercionHoleMonoid
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoercionHole -> TcRnIf TcGblEnv TcLclEnv Bool
check_hole
, tcf_tycobinder :: () -> TyVar -> ArgFlag -> ()
tcf_tycobinder = \ ()
_ TyVar
_ ArgFlag
_ -> () }
newtype UnfilledCoercionHoleMonoid = UCHM { UnfilledCoercionHoleMonoid -> TcRnIf TcGblEnv TcLclEnv Bool
unUCHM :: TcM Bool }
instance Semigroup UnfilledCoercionHoleMonoid where
UCHM TcRnIf TcGblEnv TcLclEnv Bool
l <> :: UnfilledCoercionHoleMonoid
-> UnfilledCoercionHoleMonoid -> UnfilledCoercionHoleMonoid
<> UCHM TcRnIf TcGblEnv TcLclEnv Bool
r = TcRnIf TcGblEnv TcLclEnv Bool -> UnfilledCoercionHoleMonoid
UCHM (TcRnIf TcGblEnv TcLclEnv Bool
l TcRnIf TcGblEnv TcLclEnv Bool
-> TcRnIf TcGblEnv TcLclEnv Bool -> TcRnIf TcGblEnv TcLclEnv Bool
forall (f :: * -> *). Applicative f => f Bool -> f Bool -> f Bool
<||> TcRnIf TcGblEnv TcLclEnv Bool
r)
instance Monoid UnfilledCoercionHoleMonoid where
mempty :: UnfilledCoercionHoleMonoid
mempty = TcRnIf TcGblEnv TcLclEnv Bool -> UnfilledCoercionHoleMonoid
UCHM (Bool -> TcRnIf TcGblEnv TcLclEnv Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False)