module TcType (
--------------------------------
-- Types
- TauType, RhoType, SigmaType,
+ TcType, TcSigmaType, TcPhiType, TcTauType, TcPredType, TcThetaType,
+ TcTyVar, TcTyVarSet, TcKind,
+
+ --------------------------------
+ -- TyVarDetails
+ TyVarDetails(..), isUserTyVar, isSkolemTyVar, isHoleTyVar,
+ tyVarBindingInfo,
--------------------------------
-- Builders
---------------------------------
-- Predicates.
-- Again, newtypes are opaque
- tcEqType, tcEqPred, tcCmpType, tcCmpTypes, tcCmpPred,
- isQualifiedTy, isOverloadedTy, isStrictType, isStrictPred,
+ tcEqType, tcEqTypes, tcEqPred, tcCmpType, tcCmpTypes, tcCmpPred,
+ isSigmaTy, isOverloadedTy,
isDoubleTy, isFloatTy, isIntTy,
- isIntegerTy, isAddrTy, isBoolTy, isUnitTy, isForeignPtrTy, isPrimitiveType,
+ isIntegerTy, isAddrTy, isBoolTy, isUnitTy, isForeignPtrTy,
isTauTy, tcIsTyVarTy, tcIsForAllTy,
---------------------------------
---------------------------------
-- Predicate types
- PredType, mkPredTy, mkPredTys, getClassPredTys_maybe, getClassPredTys,
+ PredType, getClassPredTys_maybe, getClassPredTys,
isPredTy, isClassPred, isTyVarClassPred, predHasFDs,
mkDictTy, tcSplitPredTy_maybe, predTyUnique,
isDictTy, tcSplitDFunTy, predTyUnique,
- mkClassPred, predMentionsIPs, inheritablePred, isIPPred, mkPredName,
+ mkClassPred, inheritablePred, 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
Kind, -- Stuff to do with kinds is insensitive to pre/post Tc
unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds,
superBoxity, liftedBoxity, hasMoreBoxityInfo, defaultKind, superKind,
+ isTypeKind,
Type, SourceType(..), PredType, ThetaType,
mkForAllTy, mkForAllTys,
mkFunTy, mkFunTys, zipFunTys,
mkTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
- mkTyVarTy, mkTyVarTys, mkTyConTy,
+ mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy, mkPredTys,
isUnLiftedType, -- Source types are always lifted
isUnboxedTupleType, -- Ditto
+ isPrimitiveType,
tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
- tidyTyVar, tidyTyVars,
+ tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars,
typeKind, eqKind, eqUsage,
tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta
import Type ( -- Re-exports
tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
- Kind, Type, TauType, SourceType(..), PredType, ThetaType,
+ Kind, Type, SourceType(..), PredType, ThetaType,
unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds,
- mkForAllTy, mkForAllTys, defaultKind,
+ mkForAllTy, mkForAllTys, defaultKind, isTypeKind,
mkFunTy, mkFunTys, zipFunTys,
mkTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
- mkTyVarTy, mkTyVarTys, mkTyConTy,
- isUnLiftedType, isUnboxedTupleType,
+ mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy, mkPredTys,
+ isUnLiftedType, isUnboxedTupleType, isPrimitiveType,
+ splitNewType_maybe, splitTyConApp_maybe,
tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
- tidyTyVar, tidyTyVars, eqKind, eqUsage,
+ tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars, eqKind, eqUsage,
hasMoreBoxityInfo, liftedBoxity, superBoxity, typeKind, superKind
)
-import TyCon ( TyCon, isPrimTyCon, tyConArity, isNewTyCon )
-import Class ( classTyCon, classHasFDs, Class )
-import Var ( TyVar, tyVarKind )
+import TyCon ( TyCon, isUnLiftedTyCon )
+import Class ( classHasFDs, Class )
+import Var ( TyVar, tyVarKind, isMutTyVar, mutTyVarDetails )
+import ForeignCall ( Safety, playSafe )
import VarEnv
import VarSet
-- others:
-import CmdLineOpts ( opt_DictsStrict )
-import Name ( Name, NamedThing(..), mkLocalName )
+import CmdLineOpts ( DynFlags, DynFlag( Opt_GlasgowExts ), dopt )
+import Name ( Name, NamedThing(..), mkLocalName, getSrcLoc )
import OccName ( OccName, mkDictOcc )
import NameSet
-import PrelNames ( floatTyConKey, doubleTyConKey, foreignPtrTyConKey,
- integerTyConKey, intTyConKey, addrTyConKey, boolTyConKey )
-import Unique ( Unique, Uniquable(..), mkTupleTyConUnique )
+import PrelNames -- Lots (e.g. in isFFIArgumentTy)
+import TysWiredIn ( ptrTyCon, funPtrTyCon, addrTyCon, unitTyCon )
+import BasicTypes ( ipNameName )
+import Unique ( Unique, Uniquable(..) )
import SrcLoc ( SrcLoc )
-import Util ( cmpList, thenCmp )
+import Util ( cmpList, thenCmp, equalLength )
import Maybes ( maybeToBool, expectJust )
-import BasicTypes ( Boxity(..) )
import Outputable
\end{code}
%************************************************************************
%* *
-\subsection{Tau, sigma and rho}
+\subsection{Types}
+%* *
+%************************************************************************
+
+The type checker divides the generic Type world into the
+following more structured beasts:
+
+sigma ::= forall tyvars. theta => phi
+ -- A sigma type is a qualified type
+ --
+ -- Note that even if 'tyvars' is empty, theta
+ -- may not be: e.g. (?x::Int) => Int
+
+ -- 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
+
+phi ::= sigma -> phi
+ | 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}
+type SigmaType = Type
+type PhiType = 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 TcPhiType = TcType
+type TcTauType = TcType
+type TcKind = TcType
+\end{code}
+
+
+%************************************************************************
+%* *
+\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}
-type SigmaType = Type
-type RhoType = Type
+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
+ 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{Tau, sigma and rho}
+%* *
+%************************************************************************
+\begin{code}
mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkRhoTy theta tau)
mkRhoTy :: [SourceType] -> Type -> Type
isPred :: SourceType -> Bool
isPred (ClassP _ _) = True
isPred (IParam _ _) = True
-isPred (NType _ __) = False
+isPred (NType _ _) = False
isPredTy :: Type -> Bool
isPredTy (NoteTy _ ty) = isPredTy ty
tcSplitPredTy_maybe (UsageTy _ ty) = tcSplitPredTy_maybe ty
tcSplitPredTy_maybe (SourceTy p) | isPred p = Just p
tcSplitPredTy_maybe other = Nothing
-
-mkPredTy :: PredType -> Type
-mkPredTy pred = SourceTy pred
-
-mkPredTys :: ThetaType -> [Type]
-mkPredTys preds = map SourceTy preds
-
+
predTyUnique :: PredType -> Unique
-predTyUnique (IParam n _) = getUnique n
+predTyUnique (IParam n _) = getUnique (ipNameName n)
predTyUnique (ClassP clas tys) = getUnique clas
predHasFDs :: PredType -> Bool
mkPredName :: Unique -> SrcLoc -> SourceType -> Name
mkPredName uniq loc (ClassP cls tys) = mkLocalName uniq (mkDictOcc (getOccName cls)) loc
-mkPredName uniq loc (IParam name ty) = name
+mkPredName uniq loc (IParam ip ty) = mkLocalName uniq (getOccName (ipNameName ip)) loc
\end{code}
-- which can be free in g's rhs, and shared by both calls to g
inheritablePred (ClassP _ _) = True
inheritablePred other = False
-
-predMentionsIPs :: SourceType -> NameSet -> Bool
-predMentionsIPs (IParam n _) ns = n `elemNameSet` ns
-predMentionsIPs other ns = False
\end{code}
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 }
\begin{code}
cmpSourceTy :: TyVarEnv TyVar -> SourceType -> SourceType -> Ordering
-cmpSourceTy env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` (cmpTy env ty1 ty2)
+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
%* *
%************************************************************************
-isQualifiedTy returns true of any qualified type. It doesn't *necessarily* have
+isSigmaTy returns true of any qualified type. It doesn't *necessarily* have
any foralls. E.g.
f :: (?x::Int) => Int -> Int
\begin{code}
-isQualifiedTy :: Type -> Bool
-isQualifiedTy (ForAllTy tyvar ty) = True
-isQualifiedTy (FunTy a b) = isPredTy a
-isQualifiedTy (NoteTy n ty) = isQualifiedTy ty
-isQualifiedTy (UsageTy _ ty) = isQualifiedTy ty
-isQualifiedTy _ = False
+isSigmaTy :: Type -> Bool
+isSigmaTy (ForAllTy tyvar ty) = True
+isSigmaTy (FunTy a b) = isPredTy a
+isSigmaTy (NoteTy n ty) = isSigmaTy ty
+isSigmaTy (UsageTy _ ty) = isSigmaTy ty
+isSigmaTy _ = False
isOverloadedTy :: Type -> Bool
isOverloadedTy (ForAllTy tyvar ty) = isOverloadedTy ty
isIntTy = is_tc intTyConKey
isAddrTy = is_tc addrTyConKey
isBoolTy = is_tc boolTyConKey
-isUnitTy = is_tc (mkTupleTyConUnique Boxed 0)
+isUnitTy = is_tc unitTyConKey
is_tc :: Unique -> Type -> Bool
-- Newtypes are opaque to this
Nothing -> False
\end{code}
-\begin{code}
-isPrimitiveType :: Type -> Bool
--- Returns types that are opaque to Haskell.
--- Most of these are unlifted, but now that we interact with .NET, we
--- may have primtive (foreign-imported) types that are lifted
-isPrimitiveType ty = case tcSplitTyConApp_maybe ty of
- Just (tc, ty_args) -> ASSERT( length ty_args == tyConArity tc )
- isPrimTyCon tc
- other -> False
-\end{code}
-
-@isStrictType@ computes whether an argument (or let RHS) should
-be computed strictly or lazily, based only on its type
-
-\begin{code}
-isStrictType :: Type -> Bool
-isStrictType ty
- | isUnLiftedType ty = True
- | Just pred <- tcSplitPredTy_maybe ty = isStrictPred pred
- | otherwise = False
-
-isStrictPred (ClassP clas _) = opt_DictsStrict
- && not (isNewTyCon (classTyCon clas))
-isStrictPred pred = False
- -- We may be strict in dictionary types, but only if it
- -- has more than one component.
- -- [Being strict in a single-component dictionary risks
- -- poking the dictionary component, which is wrong.]
-\end{code}
-
%************************************************************************
%* *
deNoteType (UsageTy u ty) = UsageTy u (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)
+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
%************************************************************************
%* *
+\subsection[TysWiredIn-ext-type]{External types}
+%* *
+%************************************************************************
+
+The compiler's foreign function interface supports the passing of a
+restricted set of types as arguments and results (the restricting factor
+being the )
+
+\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}
+
+----------------------------------------------
+These chaps do the work; they are not exported
+----------------------------------------------
+
+\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` [ foreignObjTyConKey, foreignPtrTyConKey,
+ 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`
+ [ foreignObjTyConKey, foreignPtrTyConKey,
+ byteArrayTyConKey, mutableByteArrayTyConKey ] = False
+ | tc == unitTyCon = True
+ | otherwise = marshalableTyCon dflags tc
+
+legalFEResultTyCon :: TyCon -> Bool
+legalFEResultTyCon tc
+ | getUnique tc `elem`
+ [ foreignObjTyConKey, foreignPtrTyConKey,
+ 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, foreignObjTyConKey
+ , foreignPtrTyConKey
+ , stablePtrTyConKey
+ , byteArrayTyConKey, mutableByteArrayTyConKey
+ , boolTyConKey
+ ]
+\end{code}
+
+
+%************************************************************************
+%* *
\subsection{Unification with an explicit substitution}
%* *
%************************************************************************
| 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 && length tys1 == length tys2)
+ | (con1 == con2 && equalLength tys1 tys2)
= uTyListsX tys1 tys2 k subst
-- Applications need a bit of care!
-- 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
Nothing -> Nothing -- Fail
match (TyConApp tc1 tys1) (TyConApp tc2 tys2) tmpls k senv
- | tc1 == tc2 = match_tc_app tys1 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_tc_app tys1 tys2 tmpls k senv
+ | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
match (UsageTy _ ty1) ty2 tmpls k senv = match ty1 ty2 tmpls k senv
match ty1 (UsageTy _ ty2) tmpls k senv = match ty1 ty2 tmpls k senv
-- Catch-all fails
match _ _ _ _ _ = Nothing
-match_tc_app tys1 tys2 tmpls k senv
+match_list_exactly tys1 tys2 tmpls k senv
= match_list tys1 tys2 tmpls k' senv
where
k' (senv', tys2') | null tys2' = k senv' -- Succeed