-%
+
% (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
%
\section[TcType]{Types used in the typechecker}
-\begin{code}
-module TcType (
-
- TcTyVar,
- TcTyVarSet,
- newTyVar,
- newTyVarTy, -- Kind -> NF_TcM s TcType
- newTyVarTys, -- Int -> Kind -> NF_TcM s [TcType]
-
- newTyVarTy_OpenKind, -- NF_TcM s TcType
- newOpenTypeKind, -- NF_TcM s TcKind
-
- -----------------------------------------
- TcType, TcTauType, TcThetaType, TcRhoType,
+This module provides the Type interface for front-end parts of the
+compiler. These parts
- -- Find the type to which a type variable is bound
- tcPutTyVar, -- :: TcTyVar -> TcType -> NF_TcM TcType
- tcGetTyVar, -- :: TcTyVar -> NF_TcM (Maybe TcType) does shorting out
+ * treat "source types" as opaque:
+ newtypes, and predicates are meaningful.
+ * look through usage types
+The "tc" prefix is for "typechechecker", because the type checker
+is the principal client.
- tcSplitRhoTy,
+\begin{code}
+module TcType (
+ --------------------------------
+ -- Types
+ TcType, TcSigmaType, TcRhoType, TcTauType, TcPredType, TcThetaType,
+ TcTyVar, TcTyVarSet, TcKind,
- tcInstTyVars,
- tcInstSigVar,
- tcInstTcType,
+ BoxyTyVar, BoxySigmaType, BoxyRhoType, BoxyThetaType, BoxyType,
- typeToTcType,
+ --------------------------------
+ -- MetaDetails
+ UserTypeCtxt(..), pprUserTypeCtxt,
+ TcTyVarDetails(..), BoxInfo(..), pprTcTyVarDetails,
+ MetaDetails(Flexi, Indirect), SkolemInfo(..), pprSkolTvBinding, pprSkolInfo,
+ isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isBoxyTyVar, isSigTyVar, isExistentialTyVar,
+ metaTvRef,
+ isFlexi, isIndirect,
- tcTypeKind, -- :: TcType -> NF_TcM s TcKind
--------------------------------
- TcKind,
- newKindVar, newKindVars,
- kindToTcKind,
- zonkTcKind,
+ -- Builders
+ mkPhiTy, mkSigmaTy,
--------------------------------
- zonkTcTyVar, zonkTcTyVars, zonkTcTyVarBndr,
- zonkTcType, zonkTcTypes, zonkTcThetaType,
+ -- Splitters
+ -- These are important because they do not look through newtypes
+ tcView,
+ tcSplitForAllTys, tcSplitPhiTy,
+ tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy, tcSplitFunTysN,
+ tcSplitTyConApp, tcSplitTyConApp_maybe, tcTyConAppTyCon, tcTyConAppArgs,
+ tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys,
+ tcValidInstHeadTy, tcGetTyVar_maybe, tcGetTyVar,
+ tcSplitSigmaTy, tcMultiSplitSigmaTy,
+
+ ---------------------------------
+ -- Predicates.
+ -- Again, newtypes are opaque
+ tcEqType, tcEqTypes, tcEqPred, tcCmpType, tcCmpTypes, tcCmpPred, tcEqTypeX,
+ isSigmaTy, isOverloadedTy, isRigidTy, isBoxyTy,
+ isDoubleTy, isFloatTy, isIntTy, isStringTy,
+ isIntegerTy, isAddrTy, isBoolTy, isUnitTy,
+ isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy,
+
+ ---------------------------------
+ -- Misc type manipulators
+ deNoteType, classesOfTheta,
+ tyClsNamesOfType, tyClsNamesOfDFunHead,
+ getDFunTyKey,
+
+ ---------------------------------
+ -- Predicate types
+ getClassPredTys_maybe, getClassPredTys,
+ isClassPred, isTyVarClassPred,
+ mkDictTy, tcSplitPredTy_maybe,
+ isPredTy, isDictTy, tcSplitDFunTy, tcSplitDFunHead, predTyUnique,
+ mkClassPred, isInheritablePred, isLinearPred, isIPPred, mkPredName,
+ dataConsStupidTheta, isRefineableTy,
+
+ ---------------------------------
+ -- Foreign import and export
+ isFFIArgumentTy, -- :: DynFlags -> Safety -> Type -> Bool
+ isFFIImportResultTy, -- :: DynFlags -> Type -> Bool
+ isFFIExportResultTy, -- :: Type -> Bool
+ isFFIExternalTy, -- :: Type -> Bool
+ isFFIDynArgumentTy, -- :: Type -> Bool
+ isFFIDynResultTy, -- :: Type -> Bool
+ isFFILabelTy, -- :: Type -> Bool
+ isFFIDotnetTy, -- :: DynFlags -> Type -> Bool
+ isFFIDotnetObjTy, -- :: Type -> Bool
+ isFFITy, -- :: Type -> Bool
+
+ toDNType, -- :: Type -> DNType
- zonkTcTypeToType, zonkTcTyVarToTyVar,
- zonkTcKindToKind
+ --------------------------------
+ -- Rexported from Type
+ Kind, -- Stuff to do with kinds is insensitive to pre/post Tc
+ unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds,
+ isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind,
+ isArgTypeKind, isSubKind, defaultKind,
+
+ Type, PredType(..), ThetaType,
+ mkForAllTy, mkForAllTys,
+ mkFunTy, mkFunTys, zipFunTys,
+ 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, notElemTvSubst,
+ getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope, lookupTyVar,
+ extendTvSubst, extendTvSubstList, isInScope, mkTvSubst, zipTyEnv,
+ substTy, substTys, substTyWith, substTheta, substTyVar, substTyVarBndr,
+
+ isUnLiftedType, -- Source types are always lifted
+ isUnboxedTupleType, -- Ditto
+ isPrimitiveType,
+
+ tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
+ tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars, tidySkolemTyVar,
+ typeKind, tidyKind,
+
+ tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
+ tcTyVarsOfType, tcTyVarsOfTypes, exactTyVarsOfType, exactTyVarsOfTypes,
+
+ pprKind, pprParendKind,
+ pprType, pprParendType, pprTyThingCategory,
+ pprPred, pprTheta, pprThetaArrow, pprClassPred
) where
#include "HsVersions.h"
-
-- friends:
-import PprType ( pprType )
-import Type ( Type(..), Kind, ThetaType, TyNote(..),
- mkAppTy, mkTyConApp,
- splitDictTy_maybe, splitForAllTys, isNotUsgTy,
- isTyVarTy, mkTyVarTy, mkTyVarTys,
- typeCon, openTypeKind, boxedTypeKind, boxedKind, superKind, superBoxity
+import TypeRep ( Type(..), funTyCon ) -- friend
+
+import Type ( -- Re-exports
+ tyVarsOfType, tyVarsOfTypes, tyVarsOfPred,
+ tyVarsOfTheta, Kind, PredType(..),
+ ThetaType, unliftedTypeKind,
+ liftedTypeKind, openTypeKind, mkArrowKind,
+ isLiftedTypeKind, isUnliftedTypeKind,
+ mkArrowKinds, mkForAllTy, mkForAllTys,
+ defaultKind, isArgTypeKind, isOpenTypeKind,
+ mkFunTy, mkFunTys, zipFunTys,
+ mkTyConApp, mkAppTy,
+ mkAppTys, applyTy, applyTys,
+ mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy,
+ mkPredTys, isUnLiftedType,
+ isUnboxedTupleType, isPrimitiveType,
+ splitTyConApp_maybe,
+ tidyTopType, tidyType, tidyPred, tidyTypes,
+ tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
+ tidyTyVarBndr, tidyOpenTyVar,
+ tidyOpenTyVars, tidyKind,
+ isSubKind, tcView,
+
+ tcEqType, tcEqTypes, tcCmpType, tcCmpTypes,
+ tcEqPred, tcCmpPred, tcEqTypeX,
+
+ TvSubst(..),
+ TvSubstEnv, emptyTvSubst, mkTvSubst, zipTyEnv,
+ mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst,
+ getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope,
+ extendTvSubst, extendTvSubstList, isInScope, notElemTvSubst,
+ substTy, substTys, substTyWith, substTheta,
+ substTyVar, substTyVarBndr, substPred, lookupTyVar,
+
+ typeKind, repType,
+ pprKind, pprParendKind,
+ pprType, pprParendType, pprTyThingCategory,
+ pprPred, pprTheta, pprThetaArrow, pprClassPred
)
-import Subst ( Subst, mkTopTyVarSubst, substTy )
-import TyCon ( tyConKind, mkPrimTyCon )
-import PrimRep ( PrimRep(VoidRep) )
-import VarEnv
-import VarSet ( emptyVarSet )
-import Var ( TyVar, tyVarKind, tyVarName, isTyVar, isMutTyVar, mkTyVar )
+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 TcMonad
-import TysWiredIn ( voidTy )
-
-import Name ( NamedThing(..), setNameUnique, mkSysLocalName,
- mkDerivedName, mkDerivedTyConOcc
- )
-import Unique ( Unique, Uniquable(..) )
-import Util ( nOfThem )
+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(..), Arity, ipNameName )
+import SrcLoc ( SrcLoc, SrcSpan )
+import Util ( snocView, equalLength )
+import Maybes ( maybeToBool, expectJust, mapCatMaybes )
+import ListSetOps ( hasNoDups )
+import List ( nubBy )
import Outputable
+import DATA_IOREF
\end{code}
+%************************************************************************
+%* *
+\subsection{Types}
+%* *
+%************************************************************************
-Coercions
-~~~~~~~~~~
-Type definitions are in TcMonad.lhs
+The type checker divides the generic Type world into the
+following more structured beasts:
-\begin{code}
-typeToTcType :: Type -> TcType
-typeToTcType ty = ty
+sigma ::= forall tyvars. phi
+ -- A sigma type is a qualified type
+ --
+ -- Note that even if 'tyvars' is empty, theta
+ -- may not be: e.g. (?x::Int) => Int
-kindToTcKind :: Kind -> TcKind
-kindToTcKind kind = kind
-\end{code}
+ -- Note that 'sigma' is in prenex form:
+ -- all the foralls are at the front.
+ -- A 'phi' type has no foralls to the right of
+ -- an arrow
-Utility functions
-~~~~~~~~~~~~~~~~~
-These tcSplit functions are like their non-Tc analogues, but they
-follow through bound type variables.
+phi :: theta => rho
-No need for tcSplitForAllTy because a type variable can't be instantiated
-to a for-all type.
+rho ::= sigma -> rho
+ | tau
+
+-- A 'tau' type has no quantification anywhere
+-- Note that the args of a type constructor must be taus
+tau ::= tyvar
+ | tycon tau_1 .. tau_n
+ | tau_1 tau_2
+ | tau_1 -> tau_2
+
+-- In all cases, a (saturated) type synonym application is legal,
+-- provided it expands to the required form.
\begin{code}
-tcSplitRhoTy :: TcType -> NF_TcM s (TcThetaType, TcType)
-tcSplitRhoTy t
- = go t t []
- where
- -- A type variable is never instantiated to a dictionary type,
- -- so we don't need to do a tcReadVar on the "arg".
- go syn_t (FunTy arg res) ts = case splitDictTy_maybe arg of
- Just pair -> go res res (pair:ts)
- Nothing -> returnNF_Tc (reverse ts, syn_t)
- go syn_t (NoteTy _ t) ts = go syn_t t ts
- go syn_t (TyVarTy tv) ts = tcGetTyVar tv `thenNF_Tc` \ maybe_ty ->
- case maybe_ty of
- Just ty | not (isTyVarTy ty) -> go syn_t ty ts
- other -> returnNF_Tc (reverse ts, syn_t)
- go syn_t t ts = returnNF_Tc (reverse ts, syn_t)
+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 TcRhoType = 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}
%************************************************************************
%* *
-\subsection{New type variables}
+\subsection{TyVarDetails}
%* *
%************************************************************************
+TyVarDetails gives extra info about type variables, used during type
+checking. It's attached to mutable type variables only.
+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
+
+ 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}
-newTyVar :: Kind -> NF_TcM s TcTyVar
-newTyVar kind
- = tcGetUnique `thenNF_Tc` \ uniq ->
- tcNewMutTyVar (mkSysLocalName uniq SLIT("t")) kind
-
-newTyVarTy :: Kind -> NF_TcM s TcType
-newTyVarTy kind
- = newTyVar kind `thenNF_Tc` \ tc_tyvar ->
- returnNF_Tc (TyVarTy tc_tyvar)
-
-newTyVarTys :: Int -> Kind -> NF_TcM s [TcType]
-newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind)
-
-newKindVar :: NF_TcM s TcKind
-newKindVar
- = tcGetUnique `thenNF_Tc` \ uniq ->
- tcNewMutTyVar (mkSysLocalName uniq SLIT("k")) superKind `thenNF_Tc` \ kv ->
- returnNF_Tc (TyVarTy kv)
-
-newKindVars :: Int -> NF_TcM s [TcKind]
-newKindVars n = mapNF_Tc (\ _ -> newKindVar) (nOfThem n ())
-
--- Returns a type variable of kind (Type bv) where bv is a new boxity var
--- Used when you need a type variable that's definitely a , but you don't know
--- what kind of type (boxed or unboxed).
-newTyVarTy_OpenKind :: NF_TcM s TcType
-newTyVarTy_OpenKind = newOpenTypeKind `thenNF_Tc` \ kind ->
- newTyVarTy kind
-
-newOpenTypeKind :: NF_TcM s TcKind
-newOpenTypeKind = newTyVarTy superBoxity `thenNF_Tc` \ bv ->
- returnNF_Tc (mkTyConApp typeCon [bv])
+-- A TyVarDetails is inside a TyVar
+data TcTyVarDetails
+ = 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 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
+ SrcSpan -- a data constructor with an existential type. E.g.
+ -- data T = forall a. Eq a => MkT a
+ -- f (MkT x) = ...
+ -- The pattern MkT x will allocate an existential type
+ -- variable for 'a'.
+ | ArrowSkol SrcSpan -- An arrow form (see TcArrows)
+
+ | GenSkol [TcTyVar] -- Bound when doing a subsumption check for
+ TcType -- (forall tvs. ty)
+ SrcSpan
+
+ | 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}
-
%************************************************************************
%* *
-\subsection{Type instantiation}
+ Pretty-printing
%* *
%************************************************************************
-Instantiating a bunch of type variables
-
\begin{code}
-tcInstTyVars :: [TyVar]
- -> NF_TcM s ([TcTyVar], [TcType], Subst)
-
-tcInstTyVars tyvars
- = mapNF_Tc tcInstTyVar tyvars `thenNF_Tc` \ tc_tyvars ->
- let
- tys = mkTyVarTys tc_tyvars
- in
- returnNF_Tc (tc_tyvars, tys, mkTopTyVarSubst tyvars tys)
- -- Since the tyvars are freshly made,
- -- they cannot possibly be captured by
- -- any existing for-alls. Hence mkTopTyVarSubst
-
-tcInstTyVar tyvar
- = tcGetUnique `thenNF_Tc` \ uniq ->
- let
- name = setNameUnique (tyVarName tyvar) uniq
- -- Note that we don't change the print-name
- -- This won't confuse the type checker but there's a chance
- -- that two different tyvars will print the same way
- -- in an error message. -dppr-debug will show up the difference
- -- Better watch out for this. If worst comes to worst, just
- -- use mkSysLocalName.
-
- kind = tyVarKind tyvar
- in
-
- -- Hack alert! Certain system functions (like error) are quantified
- -- over type variables with an 'open' kind (a :: ?). When we instantiate
- -- these tyvars we want to make a type variable whose kind is (Type bv)
- -- where bv is a boxity variable. This makes sure it's a type, but
- -- is open about its boxity. We *don't* want to give the thing the
- -- kind '?' (= Type AnyBox).
- --
- -- This is all a hack to avoid giving error it's "proper" type:
- -- error :: forall bv. forall a::Type bv. String -> a
-
- (if kind == openTypeKind then
- newOpenTypeKind
- else
- returnNF_Tc kind) `thenNF_Tc` \ kind' ->
-
- tcNewMutTyVar name kind'
-
-tcInstSigVar tyvar -- Very similar to tcInstTyVar
- = tcGetUnique `thenNF_Tc` \ uniq ->
- let
- name = setNameUnique (tyVarName tyvar) uniq
- kind = tyVarKind tyvar
- in
- ASSERT( not (kind == openTypeKind) ) -- Shouldn't happen
- tcNewSigTyVar name kind
+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 )
+ (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}
-@tcInstTcType@ instantiates the outer-level for-alls of a TcType with
-fresh type variables, returning them and the instantiated body of the for-all.
+
+%************************************************************************
+%* *
+ Predicates
+%* *
+%************************************************************************
\begin{code}
-tcInstTcType :: TcType -> NF_TcM s ([TcTyVar], TcType)
-tcInstTcType ty
- = case splitForAllTys ty of
- ([], _) -> returnNF_Tc ([], ty) -- Nothing to do
- (tyvars, rho) -> tcInstTyVars tyvars `thenNF_Tc` \ (tyvars', _, tenv) ->
- returnNF_Tc (tyvars', substTy tenv rho)
+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
+
+isExistentialTyVar tv -- Existential type variable, bound by a pattern
+ = ASSERT( isTcTyVar tv )
+ case tcTyVarDetails tv of
+ SkolemTv (PatSkol _ _) -> True
+ 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
+ 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
+ other -> pprPanic "metaTvRef" (ppr tv)
+
+isFlexi, isIndirect :: MetaDetails -> Bool
+isFlexi Flexi = True
+isFlexi other = False
+
+isIndirect (Indirect _) = True
+isIndirect other = False
\end{code}
-
%************************************************************************
%* *
-\subsection{Putting and getting mutable type variables}
+\subsection{Tau, sigma and rho}
%* *
%************************************************************************
\begin{code}
-tcPutTyVar :: TcTyVar -> TcType -> NF_TcM s TcType
-tcGetTyVar :: TcTyVar -> NF_TcM s (Maybe TcType)
+mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkPhiTy theta tau)
+
+mkPhiTy :: [PredType] -> Type -> Type
+mkPhiTy theta ty = foldr (\p r -> FunTy (mkPredTy p) r) ty theta
\end{code}
-Putting is easy:
+@isTauTy@ tests for nested for-alls. It should not be called on a boxy type.
\begin{code}
-tcPutTyVar tyvar ty = tcWriteMutTyVar tyvar (Just ty) `thenNF_Tc_`
- returnNF_Tc ty
+isTauTy :: Type -> Bool
+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 (FunTy arg _) = getOccName funTyCon
+getDFunTyKey (ForAllTy _ t) = getDFunTyKey t
+getDFunTyKey ty = pprPanic "getDFunTyKey" (pprType ty)
+-- PredTy shouldn't happen
\end{code}
-Getting is more interesting. The easy thing to do is just to read, thus:
-\begin{verbatim}
-tcGetTyVar tyvar = tcReadMutTyVar tyvar
-\end{verbatim}
+%************************************************************************
+%* *
+\subsection{Expanding and splitting}
+%* *
+%************************************************************************
-But it's more fun to short out indirections on the way: If this
-version returns a TyVar, then that TyVar is unbound. If it returns
-any other type, then there might be bound TyVars embedded inside it.
+These tcSplit functions are like their non-Tc analogues, but
+ a) they do not look through newtypes
+ b) they do not look through PredTys
+ c) [future] they ignore usage-type annotations
-We return Nothing iff the original box was unbound.
+However, they are non-monadic and do not follow through mutable type
+variables. It's up to you to make sure this doesn't matter.
\begin{code}
-tcGetTyVar tyvar
- = ASSERT2( isMutTyVar tyvar, ppr tyvar )
- tcReadMutTyVar tyvar `thenNF_Tc` \ maybe_ty ->
- case maybe_ty of
- Just ty -> short_out ty `thenNF_Tc` \ ty' ->
- tcWriteMutTyVar tyvar (Just ty') `thenNF_Tc_`
- returnNF_Tc (Just 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 t tvs = (reverse tvs, orig_ty)
+
+tcIsForAllTy ty | Just ty' <- tcView ty = tcIsForAllTy ty'
+tcIsForAllTy (ForAllTy tv ty) = True
+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 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)
+
+tcTyConAppArgs :: Type -> [Type]
+tcTyConAppArgs ty = snd (tcSplitTyConApp 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' <- tcView ty = tcSplitTyConApp_maybe ty'
+tcSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
+tcSplitTyConApp_maybe (FunTy arg res) = Just (funTyCon, [arg,res])
+ -- Newtypes are opaque, so they may be split
+ -- However, predicates are not treated
+ -- as tycon applications by the type checker
+tcSplitTyConApp_maybe other = 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' <- tcView ty = tcSplitFunTy_maybe ty'
+tcSplitFunTy_maybe (FunTy arg res) = Just (arg, res)
+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)
- Nothing -> returnNF_Tc Nothing
+tcFunArgTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> arg }
+tcFunResultTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> res }
-short_out :: TcType -> NF_TcM s TcType
-short_out ty@(TyVarTy tyvar)
- | not (isMutTyVar tyvar)
- = returnNF_Tc ty
- | otherwise
- = tcReadMutTyVar tyvar `thenNF_Tc` \ maybe_ty ->
- case maybe_ty of
- Just ty' -> short_out ty' `thenNF_Tc` \ ty' ->
- tcWriteMutTyVar tyvar (Just ty') `thenNF_Tc_`
- returnNF_Tc ty'
+-----------------------
+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 (TyConApp tc tys) = case snocView tys of
+ Just (tys', ty') -> Just (TyConApp tc tys', ty')
+ Nothing -> Nothing
+tcSplitAppTy_maybe other = Nothing
- other -> returnNF_Tc ty
+tcSplitAppTy ty = case tcSplitAppTy_maybe ty of
+ Just stuff -> stuff
+ Nothing -> pprPanic "tcSplitAppTy" (pprType ty)
-short_out other_ty = returnNF_Tc other_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' <- tcView ty = tcGetTyVar_maybe ty'
+tcGetTyVar_maybe (TyVarTy tv) = Just tv
+tcGetTyVar_maybe other = Nothing
+
+tcGetTyVar :: String -> Type -> TyVar
+tcGetTyVar msg ty = expectJust msg (tcGetTyVar_maybe ty)
+
+tcIsTyVarTy :: Type -> Bool
+tcIsTyVarTy ty = maybeToBool (tcGetTyVar_maybe ty)
+
+-----------------------
+tcSplitDFunTy :: Type -> ([TyVar], [PredType], Class, [Type])
+-- Split the type of a dictionary function
+tcSplitDFunTy ty
+ = case tcSplitSigmaTy ty of { (tvs, theta, tau) ->
+ case tcSplitDFunHead tau of { (clas, tys) ->
+ (tvs, theta, clas, tys) }}
+
+tcSplitDFunHead :: Type -> (Class, [Type])
+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 -- Again, do not look
+ get_tv (TyVarTy tv) = Just tv -- through synonyms
+ get_tv other = Nothing
\end{code}
+
%************************************************************************
%* *
-\subsection{Zonking -- the exernal interfaces}
+\subsection{Predicate types}
%* *
%************************************************************************
------------------ Type variables
-
\begin{code}
-zonkTcTyVars :: [TcTyVar] -> NF_TcM s [TcType]
-zonkTcTyVars tyvars = mapNF_Tc zonkTcTyVar tyvars
-
-zonkTcTyVarBndr :: TcTyVar -> NF_TcM s TcTyVar
-zonkTcTyVarBndr tyvar
- = zonkTcTyVar tyvar `thenNF_Tc` \ (TyVarTy tyvar') ->
- returnNF_Tc tyvar'
+tcSplitPredTy_maybe :: Type -> Maybe PredType
+ -- Returns Just for predicates only
+tcSplitPredTy_maybe ty | Just ty' <- tcView ty = tcSplitPredTy_maybe ty'
+tcSplitPredTy_maybe (PredTy p) = Just p
+tcSplitPredTy_maybe other = Nothing
-zonkTcTyVar :: TcTyVar -> NF_TcM s TcType
-zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnNF_Tc (TyVarTy tv)) tyvar
+predTyUnique :: PredType -> Unique
+predTyUnique (IParam n _) = getUnique (ipNameName n)
+predTyUnique (ClassP clas tys) = getUnique clas
+
+mkPredName :: Unique -> SrcLoc -> PredType -> Name
+mkPredName uniq loc (ClassP cls tys) = mkInternalName uniq (mkDictOcc (getOccName cls)) loc
+mkPredName uniq loc (IParam ip ty) = mkInternalName uniq (getOccName (ipNameName ip)) loc
\end{code}
------------------ Types
+
+--------------------- Dictionary types ---------------------------------
\begin{code}
-zonkTcType :: TcType -> NF_TcM s TcType
-zonkTcType ty = zonkType (\ tv -> returnNF_Tc (TyVarTy tv)) ty
+mkClassPred clas tys = ClassP clas tys
-zonkTcTypes :: [TcType] -> NF_TcM s [TcType]
-zonkTcTypes tys = mapNF_Tc zonkTcType tys
+isClassPred :: PredType -> Bool
+isClassPred (ClassP clas tys) = True
+isClassPred other = False
-zonkTcThetaType :: TcThetaType -> NF_TcM s TcThetaType
-zonkTcThetaType theta = mapNF_Tc zonk theta
- where
- zonk (c,ts) = zonkTcTypes ts `thenNF_Tc` \ new_ts ->
- returnNF_Tc (c, new_ts)
+isTyVarClassPred (ClassP clas tys) = all tcIsTyVarTy tys
+isTyVarClassPred other = False
-zonkTcKind :: TcKind -> NF_TcM s TcKind
-zonkTcKind = zonkTcType
+getClassPredTys_maybe :: PredType -> Maybe (Class, [Type])
+getClassPredTys_maybe (ClassP clas tys) = Just (clas, tys)
+getClassPredTys_maybe _ = Nothing
+
+getClassPredTys :: PredType -> (Class, [Type])
+getClassPredTys (ClassP clas tys) = (clas, tys)
+
+mkDictTy :: Class -> [Type] -> Type
+mkDictTy clas tys = mkPredTy (ClassP clas tys)
+
+isDictTy :: Type -> Bool
+isDictTy ty | Just ty' <- tcView ty = isDictTy ty'
+isDictTy (PredTy p) = isClassPred p
+isDictTy other = False
\end{code}
-------------------- These ...ToType, ...ToKind versions
- are used at the end of type checking
+--------------------- Implicit parameters ---------------------------------
\begin{code}
-zonkTcKindToKind :: TcKind -> NF_TcM s Kind
-zonkTcKindToKind kind = zonkType zonk_unbound_kind_var kind
- where
- -- Zonk a mutable but unbound kind variable to
- -- (Type Boxed) if it has kind superKind
- -- Boxed if it has kind superBoxity
- zonk_unbound_kind_var kv
- | super_kind == superKind = tcPutTyVar kv boxedTypeKind
- | otherwise = ASSERT( super_kind == superBoxity )
- tcPutTyVar kv boxedKind
- where
- super_kind = tyVarKind kv
-
-
-zonkTcTypeToType :: TcType -> NF_TcM s Type
-zonkTcTypeToType ty = zonkType zonk_unbound_tyvar ty
+isIPPred :: PredType -> Bool
+isIPPred (IParam _ _) = True
+isIPPred other = False
+
+isInheritablePred :: PredType -> Bool
+-- Can be inherited by a context. For example, consider
+-- f x = let g y = (?v, y+x)
+-- in (g 3 with ?v = 8,
+-- g 4 with ?v = 9)
+-- The point is that g's type must be quantifed over ?v:
+-- g :: (?v :: a) => a -> a
+-- but it doesn't need to be quantified over the Num a dictionary
+-- which can be free in g's rhs, and shared by both calls to g
+isInheritablePred (ClassP _ _) = True
+isInheritablePred other = False
+
+isLinearPred :: TcPredType -> Bool
+isLinearPred (IParam (Linear n) _) = True
+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
- -- Zonk a mutable but unbound type variable to
- -- Void if it has kind (Type Boxed)
- -- Voidxxx otherwise
- zonk_unbound_tyvar tv
- = zonkTcKindToKind (tyVarKind tv) `thenNF_Tc` \ kind ->
- if kind == boxedTypeKind then
- tcPutTyVar tv voidTy -- Just to avoid creating a new tycon in
- -- this vastly common case
- else
- tcPutTyVar tv (TyConApp (mk_void_tycon tv kind) [])
-
- mk_void_tycon tv kind -- Make a new TyCon with the same kind as the
- -- type variable tv. Same name too, apart from
- -- making it start with a colon (sigh)
- = mkPrimTyCon tc_name kind 0 [] VoidRep
- where
- tc_name = mkDerivedName mkDerivedTyConOcc (getName tv) (getUnique tv)
-
--- zonkTcTyVarToTyVar is applied to the *binding* occurrence
--- of a type variable, at the *end* of type checking.
--- It zonks the type variable, to get a mutable, but unbound, tyvar, tv;
--- zonks its kind, and then makes an immutable version of tv and binds tv to it.
--- Now any bound occurences of the original type variable will get
--- zonked to the immutable version.
-
-zonkTcTyVarToTyVar :: TcTyVar -> NF_TcM s TyVar
-zonkTcTyVarToTyVar tv
- = zonkTcKindToKind (tyVarKind tv) `thenNF_Tc` \ kind ->
- let
- -- Make an immutable version
- immut_tv = mkTyVar (tyVarName tv) kind
- immut_tv_ty = mkTyVarTy immut_tv
-
- zap tv = tcPutTyVar tv immut_tv_ty
- -- Bind the mutable version to the immutable one
- in
- -- If the type variable is mutable, then bind it to immut_tv_ty
- -- so that all other occurrences of the tyvar will get zapped too
- zonkTyVar zap tv `thenNF_Tc` \ ty2 ->
- ASSERT2( immut_tv_ty == ty2, ppr tv $$ ppr immut_tv $$ ppr ty2 )
-
- returnNF_Tc immut_tv
+ 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}
%************************************************************************
%* *
-\subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
-%* *
-%* For internal use only! *
+\subsection{Predicates}
%* *
%************************************************************************
-\begin{code}
--- zonkType is used for Kinds as well
-
--- For unbound, mutable tyvars, zonkType uses the function given to it
--- For tyvars bound at a for-all, zonkType zonks them to an immutable
--- type variable and zonks the kind too
+isSigmaTy returns true of any qualified type. It doesn't *necessarily* have
+any foralls. E.g.
+ f :: (?x::Int) => Int -> Int
-zonkType :: (TcTyVar -> NF_TcM s Type) -- What to do with unbound mutable type variables
- -- see zonkTcType, and zonkTcTypeToType
- -> TcType
- -> NF_TcM s Type
-zonkType unbound_var_fn ty
- = go ty
- where
- go (TyConApp tycon tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
- returnNF_Tc (TyConApp tycon tys')
+\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 _ = 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 _ = False
+
+isPredTy :: Type -> Bool -- Belongs in TcType because it does
+ -- not look through newtypes, or predtypes (of course)
+isPredTy ty | Just ty' <- tcView ty = isPredTy ty'
+isPredTy (PredTy sty) = True
+isPredTy _ = False
+\end{code}
- go (NoteTy (SynNote ty1) ty2) = go ty1 `thenNF_Tc` \ ty1' ->
- go ty2 `thenNF_Tc` \ ty2' ->
- returnNF_Tc (NoteTy (SynNote ty1') ty2')
+\begin{code}
+isFloatTy = is_tc floatTyConKey
+isDoubleTy = is_tc doubleTyConKey
+isIntegerTy = is_tc integerTyConKey
+isIntTy = is_tc intTyConKey
+isAddrTy = is_tc addrTyConKey
+isBoolTy = is_tc boolTyConKey
+isUnitTy = is_tc unitTyConKey
+
+is_tc :: Unique -> Type -> Bool
+-- Newtypes are opaque to this
+is_tc uniq ty = case tcSplitTyConApp_maybe ty of
+ Just (tc, _) -> uniq == getUnique tc
+ Nothing -> False
+\end{code}
- go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard free-tyvar annotations
- go (NoteTy (UsgNote usg) ty2) = go ty2 `thenNF_Tc` \ ty2' ->
- returnNF_Tc (NoteTy (UsgNote usg) ty2')
+%************************************************************************
+%* *
+\subsection{Misc}
+%* *
+%************************************************************************
- go (FunTy arg res) = go arg `thenNF_Tc` \ arg' ->
- go res `thenNF_Tc` \ res' ->
- returnNF_Tc (FunTy arg' res')
-
- go (AppTy fun arg) = go fun `thenNF_Tc` \ fun' ->
- go arg `thenNF_Tc` \ arg' ->
- returnNF_Tc (mkAppTy fun' arg')
+\begin{code}
+deNoteType :: Type -> Type
+-- Remove all *outermost* type synonyms and other notes
+deNoteType ty | Just ty' <- tcView ty = deNoteType ty'
+deNoteType ty = ty
+\end{code}
- -- The two interesting cases!
- go (TyVarTy tyvar) = zonkTyVar unbound_var_fn tyvar
+\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}
- go (ForAllTy tyvar ty)
- = zonkTcTyVarToTyVar tyvar `thenNF_Tc` \ tyvar' ->
- go ty `thenNF_Tc` \ ty' ->
- returnNF_Tc (ForAllTy tyvar' ty')
+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}
-zonkTyVar :: (TcTyVar -> NF_TcM s Type) -- What to do for an unbound mutable variable
- -> TcTyVar -> NF_TcM s TcType
-zonkTyVar unbound_var_fn tyvar
- | not (isMutTyVar tyvar) -- Not a mutable tyvar. This can happen when
- -- zonking a forall type, when the bound type variable
- -- needn't be mutable
- = ASSERT( isTyVar tyvar ) -- Should not be any immutable kind vars
- returnNF_Tc (TyVarTy tyvar)
+Find the free tycons and classes of a type. This is used in the front
+end of the compiler.
- | otherwise
- = tcGetTyVar tyvar `thenNF_Tc` \ maybe_ty ->
- case maybe_ty of
- Nothing -> unbound_var_fn tyvar -- Mutable and unbound
- Just other_ty -> ASSERT( isNotUsgTy other_ty )
- zonkType unbound_var_fn other_ty -- Bound
+\begin{code}
+tyClsNamesOfType :: Type -> NameSet
+tyClsNamesOfType (TyVarTy tv) = emptyNameSet
+tyClsNamesOfType (TyConApp tycon tys) = unitNameSet (getName tycon) `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
+
+tyClsNamesOfTypes tys = foldr (unionNameSets . tyClsNamesOfType) emptyNameSet tys
+
+tyClsNamesOfDFunHead :: Type -> NameSet
+-- Find the free type constructors and classes
+-- of the head of the dfun instance type
+-- The 'dfun_head_type' is because of
+-- instance Foo a => Baz T where ...
+-- The decl is an orphan if Baz and T are both not locally defined,
+-- even if Foo *is* locally defined
+tyClsNamesOfDFunHead dfun_ty
+ = case tcSplitSigmaTy dfun_ty of
+ (tvs,_,head_ty) -> tyClsNamesOfType head_ty
+
+classesOfTheta :: ThetaType -> [Class]
+-- Looks just for ClassP things; maybe it should check
+classesOfTheta preds = [ c | ClassP c _ <- preds ]
\end{code}
+
%************************************************************************
%* *
-\subsection{tcTypeKind}
+\subsection[TysWiredIn-ext-type]{External types}
%* *
%************************************************************************
-Sadly, we need a Tc version of typeKind, that looks though mutable
-kind variables. See the notes with Type.typeKind for the typeKindF nonsense
+The compiler's foreign function interface supports the passing of a
+restricted set of types as arguments and results (the restricting factor
+being the )
-This is pretty gruesome.
+\begin{code}
+isFFITy :: Type -> Bool
+-- True for any TyCon that can possibly be an arg or result of an FFI call
+isFFITy ty = checkRepTyCon legalFFITyCon ty
+
+isFFIArgumentTy :: DynFlags -> Safety -> Type -> Bool
+-- Checks for valid argument type for a 'foreign import'
+isFFIArgumentTy dflags safety ty
+ = checkRepTyCon (legalOutgoingTyCon dflags safety) ty
+
+isFFIExternalTy :: Type -> Bool
+-- Types that are allowed as arguments of a 'foreign export'
+isFFIExternalTy ty = checkRepTyCon legalFEArgTyCon ty
+
+isFFIImportResultTy :: DynFlags -> Type -> Bool
+isFFIImportResultTy dflags ty
+ = checkRepTyCon (legalFIResultTyCon dflags) ty
+
+isFFIExportResultTy :: Type -> Bool
+isFFIExportResultTy ty = checkRepTyCon legalFEResultTyCon ty
+
+isFFIDynArgumentTy :: Type -> Bool
+-- The argument type of a foreign import dynamic must be Ptr, FunPtr, Addr,
+-- or a newtype of either.
+isFFIDynArgumentTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey, addrTyConKey]
+
+isFFIDynResultTy :: Type -> Bool
+-- The result type of a foreign export dynamic must be Ptr, FunPtr, Addr,
+-- or a newtype of either.
+isFFIDynResultTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey, addrTyConKey]
+
+isFFILabelTy :: Type -> Bool
+-- The type of a foreign label must be Ptr, FunPtr, Addr,
+-- or a newtype of either.
+isFFILabelTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey, addrTyConKey]
+
+isFFIDotnetTy :: DynFlags -> Type -> Bool
+isFFIDotnetTy dflags ty
+ = checkRepTyCon (\ tc -> not (isByteArrayLikeTyCon tc) &&
+ (legalFIResultTyCon dflags tc ||
+ isFFIDotnetObjTy ty || isStringTy ty)) ty
+
+-- Support String as an argument or result from a .NET FFI call.
+isStringTy ty =
+ case tcSplitTyConApp_maybe (repType ty) of
+ Just (tc, [arg_ty])
+ | tc == listTyCon ->
+ case tcSplitTyConApp_maybe (repType arg_ty) of
+ Just (cc,[]) -> cc == charTyCon
+ _ -> False
+ _ -> False
+
+-- Support String as an argument or result from a .NET FFI call.
+isFFIDotnetObjTy ty =
+ let
+ (_, t_ty) = tcSplitForAllTys ty
+ in
+ case tcSplitTyConApp_maybe (repType t_ty) of
+ Just (tc, [arg_ty]) | getName tc == objectTyConName -> True
+ _ -> False
+
+toDNType :: Type -> DNType
+toDNType ty
+ | isStringTy ty = DNString
+ | isFFIDotnetObjTy ty = DNObject
+ | Just (tc,argTys) <- tcSplitTyConApp_maybe ty =
+ case lookup (getUnique tc) dn_assoc of
+ Just x -> x
+ Nothing
+ | tc `hasKey` ioTyConKey -> toDNType (head argTys)
+ | otherwise -> pprPanic ("toDNType: unsupported .NET type") (pprType ty <+> parens (hcat (map pprType argTys)) <+> ppr tc)
+ where
+ dn_assoc :: [ (Unique, DNType) ]
+ dn_assoc = [ (unitTyConKey, DNUnit)
+ , (intTyConKey, DNInt)
+ , (int8TyConKey, DNInt8)
+ , (int16TyConKey, DNInt16)
+ , (int32TyConKey, DNInt32)
+ , (int64TyConKey, DNInt64)
+ , (wordTyConKey, DNInt)
+ , (word8TyConKey, DNWord8)
+ , (word16TyConKey, DNWord16)
+ , (word32TyConKey, DNWord32)
+ , (word64TyConKey, DNWord64)
+ , (floatTyConKey, DNFloat)
+ , (doubleTyConKey, DNDouble)
+ , (addrTyConKey, DNPtr)
+ , (ptrTyConKey, DNPtr)
+ , (funPtrTyConKey, DNPtr)
+ , (charTyConKey, DNChar)
+ , (boolTyConKey, DNBool)
+ ]
+
+checkRepTyCon :: (TyCon -> Bool) -> Type -> Bool
+ -- Look through newtypes
+ -- Non-recursive ones are transparent to splitTyConApp,
+ -- but recursive ones aren't. Manuel had:
+ -- newtype T = MkT (Ptr T)
+ -- and wanted it to work...
+checkRepTyCon check_tc ty
+ | Just (tc,_) <- splitTyConApp_maybe (repType ty) = check_tc tc
+ | otherwise = False
+
+checkRepTyConKey :: [Unique] -> Type -> Bool
+-- Like checkRepTyCon, but just looks at the TyCon key
+checkRepTyConKey keys
+ = checkRepTyCon (\tc -> tyConUnique tc `elem` keys)
+\end{code}
+
+----------------------------------------------
+These chaps do the work; they are not exported
+----------------------------------------------
\begin{code}
-tcTypeKind :: TcType -> NF_TcM s TcKind
-
-tcTypeKind (TyVarTy tyvar) = returnNF_Tc (tyVarKind tyvar)
-tcTypeKind (TyConApp tycon tys) = foldlTc (\k _ -> tcFunResultTy k) (tyConKind tycon) tys
-tcTypeKind (NoteTy _ ty) = tcTypeKind ty
-tcTypeKind (AppTy fun arg) = tcTypeKind fun `thenNF_Tc` \ fun_kind ->
- tcFunResultTy fun_kind
-tcTypeKind (FunTy fun arg) = tcTypeKindF arg
-tcTypeKind (ForAllTy _ ty) = tcTypeKindF ty
-
-tcTypeKindF :: TcType -> NF_TcM s TcKind
-tcTypeKindF (NoteTy _ ty) = tcTypeKindF ty
-tcTypeKindF (FunTy _ ty) = tcTypeKindF ty
-tcTypeKindF (ForAllTy _ ty) = tcTypeKindF ty
-tcTypeKindF other = tcTypeKind other `thenNF_Tc` \ kind ->
- fix_up kind
- where
- fix_up (TyConApp kc _) | kc == typeCon = returnNF_Tc boxedTypeKind
- -- Functions at the type level are always boxed
- fix_up (NoteTy _ kind) = fix_up kind
- fix_up kind@(TyVarTy tv) = tcGetTyVar tv `thenNF_Tc` \ maybe_ty ->
- case maybe_ty of
- Just kind' -> fix_up kind'
- Nothing -> returnNF_Tc kind
- fix_up kind = returnNF_Tc kind
-
-tcFunResultTy (NoteTy _ ty) = tcFunResultTy ty
-tcFunResultTy (FunTy arg res) = returnNF_Tc res
-tcFunResultTy (TyVarTy tv) = tcGetTyVar tv `thenNF_Tc` \ maybe_ty ->
- case maybe_ty of
- Just ty' -> tcFunResultTy ty'
- -- The Nothing case, and the other cases for tcFunResultTy
- -- should never happen... pattern match failure
+legalFEArgTyCon :: TyCon -> Bool
+-- It's illegal to return foreign objects and (mutable)
+-- bytearrays from a _ccall_ / foreign declaration
+-- (or be passed them as arguments in foreign exported functions).
+legalFEArgTyCon tc
+ | isByteArrayLikeTyCon tc
+ = False
+ -- It's also illegal to make foreign exports that take unboxed
+ -- arguments. The RTS API currently can't invoke such things. --SDM 7/2000
+ | otherwise
+ = boxedMarshalableTyCon tc
+
+legalFIResultTyCon :: DynFlags -> TyCon -> Bool
+legalFIResultTyCon dflags tc
+ | isByteArrayLikeTyCon tc = False
+ | tc == unitTyCon = True
+ | otherwise = marshalableTyCon dflags tc
+
+legalFEResultTyCon :: TyCon -> Bool
+legalFEResultTyCon tc
+ | isByteArrayLikeTyCon tc = False
+ | tc == unitTyCon = True
+ | otherwise = boxedMarshalableTyCon tc
+
+legalOutgoingTyCon :: DynFlags -> Safety -> TyCon -> Bool
+-- Checks validity of types going from Haskell -> external world
+legalOutgoingTyCon dflags safety tc
+ | playSafe safety && isByteArrayLikeTyCon tc
+ = False
+ | otherwise
+ = marshalableTyCon dflags tc
+
+legalFFITyCon :: TyCon -> Bool
+-- True for any TyCon that can possibly be an arg or result of an FFI call
+legalFFITyCon tc
+ = isUnLiftedTyCon tc || boxedMarshalableTyCon tc || tc == unitTyCon
+
+marshalableTyCon dflags tc
+ = (dopt Opt_GlasgowExts dflags && isUnLiftedTyCon tc)
+ || boxedMarshalableTyCon tc
+
+boxedMarshalableTyCon tc
+ = getUnique tc `elem` [ intTyConKey, int8TyConKey, int16TyConKey
+ , int32TyConKey, int64TyConKey
+ , wordTyConKey, word8TyConKey, word16TyConKey
+ , word32TyConKey, word64TyConKey
+ , floatTyConKey, doubleTyConKey
+ , addrTyConKey, ptrTyConKey, funPtrTyConKey
+ , charTyConKey
+ , stablePtrTyConKey
+ , byteArrayTyConKey, mutableByteArrayTyConKey
+ , boolTyConKey
+ ]
+
+isByteArrayLikeTyCon :: TyCon -> Bool
+isByteArrayLikeTyCon tc =
+ getUnique tc `elem` [byteArrayTyConKey, mutableByteArrayTyConKey]
\end{code}
projects / ghc-hetmet.git / blobdiff