TcType, TcSigmaType, TcRhoType, TcTauType, TcPredType, TcThetaType,
TcTyVar, TcTyVarSet, TcKind,
+ BoxyTyVar, BoxySigmaType, BoxyRhoType, BoxyThetaType, BoxyType,
+
--------------------------------
-- MetaDetails
- Expected(..), TcRef, TcTyVarDetails(..),
- MetaDetails(Flexi, Indirect), SkolemInfo(..), pprTcTyVar, pprSkolInfo,
- isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isExistentialTyVar, metaTvRef,
+ UserTypeCtxt(..), pprUserTypeCtxt,
+ TcTyVarDetails(..), BoxInfo(..), pprTcTyVarDetails,
+ MetaDetails(Flexi, Indirect), SkolemInfo(..), pprSkolTvBinding, pprSkolInfo,
+ isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isBoxyTyVar, isSigTyVar, isExistentialTyVar,
+ metaTvRef,
isFlexi, isIndirect,
--------------------------------
-- Builders
- mkPhiTy, mkSigmaTy, hoistForAllTys,
+ mkPhiTy, mkSigmaTy,
--------------------------------
-- 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,
+ 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,
- mkOpenTvSubst, zipOpenTvSubst, 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
tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars, tidySkolemTyVar,
- typeKind,
+ 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, deShadowTy,
+ tidyOpenTyVars, tidyKind,
+ isSubKind, tcView,
tcEqType, tcEqTypes, tcCmpType, tcCmpTypes,
tcEqPred, tcCmpPred, tcEqTypeX,
TvSubst(..),
- TvSubstEnv, emptyTvSubst,
+ 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, mkTcTyVar, tyVarName, tyVarKind, tcTyVarDetails )
import ForeignCall ( Safety, playSafe, DNType(..) )
+import Unify ( tcMatchTys )
import VarSet
-- others:
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 TcKind = Kind
type TcTyVarSet = TyVarSet
-type TcRef a = IORef a
-data Expected ty = Infer (TcRef ty) -- The hole to fill in for type inference
- | Check ty -- The type to check during type checking
+-- 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.
+
Note [Signature skolems]
~~~~~~~~~~~~~~~~~~~~~~~~
Consider this
On the other hand, we *must* use skolems for signature type variables,
becuase GADT type refinement refines skolems only.
-One solution woudl be insist that in the above defn the programmer uses
+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
\begin{code}
-type TcTyVar = TyVar -- Used only during type inference
-
-- A TyVarDetails is inside a TyVar
data TcTyVarDetails
- = MetaTv (IORef MetaDetails) -- A meta type variable stands for a tau-type
- | SkolemTv SkolemInfo -- A skolem constant
- | SigSkolTv Name (IORef MetaDetails) -- Ditto, but from a type signature;
- -- see Note [Signature skolems]
- -- The MetaDetails, if filled in, will
- -- always be another SigSkolTv
+ = 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
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
+%* *
+%************************************************************************
+\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
(env2, ty1) = tidyOpenType env1 ty
info -> (env, info)
-pprTcTyVar :: TcTyVar -> SDoc
--- Print tyvar with info about its binding
-pprTcTyVar tv
- = quotes (ppr tv) <+> ppr_details (tcTyVarDetails tv)
+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 _) = ptext SLIT("is a meta type variable")
- ppr_details (SigSkolTv id _) = ptext SLIT("is bound by") <+> pprSkolInfo (SigSkol id)
- ppr_details (SkolemTv info) = ptext SLIT("is bound by") <+> pprSkolInfo info
+ 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 id) = ptext SLIT("the type signature for") <+> quotes (ppr id)
-pprSkolInfo (ClsSkol cls) = ptext SLIT("the class declaration for") <+> quotes (ppr cls)
-pprSkolInfo (InstSkol df) = ptext SLIT("the instance declaration at") <+> ppr (getSrcLoc df)
-pprSkolInfo (ArrowSkol loc) = ptext SLIT("the arrow form at") <+> ppr loc
-pprSkolInfo (PatSkol dc loc) = sep [ptext SLIT("the pattern for") <+> quotes (ppr dc),
+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 [ptext SLIT("the polymorphic type")
- <+> quotes (ppr (mkForAllTys tvs ty)),
+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
- SigSkolTv _ _ -> True
- MetaTv _ -> False
+ SkolemTv _ -> True
+ MetaTv _ _ -> False
isExistentialTyVar tv -- Existential type variable, bound by a pattern
= ASSERT( isTcTyVar tv )
other -> False
isMetaTyVar tv
- = ASSERT( isTcTyVar tv )
+ = ASSERT2( isTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
- MetaTv _ -> True
+ MetaTv _ _ -> True
other -> False
+isBoxyTyVar tv
+ = ASSERT( isTcTyVar tv )
+ case tcTyVarDetails tv of
+ MetaTv BoxTv _ -> True
+ other -> False
+
+isSigTyVar tv
+ = ASSERT( isTcTyVar tv )
+ case tcTyVarDetails tv of
+ 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
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}
\end{code}
-
-
%************************************************************************
%* *
- Hoisting for-alls
+\subsection{Misc}
%* *
%************************************************************************
-hoistForAllTys is used for user-written type signatures only
-We want to 'look through' type synonyms when doing this
-so it's better done on the Type than the HsType
-
-It moves all the foralls and constraints to the top
-e.g. T -> forall a. a ==> forall a. T -> a
- T -> (?x::Int) -> Int ==> (?x::Int) -> T -> Int
-
-Also: it eliminates duplicate constraints. These can show up
-when hoisting constraints, notably implicit parameters.
-
-It tries hard to retain type synonyms if hoisting does not break one
-up. Not only does this improve error messages, but there's a tricky
-interaction with Haskell 98. H98 requires no unsaturated type
-synonyms, which is checked by checkValidType. This runs after
-hoisting, so we don't want hoisting to remove the SynNotes! (We can't
-run validity checking before hoisting because in mutually-recursive
-type definitions we postpone validity checking until after the knot is
-tied.)
-
\begin{code}
-hoistForAllTys :: Type -> Type
-hoistForAllTys ty
- = go (deShadowTy ty)
- -- Running over ty with an empty substitution gives it the
- -- no-shadowing property. This is important. For example:
- -- type Foo r = forall a. a -> r
- -- foo :: Foo (Foo ())
- -- Here the hoisting should give
- -- foo :: forall a a1. a -> a1 -> ()
- --
- -- What about type vars that are lexically in scope in the envt?
- -- We simply rely on them having a different unique to any
- -- binder in 'ty'. Otherwise we'd have to slurp the in-scope-tyvars
- -- out of the envt, which is boring and (I think) not necessary.
-
- where
- go (TyVarTy tv) = TyVarTy tv
- go (TyConApp tc tys) = TyConApp tc (map go tys)
- go (PredTy pred) = PredTy pred -- No nested foralls
- go (NoteTy (SynNote ty1) ty2) = NoteTy (SynNote (go ty1)) (go ty2)
- go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard the free tyvar note
- go (FunTy arg res) = mk_fun_ty (go arg) (go res)
- go (AppTy fun arg) = AppTy (go fun) (go arg)
- go (ForAllTy tv ty) = ForAllTy tv (go ty)
-
- -- mk_fun_ty does all the work.
- -- It's building t1 -> t2:
- -- if t2 is a for-all type, push t1 inside it
- -- if t2 is (pred -> t3), check for duplicates
- mk_fun_ty ty1 ty2
- | not (isSigmaTy ty2) -- No forall's, or context =>
- = FunTy ty1 ty2
- | PredTy p1 <- ty1 -- ty1 is a predicate
- = if p1 `elem` theta then -- so check for duplicates
- ty2
- else
- mkSigmaTy tvs (p1:theta) tau
- | otherwise
- = mkSigmaTy tvs theta (FunTy ty1 tau)
- where
- (tvs, theta, tau) = tcSplitSigmaTy ty2
+deNoteType :: Type -> Type
+-- 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}
-%************************************************************************
-%* *
-\subsection{Misc}
-%* *
-%************************************************************************
+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}
-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)
+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}
-
-
projects / ghc-hetmet.git / blobdiff