%
\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,
-
- tcInstTyVars,
- tcInstSigVar,
- tcInstTcType,
-
- typeToTcType,
+\begin{code}
+module TcType (
+ --------------------------------
+ -- Types
+ TcType, TcSigmaType, TcRhoType, TcTauType, TcPredType, TcThetaType,
+ TcTyVar, TcTyVarSet, TcKind,
- tcTypeKind, -- :: TcType -> NF_TcM s TcKind
--------------------------------
- TcKind,
- newKindVar, newKindVars,
- kindToTcKind,
- zonkTcKind,
+ -- TyVarDetails
+ TyVarDetails(..), isUserTyVar, isSkolemTyVar, isHoleTyVar,
+ tyVarBindingInfo,
--------------------------------
- zonkTcTyVar, zonkTcTyVars, zonkTcTyVarBndr,
- zonkTcType, zonkTcTypes, zonkTcThetaType,
+ -- Builders
+ mkPhiTy, mkSigmaTy,
- zonkTcTypeToType, zonkTcTyVarToTyVar,
- zonkTcKindToKind
+ --------------------------------
+ -- Splitters
+ -- These are important because they do not look through newtypes
+ tcSplitForAllTys, tcSplitPhiTy,
+ tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy,
+ tcSplitTyConApp, tcSplitTyConApp_maybe, tcTyConAppTyCon, tcTyConAppArgs,
+ tcSplitAppTy_maybe, tcSplitAppTy, tcSplitSigmaTy,
+ tcSplitMethodTy, tcGetTyVar_maybe, tcGetTyVar,
+
+ ---------------------------------
+ -- Predicates.
+ -- Again, newtypes are opaque
+ tcEqType, tcEqTypes, tcEqPred, tcCmpType, tcCmpTypes, tcCmpPred,
+ isSigmaTy, isOverloadedTy,
+ isDoubleTy, isFloatTy, isIntTy,
+ isIntegerTy, isAddrTy, isBoolTy, isUnitTy,
+ isTauTy, tcIsTyVarTy, tcIsForAllTy,
+ allDistinctTyVars,
+
+ ---------------------------------
+ -- Misc type manipulators
+ deNoteType,
+ namesOfType, namesOfDFunHead,
+ getDFunTyKey,
+
+ ---------------------------------
+ -- Predicate types
+ PredType, getClassPredTys_maybe, getClassPredTys,
+ isPredTy, isClassPred, isTyVarClassPred, predHasFDs,
+ mkDictTy, tcSplitPredTy_maybe, predTyUnique,
+ isDictTy, tcSplitDFunTy, predTyUnique,
+ mkClassPred, isInheritablePred, isLinearPred, isIPPred, mkPredName,
+
+ ---------------------------------
+ -- 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
+
+ ---------------------------------
+ -- Unifier and matcher
+ unifyTysX, unifyTyListsX, unifyExtendTysX,
+ matchTy, matchTys, match,
+ --------------------------------
+ -- Rexported from Type
+ Kind, -- Stuff to do with kinds is insensitive to pre/post Tc
+ unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds,
+ superBoxity, liftedBoxity, hasMoreBoxityInfo, defaultKind, superKind,
+ isTypeKind, isAnyTypeKind,
+
+ Type, SourceType(..), PredType, ThetaType,
+ mkForAllTy, mkForAllTys,
+ mkFunTy, mkFunTys, zipFunTys,
+ mkTyConApp, mkGenTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
+ mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy, mkPredTys,
+
+ isUnLiftedType, -- Source types are always lifted
+ isUnboxedTupleType, -- Ditto
+ isPrimitiveType, isTyVarTy,
+
+ tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
+ tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars,
+ typeKind, eqKind, eqUsage,
+
+ tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta
) where
#include "HsVersions.h"
+import {-# SOURCE #-} PprType( pprType )
+
-- friends:
-import PprType ( pprType )
-import TypeRep ( Type(..), Kind, TyNote(..),
- typeCon, openTypeKind, boxedTypeKind, boxedKind, superKind, superBoxity
- ) -- friend
-import Type ( ThetaType,
- mkAppTy, mkTyConApp,
- splitDictTy_maybe, splitForAllTys, isNotUsgTy,
- isTyVarTy, mkTyVarTy, mkTyVarTys,
+import TypeRep ( Type(..), TyNote(..), funTyCon ) -- friend
+
+import Type ( -- Re-exports
+ tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
+ Kind, Type, SourceType(..), PredType, ThetaType,
+ unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds,
+ mkForAllTy, mkForAllTys, defaultKind, isTypeKind, isAnyTypeKind,
+ mkFunTy, mkFunTys, zipFunTys, isTyVarTy,
+ mkTyConApp, mkGenTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
+ mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy, mkPredTys,
+ isUnLiftedType, isUnboxedTupleType, isPrimitiveType,
+ splitNewType_maybe, splitTyConApp_maybe,
+ tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
+ tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars, eqKind, eqUsage,
+ hasMoreBoxityInfo, liftedBoxity, superBoxity, typeKind, superKind
)
-import Subst ( Subst, mkTopTyVarSubst, substTy )
-import TyCon ( tyConKind, mkPrimTyCon )
-import PrimRep ( PrimRep(VoidRep) )
+import TyCon ( TyCon, isUnLiftedTyCon )
+import Class ( classHasFDs, Class )
+import Var ( TyVar, tyVarKind, isMutTyVar, mutTyVarDetails )
+import ForeignCall ( Safety, playSafe )
import VarEnv
-import VarSet ( emptyVarSet )
-import Var ( TyVar, tyVarKind, tyVarName, isTyVar, isMutTyVar, mkTyVar )
+import VarSet
-- others:
-import TcMonad
-import TysWiredIn ( voidTy )
-
-import Name ( NamedThing(..), setNameUnique, mkSysLocalName,
- mkDerivedName, mkDerivedTyConOcc
- )
+import CmdLineOpts ( DynFlags, DynFlag( Opt_GlasgowExts ), dopt )
+import Name ( Name, NamedThing(..), mkInternalName, getSrcLoc )
+import OccName ( OccName, mkDictOcc )
+import NameSet
+import PrelNames -- Lots (e.g. in isFFIArgumentTy)
+import TysWiredIn ( ptrTyCon, funPtrTyCon, addrTyCon, unitTyCon )
+import BasicTypes ( IPName(..), ipNameName )
import Unique ( Unique, Uniquable(..) )
-import Util ( nOfThem )
+import SrcLoc ( SrcLoc )
+import Util ( cmpList, thenCmp, equalLength )
+import Maybes ( maybeToBool, expectJust )
import Outputable
\end{code}
+%************************************************************************
+%* *
+\subsection{Types}
+%* *
+%************************************************************************
+
+The type checker divides the generic Type world into the
+following more structured beasts:
-Coercions
-~~~~~~~~~~
-Type definitions are in TcMonad.lhs
+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
-\begin{code}
-typeToTcType :: Type -> TcType
-typeToTcType ty = ty
+ -- 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
-kindToTcKind :: Kind -> TcKind
-kindToTcKind kind = kind
-\end{code}
+phi :: theta => rho
+
+rho ::= sigma -> rho
+ | tau
-Utility functions
-~~~~~~~~~~~~~~~~~
-These tcSplit functions are like their non-Tc analogues, but they
-follow through bound type variables.
+-- 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.
-No need for tcSplitForAllTy because a type variable can't be instantiated
-to a for-all type.
\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 SigmaType = Type
+type RhoType = Type
+type TauType = Type
+\end{code}
+
+\begin{code}
+type TcTyVar = TyVar -- Might be a mutable tyvar
+type TcTyVarSet = TyVarSet
+
+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
+
+type TcPredType = PredType
+type TcThetaType = ThetaType
+type TcSigmaType = TcType
+type TcRhoType = TcType
+type TcTauType = TcType
+type TcKind = 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.
+
\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])
+data TyVarDetails
+ = HoleTv -- Used *only* by the type checker when passing in a type
+ -- variable that should be side-effected to the result type.
+ -- Always has kind openTypeKind.
+ -- Never appears in types
+
+ | SigTv -- Introduced when instantiating a type signature,
+ -- prior to checking that the defn of a fn does
+ -- have the expected type. Should not be instantiated.
+ --
+ -- f :: forall a. a -> a
+ -- f = e
+ -- When checking e, with expected type (a->a), we
+ -- should not instantiate a
+
+ | ClsTv -- Scoped type variable introduced by a class decl
+ -- class C a where ...
+
+ | InstTv -- Ditto, but instance decl
+
+ | PatSigTv -- Scoped type variable, introduced by a pattern
+ -- type signature
+ -- \ x::a -> e
+
+ | VanillaTv -- Everything else
+
+isUserTyVar :: TcTyVar -> Bool -- Avoid unifying these if possible
+isUserTyVar tv = case mutTyVarDetails tv of
+ VanillaTv -> False
+ other -> True
+
+isSkolemTyVar :: TcTyVar -> Bool
+isSkolemTyVar tv = case mutTyVarDetails tv of
+ SigTv -> True
+ ClsTv -> True
+ InstTv -> True
+ oteher -> False
+
+isHoleTyVar :: TcTyVar -> Bool
+-- NB: the hole might be filled in by now, and this
+-- function does not check for that
+isHoleTyVar tv = ASSERT( isMutTyVar tv )
+ case mutTyVarDetails tv of
+ HoleTv -> True
+ other -> False
+
+tyVarBindingInfo :: TyVar -> SDoc -- Used in checkSigTyVars
+tyVarBindingInfo tv
+ | isMutTyVar tv
+ = sep [ptext SLIT("is bound by the") <+> details (mutTyVarDetails tv),
+ ptext SLIT("at") <+> ppr (getSrcLoc tv)]
+ | otherwise
+ = empty
+ where
+ details SigTv = ptext SLIT("type signature")
+ details ClsTv = ptext SLIT("class declaration")
+ details InstTv = ptext SLIT("instance declaration")
+ details PatSigTv = ptext SLIT("pattern type signature")
+ details HoleTv = ptext SLIT("//hole//") -- Should not happen
+ details VanillaTv = ptext SLIT("//vanilla//") -- Ditto
\end{code}
%************************************************************************
%* *
-\subsection{Type instantiation}
+\subsection{Tau, sigma and rho}
%* *
%************************************************************************
-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
+mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkPhiTy theta tau)
+
+mkPhiTy :: [SourceType] -> Type -> Type
+mkPhiTy theta ty = foldr (\p r -> FunTy (mkPredTy p) r) ty theta
\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.
+
+@isTauTy@ tests for nested for-alls.
\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)
+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 (SourceTy p) = True -- Don't look through source types
+isTauTy (NoteTy _ ty) = isTauTy ty
+isTauTy other = False
\end{code}
+\begin{code}
+getDFunTyKey :: Type -> OccName -- Get some string from a type, to be used to
+ -- construct a dictionary function name
+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 (SourceTy (NType tc _)) = getOccName tc -- Newtypes are quite reasonable
+getDFunTyKey ty = pprPanic "getDFunTyKey" (pprType ty)
+-- SourceTy shouldn't happen
+\end{code}
%************************************************************************
%* *
-\subsection{Putting and getting mutable type variables}
+\subsection{Expanding and splitting}
%* *
%************************************************************************
+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
+
+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}
-tcPutTyVar :: TcTyVar -> TcType -> NF_TcM s TcType
-tcGetTyVar :: TcTyVar -> NF_TcM s (Maybe TcType)
+tcSplitForAllTys :: Type -> ([TyVar], Type)
+tcSplitForAllTys ty = split ty ty []
+ where
+ 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 (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 (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)
+
+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 (TyConApp tc tys) = Just (tc, tys)
+tcSplitTyConApp_maybe (FunTy arg res) = Just (funTyCon, [arg,res])
+tcSplitTyConApp_maybe (NoteTy n ty) = tcSplitTyConApp_maybe ty
+tcSplitTyConApp_maybe (SourceTy (NType tc tys)) = Just (tc,tys)
+ -- 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 (FunTy arg res) = Just (arg, res)
+tcSplitFunTy_maybe (NoteTy n ty) = tcSplitFunTy_maybe ty
+tcSplitFunTy_maybe other = Nothing
+
+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 (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 (SourceTy (NType tc tys)) = tc_split_app tc tys
+ --- Don't forget that newtype!
+tcSplitAppTy_maybe (TyConApp tc tys) = tc_split_app tc tys
+tcSplitAppTy_maybe other = Nothing
+
+tc_split_app tc [] = Nothing
+tc_split_app tc tys = split tys []
+ where
+ split [ty2] acc = Just (TyConApp tc (reverse acc), ty2)
+ split (ty:tys) acc = split tys (ty:acc)
+
+tcSplitAppTy ty = case tcSplitAppTy_maybe ty of
+ Just stuff -> stuff
+ Nothing -> pprPanic "tcSplitAppTy" (pprType ty)
+
+tcGetTyVar_maybe :: Type -> Maybe TyVar
+tcGetTyVar_maybe (TyVarTy tv) = Just tv
+tcGetTyVar_maybe (NoteTy _ t) = tcGetTyVar_maybe t
+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)
\end{code}
-Putting is easy:
+The type of a method for class C is always of the form:
+ Forall a1..an. C a1..an => sig_ty
+where sig_ty is the type given by the method's signature, and thus in general
+is a ForallTy. At the point that splitMethodTy is called, it is expected
+that the outer Forall has already been stripped off. splitMethodTy then
+returns (C a1..an, sig_ty') where sig_ty' is sig_ty with any Notes or
+Usages stripped off.
\begin{code}
-tcPutTyVar tyvar ty = tcWriteMutTyVar tyvar (Just ty) `thenNF_Tc_`
- returnNF_Tc ty
+tcSplitMethodTy :: Type -> (PredType, Type)
+tcSplitMethodTy ty = split ty
+ where
+ split (FunTy arg res) = case tcSplitPredTy_maybe arg of
+ Just p -> (p, res)
+ Nothing -> panic "splitMethodTy"
+ split (NoteTy n ty) = split ty
+ split _ = panic "splitMethodTy"
+
+tcSplitDFunTy :: Type -> ([TyVar], [SourceType], Class, [Type])
+-- Split the type of a dictionary function
+tcSplitDFunTy ty
+ = case tcSplitSigmaTy ty of { (tvs, theta, tau) ->
+ case tcSplitPredTy_maybe tau of { Just (ClassP clas tys) ->
+ (tvs, theta, clas, tys) }}
\end{code}
-Getting is more interesting. The easy thing to do is just to read, thus:
+(allDistinctTyVars tys tvs) = True
+ iff
+all the types tys are type variables,
+distinct from each other and from tvs.
+
+This is useful when checking that unification hasn't unified signature
+type variables. For example, if the type sig is
+ f :: forall a b. a -> b -> b
+we want to check that 'a' and 'b' havn't
+ (a) been unified with a non-tyvar type
+ (b) been unified with each other (all distinct)
+ (c) been unified with a variable free in the environment
+
+\begin{code}
+allDistinctTyVars :: [Type] -> TyVarSet -> Bool
-\begin{verbatim}
-tcGetTyVar tyvar = tcReadMutTyVar tyvar
-\end{verbatim}
+allDistinctTyVars [] acc
+ = True
+allDistinctTyVars (ty:tys) acc
+ = case tcGetTyVar_maybe ty of
+ Nothing -> False -- (a)
+ Just tv | tv `elemVarSet` acc -> False -- (b) or (c)
+ | otherwise -> allDistinctTyVars tys (acc `extendVarSet` tv)
+\end{code}
-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.
-We return Nothing iff the original box was unbound.
+%************************************************************************
+%* *
+\subsection{Predicate types}
+%* *
+%************************************************************************
+
+"Predicates" are particular source types, namelyClassP or IParams
\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')
+isPred :: SourceType -> Bool
+isPred (ClassP _ _) = True
+isPred (IParam _ _) = True
+isPred (NType _ _) = False
+
+isPredTy :: Type -> Bool
+isPredTy (NoteTy _ ty) = isPredTy ty
+isPredTy (SourceTy sty) = isPred sty
+isPredTy _ = False
+
+tcSplitPredTy_maybe :: Type -> Maybe PredType
+ -- Returns Just for predicates only
+tcSplitPredTy_maybe (NoteTy _ ty) = tcSplitPredTy_maybe ty
+tcSplitPredTy_maybe (SourceTy p) | isPred p = Just p
+tcSplitPredTy_maybe other = Nothing
+
+predTyUnique :: PredType -> Unique
+predTyUnique (IParam n _) = getUnique (ipNameName n)
+predTyUnique (ClassP clas tys) = getUnique clas
+
+predHasFDs :: PredType -> Bool
+-- True if the predicate has functional depenencies;
+-- I.e. should participate in improvement
+predHasFDs (IParam _ _) = True
+predHasFDs (ClassP cls _) = classHasFDs cls
+
+mkPredName :: Unique -> SrcLoc -> SourceType -> 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}
- Nothing -> returnNF_Tc Nothing
-short_out :: TcType -> NF_TcM s TcType
-short_out ty@(TyVarTy tyvar)
- | not (isMutTyVar tyvar)
- = returnNF_Tc ty
+--------------------- Dictionary types ---------------------------------
- | 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'
+\begin{code}
+mkClassPred clas tys = ClassP clas tys
+
+isClassPred :: SourceType -> Bool
+isClassPred (ClassP clas tys) = True
+isClassPred other = False
- other -> returnNF_Tc ty
+isTyVarClassPred (ClassP clas tys) = all tcIsTyVarTy tys
+isTyVarClassPred other = False
-short_out other_ty = returnNF_Tc other_ty
+getClassPredTys_maybe :: SourceType -> 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 (SourceTy p) = isClassPred p
+isDictTy (NoteTy _ ty) = isDictTy ty
+isDictTy other = False
+\end{code}
+
+--------------------- Implicit parameters ---------------------------------
+
+\begin{code}
+isIPPred :: SourceType -> 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}
%************************************************************************
%* *
-\subsection{Zonking -- the exernal interfaces}
+\subsection{Comparison}
%* *
%************************************************************************
------------------ Type variables
+Comparison, taking note of newtypes, predicates, etc,
+But ignoring usage types
\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` \ ty ->
- case ty of
- TyVarTy tyvar' -> returnNF_Tc tyvar'
- _ -> pprTrace "zonkTcTyVarBndr" (ppr tyvar <+> ppr ty) $
- returnNF_Tc tyvar
-
-zonkTcTyVar :: TcTyVar -> NF_TcM s TcType
-zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnNF_Tc (TyVarTy tv)) tyvar
+tcEqType :: Type -> Type -> Bool
+tcEqType ty1 ty2 = case ty1 `tcCmpType` ty2 of { EQ -> True; other -> False }
+
+tcEqTypes :: [Type] -> [Type] -> Bool
+tcEqTypes ty1 ty2 = case ty1 `tcCmpTypes` ty2 of { EQ -> True; other -> False }
+
+tcEqPred :: PredType -> PredType -> Bool
+tcEqPred p1 p2 = case p1 `tcCmpPred` p2 of { EQ -> True; other -> False }
+
+-------------
+tcCmpType :: Type -> Type -> Ordering
+tcCmpType ty1 ty2 = cmpTy emptyVarEnv ty1 ty2
+
+tcCmpTypes tys1 tys2 = cmpTys emptyVarEnv tys1 tys2
+
+tcCmpPred p1 p2 = cmpSourceTy emptyVarEnv p1 p2
+-------------
+cmpTys env tys1 tys2 = cmpList (cmpTy env) tys1 tys2
+
+-------------
+cmpTy :: TyVarEnv TyVar -> Type -> Type -> Ordering
+ -- The "env" maps type variables in ty1 to type variables in ty2
+ -- So when comparing for-alls.. (forall tv1 . t1) (forall tv2 . t2)
+ -- we in effect substitute tv2 for tv1 in t1 before continuing
+
+ -- Look through NoteTy
+cmpTy env (NoteTy _ ty1) ty2 = cmpTy env ty1 ty2
+cmpTy env ty1 (NoteTy _ ty2) = cmpTy env ty1 ty2
+
+ -- Deal with equal constructors
+cmpTy env (TyVarTy tv1) (TyVarTy tv2) = case lookupVarEnv env tv1 of
+ Just tv1a -> tv1a `compare` tv2
+ Nothing -> tv1 `compare` tv2
+
+cmpTy env (SourceTy p1) (SourceTy p2) = cmpSourceTy env p1 p2
+cmpTy env (AppTy f1 a1) (AppTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
+cmpTy env (FunTy f1 a1) (FunTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
+cmpTy env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
+cmpTy env (ForAllTy tv1 t1) (ForAllTy tv2 t2) = cmpTy (extendVarEnv env tv1 tv2) t1 t2
+
+ -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy < SourceTy
+cmpTy env (AppTy _ _) (TyVarTy _) = GT
+
+cmpTy env (FunTy _ _) (TyVarTy _) = GT
+cmpTy env (FunTy _ _) (AppTy _ _) = GT
+
+cmpTy env (TyConApp _ _) (TyVarTy _) = GT
+cmpTy env (TyConApp _ _) (AppTy _ _) = GT
+cmpTy env (TyConApp _ _) (FunTy _ _) = GT
+
+cmpTy env (ForAllTy _ _) (TyVarTy _) = GT
+cmpTy env (ForAllTy _ _) (AppTy _ _) = GT
+cmpTy env (ForAllTy _ _) (FunTy _ _) = GT
+cmpTy env (ForAllTy _ _) (TyConApp _ _) = GT
+
+cmpTy env (SourceTy _) t2 = GT
+
+cmpTy env _ _ = LT
\end{code}
------------------ Types
+\begin{code}
+cmpSourceTy :: TyVarEnv TyVar -> SourceType -> SourceType -> Ordering
+cmpSourceTy env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` (cmpTy env ty1 ty2)
+ -- Compare types as well as names for implicit parameters
+ -- This comparison is used exclusively (I think) for the
+ -- finite map built in TcSimplify
+cmpSourceTy env (IParam _ _) sty = LT
+
+cmpSourceTy env (ClassP _ _) (IParam _ _) = GT
+cmpSourceTy env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` (cmpTys env tys1 tys2)
+cmpSourceTy env (ClassP _ _) (NType _ _) = LT
+
+cmpSourceTy env (NType tc1 tys1) (NType tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
+cmpSourceTy env (NType _ _) sty = GT
+\end{code}
+
+PredTypes are used as a FM key in TcSimplify,
+so we take the easy path and make them an instance of Ord
\begin{code}
-zonkTcType :: TcType -> NF_TcM s TcType
-zonkTcType ty = zonkType (\ tv -> returnNF_Tc (TyVarTy tv)) ty
+instance Eq SourceType where { (==) = tcEqPred }
+instance Ord SourceType where { compare = tcCmpPred }
+\end{code}
-zonkTcTypes :: [TcType] -> NF_TcM s [TcType]
-zonkTcTypes tys = mapNF_Tc zonkTcType tys
-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)
+%************************************************************************
+%* *
+\subsection{Predicates}
+%* *
+%************************************************************************
-zonkTcKind :: TcKind -> NF_TcM s TcKind
-zonkTcKind = zonkTcType
-\end{code}
+isSigmaTy returns true of any qualified type. It doesn't *necessarily* have
+any foralls. E.g.
+ f :: (?x::Int) => Int -> Int
-------------------- These ...ToType, ...ToKind versions
- are used at the end of type checking
+\begin{code}
+isSigmaTy :: Type -> Bool
+isSigmaTy (ForAllTy tyvar ty) = True
+isSigmaTy (FunTy a b) = isPredTy a
+isSigmaTy (NoteTy n ty) = isSigmaTy ty
+isSigmaTy _ = False
+
+isOverloadedTy :: Type -> Bool
+isOverloadedTy (ForAllTy tyvar ty) = isOverloadedTy ty
+isOverloadedTy (FunTy a b) = isPredTy a
+isOverloadedTy (NoteTy n ty) = isOverloadedTy ty
+isOverloadedTy _ = False
+\end{code}
\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
- 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
+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}
%************************************************************************
%* *
-\subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
-%* *
-%* For internal use only! *
+\subsection{Misc}
%* *
%************************************************************************
\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
-
-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')
+deNoteType :: Type -> Type
+ -- Remove synonyms, but not source types
+deNoteType ty@(TyVarTy tyvar) = ty
+deNoteType (TyConApp tycon tys) = TyConApp tycon (map deNoteType tys)
+deNoteType (SourceTy p) = SourceTy (deNoteSourceType 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)
+
+deNoteSourceType :: SourceType -> SourceType
+deNoteSourceType (ClassP c tys) = ClassP c (map deNoteType tys)
+deNoteSourceType (IParam n ty) = IParam n (deNoteType ty)
+deNoteSourceType (NType tc tys) = NType tc (map deNoteType tys)
+\end{code}
+
+Find the free names of a type, including the type constructors and classes it mentions
+This is used in the front end of the compiler
+
+\begin{code}
+namesOfType :: Type -> NameSet
+namesOfType (TyVarTy tv) = unitNameSet (getName tv)
+namesOfType (TyConApp tycon tys) = unitNameSet (getName tycon) `unionNameSets` namesOfTypes tys
+namesOfType (NoteTy (SynNote ty1) ty2) = namesOfType ty1
+namesOfType (NoteTy other_note ty2) = namesOfType ty2
+namesOfType (SourceTy (IParam n ty)) = namesOfType ty
+namesOfType (SourceTy (ClassP cl tys)) = unitNameSet (getName cl) `unionNameSets` namesOfTypes tys
+namesOfType (SourceTy (NType tc tys)) = unitNameSet (getName tc) `unionNameSets` namesOfTypes tys
+namesOfType (FunTy arg res) = namesOfType arg `unionNameSets` namesOfType res
+namesOfType (AppTy fun arg) = namesOfType fun `unionNameSets` namesOfType arg
+namesOfType (ForAllTy tyvar ty) = namesOfType ty `delFromNameSet` getName tyvar
+
+namesOfTypes tys = foldr (unionNameSets . namesOfType) emptyNameSet tys
+
+namesOfDFunHead :: 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
+namesOfDFunHead dfun_ty = case tcSplitSigmaTy dfun_ty of
+ (tvs,_,head_ty) -> delListFromNameSet (namesOfType head_ty)
+ (map getName tvs)
+\end{code}
- go (NoteTy (SynNote ty1) ty2) = go ty1 `thenNF_Tc` \ ty1' ->
- go ty2 `thenNF_Tc` \ ty2' ->
- returnNF_Tc (NoteTy (SynNote ty1') ty2')
- go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard free-tyvar annotations
+%************************************************************************
+%* *
+\subsection[TysWiredIn-ext-type]{External types}
+%* *
+%************************************************************************
- go (NoteTy (UsgNote usg) ty2) = go ty2 `thenNF_Tc` \ ty2' ->
- returnNF_Tc (NoteTy (UsgNote usg) ty2')
+The compiler's foreign function interface supports the passing of a
+restricted set of types as arguments and results (the restricting factor
+being the )
- go (NoteTy (UsgForAll uv) ty2)= go ty2 `thenNF_Tc` \ ty2' ->
- returnNF_Tc (NoteTy (UsgForAll uv) ty2')
+\begin{code}
+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 = checkRepTyCon (\tc -> tc == ptrTyCon || tc == funPtrTyCon || tc == addrTyCon)
+
+isFFIDynResultTy :: Type -> Bool
+-- The result type of a foreign export dynamic must be Ptr, FunPtr, Addr,
+-- or a newtype of either.
+isFFIDynResultTy = checkRepTyCon (\tc -> tc == ptrTyCon || tc == funPtrTyCon || tc == addrTyCon)
+
+isFFILabelTy :: Type -> Bool
+-- The type of a foreign label must be Ptr, FunPtr, Addr,
+-- or a newtype of either.
+isFFILabelTy = checkRepTyCon (\tc -> tc == ptrTyCon || tc == funPtrTyCon || tc == addrTyCon)
+
+checkRepTyCon :: (TyCon -> Bool) -> Type -> Bool
+ -- Look through newtypes
+ -- Non-recursive ones are transparent to splitTyConApp,
+ -- but recursive ones aren't; hence the splitNewType_maybe
+checkRepTyCon check_tc ty
+ | Just ty' <- splitNewType_maybe ty = checkRepTyCon check_tc ty'
+ | Just (tc,_) <- splitTyConApp_maybe ty = check_tc tc
+ | otherwise = False
+\end{code}
- 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')
+----------------------------------------------
+These chaps do the work; they are not exported
+----------------------------------------------
- -- The two interesting cases!
- go (TyVarTy tyvar) = zonkTyVar unbound_var_fn tyvar
+\begin{code}
+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
+ | getUnique tc `elem` [ byteArrayTyConKey, mutableByteArrayTyConKey ]
+ = 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
+ | getUnique tc `elem`
+ [ byteArrayTyConKey, mutableByteArrayTyConKey ] = False
+ | tc == unitTyCon = True
+ | otherwise = marshalableTyCon dflags tc
+
+legalFEResultTyCon :: TyCon -> Bool
+legalFEResultTyCon tc
+ | getUnique tc `elem`
+ [ byteArrayTyConKey, mutableByteArrayTyConKey ] = 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 && getUnique tc `elem` [byteArrayTyConKey, mutableByteArrayTyConKey]
+ = False
+ | otherwise
+ = marshalableTyCon dflags tc
+
+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
+ ]
+\end{code}
- go (ForAllTy tyvar ty)
- = zonkTcTyVarToTyVar tyvar `thenNF_Tc` \ tyvar' ->
- go ty `thenNF_Tc` \ ty' ->
- returnNF_Tc (ForAllTy tyvar' ty')
+%************************************************************************
+%* *
+\subsection{Unification with an explicit substitution}
+%* *
+%************************************************************************
-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)
+Unify types with an explicit substitution and no monad.
+Ignore usage annotations.
- | 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}
+type MySubst
+ = (TyVarSet, -- Set of template tyvars
+ TyVarSubstEnv) -- Not necessarily idempotent
+
+unifyTysX :: TyVarSet -- Template tyvars
+ -> Type
+ -> Type
+ -> Maybe TyVarSubstEnv
+unifyTysX tmpl_tyvars ty1 ty2
+ = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
+
+unifyExtendTysX :: TyVarSet -- Template tyvars
+ -> TyVarSubstEnv -- Substitution to start with
+ -> Type
+ -> Type
+ -> Maybe TyVarSubstEnv -- Extended substitution
+unifyExtendTysX tmpl_tyvars subst ty1 ty2
+ = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, subst)
+
+unifyTyListsX :: TyVarSet -> [Type] -> [Type]
+ -> Maybe TyVarSubstEnv
+unifyTyListsX tmpl_tyvars tys1 tys2
+ = uTyListsX tys1 tys2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
+
+
+uTysX :: Type
+ -> Type
+ -> (MySubst -> Maybe result)
+ -> MySubst
+ -> Maybe result
+
+uTysX (NoteTy _ ty1) ty2 k subst = uTysX ty1 ty2 k subst
+uTysX ty1 (NoteTy _ ty2) k subst = uTysX ty1 ty2 k subst
+
+ -- Variables; go for uVar
+uTysX (TyVarTy tyvar1) (TyVarTy tyvar2) k subst
+ | tyvar1 == tyvar2
+ = k subst
+uTysX (TyVarTy tyvar1) ty2 k subst@(tmpls,_)
+ | tyvar1 `elemVarSet` tmpls
+ = uVarX tyvar1 ty2 k subst
+uTysX ty1 (TyVarTy tyvar2) k subst@(tmpls,_)
+ | tyvar2 `elemVarSet` tmpls
+ = uVarX tyvar2 ty1 k subst
+
+ -- Predicates
+uTysX (SourceTy (IParam n1 t1)) (SourceTy (IParam n2 t2)) k subst
+ | n1 == n2 = uTysX t1 t2 k subst
+uTysX (SourceTy (ClassP c1 tys1)) (SourceTy (ClassP c2 tys2)) k subst
+ | c1 == c2 = uTyListsX tys1 tys2 k subst
+uTysX (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) k subst
+ | tc1 == tc2 = uTyListsX tys1 tys2 k subst
+
+ -- Functions; just check the two parts
+uTysX (FunTy fun1 arg1) (FunTy fun2 arg2) k subst
+ = uTysX fun1 fun2 (uTysX arg1 arg2 k) subst
+
+ -- Type constructors must match
+uTysX (TyConApp con1 tys1) (TyConApp con2 tys2) k subst
+ | (con1 == con2 && equalLength tys1 tys2)
+ = uTyListsX tys1 tys2 k subst
+
+ -- Applications need a bit of care!
+ -- They can match FunTy and TyConApp, so use splitAppTy_maybe
+ -- NB: we've already dealt with type variables and Notes,
+ -- so if one type is an App the other one jolly well better be too
+uTysX (AppTy s1 t1) ty2 k subst
+ = case tcSplitAppTy_maybe ty2 of
+ Just (s2, t2) -> uTysX s1 s2 (uTysX t1 t2 k) subst
+ Nothing -> Nothing -- Fail
+
+uTysX ty1 (AppTy s2 t2) k subst
+ = case tcSplitAppTy_maybe ty1 of
+ Just (s1, t1) -> uTysX s1 s2 (uTysX t1 t2 k) subst
+ Nothing -> Nothing -- Fail
+
+ -- Not expecting for-alls in unification
+#ifdef DEBUG
+uTysX (ForAllTy _ _) ty2 k subst = panic "Unify.uTysX subst:ForAllTy (1st arg)"
+uTysX ty1 (ForAllTy _ _) k subst = panic "Unify.uTysX subst:ForAllTy (2nd arg)"
+#endif
+
+ -- Anything else fails
+uTysX ty1 ty2 k subst = Nothing
+
+
+uTyListsX [] [] k subst = k subst
+uTyListsX (ty1:tys1) (ty2:tys2) k subst = uTysX ty1 ty2 (uTyListsX tys1 tys2 k) subst
+uTyListsX tys1 tys2 k subst = Nothing -- Fail if the lists are different lengths
\end{code}
+\begin{code}
+-- Invariant: tv1 is a unifiable variable
+uVarX tv1 ty2 k subst@(tmpls, env)
+ = case lookupSubstEnv env tv1 of
+ Just (DoneTy ty1) -> -- Already bound
+ uTysX ty1 ty2 k subst
+
+ Nothing -- Not already bound
+ | typeKind ty2 `eqKind` tyVarKind tv1
+ && occur_check_ok ty2
+ -> -- No kind mismatch nor occur check
+ k (tmpls, extendSubstEnv env tv1 (DoneTy ty2))
+
+ | otherwise -> Nothing -- Fail if kind mis-match or occur check
+ where
+ occur_check_ok ty = all occur_check_ok_tv (varSetElems (tyVarsOfType ty))
+ occur_check_ok_tv tv | tv1 == tv = False
+ | otherwise = case lookupSubstEnv env tv of
+ Nothing -> True
+ Just (DoneTy ty) -> occur_check_ok ty
+\end{code}
+
+
+
%************************************************************************
%* *
-\subsection{tcTypeKind}
+\subsection{Matching on 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
+Matching is a {\em unidirectional} process, matching a type against a
+template (which is just a type with type variables in it). The
+matcher assumes that there are no repeated type variables in the
+template, so that it simply returns a mapping of type variables to
+types. It also fails on nested foralls.
-This is pretty gruesome.
+@matchTys@ matches corresponding elements of a list of templates and
+types. It and @matchTy@ both ignore usage annotations, unlike the
+main function @match@.
\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
+matchTy :: TyVarSet -- Template tyvars
+ -> Type -- Template
+ -> Type -- Proposed instance of template
+ -> Maybe TyVarSubstEnv -- Matching substitution
+
+
+matchTys :: TyVarSet -- Template tyvars
+ -> [Type] -- Templates
+ -> [Type] -- Proposed instance of template
+ -> Maybe (TyVarSubstEnv, -- Matching substitution
+ [Type]) -- Left over instance types
+
+matchTy tmpls ty1 ty2 = match ty1 ty2 tmpls (\ senv -> Just senv) emptySubstEnv
+
+matchTys tmpls tys1 tys2 = match_list tys1 tys2 tmpls
+ (\ (senv,tys) -> Just (senv,tys))
+ emptySubstEnv
+\end{code}
+
+@match@ is the main function. It takes a flag indicating whether
+usage annotations are to be respected.
+
+\begin{code}
+match :: Type -> Type -- Current match pair
+ -> TyVarSet -- Template vars
+ -> (TyVarSubstEnv -> Maybe result) -- Continuation
+ -> TyVarSubstEnv -- Current subst
+ -> Maybe result
+
+-- When matching against a type variable, see if the variable
+-- has already been bound. If so, check that what it's bound to
+-- is the same as ty; if not, bind it and carry on.
+
+match (TyVarTy v) ty tmpls k senv
+ | v `elemVarSet` tmpls
+ = -- v is a template variable
+ case lookupSubstEnv senv v of
+ Nothing | typeKind ty `eqKind` tyVarKind v
+ -- We do a kind check, just as in the uVarX above
+ -- The kind check is needed to avoid bogus matches
+ -- of (a b) with (c d), where the kinds don't match
+ -- An occur check isn't needed when matching.
+ -> k (extendSubstEnv senv v (DoneTy ty))
+
+ | otherwise -> Nothing -- Fails
+
+ Just (DoneTy ty') | ty' `tcEqType` ty -> k senv -- Succeeds
+ | otherwise -> Nothing -- Fails
+
+ | otherwise
+ = -- v is not a template variable; ty had better match
+ -- Can't use (==) because types differ
+ case tcGetTyVar_maybe ty of
+ Just v' | v == v' -> k senv -- Success
+ other -> Nothing -- Failure
+ -- This tcGetTyVar_maybe is *required* because it must strip Notes.
+ -- I guess the reason the Note-stripping case is *last* rather than first
+ -- is to preserve type synonyms etc., so I'm not moving it to the
+ -- top; but this means that (without the deNotetype) a type
+ -- variable may not match the pattern (TyVarTy v') as one would
+ -- expect, due to an intervening Note. KSW 2000-06.
+
+ -- Predicates
+match (SourceTy (IParam n1 t1)) (SourceTy (IParam n2 t2)) tmpls k senv
+ | n1 == n2 = match t1 t2 tmpls k senv
+match (SourceTy (ClassP c1 tys1)) (SourceTy (ClassP c2 tys2)) tmpls k senv
+ | c1 == c2 = match_list_exactly tys1 tys2 tmpls k senv
+match (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) tmpls k senv
+ | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
+
+ -- Functions; just check the two parts
+match (FunTy arg1 res1) (FunTy arg2 res2) tmpls k senv
+ = match arg1 arg2 tmpls (match res1 res2 tmpls k) senv
+
+match (AppTy fun1 arg1) ty2 tmpls k senv
+ = case tcSplitAppTy_maybe ty2 of
+ Just (fun2,arg2) -> match fun1 fun2 tmpls (match arg1 arg2 tmpls k) senv
+ Nothing -> Nothing -- Fail
+
+match (TyConApp tc1 tys1) (TyConApp tc2 tys2) tmpls k senv
+ | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
+
+-- Newtypes are opaque; other source types should not happen
+match (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) tmpls k senv
+ | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
+
+ -- With type synonyms, we have to be careful for the exact
+ -- same reasons as in the unifier. Please see the
+ -- considerable commentary there before changing anything
+ -- here! (WDP 95/05)
+match (NoteTy n1 ty1) ty2 tmpls k senv = match ty1 ty2 tmpls k senv
+match ty1 (NoteTy n2 ty2) tmpls k senv = match ty1 ty2 tmpls k senv
+
+-- Catch-all fails
+match _ _ _ _ _ = Nothing
+
+match_list_exactly tys1 tys2 tmpls k senv
+ = match_list tys1 tys2 tmpls k' senv
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
+ k' (senv', tys2') | null tys2' = k senv' -- Succeed
+ | otherwise = Nothing -- Fail
+
+match_list [] tys2 tmpls k senv = k (senv, tys2)
+match_list (ty1:tys1) [] tmpls k senv = Nothing -- Not enough arg tys => failure
+match_list (ty1:tys1) (ty2:tys2) tmpls k senv
+ = match ty1 ty2 tmpls (match_list tys1 tys2 tmpls k) senv
\end{code}
projects / ghc-hetmet.git / blobdiff