TcType, TcSigmaType, TcRhoType, TcTauType, TcPredType, TcThetaType,
TcTyVar, TcTyVarSet, TcKind,
+ BoxyTyVar, BoxySigmaType, BoxyRhoType, BoxyThetaType, BoxyType,
+
--------------------------------
-- MetaDetails
- TcTyVarDetails(..),
- MetaDetails(Flexi, Indirect), SkolemInfo(..), pprSkolemTyVar,
- isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isExistentialTyVar, skolemTvInfo, metaTvRef,
- isFlexi, isIndirect,
+ UserTypeCtxt(..), pprUserTypeCtxt,
+ TcTyVarDetails(..), BoxInfo(..), pprTcTyVarDetails,
+ MetaDetails(Flexi, Indirect), SkolemInfo(..), pprSkolTvBinding, pprSkolInfo,
+ isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isBoxyTyVar, isSigTyVar, isExistentialTyVar,
+ metaTvRef,
+ isFlexi, isIndirect,
--------------------------------
-- Builders
--------------------------------
-- Splitters
-- These are important because they do not look through newtypes
+ tcView,
tcSplitForAllTys, tcSplitPhiTy,
- tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy,
+ tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy, tcSplitFunTysN,
tcSplitTyConApp, tcSplitTyConApp_maybe, tcTyConAppTyCon, tcTyConAppArgs,
- tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, tcSplitSigmaTy,
- tcGetTyVar_maybe, tcGetTyVar,
+ tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys,
+ tcValidInstHeadTy, tcGetTyVar_maybe, tcGetTyVar,
+ tcSplitSigmaTy, tcMultiSplitSigmaTy,
---------------------------------
-- Predicates.
-- Again, newtypes are opaque
tcEqType, tcEqTypes, tcEqPred, tcCmpType, tcCmpTypes, tcCmpPred, tcEqTypeX,
- isSigmaTy, isOverloadedTy,
- isDoubleTy, isFloatTy, isIntTy,
+ isSigmaTy, isOverloadedTy, isRigidTy, isBoxyTy,
+ isDoubleTy, isFloatTy, isIntTy, isStringTy,
isIntegerTy, isAddrTy, isBoolTy, isUnitTy,
- isTauTy, tcIsTyVarTy, tcIsForAllTy,
+ isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy,
---------------------------------
-- Misc type manipulators
mkDictTy, tcSplitPredTy_maybe,
isPredTy, isDictTy, tcSplitDFunTy, tcSplitDFunHead, predTyUnique,
mkClassPred, isInheritablePred, isLinearPred, isIPPred, mkPredName,
+ dataConsStupidTheta, isRefineableTy,
---------------------------------
-- Foreign import and export
Type, PredType(..), ThetaType,
mkForAllTy, mkForAllTys,
mkFunTy, mkFunTys, zipFunTys,
- mkTyConApp, mkGenTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
+ mkTyConApp, mkAppTy, mkAppTys, applyTy, applyTys,
mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy, mkPredTys,
-- Type substitutions
TvSubst(..), -- Representation visible to a few friends
TvSubstEnv, emptyTvSubst,
- mkTvSubst, zipTvSubst, zipTopTvSubst, mkTopTvSubst,
- getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope,
- extendTvSubst, extendTvSubstList, isInScope,
+ mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst, notElemTvSubst,
+ getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope, lookupTyVar,
+ extendTvSubst, extendTvSubstList, isInScope, mkTvSubst, zipTyEnv,
substTy, substTys, substTyWith, substTheta, substTyVar, substTyVarBndr,
isUnLiftedType, -- Source types are always lifted
isPrimitiveType,
tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
- tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars,
- typeKind,
+ tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars, tidySkolemTyVar,
+ typeKind, tidyKind,
tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
+ tcTyVarsOfType, tcTyVarsOfTypes, exactTyVarsOfType, exactTyVarsOfTypes,
pprKind, pprParendKind,
pprType, pprParendType, pprTyThingCategory,
#include "HsVersions.h"
-- friends:
-import TypeRep ( Type(..), TyNote(..), funTyCon ) -- friend
+import TypeRep ( Type(..), funTyCon ) -- friend
import Type ( -- Re-exports
tyVarsOfType, tyVarsOfTypes, tyVarsOfPred,
mkArrowKinds, mkForAllTy, mkForAllTys,
defaultKind, isArgTypeKind, isOpenTypeKind,
mkFunTy, mkFunTys, zipFunTys,
- mkTyConApp, mkGenTyConApp, mkAppTy,
- mkAppTys, mkSynTy, applyTy, applyTys,
+ mkTyConApp, mkAppTy,
+ mkAppTys, applyTy, applyTys,
mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy,
mkPredTys, isUnLiftedType,
isUnboxedTupleType, isPrimitiveType,
tidyTopType, tidyType, tidyPred, tidyTypes,
tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
tidyTyVarBndr, tidyOpenTyVar,
- tidyOpenTyVars,
- isSubKind,
+ tidyOpenTyVars, tidyKind,
+ isSubKind, tcView,
tcEqType, tcEqTypes, tcCmpType, tcCmpTypes,
tcEqPred, tcCmpPred, tcEqTypeX,
TvSubst(..),
- TvSubstEnv, emptyTvSubst,
- mkTvSubst, zipTvSubst, zipTopTvSubst, mkTopTvSubst,
+ TvSubstEnv, emptyTvSubst, mkTvSubst, zipTyEnv,
+ mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst,
getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope,
- extendTvSubst, extendTvSubstList, isInScope,
- substTy, substTys, substTyWith, substTheta, substTyVar, substTyVarBndr,
+ extendTvSubst, extendTvSubstList, isInScope, notElemTvSubst,
+ substTy, substTys, substTyWith, substTheta,
+ substTyVar, substTyVarBndr, substPred, lookupTyVar,
typeKind, repType,
pprKind, pprParendKind,
pprType, pprParendType, pprTyThingCategory,
pprPred, pprTheta, pprThetaArrow, pprClassPred
)
-import TyCon ( TyCon, isUnLiftedTyCon, tyConUnique )
-import DataCon ( DataCon )
+import TyCon ( TyCon, isUnLiftedTyCon, isSynTyCon, synTyConDefn, tyConUnique )
+import DataCon ( DataCon, dataConStupidTheta, dataConResTys )
import Class ( Class )
-import Var ( TyVar, Id, isTcTyVar, tcTyVarDetails )
+import Var ( TyVar, Id, isTcTyVar, mkTcTyVar, tyVarName, tyVarKind, tcTyVarDetails )
import ForeignCall ( Safety, playSafe, DNType(..) )
+import Unify ( tcMatchTys )
import VarSet
-- others:
-import CmdLineOpts ( DynFlags, DynFlag( Opt_GlasgowExts ), dopt )
+import DynFlags ( DynFlags, DynFlag( Opt_GlasgowExts ), dopt )
import Name ( Name, NamedThing(..), mkInternalName, getSrcLoc )
import NameSet
+import VarEnv ( TidyEnv )
import OccName ( OccName, mkDictOcc )
import PrelNames -- Lots (e.g. in isFFIArgumentTy)
import TysWiredIn ( unitTyCon, charTyCon, listTyCon )
-import BasicTypes ( IPName(..), ipNameName )
+import BasicTypes ( IPName(..), Arity, ipNameName )
import SrcLoc ( SrcLoc, SrcSpan )
-import Util ( snocView )
-import Maybes ( maybeToBool, expectJust )
+import Util ( snocView, equalLength )
+import Maybes ( maybeToBool, expectJust, mapCatMaybes )
+import ListSetOps ( hasNoDups )
+import List ( nubBy )
import Outputable
import DATA_IOREF
\end{code}
-- provided it expands to the required form.
\begin{code}
-type TcType = Type -- A TcType can have mutable type variables
+type TcTyVar = TyVar -- Used only during type inference
+type TcType = Type -- A TcType can have mutable type variables
-- Invariant on ForAllTy in TcTypes:
-- forall a. T
-- a cannot occur inside a MutTyVar in T; that is,
-- T is "flattened" before quantifying over a
+-- These types do not have boxy type variables in them
type TcPredType = PredType
type TcThetaType = ThetaType
type TcSigmaType = TcType
type TcTauType = TcType
type TcKind = Kind
type TcTyVarSet = TyVarSet
+
+-- These types may have boxy type variables in them
+type BoxyTyVar = TcTyVar
+type BoxyRhoType = TcType
+type BoxyThetaType = TcThetaType
+type BoxySigmaType = TcType
+type BoxyType = TcType
\end{code}
It's knot-tied back to Var.lhs. There is no reason in principle
why Var.lhs shouldn't actually have the definition, but it "belongs" here.
-\begin{code}
-type TcTyVar = TyVar -- Used only during type inference
+Note [Signature skolems]
+~~~~~~~~~~~~~~~~~~~~~~~~
+Consider this
+
+ x :: [a]
+ y :: b
+ (x,y,z) = ([y,z], z, head x)
+
+Here, x and y have type sigs, which go into the environment. We used to
+instantiate their types with skolem constants, and push those types into
+the RHS, so we'd typecheck the RHS with type
+ ( [a*], b*, c )
+where a*, b* are skolem constants, and c is an ordinary meta type varible.
+
+The trouble is that the occurrences of z in the RHS force a* and b* to
+be the *same*, so we can't make them into skolem constants that don't unify
+with each other. Alas.
+
+On the other hand, we *must* use skolems for signature type variables,
+becuase GADT type refinement refines skolems only.
+
+One solution would be insist that in the above defn the programmer uses
+the same type variable in both type signatures. But that takes explanation.
+
+The alternative (currently implemented) is to have a special kind of skolem
+constant, SigSkokTv, which can unify with other SigSkolTvs.
+
+
+\begin{code}
-- A TyVarDetails is inside a TyVar
data TcTyVarDetails
- = SkolemTv SkolemInfo -- A skolem constant
- | MetaTv (IORef MetaDetails) -- A meta type variable stands for a tau-type
+ = SkolemTv SkolemInfo -- A skolem constant
+
+ | MetaTv BoxInfo (IORef MetaDetails)
+
+data BoxInfo
+ = BoxTv -- The contents is a (non-boxy) sigma-type
+ -- That is, this MetaTv is a "box"
+
+ | TauTv -- The contents is a (non-boxy) tau-type
+ -- That is, this MetaTv is an ordinary unification variable
+
+ | SigTv SkolemInfo -- A variant of TauTv, except that it should not be
+ -- unified with a type, only with a type variable
+ -- SigTvs are only distinguished to improve error messages
+ -- see Note [Signature skolems]
+ -- The MetaDetails, if filled in, will
+ -- always be another SigTv or a SkolemTv
+
+-- INVARIANTS:
+-- A TauTv is always filled in with a tau-type, which
+-- never contains any BoxTvs, nor any ForAlls
+--
+-- However, a BoxTv can contain a type that contains further BoxTvs
+-- Notably, when typechecking an explicit list, say [e1,e2], with
+-- expected type being a box b1, we fill in b1 with (List b2), where
+-- b2 is another (currently empty) box.
+
+data MetaDetails
+ = Flexi -- Flexi type variables unify to become
+ -- Indirects.
+
+ | Indirect TcType -- INVARIANT:
+ -- For a BoxTv, this type must be non-boxy
+ -- For a TauTv, this type must be a tau-type
data SkolemInfo
- = SigSkol Name -- Bound at a type signature
+ = SigSkol UserTypeCtxt -- A skolem that is created by instantiating
+ -- a programmer-supplied type signature
+ -- Location of the binding site is on the TyVar
+
+ -- The rest are for non-scoped skolems
| ClsSkol Class -- Bound at a class decl
| InstSkol Id -- Bound at an instance decl
| PatSkol DataCon -- An existential type variable bound by a pattern for
-- variable for 'a'.
| ArrowSkol SrcSpan -- An arrow form (see TcArrows)
- | GenSkol TcType -- Bound when doing a subsumption check for this type
+ | GenSkol [TcTyVar] -- Bound when doing a subsumption check for
+ TcType -- (forall tvs. ty)
SrcSpan
-data MetaDetails
- = Flexi -- Flexi type variables unify to become
- -- Indirects.
+ | UnkSkol -- Unhelpful info (until I improve it)
+
+-------------------------------------
+-- UserTypeCtxt describes the places where a
+-- programmer-written type signature can occur
+data UserTypeCtxt
+ = FunSigCtxt Name -- Function type signature
+ -- Also used for types in SPECIALISE pragmas
+ | ExprSigCtxt -- Expression type signature
+ | ConArgCtxt Name -- Data constructor argument
+ | TySynCtxt Name -- RHS of a type synonym decl
+ | GenPatCtxt -- Pattern in generic decl
+ -- f{| a+b |} (Inl x) = ...
+ | LamPatSigCtxt -- Type sig in lambda pattern
+ -- f (x::t) = ...
+ | BindPatSigCtxt -- Type sig in pattern binding pattern
+ -- (x::t, y) = e
+ | ResSigCtxt -- Result type sig
+ -- f x :: t = ....
+ | ForSigCtxt Name -- Foreign inport or export signature
+ | RuleSigCtxt Name -- Signature on a forall'd variable in a RULE
+ | DefaultDeclCtxt -- Types in a default declaration
+ | SpecInstCtxt -- SPECIALISE instance pragma
+
+-- Notes re TySynCtxt
+-- We allow type synonyms that aren't types; e.g. type List = []
+--
+-- If the RHS mentions tyvars that aren't in scope, we'll
+-- quantify over them:
+-- e.g. type T = a->a
+-- will become type T = forall a. a->a
+--
+-- With gla-exts that's right, but for H98 we should complain.
+\end{code}
- | Indirect TcType -- Type indirections, treated as wobbly
- -- for the purpose of GADT unification.
+%************************************************************************
+%* *
+ Pretty-printing
+%* *
+%************************************************************************
-pprSkolemTyVar :: TcTyVar -> SDoc
-pprSkolemTyVar tv
+\begin{code}
+pprTcTyVarDetails :: TcTyVarDetails -> SDoc
+-- For debugging
+pprTcTyVarDetails (SkolemTv _) = ptext SLIT("sk")
+pprTcTyVarDetails (MetaTv BoxTv _) = ptext SLIT("box")
+pprTcTyVarDetails (MetaTv TauTv _) = ptext SLIT("tau")
+pprTcTyVarDetails (MetaTv (SigTv _) _) = ptext SLIT("sig")
+
+pprUserTypeCtxt :: UserTypeCtxt -> SDoc
+pprUserTypeCtxt (FunSigCtxt n) = ptext SLIT("the type signature for") <+> quotes (ppr n)
+pprUserTypeCtxt ExprSigCtxt = ptext SLIT("an expression type signature")
+pprUserTypeCtxt (ConArgCtxt c) = ptext SLIT("the type of the constructor") <+> quotes (ppr c)
+pprUserTypeCtxt (TySynCtxt c) = ptext SLIT("the RHS of the type synonym") <+> quotes (ppr c)
+pprUserTypeCtxt GenPatCtxt = ptext SLIT("the type pattern of a generic definition")
+pprUserTypeCtxt LamPatSigCtxt = ptext SLIT("a pattern type signature")
+pprUserTypeCtxt BindPatSigCtxt = ptext SLIT("a pattern type signature")
+pprUserTypeCtxt ResSigCtxt = ptext SLIT("a result type signature")
+pprUserTypeCtxt (ForSigCtxt n) = ptext SLIT("the foreign declaration for") <+> quotes (ppr n)
+pprUserTypeCtxt (RuleSigCtxt n) = ptext SLIT("the type signature for") <+> quotes (ppr n)
+pprUserTypeCtxt DefaultDeclCtxt = ptext SLIT("a type in a `default' declaration")
+pprUserTypeCtxt SpecInstCtxt = ptext SLIT("a SPECIALISE instance pragma")
+
+
+--------------------------------
+tidySkolemTyVar :: TidyEnv -> TcTyVar -> (TidyEnv, TcTyVar)
+-- Tidy the type inside a GenSkol, preparatory to printing it
+tidySkolemTyVar env tv
= ASSERT( isSkolemTyVar tv )
- quotes (ppr tv) <+> ptext SLIT("is bound by") <+> ppr (skolemTvInfo tv)
-
-instance Outputable SkolemInfo where
- ppr (SigSkol id) = ptext SLIT("the type signature for") <+> quotes (ppr id)
- ppr (ClsSkol cls) = ptext SLIT("the class declaration for") <+> quotes (ppr cls)
- ppr (InstSkol df) = ptext SLIT("the instance declaration at") <+> ppr (getSrcLoc df)
- ppr (ArrowSkol loc) = ptext SLIT("the arrow form at") <+> ppr loc
- ppr (PatSkol dc loc) = sep [ptext SLIT("the pattern for") <+> quotes (ppr dc),
- nest 2 (ptext SLIT("at") <+> ppr loc)]
- ppr (GenSkol ty loc) = sep [ptext SLIT("the polymorphic type") <+> quotes (ppr ty),
- nest 2 (ptext SLIT("at") <+> ppr loc)]
+ (env1, mkTcTyVar (tyVarName tv) (tyVarKind tv) info1)
+ where
+ (env1, info1) = case tcTyVarDetails tv of
+ SkolemTv (GenSkol tvs ty loc) -> (env2, SkolemTv (GenSkol tvs1 ty1 loc))
+ where
+ (env1, tvs1) = tidyOpenTyVars env tvs
+ (env2, ty1) = tidyOpenType env1 ty
+ info -> (env, info)
+
+pprSkolTvBinding :: TcTyVar -> SDoc
+-- Print info about the binding of a skolem tyvar,
+-- or nothing if we don't have anything useful to say
+pprSkolTvBinding tv
+ = ppr_details (tcTyVarDetails tv)
+ where
+ ppr_details (MetaTv TauTv _) = quotes (ppr tv) <+> ptext SLIT("is a meta type variable")
+ ppr_details (MetaTv BoxTv _) = quotes (ppr tv) <+> ptext SLIT("is a boxy type variable")
+ ppr_details (MetaTv (SigTv info) _) = ppr_skol info
+ ppr_details (SkolemTv info) = ppr_skol info
+
+ ppr_skol UnkSkol = empty -- Unhelpful; omit
+ ppr_skol (SigSkol ctxt) = sep [quotes (ppr tv) <+> ptext SLIT("is bound by") <+> pprUserTypeCtxt ctxt,
+ nest 2 (ptext SLIT("at") <+> ppr (getSrcLoc tv))]
+ ppr_skol info = quotes (ppr tv) <+> pprSkolInfo info
+
+pprSkolInfo :: SkolemInfo -> SDoc
+pprSkolInfo (SigSkol ctxt) = ptext SLIT("is bound by") <+> pprUserTypeCtxt ctxt
+pprSkolInfo (ClsSkol cls) = ptext SLIT("is bound by the class declaration for") <+> quotes (ppr cls)
+pprSkolInfo (InstSkol df) = ptext SLIT("is bound by the instance declaration at") <+> ppr (getSrcLoc df)
+pprSkolInfo (ArrowSkol loc) = ptext SLIT("is bound by the arrow form at") <+> ppr loc
+pprSkolInfo (PatSkol dc loc) = sep [ptext SLIT("is bound by the pattern for") <+> quotes (ppr dc),
+ nest 2 (ptext SLIT("at") <+> ppr loc)]
+pprSkolInfo (GenSkol tvs ty loc) = sep [sep [ptext SLIT("is bound by the polymorphic type"),
+ nest 2 (quotes (ppr (mkForAllTys tvs ty)))],
+ nest 2 (ptext SLIT("at") <+> ppr loc)]
+-- UnkSkol, SigSkol
+-- For type variables the others are dealt with by pprSkolTvBinding.
+-- For Insts, these cases should not happen
+pprSkolInfo UnkSkol = panic "UnkSkol"
instance Outputable MetaDetails where
ppr Flexi = ptext SLIT("Flexi")
ppr (Indirect ty) = ptext SLIT("Indirect") <+> ppr ty
+\end{code}
+
+
+%************************************************************************
+%* *
+ Predicates
+%* *
+%************************************************************************
-isImmutableTyVar, isSkolemTyVar, isExistentialTyVar, isMetaTyVar :: TyVar -> Bool
+\begin{code}
+isImmutableTyVar, isSkolemTyVar, isExistentialTyVar, isBoxyTyVar, isMetaTyVar :: TyVar -> Bool
isImmutableTyVar tv
| isTcTyVar tv = isSkolemTyVar tv
| otherwise = True
isSkolemTyVar tv
= ASSERT( isTcTyVar tv )
case tcTyVarDetails tv of
- SkolemTv _ -> True
- MetaTv _ -> False
+ SkolemTv _ -> True
+ MetaTv _ _ -> False
isExistentialTyVar tv -- Existential type variable, bound by a pattern
= ASSERT( isTcTyVar tv )
other -> False
isMetaTyVar tv
+ = ASSERT2( isTcTyVar tv, ppr tv )
+ case tcTyVarDetails tv of
+ MetaTv _ _ -> True
+ other -> False
+
+isBoxyTyVar tv
= ASSERT( isTcTyVar tv )
case tcTyVarDetails tv of
- SkolemTv _ -> False
- MetaTv _ -> True
+ MetaTv BoxTv _ -> True
+ other -> False
-skolemTvInfo :: TyVar -> SkolemInfo
-skolemTvInfo tv
+isSigTyVar tv
= ASSERT( isTcTyVar tv )
case tcTyVarDetails tv of
- SkolemTv info -> info
+ MetaTv (SigTv _) _ -> True
+ other -> False
metaTvRef :: TyVar -> IORef MetaDetails
metaTvRef tv
= ASSERT( isTcTyVar tv )
case tcTyVarDetails tv of
- MetaTv ref -> ref
+ MetaTv _ ref -> ref
+ other -> pprPanic "metaTvRef" (ppr tv)
isFlexi, isIndirect :: MetaDetails -> Bool
isFlexi Flexi = True
mkPhiTy theta ty = foldr (\p r -> FunTy (mkPredTy p) r) ty theta
\end{code}
-@isTauTy@ tests for nested for-alls.
+@isTauTy@ tests for nested for-alls. It should not be called on a boxy type.
\begin{code}
isTauTy :: Type -> Bool
-isTauTy (TyVarTy v) = True
-isTauTy (TyConApp _ tys) = all isTauTy tys
-isTauTy (AppTy a b) = isTauTy a && isTauTy b
-isTauTy (FunTy a b) = isTauTy a && isTauTy b
-isTauTy (PredTy p) = True -- Don't look through source types
-isTauTy (NoteTy _ ty) = isTauTy ty
-isTauTy other = False
-\end{code}
-
-\begin{code}
+isTauTy ty | Just ty' <- tcView ty = isTauTy ty'
+isTauTy (TyVarTy tv) = ASSERT( not (isTcTyVar tv && isBoxyTyVar tv) )
+ True
+isTauTy (TyConApp tc tys) = all isTauTy tys && isTauTyCon tc
+isTauTy (AppTy a b) = isTauTy a && isTauTy b
+isTauTy (FunTy a b) = isTauTy a && isTauTy b
+isTauTy (PredTy p) = True -- Don't look through source types
+isTauTy other = False
+
+
+isTauTyCon :: TyCon -> Bool
+-- Returns False for type synonyms whose expansion is a polytype
+isTauTyCon tc | isSynTyCon tc = isTauTy (snd (synTyConDefn tc))
+ | otherwise = True
+
+---------------
+isBoxyTy :: TcType -> Bool
+isBoxyTy ty = any isBoxyTyVar (varSetElems (tcTyVarsOfType ty))
+
+isRigidTy :: TcType -> Bool
+-- A type is rigid if it has no meta type variables in it
+isRigidTy ty = all isSkolemTyVar (varSetElems (tcTyVarsOfType ty))
+
+isRefineableTy :: TcType -> Bool
+-- A type should have type refinements applied to it if it has
+-- free type variables, and they are all rigid
+isRefineableTy ty = not (null tc_tvs) && all isSkolemTyVar tc_tvs
+ where
+ tc_tvs = varSetElems (tcTyVarsOfType ty)
+
+---------------
getDFunTyKey :: Type -> OccName -- Get some string from a type, to be used to
-- construct a dictionary function name
+getDFunTyKey ty | Just ty' <- tcView ty = getDFunTyKey ty'
getDFunTyKey (TyVarTy tv) = getOccName tv
getDFunTyKey (TyConApp tc _) = getOccName tc
getDFunTyKey (AppTy fun _) = getDFunTyKey fun
-getDFunTyKey (NoteTy _ t) = getDFunTyKey t
getDFunTyKey (FunTy arg _) = getOccName funTyCon
getDFunTyKey (ForAllTy _ t) = getDFunTyKey t
getDFunTyKey ty = pprPanic "getDFunTyKey" (pprType ty)
tcSplitForAllTys :: Type -> ([TyVar], Type)
tcSplitForAllTys ty = split ty ty []
where
+ split orig_ty ty tvs | Just ty' <- tcView ty = split orig_ty ty' tvs
split orig_ty (ForAllTy tv ty) tvs = split ty ty (tv:tvs)
- split orig_ty (NoteTy n ty) tvs = split orig_ty ty tvs
split orig_ty t tvs = (reverse tvs, orig_ty)
+tcIsForAllTy ty | Just ty' <- tcView ty = tcIsForAllTy ty'
tcIsForAllTy (ForAllTy tv ty) = True
-tcIsForAllTy (NoteTy n ty) = tcIsForAllTy ty
tcIsForAllTy t = False
tcSplitPhiTy :: Type -> ([PredType], Type)
tcSplitPhiTy ty = split ty ty []
where
+ split orig_ty ty tvs | Just ty' <- tcView ty = split orig_ty ty' tvs
split orig_ty (FunTy arg res) ts = case tcSplitPredTy_maybe arg of
Just p -> split res res (p:ts)
Nothing -> (reverse ts, orig_ty)
- split orig_ty (NoteTy n ty) ts = split orig_ty ty ts
split orig_ty ty ts = (reverse ts, orig_ty)
tcSplitSigmaTy ty = case tcSplitForAllTys ty of
(tvs, rho) -> case tcSplitPhiTy rho of
(theta, tau) -> (tvs, theta, tau)
+-----------------------
+tcMultiSplitSigmaTy
+ :: TcSigmaType
+ -> ( [([TyVar], ThetaType)], -- forall as.C => forall bs.D
+ TcSigmaType) -- The rest of the type
+
+-- We need a loop here because we are now prepared to entertain
+-- types like
+-- f:: forall a. Eq a => forall b. Baz b => tau
+-- We want to instantiate this to
+-- f2::tau {f2 = f1 b (Baz b), f1 = f a (Eq a)}
+
+tcMultiSplitSigmaTy sigma
+ = case (tcSplitSigmaTy sigma) of
+ ([],[],ty) -> ([], sigma)
+ (tvs, theta, ty) -> case tcMultiSplitSigmaTy ty of
+ (pairs, rest) -> ((tvs,theta):pairs, rest)
+
+-----------------------
tcTyConAppTyCon :: Type -> TyCon
tcTyConAppTyCon ty = fst (tcSplitTyConApp ty)
Nothing -> pprPanic "tcSplitTyConApp" (pprType ty)
tcSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
+tcSplitTyConApp_maybe ty | Just ty' <- tcView ty = tcSplitTyConApp_maybe ty'
tcSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
tcSplitTyConApp_maybe (FunTy arg res) = Just (funTyCon, [arg,res])
-tcSplitTyConApp_maybe (NoteTy n ty) = tcSplitTyConApp_maybe ty
-- Newtypes are opaque, so they may be split
-- However, predicates are not treated
-- as tycon applications by the type checker
-tcSplitTyConApp_maybe other = Nothing
+tcSplitTyConApp_maybe other = Nothing
+-----------------------
tcSplitFunTys :: Type -> ([Type], Type)
tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
Nothing -> ([], ty)
(args,res') = tcSplitFunTys res
tcSplitFunTy_maybe :: Type -> Maybe (Type, Type)
+tcSplitFunTy_maybe ty | Just ty' <- tcView ty = tcSplitFunTy_maybe ty'
tcSplitFunTy_maybe (FunTy arg res) = Just (arg, res)
-tcSplitFunTy_maybe (NoteTy n ty) = tcSplitFunTy_maybe ty
tcSplitFunTy_maybe other = Nothing
+tcSplitFunTysN
+ :: TcRhoType
+ -> Arity -- N: Number of desired args
+ -> ([TcSigmaType], -- Arg types (N or fewer)
+ TcSigmaType) -- The rest of the type
+
+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)
+
tcFunArgTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> arg }
tcFunResultTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> res }
+-----------------------
tcSplitAppTy_maybe :: Type -> Maybe (Type, Type)
+tcSplitAppTy_maybe ty | Just ty' <- tcView ty = tcSplitAppTy_maybe ty'
tcSplitAppTy_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [ty1], ty2)
tcSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
-tcSplitAppTy_maybe (NoteTy n ty) = tcSplitAppTy_maybe ty
tcSplitAppTy_maybe (TyConApp tc tys) = case snocView tys of
Just (tys', ty') -> Just (TyConApp tc tys', ty')
Nothing -> Nothing
Just (ty', arg) -> go ty' (arg:args)
Nothing -> (ty,args)
+-----------------------
tcGetTyVar_maybe :: Type -> Maybe TyVar
+tcGetTyVar_maybe ty | Just ty' <- tcView ty = tcGetTyVar_maybe ty'
tcGetTyVar_maybe (TyVarTy tv) = Just tv
-tcGetTyVar_maybe (NoteTy _ t) = tcGetTyVar_maybe t
tcGetTyVar_maybe other = Nothing
tcGetTyVar :: String -> Type -> TyVar
tcIsTyVarTy :: Type -> Bool
tcIsTyVarTy ty = maybeToBool (tcGetTyVar_maybe ty)
+-----------------------
tcSplitDFunTy :: Type -> ([TyVar], [PredType], Class, [Type])
-- Split the type of a dictionary function
tcSplitDFunTy ty
tcSplitDFunHead tau
= case tcSplitPredTy_maybe tau of
Just (ClassP clas tys) -> (clas, tys)
+
+tcValidInstHeadTy :: Type -> Bool
+-- Used in Haskell-98 mode, for the argument types of an instance head
+-- These must not be type synonyms, but everywhere else type synonyms
+-- are transparent, so we need a special function here
+tcValidInstHeadTy ty
+ = case ty of
+ NoteTy _ ty -> tcValidInstHeadTy ty
+ TyConApp tc tys -> not (isSynTyCon tc) && ok tys
+ FunTy arg res -> ok [arg, res]
+ other -> False
+ where
+ -- Check that all the types are type variables,
+ -- and that each is distinct
+ ok tys = equalLength tvs tys && hasNoDups tvs
+ where
+ tvs = mapCatMaybes get_tv tys
+
+ get_tv (NoteTy _ ty) = get_tv ty -- through synonyms
+ get_tv (TyVarTy tv) = Just tv -- Again, do not look
+ get_tv other = Nothing
\end{code}
\begin{code}
tcSplitPredTy_maybe :: Type -> Maybe PredType
-- Returns Just for predicates only
-tcSplitPredTy_maybe (NoteTy _ ty) = tcSplitPredTy_maybe ty
+tcSplitPredTy_maybe ty | Just ty' <- tcView ty = tcSplitPredTy_maybe ty'
tcSplitPredTy_maybe (PredTy p) = Just p
tcSplitPredTy_maybe other = Nothing
mkDictTy clas tys = mkPredTy (ClassP clas tys)
isDictTy :: Type -> Bool
+isDictTy ty | Just ty' <- tcView ty = isDictTy ty'
isDictTy (PredTy p) = isClassPred p
-isDictTy (NoteTy _ ty) = isDictTy ty
isDictTy other = False
\end{code}
isLinearPred other = False
\end{code}
+--------------------- The stupid theta (sigh) ---------------------------------
+
+\begin{code}
+dataConsStupidTheta :: [DataCon] -> ThetaType
+-- Union the stupid thetas from all the specified constructors (non-empty)
+-- All the constructors should have the same result type, modulo alpha conversion
+-- The resulting ThetaType uses type variables from the *first* constructor in the list
+--
+-- It's here because it's used in MkId.mkRecordSelId, and in TcExpr
+dataConsStupidTheta (con1:cons)
+ = nubBy tcEqPred all_preds
+ where
+ all_preds = dataConStupidTheta con1 ++ other_stupids
+ res_tys1 = dataConResTys con1
+ tvs1 = tyVarsOfTypes res_tys1
+ other_stupids = [ substPred subst pred
+ | con <- cons
+ , let Just subst = tcMatchTys tvs1 res_tys1 (dataConResTys con)
+ , pred <- dataConStupidTheta con ]
+\end{code}
+
%************************************************************************
%* *
\begin{code}
isSigmaTy :: Type -> Bool
+isSigmaTy ty | Just ty' <- tcView ty = isSigmaTy ty'
isSigmaTy (ForAllTy tyvar ty) = True
isSigmaTy (FunTy a b) = isPredTy a
-isSigmaTy (NoteTy n ty) = isSigmaTy ty
isSigmaTy _ = False
isOverloadedTy :: Type -> Bool
+isOverloadedTy ty | Just ty' <- tcView ty = isOverloadedTy ty'
isOverloadedTy (ForAllTy tyvar ty) = isOverloadedTy ty
isOverloadedTy (FunTy a b) = isPredTy a
-isOverloadedTy (NoteTy n ty) = isOverloadedTy ty
isOverloadedTy _ = False
isPredTy :: Type -> Bool -- Belongs in TcType because it does
-- not look through newtypes, or predtypes (of course)
-isPredTy (NoteTy _ ty) = isPredTy ty
+isPredTy ty | Just ty' <- tcView ty = isPredTy ty'
isPredTy (PredTy sty) = True
isPredTy _ = False
\end{code}
\begin{code}
deNoteType :: Type -> Type
- -- Remove synonyms, but not predicate types
-deNoteType ty@(TyVarTy tyvar) = ty
-deNoteType (TyConApp tycon tys) = TyConApp tycon (map deNoteType tys)
-deNoteType (PredTy p) = PredTy (deNotePredType p)
-deNoteType (NoteTy _ ty) = deNoteType ty
-deNoteType (AppTy fun arg) = AppTy (deNoteType fun) (deNoteType arg)
-deNoteType (FunTy fun arg) = FunTy (deNoteType fun) (deNoteType arg)
-deNoteType (ForAllTy tv ty) = ForAllTy tv (deNoteType ty)
-
-deNotePredType :: PredType -> PredType
-deNotePredType (ClassP c tys) = ClassP c (map deNoteType tys)
-deNotePredType (IParam n ty) = IParam n (deNoteType ty)
+-- Remove all *outermost* type synonyms and other notes
+deNoteType ty | Just ty' <- tcView ty = deNoteType ty'
+deNoteType ty = ty
+\end{code}
+
+\begin{code}
+tcTyVarsOfType :: Type -> TcTyVarSet
+-- Just the tc type variables free in the type
+tcTyVarsOfType (TyVarTy tv) = if isTcTyVar tv then unitVarSet tv
+ else emptyVarSet
+tcTyVarsOfType (TyConApp tycon tys) = tcTyVarsOfTypes tys
+tcTyVarsOfType (NoteTy _ ty) = tcTyVarsOfType ty
+tcTyVarsOfType (PredTy sty) = tcTyVarsOfPred sty
+tcTyVarsOfType (FunTy arg res) = tcTyVarsOfType arg `unionVarSet` tcTyVarsOfType res
+tcTyVarsOfType (AppTy fun arg) = tcTyVarsOfType fun `unionVarSet` tcTyVarsOfType arg
+tcTyVarsOfType (ForAllTy tyvar ty) = tcTyVarsOfType ty `delVarSet` tyvar
+ -- We do sometimes quantify over skolem TcTyVars
+
+tcTyVarsOfTypes :: [Type] -> TyVarSet
+tcTyVarsOfTypes tys = foldr (unionVarSet.tcTyVarsOfType) emptyVarSet tys
+
+tcTyVarsOfPred :: PredType -> TyVarSet
+tcTyVarsOfPred (IParam _ ty) = tcTyVarsOfType ty
+tcTyVarsOfPred (ClassP _ tys) = tcTyVarsOfTypes tys
+\end{code}
+
+Note [Silly type synonym]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+ type T a = Int
+What are the free tyvars of (T x)? Empty, of course!
+Here's the example that Ralf Laemmel showed me:
+ foo :: (forall a. C u a -> C u a) -> u
+ mappend :: Monoid u => u -> u -> u
+
+ bar :: Monoid u => u
+ bar = foo (\t -> t `mappend` t)
+We have to generalise at the arg to f, and we don't
+want to capture the constraint (Monad (C u a)) because
+it appears to mention a. Pretty silly, but it was useful to him.
+
+exactTyVarsOfType is used by the type checker to figure out exactly
+which type variables are mentioned in a type. It's also used in the
+smart-app checking code --- see TcExpr.tcIdApp
+
+\begin{code}
+exactTyVarsOfType :: TcType -> TyVarSet
+-- Find the free type variables (of any kind)
+-- but *expand* type synonyms. See Note [Silly type synonym] belos.
+exactTyVarsOfType ty
+ = go ty
+ where
+ go ty | Just ty' <- tcView ty = go ty' -- This is the key line
+ go (TyVarTy tv) = unitVarSet tv
+ go (TyConApp tycon tys) = exactTyVarsOfTypes tys
+ go (PredTy ty) = go_pred ty
+ go (FunTy arg res) = go arg `unionVarSet` go res
+ go (AppTy fun arg) = go fun `unionVarSet` go arg
+ go (ForAllTy tyvar ty) = delVarSet (go ty) tyvar
+
+ go_pred (IParam _ ty) = go ty
+ go_pred (ClassP _ tys) = exactTyVarsOfTypes tys
+
+exactTyVarsOfTypes :: [TcType] -> TyVarSet
+exactTyVarsOfTypes tys = foldr (unionVarSet . exactTyVarsOfType) emptyVarSet tys
\end{code}
Find the free tycons and classes of a type. This is used in the front
tyClsNamesOfType :: Type -> NameSet
tyClsNamesOfType (TyVarTy tv) = emptyNameSet
tyClsNamesOfType (TyConApp tycon tys) = unitNameSet (getName tycon) `unionNameSets` tyClsNamesOfTypes tys
-tyClsNamesOfType (NoteTy (SynNote ty1) ty2) = tyClsNamesOfType ty1
-tyClsNamesOfType (NoteTy other_note ty2) = tyClsNamesOfType ty2
-tyClsNamesOfType (PredTy (IParam n ty)) = tyClsNamesOfType ty
-tyClsNamesOfType (PredTy (ClassP cl tys)) = unitNameSet (getName cl) `unionNameSets` tyClsNamesOfTypes tys
+tyClsNamesOfType (NoteTy _ ty2) = tyClsNamesOfType ty2
+tyClsNamesOfType (PredTy (IParam n ty)) = tyClsNamesOfType ty
+tyClsNamesOfType (PredTy (ClassP cl tys)) = unitNameSet (getName cl) `unionNameSets` tyClsNamesOfTypes tys
tyClsNamesOfType (FunTy arg res) = tyClsNamesOfType arg `unionNameSets` tyClsNamesOfType res
tyClsNamesOfType (AppTy fun arg) = tyClsNamesOfType fun `unionNameSets` tyClsNamesOfType arg
tyClsNamesOfType (ForAllTy tyvar ty) = tyClsNamesOfType ty
isByteArrayLikeTyCon tc =
getUnique tc `elem` [byteArrayTyConKey, mutableByteArrayTyConKey]
\end{code}
-
-