module TcType (
TcType, TcSigmaType, TcRhoType, TcTauType, TcPredType, TcThetaType,
TcTyVar, TcTyVarSet, TcDTyVarSet, TcTyCoVarSet, TcDTyCoVarSet,
TcKind, TcCoVar, TcTyCoVar, TcTyBinder, TcTyCon,
ExpType(..), ExpSigmaType, ExpRhoType, mkCheckExpType,
SyntaxOpType(..), synKnownType, mkSynFunTys,
TcLevel(..), topTcLevel, pushTcLevel, isTopTcLevel,
strictlyDeeperThan, sameDepthAs, fmvTcLevel,
UserTypeCtxt(..), pprUserTypeCtxt, pprSigCtxt, isSigMaybe,
TcTyVarDetails(..), pprTcTyVarDetails, vanillaSkolemTv, superSkolemTv,
MetaDetails(Flexi, Indirect), MetaInfo(..), TauTvFlavour(..),
isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isMetaTyVarTy, isTyVarTy,
isSigTyVar, isOverlappableTyVar, isTyConableTyVar,
isFskTyVar, isFmvTyVar, isFlattenTyVar,
isAmbiguousTyVar, metaTvRef, metaTyVarInfo,
isFlexi, isIndirect, isRuntimeUnkSkol,
metaTyVarTcLevel, setMetaTyVarTcLevel, metaTyVarTcLevel_maybe,
isTouchableMetaTyVar, isTouchableOrFmv,
isFloatedTouchableMetaTyVar,
canUnifyWithPolyType,
mkPhiTy, mkInvSigmaTy, mkSpecSigmaTy, mkSigmaTy,
mkNakedTyConApp, mkNakedAppTys, mkNakedAppTy,
mkNakedCastTy,
getTyVar,
tcSplitForAllTy_maybe,
tcSplitForAllTys, tcSplitPiTys, tcSplitNamedPiTys,
tcSplitPhiTy, tcSplitPredFunTy_maybe,
tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy, tcSplitFunTysN,
tcSplitTyConApp, tcSplitTyConApp_maybe, tcRepSplitTyConApp_maybe,
tcTyConAppTyCon, tcTyConAppArgs,
tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, tcRepSplitAppTy_maybe,
tcGetTyVar_maybe, tcGetTyVar, nextRole,
tcSplitSigmaTy, tcDeepSplitSigmaTy_maybe,
eqType, eqTypes, cmpType, cmpTypes, eqTypeX,
pickyEqType, tcEqType, tcEqKind, tcEqTypeNoKindCheck, tcEqTypeVis,
isSigmaTy, isRhoTy, isRhoExpTy, isOverloadedTy,
isFloatingTy, isDoubleTy, isFloatTy, isIntTy, isWordTy, isStringTy,
isIntegerTy, isBoolTy, isUnitTy, isCharTy, isCallStackTy, isCallStackPred,
isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy,
isPredTy, isTyVarClassPred, isTyVarExposed, isTyVarUnderDatatype,
checkValidClsArgs, hasTyVarHead,
isRigidEqPred, isRigidTy,
deNoteType, occurCheckExpand, OccCheckResult(..),
orphNamesOfType, orphNamesOfCo,
orphNamesOfTypes, orphNamesOfCoCon,
getDFunTyKey,
evVarPred_maybe, evVarPred,
mkMinimalBySCs, transSuperClasses,
pickQuantifiablePreds,
immSuperClasses,
isImprovementPred,
tcTyFamInsts,
exactTyCoVarsOfType, exactTyCoVarsOfTypes,
allBoundVariables, allBoundVariabless,
isFFIArgumentTy,
isFFIImportResultTy,
isFFIExportResultTy,
isFFIExternalTy,
isFFIDynTy,
isFFIPrimArgumentTy,
isFFIPrimResultTy,
isFFILabelTy,
isFFITy,
isFunPtrTy,
tcSplitIOType_maybe,
Kind, typeKind,
liftedTypeKind,
constraintKind,
isLiftedTypeKind, isUnliftedTypeKind, classifiesTypeWithValues,
Type, PredType, ThetaType, TyBinder, VisibilityFlag(..),
mkForAllTy, mkForAllTys, mkInvForAllTys, mkSpecForAllTys, mkNamedForAllTy,
mkFunTy, mkFunTys,
mkTyConApp, mkAppTy, mkAppTys,
mkTyConTy, mkTyVarTy,
mkTyVarTys,
mkNamedBinder,
isClassPred, isEqPred, isNomEqPred, isIPPred,
mkClassPred,
isDictLikeTy,
tcSplitDFunTy, tcSplitDFunHead,
isRuntimeRepVar, isRuntimeRepPolymorphic,
isVisibleBinder, isInvisibleBinder,
TCvSubst(..),
TvSubstEnv, emptyTCvSubst,
zipTvSubst,
mkTvSubstPrs, notElemTCvSubst, unionTCvSubst,
getTvSubstEnv, setTvSubstEnv, getTCvInScope, extendTCvInScope,
extendTCvInScopeList, extendTCvInScopeSet, extendTvSubstAndInScope,
Type.lookupTyVar, Type.extendTCvSubst, Type.substTyVarBndr,
Type.extendTvSubst,
isInScope, mkTCvSubst, mkTvSubst, zipTyEnv, zipCoEnv,
Type.substTy, substTys, substTyWith, substTyWithCoVars,
substTyAddInScope,
substTyUnchecked, substTysUnchecked, substThetaUnchecked,
substTyWithBindersUnchecked, substTyWithUnchecked,
substCoUnchecked, substCoWithUnchecked,
substTheta,
isUnliftedType,
isUnboxedTupleType,
isPrimitiveType,
coreView,
tyCoVarsOfType, tyCoVarsOfTypes, closeOverKinds,
tyCoVarsOfTelescope,
tyCoVarsOfTypeAcc, tyCoVarsOfTypesAcc,
tyCoVarsOfTypeDSet, tyCoVarsOfTypesDSet, closeOverKindsDSet,
tyCoVarsOfTypeList, tyCoVarsOfTypesList,
toTcType,
toTcTypeBag,
pprKind, pprParendKind, pprSigmaType,
pprType, pprParendType, pprTypeApp, pprTyThingCategory,
pprTheta, pprThetaArrowTy, pprClassPred,
pprTvBndr, pprTvBndrs,
TypeSize, sizeType, sizeTypes, toposortTyVars
) where
#include "HsVersions.h"
import Kind
import TyCoRep
import Class
import Var
import ForeignCall
import VarSet
import Coercion
import Type
import TyCon
import DynFlags
import CoreFVs
import Name
import NameSet
import VarEnv
import PrelNames
import TysWiredIn
import BasicTypes
import Util
import Bag
import Maybes
import Pair
import Outputable
import FastString
import ErrUtils( Validity(..), MsgDoc, isValid )
import FV
import qualified GHC.LanguageExtensions as LangExt
import Data.IORef
import Control.Monad (liftM, ap)
#if __GLASGOW_HASKELL__ < 709
import Control.Applicative (Applicative(..), (<$>) )
#endif
import Data.Functor.Identity
type TcTyVar = TyVar
type TcCoVar = CoVar
type TcType = Type
type TcTyCoVar = Var
type TcTyBinder = TyBinder
type TcTyCon = TyCon
type TcPredType = PredType
type TcThetaType = ThetaType
type TcSigmaType = TcType
type TcRhoType = TcType
type TcTauType = TcType
type TcKind = Kind
type TcTyVarSet = TyVarSet
type TcTyCoVarSet = TyCoVarSet
type TcDTyVarSet = DTyVarSet
type TcDTyCoVarSet = DTyCoVarSet
data ExpType = Check TcType
| Infer Unique
TcLevel
Kind
(IORef (Maybe TcType))
type ExpSigmaType = ExpType
type ExpRhoType = ExpType
instance Outputable ExpType where
ppr (Check ty) = ppr ty
ppr (Infer u lvl ki _)
= parens (text "Infer" <> braces (ppr u <> comma <> ppr lvl)
<+> dcolon <+> ppr ki)
mkCheckExpType :: TcType -> ExpType
mkCheckExpType = Check
data SyntaxOpType
= SynAny
| SynRho
| SynList
| SynFun SyntaxOpType SyntaxOpType
| SynType ExpType
infixr 0 `SynFun`
synKnownType :: TcType -> SyntaxOpType
synKnownType = SynType . mkCheckExpType
mkSynFunTys :: [SyntaxOpType] -> ExpType -> SyntaxOpType
mkSynFunTys arg_tys res_ty = foldr SynFun (SynType res_ty) arg_tys
data TcTyVarDetails
= SkolemTv
Bool
| FlatSkol
TcType
| RuntimeUnk
| MetaTv { mtv_info :: MetaInfo
, mtv_ref :: IORef MetaDetails
, mtv_tclvl :: TcLevel }
vanillaSkolemTv, superSkolemTv :: TcTyVarDetails
vanillaSkolemTv = SkolemTv False
superSkolemTv = SkolemTv True
data MetaDetails
= Flexi
| Indirect TcType
instance Outputable MetaDetails where
ppr Flexi = text "Flexi"
ppr (Indirect ty) = text "Indirect" <+> ppr ty
data TauTvFlavour
= VanillaTau
| WildcardTau
data MetaInfo
= TauTv
| SigTv
| FlatMetaTv
data UserTypeCtxt
= FunSigCtxt
Name
Bool
| InfSigCtxt Name
| ExprSigCtxt
| TypeAppCtxt
| ConArgCtxt Name
| TySynCtxt Name
| PatSynBuilderCtxt Name
| PatSigCtxt
| RuleSigCtxt Name
| ResSigCtxt
| ForSigCtxt Name
| DefaultDeclCtxt
| InstDeclCtxt
| SpecInstCtxt
| ThBrackCtxt
| GenSigCtxt
| GhciCtxt
| ClassSCCtxt Name
| SigmaCtxt
| DataTyCtxt Name
newtype TcLevel = TcLevel Int deriving( Eq, Ord )
fmvTcLevel :: TcLevel -> TcLevel
fmvTcLevel (TcLevel n) = TcLevel (n1)
topTcLevel :: TcLevel
topTcLevel = TcLevel 1
isTopTcLevel :: TcLevel -> Bool
isTopTcLevel (TcLevel 1) = True
isTopTcLevel _ = False
pushTcLevel :: TcLevel -> TcLevel
pushTcLevel (TcLevel us) = TcLevel (us + 2)
strictlyDeeperThan :: TcLevel -> TcLevel -> Bool
strictlyDeeperThan (TcLevel tv_tclvl) (TcLevel ctxt_tclvl)
= tv_tclvl > ctxt_tclvl
sameDepthAs :: TcLevel -> TcLevel -> Bool
sameDepthAs (TcLevel ctxt_tclvl) (TcLevel tv_tclvl)
= ctxt_tclvl == tv_tclvl
checkTcLevelInvariant :: TcLevel -> TcLevel -> Bool
checkTcLevelInvariant (TcLevel ctxt_tclvl) (TcLevel tv_tclvl)
= ctxt_tclvl >= tv_tclvl
instance Outputable TcLevel where
ppr (TcLevel us) = ppr us
pprTcTyVarDetails :: TcTyVarDetails -> SDoc
pprTcTyVarDetails (SkolemTv True) = text "ssk"
pprTcTyVarDetails (SkolemTv False) = text "sk"
pprTcTyVarDetails (RuntimeUnk {}) = text "rt"
pprTcTyVarDetails (FlatSkol {}) = text "fsk"
pprTcTyVarDetails (MetaTv { mtv_info = info, mtv_tclvl = tclvl })
= pp_info <> colon <> ppr tclvl
where
pp_info = case info of
TauTv -> text "tau"
SigTv -> text "sig"
FlatMetaTv -> text "fuv"
pprUserTypeCtxt :: UserTypeCtxt -> SDoc
pprUserTypeCtxt (FunSigCtxt n _) = text "the type signature for" <+> quotes (ppr n)
pprUserTypeCtxt (InfSigCtxt n) = text "the inferred type for" <+> quotes (ppr n)
pprUserTypeCtxt (RuleSigCtxt n) = text "a RULE for" <+> quotes (ppr n)
pprUserTypeCtxt ExprSigCtxt = text "an expression type signature"
pprUserTypeCtxt TypeAppCtxt = text "a type argument"
pprUserTypeCtxt (ConArgCtxt c) = text "the type of the constructor" <+> quotes (ppr c)
pprUserTypeCtxt (TySynCtxt c) = text "the RHS of the type synonym" <+> quotes (ppr c)
pprUserTypeCtxt ThBrackCtxt = text "a Template Haskell quotation [t|...|]"
pprUserTypeCtxt PatSigCtxt = text "a pattern type signature"
pprUserTypeCtxt ResSigCtxt = text "a result type signature"
pprUserTypeCtxt (ForSigCtxt n) = text "the foreign declaration for" <+> quotes (ppr n)
pprUserTypeCtxt DefaultDeclCtxt = text "a type in a `default' declaration"
pprUserTypeCtxt InstDeclCtxt = text "an instance declaration"
pprUserTypeCtxt SpecInstCtxt = text "a SPECIALISE instance pragma"
pprUserTypeCtxt GenSigCtxt = text "a type expected by the context"
pprUserTypeCtxt GhciCtxt = text "a type in a GHCi command"
pprUserTypeCtxt (ClassSCCtxt c) = text "the super-classes of class" <+> quotes (ppr c)
pprUserTypeCtxt SigmaCtxt = text "the context of a polymorphic type"
pprUserTypeCtxt (DataTyCtxt tc) = text "the context of the data type declaration for" <+> quotes (ppr tc)
pprUserTypeCtxt (PatSynBuilderCtxt n)
= vcat [ text "the type signature for bidirectional pattern synonym" <+> quotes (ppr n)
, text "when used in an expression context" ]
pprSigCtxt :: UserTypeCtxt -> SDoc -> SDoc -> SDoc
pprSigCtxt ctxt extra pp_ty
| Just n <- isSigMaybe ctxt
= vcat [ text "In" <+> extra <+> ptext (sLit "the type signature:")
, nest 2 (pprPrefixOcc n <+> dcolon <+> pp_ty) ]
| otherwise
= hang (text "In" <+> extra <+> pprUserTypeCtxt ctxt <> colon)
2 pp_ty
where
isSigMaybe :: UserTypeCtxt -> Maybe Name
isSigMaybe (FunSigCtxt n _) = Just n
isSigMaybe (ConArgCtxt n) = Just n
isSigMaybe (ForSigCtxt n) = Just n
isSigMaybe (PatSynBuilderCtxt n) = Just n
isSigMaybe _ = Nothing
tcTyFamInsts :: Type -> [(TyCon, [Type])]
tcTyFamInsts ty
| Just exp_ty <- coreView ty = tcTyFamInsts exp_ty
tcTyFamInsts (TyVarTy _) = []
tcTyFamInsts (TyConApp tc tys)
| isTypeFamilyTyCon tc = [(tc, tys)]
| otherwise = concat (map tcTyFamInsts tys)
tcTyFamInsts (LitTy {}) = []
tcTyFamInsts (ForAllTy bndr ty) = tcTyFamInsts (binderType bndr)
++ tcTyFamInsts ty
tcTyFamInsts (AppTy ty1 ty2) = tcTyFamInsts ty1 ++ tcTyFamInsts ty2
tcTyFamInsts (CastTy ty _) = tcTyFamInsts ty
tcTyFamInsts (CoercionTy _) = []
exactTyCoVarsOfType :: Type -> TyCoVarSet
exactTyCoVarsOfType ty
= go ty
where
go ty | Just ty' <- coreView ty = go ty'
go (TyVarTy tv) = unitVarSet tv `unionVarSet` go (tyVarKind tv)
go (TyConApp _ tys) = exactTyCoVarsOfTypes tys
go (LitTy {}) = emptyVarSet
go (AppTy fun arg) = go fun `unionVarSet` go arg
go (ForAllTy bndr ty) = delBinderVar (go ty) bndr `unionVarSet` go (binderType bndr)
go (CastTy ty co) = go ty `unionVarSet` goCo co
go (CoercionTy co) = goCo co
goCo (Refl _ ty) = go ty
goCo (TyConAppCo _ _ args)= goCos args
goCo (AppCo co arg) = goCo co `unionVarSet` goCo arg
goCo (ForAllCo tv k_co co)
= goCo co `delVarSet` tv `unionVarSet` goCo k_co
goCo (CoVarCo v) = unitVarSet v `unionVarSet` go (varType v)
goCo (AxiomInstCo _ _ args) = goCos args
goCo (UnivCo p _ t1 t2) = goProv p `unionVarSet` go t1 `unionVarSet` go t2
goCo (SymCo co) = goCo co
goCo (TransCo co1 co2) = goCo co1 `unionVarSet` goCo co2
goCo (NthCo _ co) = goCo co
goCo (LRCo _ co) = goCo co
goCo (InstCo co arg) = goCo co `unionVarSet` goCo arg
goCo (CoherenceCo c1 c2) = goCo c1 `unionVarSet` goCo c2
goCo (KindCo co) = goCo co
goCo (SubCo co) = goCo co
goCo (AxiomRuleCo _ c) = goCos c
goCos cos = foldr (unionVarSet . goCo) emptyVarSet cos
goProv UnsafeCoerceProv = emptyVarSet
goProv (PhantomProv kco) = goCo kco
goProv (ProofIrrelProv kco) = goCo kco
goProv (PluginProv _) = emptyVarSet
goProv (HoleProv _) = emptyVarSet
exactTyCoVarsOfTypes :: [Type] -> TyVarSet
exactTyCoVarsOfTypes tys = mapUnionVarSet exactTyCoVarsOfType tys
allBoundVariables :: Type -> TyVarSet
allBoundVariables ty = runFVSet $ go ty
where
go :: Type -> FV
go (TyVarTy tv) = go (tyVarKind tv)
go (TyConApp _ tys) = mapUnionFV go tys
go (AppTy t1 t2) = go t1 `unionFV` go t2
go (ForAllTy (Anon t1) t2) = go t1 `unionFV` go t2
go (ForAllTy (Named tv _) t2) = oneVar tv `unionFV`
go (tyVarKind tv) `unionFV` go t2
go (LitTy {}) = noVars
go (CastTy ty _) = go ty
go (CoercionTy {}) = noVars
allBoundVariabless :: [Type] -> TyVarSet
allBoundVariabless = mapUnionVarSet allBoundVariables
isTouchableOrFmv :: TcLevel -> TcTyVar -> Bool
isTouchableOrFmv ctxt_tclvl tv
= ASSERT2( isTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
MetaTv { mtv_tclvl = tv_tclvl, mtv_info = info }
-> ASSERT2( checkTcLevelInvariant ctxt_tclvl tv_tclvl,
ppr tv $$ ppr tv_tclvl $$ ppr ctxt_tclvl )
case info of
FlatMetaTv -> True
_ -> tv_tclvl `sameDepthAs` ctxt_tclvl
_ -> False
isTouchableMetaTyVar :: TcLevel -> TcTyVar -> Bool
isTouchableMetaTyVar ctxt_tclvl tv
| isTyVar tv
= ASSERT2( isTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
MetaTv { mtv_tclvl = tv_tclvl }
-> ASSERT2( checkTcLevelInvariant ctxt_tclvl tv_tclvl,
ppr tv $$ ppr tv_tclvl $$ ppr ctxt_tclvl )
tv_tclvl `sameDepthAs` ctxt_tclvl
_ -> False
| otherwise = False
isFloatedTouchableMetaTyVar :: TcLevel -> TcTyVar -> Bool
isFloatedTouchableMetaTyVar ctxt_tclvl tv
| isTyVar tv
= ASSERT2( isTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
MetaTv { mtv_tclvl = tv_tclvl } -> tv_tclvl `strictlyDeeperThan` ctxt_tclvl
_ -> False
| otherwise = False
isImmutableTyVar :: TyVar -> Bool
isImmutableTyVar tv
| isTcTyVar tv = isSkolemTyVar tv
| otherwise = True
isTyConableTyVar, isSkolemTyVar, isOverlappableTyVar,
isMetaTyVar, isAmbiguousTyVar,
isFmvTyVar, isFskTyVar, isFlattenTyVar :: TcTyVar -> Bool
isTyConableTyVar tv
| isTyVar tv
= ASSERT2( isTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
MetaTv { mtv_info = SigTv } -> False
_ -> True
| otherwise = True
isFmvTyVar tv
= ASSERT2( isTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
MetaTv { mtv_info = FlatMetaTv } -> True
_ -> False
isFlattenTyVar tv
= ASSERT2( isTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
FlatSkol {} -> True
MetaTv { mtv_info = FlatMetaTv } -> True
_ -> False
isFskTyVar tv
= ASSERT2( isTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
FlatSkol {} -> True
_ -> False
isSkolemTyVar tv
= ASSERT2( isTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
MetaTv {} -> False
_other -> True
isOverlappableTyVar tv
| isTyVar tv
= ASSERT2( isTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
SkolemTv overlappable -> overlappable
_ -> False
| otherwise = False
isMetaTyVar tv
| isTyVar tv
= ASSERT2( isTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
MetaTv {} -> True
_ -> False
| otherwise = False
isAmbiguousTyVar tv
| isTyVar tv
= case tcTyVarDetails tv of
MetaTv {} -> True
RuntimeUnk {} -> True
_ -> False
| otherwise = False
isMetaTyVarTy :: TcType -> Bool
isMetaTyVarTy (TyVarTy tv) = isMetaTyVar tv
isMetaTyVarTy _ = False
metaTyVarInfo :: TcTyVar -> MetaInfo
metaTyVarInfo tv
= case tcTyVarDetails tv of
MetaTv { mtv_info = info } -> info
_ -> pprPanic "metaTyVarInfo" (ppr tv)
metaTyVarTcLevel :: TcTyVar -> TcLevel
metaTyVarTcLevel tv
= case tcTyVarDetails tv of
MetaTv { mtv_tclvl = tclvl } -> tclvl
_ -> pprPanic "metaTyVarTcLevel" (ppr tv)
metaTyVarTcLevel_maybe :: TcTyVar -> Maybe TcLevel
metaTyVarTcLevel_maybe tv
= case tcTyVarDetails tv of
MetaTv { mtv_tclvl = tclvl } -> Just tclvl
_ -> Nothing
setMetaTyVarTcLevel :: TcTyVar -> TcLevel -> TcTyVar
setMetaTyVarTcLevel tv tclvl
= case tcTyVarDetails tv of
details@(MetaTv {}) -> setTcTyVarDetails tv (details { mtv_tclvl = tclvl })
_ -> pprPanic "metaTyVarTcLevel" (ppr tv)
isSigTyVar :: Var -> Bool
isSigTyVar tv
= case tcTyVarDetails tv of
MetaTv { mtv_info = SigTv } -> True
_ -> False
metaTvRef :: TyVar -> IORef MetaDetails
metaTvRef tv
= case tcTyVarDetails tv of
MetaTv { mtv_ref = ref } -> ref
_ -> pprPanic "metaTvRef" (ppr tv)
isFlexi, isIndirect :: MetaDetails -> Bool
isFlexi Flexi = True
isFlexi _ = False
isIndirect (Indirect _) = True
isIndirect _ = False
isRuntimeUnkSkol :: TyVar -> Bool
isRuntimeUnkSkol x
| isTcTyVar x, RuntimeUnk <- tcTyVarDetails x = True
| otherwise = False
mkSigmaTy :: [TyBinder] -> [PredType] -> Type -> Type
mkSigmaTy bndrs theta tau = mkForAllTys bndrs (mkPhiTy theta tau)
mkInvSigmaTy :: [TyVar] -> [PredType] -> Type -> Type
mkInvSigmaTy tyvars
= mkSigmaTy (mkNamedBinders Invisible tyvars)
mkSpecSigmaTy :: [TyVar] -> [PredType] -> Type -> Type
mkSpecSigmaTy tyvars
= mkSigmaTy (mkNamedBinders Specified tyvars)
mkPhiTy :: [PredType] -> Type -> Type
mkPhiTy = mkFunTys
isTauTy :: Type -> Bool
isTauTy ty | Just ty' <- coreView ty = isTauTy ty'
isTauTy (TyVarTy _) = True
isTauTy (LitTy {}) = True
isTauTy (TyConApp tc tys) = all isTauTy tys && isTauTyCon tc
isTauTy (AppTy a b) = isTauTy a && isTauTy b
isTauTy (ForAllTy (Anon a) b) = isTauTy a && isTauTy b
isTauTy (ForAllTy {}) = False
isTauTy (CastTy _ _) = False
isTauTy (CoercionTy _) = False
isTauTyCon :: TyCon -> Bool
isTauTyCon tc
| Just (_, rhs) <- synTyConDefn_maybe tc = isTauTy rhs
| otherwise = True
getDFunTyKey :: Type -> OccName
getDFunTyKey ty | Just ty' <- coreView ty = getDFunTyKey ty'
getDFunTyKey (TyVarTy tv) = getOccName tv
getDFunTyKey (TyConApp tc _) = getOccName tc
getDFunTyKey (LitTy x) = getDFunTyLitKey x
getDFunTyKey (AppTy fun _) = getDFunTyKey fun
getDFunTyKey (ForAllTy (Anon _) _) = getOccName funTyCon
getDFunTyKey (ForAllTy (Named {}) t) = getDFunTyKey t
getDFunTyKey (CastTy ty _) = getDFunTyKey ty
getDFunTyKey t@(CoercionTy _) = pprPanic "getDFunTyKey" (ppr t)
getDFunTyLitKey :: TyLit -> OccName
getDFunTyLitKey (NumTyLit n) = mkOccName Name.varName (show n)
getDFunTyLitKey (StrTyLit n) = mkOccName Name.varName (show n)
mkNakedTyConApp :: TyCon -> [Type] -> Type
mkNakedTyConApp tc tys = TyConApp tc tys
mkNakedAppTys :: Type -> [Type] -> Type
mkNakedAppTys ty1 [] = ty1
mkNakedAppTys (TyConApp tc tys1) tys2 = mkNakedTyConApp tc (tys1 ++ tys2)
mkNakedAppTys ty1 tys2 = foldl AppTy ty1 tys2
mkNakedAppTy :: Type -> Type -> Type
mkNakedAppTy ty1 ty2 = mkNakedAppTys ty1 [ty2]
mkNakedCastTy :: Type -> Coercion -> Type
mkNakedCastTy = CastTy
tcSplitPiTys :: Type -> ([TyBinder], Type)
tcSplitPiTys = splitPiTys
tcSplitForAllTy_maybe :: Type -> Maybe (TyBinder, Type)
tcSplitForAllTy_maybe ty | Just ty' <- coreView ty = tcSplitForAllTy_maybe ty'
tcSplitForAllTy_maybe (ForAllTy tv ty) = Just (tv, ty)
tcSplitForAllTy_maybe _ = Nothing
tcSplitForAllTys :: Type -> ([TyVar], Type)
tcSplitForAllTys = splitForAllTys
tcSplitNamedPiTys :: Type -> ([TyBinder], Type)
tcSplitNamedPiTys = splitNamedPiTys
tcIsForAllTy :: Type -> Bool
tcIsForAllTy ty | Just ty' <- coreView ty = tcIsForAllTy ty'
tcIsForAllTy (ForAllTy (Named {}) _) = True
tcIsForAllTy _ = False
tcSplitPredFunTy_maybe :: Type -> Maybe (PredType, Type)
tcSplitPredFunTy_maybe ty
| Just ty' <- coreView ty = tcSplitPredFunTy_maybe ty'
tcSplitPredFunTy_maybe (ForAllTy (Anon arg) res)
| isPredTy arg = Just (arg, res)
tcSplitPredFunTy_maybe _
= Nothing
tcSplitPhiTy :: Type -> (ThetaType, Type)
tcSplitPhiTy ty
= split ty []
where
split ty ts
= case tcSplitPredFunTy_maybe ty of
Just (pred, ty) -> split ty (pred:ts)
Nothing -> (reverse ts, ty)
tcSplitSigmaTy :: Type -> ([TyVar], ThetaType, Type)
tcSplitSigmaTy ty = case tcSplitForAllTys ty of
(tvs, rho) -> case tcSplitPhiTy rho of
(theta, tau) -> (tvs, theta, tau)
tcDeepSplitSigmaTy_maybe
:: TcSigmaType -> Maybe ([TcType], [TyVar], ThetaType, TcSigmaType)
tcDeepSplitSigmaTy_maybe ty
| Just (arg_ty, res_ty) <- tcSplitFunTy_maybe ty
, Just (arg_tys, tvs, theta, rho) <- tcDeepSplitSigmaTy_maybe res_ty
= Just (arg_ty:arg_tys, tvs, theta, rho)
| (tvs, theta, rho) <- tcSplitSigmaTy ty
, not (null tvs && null theta)
= Just ([], tvs, theta, rho)
| otherwise = Nothing
tcTyConAppTyCon :: Type -> TyCon
tcTyConAppTyCon ty = case tcSplitTyConApp_maybe ty of
Just (tc, _) -> tc
Nothing -> pprPanic "tcTyConAppTyCon" (pprType ty)
tcTyConAppArgs :: Type -> [Type]
tcTyConAppArgs ty = case tcSplitTyConApp_maybe ty of
Just (_, args) -> args
Nothing -> pprPanic "tcTyConAppArgs" (pprType ty)
tcSplitTyConApp :: Type -> (TyCon, [Type])
tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of
Just stuff -> stuff
Nothing -> pprPanic "tcSplitTyConApp" (pprType ty)
tcSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
tcSplitTyConApp_maybe ty | Just ty' <- coreView ty = tcSplitTyConApp_maybe ty'
tcSplitTyConApp_maybe ty = tcRepSplitTyConApp_maybe ty
tcRepSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
tcRepSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
tcRepSplitTyConApp_maybe (ForAllTy (Anon arg) res) = Just (funTyCon, [arg,res])
tcRepSplitTyConApp_maybe _ = Nothing
tcSplitFunTys :: Type -> ([Type], Type)
tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
Nothing -> ([], ty)
Just (arg,res) -> (arg:args, res')
where
(args,res') = tcSplitFunTys res
tcSplitFunTy_maybe :: Type -> Maybe (Type, Type)
tcSplitFunTy_maybe ty | Just ty' <- coreView ty = tcSplitFunTy_maybe ty'
tcSplitFunTy_maybe (ForAllTy (Anon arg) res)
| not (isPredTy arg) = Just (arg, res)
tcSplitFunTy_maybe _ = Nothing
tcSplitFunTysN
:: TcRhoType
-> Arity
-> ([TcSigmaType],
TcSigmaType)
tcSplitFunTysN ty n_args
| n_args == 0
= ([], ty)
| Just (arg,res) <- tcSplitFunTy_maybe ty
= case tcSplitFunTysN res (n_args 1) of
(args, res) -> (arg:args, res)
| otherwise
= ([], ty)
tcSplitFunTy :: Type -> (Type, Type)
tcSplitFunTy ty = expectJust "tcSplitFunTy" (tcSplitFunTy_maybe ty)
tcFunArgTy :: Type -> Type
tcFunArgTy ty = fst (tcSplitFunTy ty)
tcFunResultTy :: Type -> Type
tcFunResultTy ty = snd (tcSplitFunTy ty)
tcSplitAppTy_maybe :: Type -> Maybe (Type, Type)
tcSplitAppTy_maybe ty | Just ty' <- coreView ty = tcSplitAppTy_maybe ty'
tcSplitAppTy_maybe ty = tcRepSplitAppTy_maybe ty
tcSplitAppTy :: Type -> (Type, Type)
tcSplitAppTy ty = case tcSplitAppTy_maybe ty of
Just stuff -> stuff
Nothing -> pprPanic "tcSplitAppTy" (pprType ty)
tcSplitAppTys :: Type -> (Type, [Type])
tcSplitAppTys ty
= go ty []
where
go ty args = case tcSplitAppTy_maybe ty of
Just (ty', arg) -> go ty' (arg:args)
Nothing -> (ty,args)
tcGetTyVar_maybe :: Type -> Maybe TyVar
tcGetTyVar_maybe ty | Just ty' <- coreView ty = tcGetTyVar_maybe ty'
tcGetTyVar_maybe (TyVarTy tv) = Just tv
tcGetTyVar_maybe _ = Nothing
tcGetTyVar :: String -> Type -> TyVar
tcGetTyVar msg ty = expectJust msg (tcGetTyVar_maybe ty)
tcIsTyVarTy :: Type -> Bool
tcIsTyVarTy ty | Just ty' <- coreView ty = tcIsTyVarTy ty'
tcIsTyVarTy (CastTy ty _) = tcIsTyVarTy ty
tcIsTyVarTy (TyVarTy _) = True
tcIsTyVarTy _ = False
tcSplitDFunTy :: Type -> ([TyVar], [Type], Class, [Type])
tcSplitDFunTy ty
= case tcSplitForAllTys ty of { (tvs, rho) ->
case splitFunTys rho of { (theta, tau) ->
case tcSplitDFunHead tau of { (clas, tys) ->
(tvs, theta, clas, tys) }}}
tcSplitDFunHead :: Type -> (Class, [Type])
tcSplitDFunHead = getClassPredTys
tcEqKind :: TcKind -> TcKind -> Bool
tcEqKind = tcEqType
tcEqType :: TcType -> TcType -> Bool
tcEqType ty1 ty2
= isNothing (tc_eq_type coreView ki1 ki2) &&
isNothing (tc_eq_type coreView ty1 ty2)
where
ki1 = typeKind ty1
ki2 = typeKind ty2
tcEqTypeNoKindCheck :: TcType -> TcType -> Bool
tcEqTypeNoKindCheck ty1 ty2
= isNothing $ tc_eq_type coreView ty1 ty2
tcEqTypeVis :: TcType -> TcType -> Maybe VisibilityFlag
tcEqTypeVis ty1 ty2
= tc_eq_type coreView ty1 ty2 <!> invis (tc_eq_type coreView ki1 ki2)
where
ki1 = typeKind ty1
ki2 = typeKind ty2
invis :: Maybe VisibilityFlag -> Maybe VisibilityFlag
invis = fmap (const Invisible)
(<!>) :: Maybe VisibilityFlag -> Maybe VisibilityFlag -> Maybe VisibilityFlag
Nothing <!> x = x
Just Visible <!> _ = Just Visible
Just _inv <!> Just Visible = Just Visible
Just inv <!> _ = Just inv
infixr 3 <!>
tc_eq_type :: (TcType -> Maybe TcType)
-> Type -> Type -> Maybe VisibilityFlag
tc_eq_type view_fun orig_ty1 orig_ty2 = go Visible orig_env orig_ty1 orig_ty2
where
go vis env t1 t2 | Just t1' <- view_fun t1 = go vis env t1' t2
go vis env t1 t2 | Just t2' <- view_fun t2 = go vis env t1 t2'
go vis env (TyVarTy tv1) (TyVarTy tv2)
= check vis $ rnOccL env tv1 == rnOccR env tv2
go vis _ (LitTy lit1) (LitTy lit2)
= check vis $ lit1 == lit2
go vis env (ForAllTy (Named tv1 vis1) ty1)
(ForAllTy (Named tv2 vis2) ty2)
= go vis1 env (tyVarKind tv1) (tyVarKind tv2)
<!> go vis (rnBndr2 env tv1 tv2) ty1 ty2
<!> check vis (vis1 == vis2)
go vis env (ForAllTy (Anon arg1) res1) (ForAllTy (Anon arg2) res2)
= go vis env arg1 arg2 <!> go vis env res1 res2
go vis env (AppTy s1 t1) ty2
| Just (s2, t2) <- tcRepSplitAppTy_maybe ty2
= go vis env s1 s2 <!> go vis env t1 t2
go vis env ty1 (AppTy s2 t2)
| Just (s1, t1) <- tcRepSplitAppTy_maybe ty1
= go vis env s1 s2 <!> go vis env t1 t2
go vis env (TyConApp tc1 ts1) (TyConApp tc2 ts2)
= check vis (tc1 == tc2) <!> gos (tc_vis vis tc1) env ts1 ts2
go vis env (CastTy t1 _) t2 = go vis env t1 t2
go vis env t1 (CastTy t2 _) = go vis env t1 t2
go _ _ (CoercionTy {}) (CoercionTy {}) = Nothing
go vis _ _ _ = Just vis
gos _ _ [] [] = Nothing
gos (v:vs) env (t1:ts1) (t2:ts2) = go v env t1 t2 <!> gos vs env ts1 ts2
gos (v:_) _ _ _ = Just v
gos _ _ _ _ = panic "tc_eq_type"
tc_vis :: VisibilityFlag -> TyCon -> [VisibilityFlag]
tc_vis Visible tc = viss ++ repeat Visible
where
bndrs = tyConBinders tc
viss = map binderVisibility bndrs
tc_vis vis _ = repeat vis
check :: VisibilityFlag -> Bool -> Maybe VisibilityFlag
check _ True = Nothing
check vis False = Just vis
orig_env = mkRnEnv2 $ mkInScopeSet $ tyCoVarsOfTypes [orig_ty1, orig_ty2]
pickyEqType :: TcType -> TcType -> Bool
pickyEqType ty1 ty2
= isNothing $
tc_eq_type (const Nothing) ty1 ty2
data OccCheckResult a
= OC_OK a
| OC_Forall
| OC_NonTyVar
| OC_Occurs
instance Functor OccCheckResult where
fmap = liftM
instance Applicative OccCheckResult where
pure = OC_OK
(<*>) = ap
instance Monad OccCheckResult where
return = pure
OC_OK x >>= k = k x
OC_Forall >>= _ = OC_Forall
OC_NonTyVar >>= _ = OC_NonTyVar
OC_Occurs >>= _ = OC_Occurs
occurCheckExpand :: DynFlags -> TcTyVar -> Type -> OccCheckResult Type
occurCheckExpand dflags tv ty
| MetaTv { mtv_info = SigTv } <- details
= go_sig_tv ty
| fast_check ty = return ty
| otherwise = go emptyVarEnv ty
where
details = tcTyVarDetails tv
impredicative = canUnifyWithPolyType dflags details
go_sig_tv ty@(TyVarTy tv')
| fast_check (tyVarKind tv') = return ty
| otherwise = do { k' <- go emptyVarEnv (tyVarKind tv')
; return (mkTyVarTy (setTyVarKind tv' k')) }
go_sig_tv ty | Just ty' <- coreView ty = go_sig_tv ty'
go_sig_tv _ = OC_NonTyVar
fast_check (LitTy {}) = True
fast_check (TyVarTy tv') = tv /= tv' && fast_check (tyVarKind tv')
fast_check (TyConApp tc tys) = all fast_check tys
&& (isTauTyCon tc || impredicative)
fast_check (ForAllTy (Anon a) r) = fast_check a && fast_check r
fast_check (AppTy fun arg) = fast_check fun && fast_check arg
fast_check (ForAllTy (Named tv' _) ty)
= impredicative
&& fast_check (tyVarKind tv')
&& (tv == tv' || fast_check ty)
fast_check (CastTy ty co) = fast_check ty && fast_check_co co
fast_check (CoercionTy co) = fast_check_co co
fast_check_co co = not (tv `elemVarSet` tyCoVarsOfCo co)
go :: VarEnv TyVar
-> Type -> OccCheckResult Type
go env (TyVarTy tv')
| tv == tv' = OC_Occurs
| Just tv'' <- lookupVarEnv env tv' = return (mkTyVarTy tv'')
| otherwise = do { k' <- go env (tyVarKind tv')
; return (mkTyVarTy $
setTyVarKind tv' k') }
go _ ty@(LitTy {}) = return ty
go env (AppTy ty1 ty2) = do { ty1' <- go env ty1
; ty2' <- go env ty2
; return (mkAppTy ty1' ty2') }
go env (ForAllTy (Anon ty1) ty2)
= do { ty1' <- go env ty1
; ty2' <- go env ty2
; return (mkFunTy ty1' ty2') }
go env ty@(ForAllTy (Named tv' vis) body_ty)
| not impredicative = OC_Forall
| tv == tv' = return ty
| otherwise = do { ki' <- go env ki
; let tv'' = setTyVarKind tv' ki'
env' = extendVarEnv env tv' tv''
; body' <- go env' body_ty
; return (ForAllTy (Named tv'' vis) body') }
where ki = tyVarKind tv'
go env ty@(TyConApp tc tys)
= case do { tys <- mapM (go env) tys
; return (mkTyConApp tc tys) } of
OC_OK ty
| impredicative || isTauTyCon tc
-> return ty
| otherwise
-> OC_Forall
bad | Just ty' <- coreView ty -> go env ty'
| otherwise -> bad
go env (CastTy ty co) = do { ty' <- go env ty
; co' <- go_co env co
; return (mkCastTy ty' co') }
go env (CoercionTy co) = do { co' <- go_co env co
; return (mkCoercionTy co') }
go_co env (Refl r ty) = do { ty' <- go env ty
; return (mkReflCo r ty') }
go_co env (TyConAppCo r tc args) = do { args' <- mapM (go_co env) args
; return (mkTyConAppCo r tc args') }
go_co env (AppCo co arg) = do { co' <- go_co env co
; arg' <- go_co env arg
; return (mkAppCo co' arg') }
go_co env co@(ForAllCo tv' kind_co body_co)
| not impredicative = OC_Forall
| tv == tv' = return co
| otherwise = do { kind_co' <- go_co env kind_co
; let tv'' = setTyVarKind tv' $
pFst (coercionKind kind_co')
env' = extendVarEnv env tv' tv''
; body' <- go_co env' body_co
; return (ForAllCo tv'' kind_co' body') }
go_co env (CoVarCo c) = do { k' <- go env (varType c)
; return (mkCoVarCo (setVarType c k')) }
go_co env (AxiomInstCo ax ind args) = do { args' <- mapM (go_co env) args
; return (mkAxiomInstCo ax ind args') }
go_co env (UnivCo p r ty1 ty2) = do { p' <- go_prov env p
; ty1' <- go env ty1
; ty2' <- go env ty2
; return (mkUnivCo p' r ty1' ty2') }
go_co env (SymCo co) = do { co' <- go_co env co
; return (mkSymCo co') }
go_co env (TransCo co1 co2) = do { co1' <- go_co env co1
; co2' <- go_co env co2
; return (mkTransCo co1' co2') }
go_co env (NthCo n co) = do { co' <- go_co env co
; return (mkNthCo n co') }
go_co env (LRCo lr co) = do { co' <- go_co env co
; return (mkLRCo lr co') }
go_co env (InstCo co arg) = do { co' <- go_co env co
; arg' <- go_co env arg
; return (mkInstCo co' arg') }
go_co env (CoherenceCo co1 co2) = do { co1' <- go_co env co1
; co2' <- go_co env co2
; return (mkCoherenceCo co1' co2') }
go_co env (KindCo co) = do { co' <- go_co env co
; return (mkKindCo co') }
go_co env (SubCo co) = do { co' <- go_co env co
; return (mkSubCo co') }
go_co env (AxiomRuleCo ax cs) = do { cs' <- mapM (go_co env) cs
; return (mkAxiomRuleCo ax cs') }
go_prov _ UnsafeCoerceProv = return UnsafeCoerceProv
go_prov env (PhantomProv co) = PhantomProv <$> go_co env co
go_prov env (ProofIrrelProv co) = ProofIrrelProv <$> go_co env co
go_prov _ p@(PluginProv _) = return p
go_prov _ p@(HoleProv _) = return p
canUnifyWithPolyType :: DynFlags -> TcTyVarDetails -> Bool
canUnifyWithPolyType dflags details
= case details of
MetaTv { mtv_info = SigTv } -> False
MetaTv { mtv_info = TauTv } -> xopt LangExt.ImpredicativeTypes dflags
_other -> True
isTyVarClassPred :: PredType -> Bool
isTyVarClassPred ty = case getClassPredTys_maybe ty of
Just (_, tys) -> all isTyVarTy tys
_ -> False
checkValidClsArgs :: Bool -> Class -> [KindOrType] -> Bool
checkValidClsArgs flexible_contexts cls kts
| flexible_contexts = True
| otherwise = all hasTyVarHead tys
where
tys = filterOutInvisibleTypes (classTyCon cls) kts
hasTyVarHead :: Type -> Bool
hasTyVarHead ty
| tcIsTyVarTy ty = True
| otherwise
= case tcSplitAppTy_maybe ty of
Just (ty, _) -> hasTyVarHead ty
Nothing -> False
evVarPred_maybe :: EvVar -> Maybe PredType
evVarPred_maybe v = if isPredTy ty then Just ty else Nothing
where ty = varType v
evVarPred :: EvVar -> PredType
evVarPred var
| debugIsOn
= case evVarPred_maybe var of
Just pred -> pred
Nothing -> pprPanic "tcEvVarPred" (ppr var <+> ppr (varType var))
| otherwise
= varType var
pickQuantifiablePreds
:: TyVarSet
-> TcThetaType
-> TcThetaType
-> TcThetaType
pickQuantifiablePreds qtvs annotated_theta theta
= let flex_ctxt = True in
filter (pick_me flex_ctxt) theta
where
pick_me flex_ctxt pred
= case classifyPredType pred of
ClassPred cls tys
| Just str <- isCallStackPred pred
-> str `elem` givenStks
| isIPClass cls -> True
| otherwise
-> pick_cls_pred flex_ctxt cls tys
EqPred ReprEq ty1 ty2 -> pick_cls_pred flex_ctxt coercibleClass [ty1, ty2]
EqPred NomEq ty1 ty2 -> quant_fun ty1 || quant_fun ty2
IrredPred ty -> tyCoVarsOfType ty `intersectsVarSet` qtvs
givenStks = [ str | (str, ty) <- mapMaybe isIPPred_maybe annotated_theta
, isCallStackTy ty ]
pick_cls_pred flex_ctxt cls tys
= tyCoVarsOfTypes tys `intersectsVarSet` qtvs
&& (checkValidClsArgs flex_ctxt cls tys)
quant_fun ty
= case tcSplitTyConApp_maybe ty of
Just (tc, tys) | isTypeFamilyTyCon tc
-> tyCoVarsOfTypes tys `intersectsVarSet` qtvs
_ -> False
type PredWithSCs = (PredType, [PredType])
mkMinimalBySCs :: [PredType] -> [PredType]
mkMinimalBySCs ptys = go preds_with_scs []
where
preds_with_scs :: [PredWithSCs]
preds_with_scs = [ (pred, transSuperClasses pred)
| pred <- ptys ]
go :: [PredWithSCs]
-> [PredWithSCs]
-> [PredType]
go [] min_preds = map fst min_preds
go (work_item@(p,_) : work_list) min_preds
| p `in_cloud` work_list || p `in_cloud` min_preds
= go work_list min_preds
| otherwise
= go work_list (work_item : min_preds)
in_cloud :: PredType -> [PredWithSCs] -> Bool
in_cloud p ps = or [ p `eqType` p' | (_, scs) <- ps, p' <- scs ]
transSuperClasses :: PredType -> [PredType]
transSuperClasses p
= go emptyNameSet p
where
go :: NameSet -> PredType -> [PredType]
go rec_clss p
| ClassPred cls tys <- classifyPredType p
, let cls_nm = className cls
, not (cls_nm `elemNameSet` rec_clss)
, let rec_clss' | isCTupleClass cls = rec_clss
| otherwise = rec_clss `extendNameSet` cls_nm
= [ p' | sc <- immSuperClasses cls tys
, p' <- sc : go rec_clss' sc ]
| otherwise
= []
immSuperClasses :: Class -> [Type] -> [PredType]
immSuperClasses cls tys
= substTheta (zipTvSubst tyvars tys) sc_theta
where
(tyvars,sc_theta,_,_) = classBigSig cls
isImprovementPred :: PredType -> Bool
isImprovementPred ty
= case classifyPredType ty of
EqPred NomEq t1 t2 -> not (t1 `tcEqType` t2)
EqPred ReprEq _ _ -> False
ClassPred cls _ -> classHasFds cls
IrredPred {} -> True
isSigmaTy :: TcType -> Bool
isSigmaTy ty | Just ty' <- coreView ty = isSigmaTy ty'
isSigmaTy (ForAllTy (Named {}) _) = True
isSigmaTy (ForAllTy (Anon a) _) = isPredTy a
isSigmaTy _ = False
isRhoTy :: TcType -> Bool
isRhoTy ty | Just ty' <- coreView ty = isRhoTy ty'
isRhoTy (ForAllTy (Named {}) _) = False
isRhoTy (ForAllTy (Anon a) r) = not (isPredTy a) && isRhoTy r
isRhoTy _ = True
isRhoExpTy :: ExpType -> Bool
isRhoExpTy (Check ty) = isRhoTy ty
isRhoExpTy (Infer {}) = True
isOverloadedTy :: Type -> Bool
isOverloadedTy ty | Just ty' <- coreView ty = isOverloadedTy ty'
isOverloadedTy (ForAllTy (Named {}) ty) = isOverloadedTy ty
isOverloadedTy (ForAllTy (Anon a) _) = isPredTy a
isOverloadedTy _ = False
isFloatTy, isDoubleTy, isIntegerTy, isIntTy, isWordTy, isBoolTy,
isUnitTy, isCharTy, isAnyTy :: Type -> Bool
isFloatTy = is_tc floatTyConKey
isDoubleTy = is_tc doubleTyConKey
isIntegerTy = is_tc integerTyConKey
isIntTy = is_tc intTyConKey
isWordTy = is_tc wordTyConKey
isBoolTy = is_tc boolTyConKey
isUnitTy = is_tc unitTyConKey
isCharTy = is_tc charTyConKey
isAnyTy = is_tc anyTyConKey
isFloatingTy :: Type -> Bool
isFloatingTy ty = isFloatTy ty || isDoubleTy ty
isStringTy :: Type -> Bool
isStringTy ty
= case tcSplitTyConApp_maybe ty of
Just (tc, [arg_ty]) -> tc == listTyCon && isCharTy arg_ty
_ -> False
isCallStackTy :: Type -> Bool
isCallStackTy ty
| Just tc <- tyConAppTyCon_maybe ty
= tc `hasKey` callStackTyConKey
| otherwise
= False
isCallStackPred :: PredType -> Maybe FastString
isCallStackPred pred
| Just (str, ty) <- isIPPred_maybe pred
, isCallStackTy ty
= Just str
| otherwise
= Nothing
is_tc :: Unique -> Type -> Bool
is_tc uniq ty = case tcSplitTyConApp_maybe ty of
Just (tc, _) -> uniq == getUnique tc
Nothing -> False
isTyVarExposed :: TcTyVar -> TcType -> Bool
isTyVarExposed tv (TyVarTy tv') = tv == tv'
isTyVarExposed tv (TyConApp tc tys)
| isNewTyCon tc = any (isTyVarExposed tv) tys
| otherwise = False
isTyVarExposed _ (LitTy {}) = False
isTyVarExposed tv (AppTy fun arg) = isTyVarExposed tv fun
|| isTyVarExposed tv arg
isTyVarExposed _ (ForAllTy {}) = False
isTyVarExposed tv (CastTy ty _) = isTyVarExposed tv ty
isTyVarExposed _ (CoercionTy {}) = False
isTyVarUnderDatatype :: TcTyVar -> TcType -> Bool
isTyVarUnderDatatype tv = go False
where
go under_dt ty | Just ty' <- coreView ty = go under_dt ty'
go under_dt (TyVarTy tv') = under_dt && (tv == tv')
go under_dt (TyConApp tc tys) = let under_dt' = under_dt ||
isGenerativeTyCon tc
Representational
in any (go under_dt') tys
go _ (LitTy {}) = False
go _ (ForAllTy (Anon arg) res) = go True arg || go True res
go under_dt (AppTy fun arg) = go under_dt fun || go under_dt arg
go under_dt (ForAllTy (Named tv' _) inner_ty)
| tv' == tv = False
| otherwise = go under_dt inner_ty
go under_dt (CastTy ty _) = go under_dt ty
go _ (CoercionTy {}) = False
isRigidTy :: TcType -> Bool
isRigidTy ty
| Just (tc,_) <- tcSplitTyConApp_maybe ty = isGenerativeTyCon tc Nominal
| Just {} <- tcSplitAppTy_maybe ty = True
| isForAllTy ty = True
| otherwise = False
isRigidEqPred :: TcLevel -> PredTree -> Bool
isRigidEqPred tc_lvl (EqPred NomEq ty1 _)
| Just tv1 <- tcGetTyVar_maybe ty1
= ASSERT2( isTcTyVar tv1, ppr tv1 )
not (isMetaTyVar tv1) || isTouchableMetaTyVar tc_lvl tv1
| otherwise
= True
isRigidEqPred _ _ = False
toTcType :: Type -> TcType
toTcType = runIdentity . to_tc_type emptyVarSet
toTcTypeBag :: Bag EvVar -> Bag EvVar
toTcTypeBag evvars = mapBag (\tv -> setTyVarKind tv (toTcType (tyVarKind tv))) evvars
to_tc_mapper :: TyCoMapper VarSet Identity
to_tc_mapper
= TyCoMapper { tcm_smart = False
, tcm_tyvar = tyvar
, tcm_covar = covar
, tcm_hole = hole
, tcm_tybinder = tybinder }
where
tyvar :: VarSet -> TyVar -> Identity Type
tyvar ftvs tv
| Just var <- lookupVarSet ftvs tv = return $ TyVarTy var
| isTcTyVar tv = TyVarTy <$> updateTyVarKindM (to_tc_type ftvs) tv
| otherwise
= do { kind' <- to_tc_type ftvs (tyVarKind tv)
; return $ TyVarTy $ mkTcTyVar (tyVarName tv) kind' vanillaSkolemTv }
covar :: VarSet -> CoVar -> Identity Coercion
covar ftvs cv
| Just var <- lookupVarSet ftvs cv = return $ CoVarCo var
| otherwise = CoVarCo <$> updateVarTypeM (to_tc_type ftvs) cv
hole :: VarSet -> CoercionHole -> Role -> Type -> Type
-> Identity Coercion
hole ftvs h r t1 t2 = mkHoleCo h r <$> to_tc_type ftvs t1
<*> to_tc_type ftvs t2
tybinder :: VarSet -> TyVar -> VisibilityFlag -> Identity (VarSet, TyVar)
tybinder ftvs tv _vis = do { kind' <- to_tc_type ftvs (tyVarKind tv)
; let tv' = mkTcTyVar (tyVarName tv) kind'
vanillaSkolemTv
; return (ftvs `extendVarSet` tv', tv') }
to_tc_type :: VarSet -> Type -> Identity TcType
to_tc_type = mapType to_tc_mapper
deNoteType :: Type -> Type
deNoteType ty | Just ty' <- coreView ty = deNoteType ty'
deNoteType ty = ty
tcSplitIOType_maybe :: Type -> Maybe (TyCon, Type)
tcSplitIOType_maybe ty
= case tcSplitTyConApp_maybe ty of
Just (io_tycon, [io_res_ty])
| io_tycon `hasKey` ioTyConKey ->
Just (io_tycon, io_res_ty)
_ ->
Nothing
isFFITy :: Type -> Bool
isFFITy ty = isValid (checkRepTyCon legalFFITyCon ty)
isFFIArgumentTy :: DynFlags -> Safety -> Type -> Validity
isFFIArgumentTy dflags safety ty
= checkRepTyCon (legalOutgoingTyCon dflags safety) ty
isFFIExternalTy :: Type -> Validity
isFFIExternalTy ty = checkRepTyCon legalFEArgTyCon ty
isFFIImportResultTy :: DynFlags -> Type -> Validity
isFFIImportResultTy dflags ty
= checkRepTyCon (legalFIResultTyCon dflags) ty
isFFIExportResultTy :: Type -> Validity
isFFIExportResultTy ty = checkRepTyCon legalFEResultTyCon ty
isFFIDynTy :: Type -> Type -> Validity
isFFIDynTy expected ty
| Just (tc, [ty']) <- splitTyConApp_maybe ty
, tyConUnique tc `elem` [ptrTyConKey, funPtrTyConKey]
, eqType ty' expected
= IsValid
| otherwise
= NotValid (vcat [ text "Expected: Ptr/FunPtr" <+> pprParendType expected <> comma
, text " Actual:" <+> ppr ty ])
isFFILabelTy :: Type -> Validity
isFFILabelTy ty = checkRepTyCon ok ty
where
ok tc | tc `hasKey` funPtrTyConKey || tc `hasKey` ptrTyConKey
= IsValid
| otherwise
= NotValid (text "A foreign-imported address (via &foo) must have type (Ptr a) or (FunPtr a)")
isFFIPrimArgumentTy :: DynFlags -> Type -> Validity
isFFIPrimArgumentTy dflags ty
| isAnyTy ty = IsValid
| otherwise = checkRepTyCon (legalFIPrimArgTyCon dflags) ty
isFFIPrimResultTy :: DynFlags -> Type -> Validity
isFFIPrimResultTy dflags ty
| isAnyTy ty = IsValid
| otherwise = checkRepTyCon (legalFIPrimResultTyCon dflags) ty
isFunPtrTy :: Type -> Bool
isFunPtrTy ty
| Just (tc, [_]) <- splitTyConApp_maybe ty
= tc `hasKey` funPtrTyConKey
| otherwise
= False
checkRepTyCon :: (TyCon -> Validity) -> Type -> Validity
checkRepTyCon check_tc ty
= case splitTyConApp_maybe ty of
Just (tc, tys)
| isNewTyCon tc -> NotValid (hang msg 2 (mk_nt_reason tc tys $$ nt_fix))
| otherwise -> case check_tc tc of
IsValid -> IsValid
NotValid extra -> NotValid (msg $$ extra)
Nothing -> NotValid (quotes (ppr ty) <+> text "is not a data type")
where
msg = quotes (ppr ty) <+> text "cannot be marshalled in a foreign call"
mk_nt_reason tc tys
| null tys = text "because its data constructor is not in scope"
| otherwise = text "because the data constructor for"
<+> quotes (ppr tc) <+> text "is not in scope"
nt_fix = text "Possible fix: import the data constructor to bring it into scope"
legalFEArgTyCon :: TyCon -> Validity
legalFEArgTyCon tc
= boxedMarshalableTyCon tc
legalFIResultTyCon :: DynFlags -> TyCon -> Validity
legalFIResultTyCon dflags tc
| tc == unitTyCon = IsValid
| otherwise = marshalableTyCon dflags tc
legalFEResultTyCon :: TyCon -> Validity
legalFEResultTyCon tc
| tc == unitTyCon = IsValid
| otherwise = boxedMarshalableTyCon tc
legalOutgoingTyCon :: DynFlags -> Safety -> TyCon -> Validity
legalOutgoingTyCon dflags _ tc
= marshalableTyCon dflags tc
legalFFITyCon :: TyCon -> Validity
legalFFITyCon tc
| isUnliftedTyCon tc = IsValid
| tc == unitTyCon = IsValid
| otherwise = boxedMarshalableTyCon tc
marshalableTyCon :: DynFlags -> TyCon -> Validity
marshalableTyCon dflags tc
| isUnliftedTyCon tc
, not (isUnboxedTupleTyCon tc)
, case tyConPrimRep tc of
VoidRep -> False
_ -> True
= validIfUnliftedFFITypes dflags
| otherwise
= boxedMarshalableTyCon tc
boxedMarshalableTyCon :: TyCon -> Validity
boxedMarshalableTyCon tc
| getUnique tc `elem` [ intTyConKey, int8TyConKey, int16TyConKey
, int32TyConKey, int64TyConKey
, wordTyConKey, word8TyConKey, word16TyConKey
, word32TyConKey, word64TyConKey
, floatTyConKey, doubleTyConKey
, ptrTyConKey, funPtrTyConKey
, charTyConKey
, stablePtrTyConKey
, boolTyConKey
]
= IsValid
| otherwise = NotValid empty
legalFIPrimArgTyCon :: DynFlags -> TyCon -> Validity
legalFIPrimArgTyCon dflags tc
| isUnliftedTyCon tc
, not (isUnboxedTupleTyCon tc)
= validIfUnliftedFFITypes dflags
| otherwise
= NotValid unlifted_only
legalFIPrimResultTyCon :: DynFlags -> TyCon -> Validity
legalFIPrimResultTyCon dflags tc
| isUnliftedTyCon tc
, (isUnboxedTupleTyCon tc
|| case tyConPrimRep tc of
VoidRep -> False
_ -> True)
= validIfUnliftedFFITypes dflags
| otherwise
= NotValid unlifted_only
unlifted_only :: MsgDoc
unlifted_only = text "foreign import prim only accepts simple unlifted types"
validIfUnliftedFFITypes :: DynFlags -> Validity
validIfUnliftedFFITypes dflags
| xopt LangExt.UnliftedFFITypes dflags = IsValid
| otherwise = NotValid (text "To marshal unlifted types, use UnliftedFFITypes")
type TypeSize = IntWithInf
sizeType :: Type -> TypeSize
sizeType = go
where
go ty | Just exp_ty <- coreView ty = go exp_ty
go (TyVarTy {}) = 1
go (TyConApp tc tys)
| isTypeFamilyTyCon tc = infinity
| otherwise = sizeTypes (filterOutInvisibleTypes tc tys) + 1
go (LitTy {}) = 1
go (ForAllTy (Anon arg) res) = go arg + go res + 1
go (AppTy fun arg) = go fun + go arg
go (ForAllTy (Named tv vis) ty)
| Visible <- vis = go (tyVarKind tv) + go ty + 1
| otherwise = go ty + 1
go (CastTy ty _) = go ty
go (CoercionTy {}) = 0
sizeTypes :: [Type] -> TypeSize
sizeTypes tys = sum (map sizeType tys)