2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 \section[TcType]{Types used in the typechecker}
6 This module provides the Type interface for front-end parts of the
9 * treat "source types" as opaque:
10 newtypes, and predicates are meaningful.
11 * look through usage types
13 The "tc" prefix is for "typechechecker", because the type checker
14 is the principal client.
18 --------------------------------
20 TcType, TcSigmaType, TcPhiType, TcTauType, TcPredType, TcThetaType,
21 TcTyVar, TcTyVarSet, TcKind,
23 --------------------------------
25 TyVarDetails(..), isUserTyVar, isSkolemTyVar, isHoleTyVar,
28 --------------------------------
32 --------------------------------
34 -- These are important because they do not look through newtypes
35 tcSplitForAllTys, tcSplitRhoTy,
36 tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy,
37 tcSplitTyConApp, tcSplitTyConApp_maybe, tcTyConAppTyCon, tcTyConAppArgs,
38 tcSplitAppTy_maybe, tcSplitAppTy, tcSplitSigmaTy,
39 tcSplitMethodTy, tcGetTyVar_maybe, tcGetTyVar,
41 ---------------------------------
43 -- Again, newtypes are opaque
44 tcEqType, tcEqTypes, tcEqPred, tcCmpType, tcCmpTypes, tcCmpPred,
45 isSigmaTy, isOverloadedTy,
46 isDoubleTy, isFloatTy, isIntTy,
47 isIntegerTy, isAddrTy, isBoolTy, isUnitTy, isForeignPtrTy,
48 isTauTy, tcIsTyVarTy, tcIsForAllTy,
50 ---------------------------------
51 -- Misc type manipulators
52 hoistForAllTys, deNoteType,
53 namesOfType, namesOfDFunHead,
56 ---------------------------------
58 PredType, getClassPredTys_maybe, getClassPredTys,
59 isPredTy, isClassPred, isTyVarClassPred, predHasFDs,
60 mkDictTy, tcSplitPredTy_maybe, predTyUnique,
61 isDictTy, tcSplitDFunTy, predTyUnique,
62 mkClassPred, inheritablePred, isIPPred, mkPredName,
64 ---------------------------------
65 -- Foreign import and export
66 isFFIArgumentTy, -- :: DynFlags -> Safety -> Type -> Bool
67 isFFIImportResultTy, -- :: DynFlags -> Type -> Bool
68 isFFIExportResultTy, -- :: Type -> Bool
69 isFFIExternalTy, -- :: Type -> Bool
70 isFFIDynArgumentTy, -- :: Type -> Bool
71 isFFIDynResultTy, -- :: Type -> Bool
72 isFFILabelTy, -- :: Type -> Bool
74 ---------------------------------
75 -- Unifier and matcher
76 unifyTysX, unifyTyListsX, unifyExtendTysX,
78 matchTy, matchTys, match,
80 --------------------------------
81 -- Rexported from Type
82 Kind, -- Stuff to do with kinds is insensitive to pre/post Tc
83 unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds,
84 superBoxity, liftedBoxity, hasMoreBoxityInfo, defaultKind, superKind,
87 Type, SourceType(..), PredType, ThetaType,
88 mkForAllTy, mkForAllTys,
89 mkFunTy, mkFunTys, zipFunTys,
90 mkTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
91 mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy, mkPredTys,
93 isUnLiftedType, -- Source types are always lifted
94 isUnboxedTupleType, -- Ditto
97 tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
98 tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars,
99 typeKind, eqKind, eqUsage,
101 tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta
104 #include "HsVersions.h"
107 import {-# SOURCE #-} PprType( pprType )
110 import TypeRep ( Type(..), TyNote(..), funTyCon ) -- friend
111 import Type ( mkUTyM, unUTy ) -- Used locally
113 import Type ( -- Re-exports
114 tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
115 Kind, Type, SourceType(..), PredType, ThetaType,
116 unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds,
117 mkForAllTy, mkForAllTys, defaultKind, isTypeKind,
118 mkFunTy, mkFunTys, zipFunTys,
119 mkTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
120 mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy, mkPredTys,
121 isUnLiftedType, isUnboxedTupleType, isPrimitiveType,
122 splitNewType_maybe, splitTyConApp_maybe,
123 tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
124 tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars, eqKind, eqUsage,
125 hasMoreBoxityInfo, liftedBoxity, superBoxity, typeKind, superKind
127 import TyCon ( TyCon, isUnLiftedTyCon )
128 import Class ( classHasFDs, Class )
129 import Var ( TyVar, tyVarKind, isMutTyVar, mutTyVarDetails )
130 import ForeignCall ( Safety, playSafe )
135 import CmdLineOpts ( DynFlags, DynFlag( Opt_GlasgowExts ), dopt )
136 import Name ( Name, NamedThing(..), mkLocalName, getSrcLoc )
137 import OccName ( OccName, mkDictOcc )
139 import PrelNames -- Lots (e.g. in isFFIArgumentTy)
140 import TysWiredIn ( ptrTyCon, funPtrTyCon, addrTyCon, unitTyCon )
141 import BasicTypes ( ipNameName )
142 import Unique ( Unique, Uniquable(..) )
143 import SrcLoc ( SrcLoc )
144 import Util ( cmpList, thenCmp, equalLength )
145 import Maybes ( maybeToBool, expectJust )
150 %************************************************************************
154 %************************************************************************
156 The type checker divides the generic Type world into the
157 following more structured beasts:
159 sigma ::= forall tyvars. theta => phi
160 -- A sigma type is a qualified type
162 -- Note that even if 'tyvars' is empty, theta
163 -- may not be: e.g. (?x::Int) => Int
165 -- Note that 'sigma' is in prenex form:
166 -- all the foralls are at the front.
167 -- A 'phi' type has no foralls to the right of
173 -- A 'tau' type has no quantification anywhere
174 -- Note that the args of a type constructor must be taus
176 | tycon tau_1 .. tau_n
180 -- In all cases, a (saturated) type synonym application is legal,
181 -- provided it expands to the required form.
185 type SigmaType = Type
191 type TcTyVar = TyVar -- Might be a mutable tyvar
192 type TcTyVarSet = TyVarSet
194 type TcType = Type -- A TcType can have mutable type variables
195 -- Invariant on ForAllTy in TcTypes:
197 -- a cannot occur inside a MutTyVar in T; that is,
198 -- T is "flattened" before quantifying over a
200 type TcPredType = PredType
201 type TcThetaType = ThetaType
202 type TcSigmaType = TcType
203 type TcPhiType = TcType
204 type TcTauType = TcType
209 %************************************************************************
211 \subsection{TyVarDetails}
213 %************************************************************************
215 TyVarDetails gives extra info about type variables, used during type
216 checking. It's attached to mutable type variables only.
217 It's knot-tied back to Var.lhs. There is no reason in principle
218 why Var.lhs shouldn't actually have the definition, but it "belongs" here.
222 = HoleTv -- Used *only* by the type checker when passing in a type
223 -- variable that should be side-effected to the result type.
224 -- Always has kind openTypeKind.
225 -- Never appears in types
227 | SigTv -- Introduced when instantiating a type signature,
228 -- prior to checking that the defn of a fn does
229 -- have the expected type. Should not be instantiated.
231 -- f :: forall a. a -> a
233 -- When checking e, with expected type (a->a), we
234 -- should not instantiate a
236 | ClsTv -- Scoped type variable introduced by a class decl
237 -- class C a where ...
239 | InstTv -- Ditto, but instance decl
241 | PatSigTv -- Scoped type variable, introduced by a pattern
245 | VanillaTv -- Everything else
247 isUserTyVar :: TcTyVar -> Bool -- Avoid unifying these if possible
248 isUserTyVar tv = case mutTyVarDetails tv of
252 isSkolemTyVar :: TcTyVar -> Bool
253 isSkolemTyVar tv = case mutTyVarDetails tv of
257 isHoleTyVar :: TcTyVar -> Bool
258 -- NB: the hole might be filled in by now, and this
259 -- function does not check for that
260 isHoleTyVar tv = ASSERT( isMutTyVar tv )
261 case mutTyVarDetails tv of
265 tyVarBindingInfo :: TyVar -> SDoc -- Used in checkSigTyVars
268 = sep [ptext SLIT("is bound by the") <+> details (mutTyVarDetails tv),
269 ptext SLIT("at") <+> ppr (getSrcLoc tv)]
273 details SigTv = ptext SLIT("type signature")
274 details ClsTv = ptext SLIT("class declaration")
275 details InstTv = ptext SLIT("instance declaration")
276 details PatSigTv = ptext SLIT("pattern type signature")
277 details HoleTv = ptext SLIT("//hole//") -- Should not happen
278 details VanillaTv = ptext SLIT("//vanilla//") -- Ditto
282 %************************************************************************
284 \subsection{Tau, sigma and rho}
286 %************************************************************************
289 mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkRhoTy theta tau)
291 mkRhoTy :: [SourceType] -> Type -> Type
292 mkRhoTy theta ty = UASSERT2( not (isUTy ty), pprType ty )
293 foldr (\p r -> FunTy (mkUTyM (mkPredTy p)) (mkUTyM r)) ty theta
298 @isTauTy@ tests for nested for-alls.
301 isTauTy :: Type -> Bool
302 isTauTy (TyVarTy v) = True
303 isTauTy (TyConApp _ tys) = all isTauTy tys
304 isTauTy (AppTy a b) = isTauTy a && isTauTy b
305 isTauTy (FunTy a b) = isTauTy a && isTauTy b
306 isTauTy (SourceTy p) = True -- Don't look through source types
307 isTauTy (NoteTy _ ty) = isTauTy ty
308 isTauTy (UsageTy _ ty) = isTauTy ty
309 isTauTy other = False
313 getDFunTyKey :: Type -> OccName -- Get some string from a type, to be used to
314 -- construct a dictionary function name
315 getDFunTyKey (TyVarTy tv) = getOccName tv
316 getDFunTyKey (TyConApp tc _) = getOccName tc
317 getDFunTyKey (AppTy fun _) = getDFunTyKey fun
318 getDFunTyKey (NoteTy _ t) = getDFunTyKey t
319 getDFunTyKey (FunTy arg _) = getOccName funTyCon
320 getDFunTyKey (ForAllTy _ t) = getDFunTyKey t
321 getDFunTyKey (UsageTy _ t) = getDFunTyKey t
322 getDFunTyKey (SourceTy (NType tc _)) = getOccName tc -- Newtypes are quite reasonable
323 getDFunTyKey ty = pprPanic "getDFunTyKey" (pprType ty)
324 -- SourceTy shouldn't happen
328 %************************************************************************
330 \subsection{Expanding and splitting}
332 %************************************************************************
334 These tcSplit functions are like their non-Tc analogues, but
335 a) they do not look through newtypes
336 b) they do not look through PredTys
337 c) [future] they ignore usage-type annotations
339 However, they are non-monadic and do not follow through mutable type
340 variables. It's up to you to make sure this doesn't matter.
343 tcSplitForAllTys :: Type -> ([TyVar], Type)
344 tcSplitForAllTys ty = split ty ty []
346 split orig_ty (ForAllTy tv ty) tvs = split ty ty (tv:tvs)
347 split orig_ty (NoteTy n ty) tvs = split orig_ty ty tvs
348 split orig_ty (UsageTy _ ty) tvs = split orig_ty ty tvs
349 split orig_ty t tvs = (reverse tvs, orig_ty)
351 tcIsForAllTy (ForAllTy tv ty) = True
352 tcIsForAllTy (NoteTy n ty) = tcIsForAllTy ty
353 tcIsForAllTy (UsageTy n ty) = tcIsForAllTy ty
354 tcIsForAllTy t = False
356 tcSplitRhoTy :: Type -> ([PredType], Type)
357 tcSplitRhoTy ty = split ty ty []
359 split orig_ty (FunTy arg res) ts = case tcSplitPredTy_maybe arg of
360 Just p -> split res res (p:ts)
361 Nothing -> (reverse ts, orig_ty)
362 split orig_ty (NoteTy n ty) ts = split orig_ty ty ts
363 split orig_ty (UsageTy _ ty) ts = split orig_ty ty ts
364 split orig_ty ty ts = (reverse ts, orig_ty)
366 tcSplitSigmaTy ty = case tcSplitForAllTys ty of
367 (tvs, rho) -> case tcSplitRhoTy rho of
368 (theta, tau) -> (tvs, theta, tau)
370 tcTyConAppTyCon :: Type -> TyCon
371 tcTyConAppTyCon ty = fst (tcSplitTyConApp ty)
373 tcTyConAppArgs :: Type -> [Type]
374 tcTyConAppArgs ty = snd (tcSplitTyConApp ty)
376 tcSplitTyConApp :: Type -> (TyCon, [Type])
377 tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of
379 Nothing -> pprPanic "tcSplitTyConApp" (pprType ty)
381 tcSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
382 -- Newtypes are opaque, so they may be split
383 tcSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
384 tcSplitTyConApp_maybe (FunTy arg res) = Just (funTyCon, [unUTy arg,unUTy res])
385 tcSplitTyConApp_maybe (NoteTy n ty) = tcSplitTyConApp_maybe ty
386 tcSplitTyConApp_maybe (UsageTy _ ty) = tcSplitTyConApp_maybe ty
387 tcSplitTyConApp_maybe (SourceTy (NType tc tys)) = Just (tc,tys)
388 -- However, predicates are not treated
389 -- as tycon applications by the type checker
390 tcSplitTyConApp_maybe other = Nothing
392 tcSplitFunTys :: Type -> ([Type], Type)
393 tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
395 Just (arg,res) -> (arg:args, res')
397 (args,res') = tcSplitFunTys res
399 tcSplitFunTy_maybe :: Type -> Maybe (Type, Type)
400 tcSplitFunTy_maybe (FunTy arg res) = Just (arg, res)
401 tcSplitFunTy_maybe (NoteTy n ty) = tcSplitFunTy_maybe ty
402 tcSplitFunTy_maybe (UsageTy _ ty) = tcSplitFunTy_maybe ty
403 tcSplitFunTy_maybe other = Nothing
405 tcFunArgTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> arg }
406 tcFunResultTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> res }
409 tcSplitAppTy_maybe :: Type -> Maybe (Type, Type)
410 tcSplitAppTy_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [unUTy ty1], unUTy ty2)
411 tcSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
412 tcSplitAppTy_maybe (NoteTy n ty) = tcSplitAppTy_maybe ty
413 tcSplitAppTy_maybe (UsageTy _ ty) = tcSplitAppTy_maybe ty
414 tcSplitAppTy_maybe (SourceTy (NType tc tys)) = tc_split_app tc tys
415 --- Don't forget that newtype!
416 tcSplitAppTy_maybe (TyConApp tc tys) = tc_split_app tc tys
417 tcSplitAppTy_maybe other = Nothing
419 tc_split_app tc [] = Nothing
420 tc_split_app tc tys = split tys []
422 split [ty2] acc = Just (TyConApp tc (reverse acc), ty2)
423 split (ty:tys) acc = split tys (ty:acc)
425 tcSplitAppTy ty = case tcSplitAppTy_maybe ty of
427 Nothing -> pprPanic "tcSplitAppTy" (pprType ty)
429 tcGetTyVar_maybe :: Type -> Maybe TyVar
430 tcGetTyVar_maybe (TyVarTy tv) = Just tv
431 tcGetTyVar_maybe (NoteTy _ t) = tcGetTyVar_maybe t
432 tcGetTyVar_maybe ty@(UsageTy _ _) = pprPanic "tcGetTyVar_maybe: UTy:" (pprType ty)
433 tcGetTyVar_maybe other = Nothing
435 tcGetTyVar :: String -> Type -> TyVar
436 tcGetTyVar msg ty = expectJust msg (tcGetTyVar_maybe ty)
438 tcIsTyVarTy :: Type -> Bool
439 tcIsTyVarTy ty = maybeToBool (tcGetTyVar_maybe ty)
442 The type of a method for class C is always of the form:
443 Forall a1..an. C a1..an => sig_ty
444 where sig_ty is the type given by the method's signature, and thus in general
445 is a ForallTy. At the point that splitMethodTy is called, it is expected
446 that the outer Forall has already been stripped off. splitMethodTy then
447 returns (C a1..an, sig_ty') where sig_ty' is sig_ty with any Notes or
451 tcSplitMethodTy :: Type -> (PredType, Type)
452 tcSplitMethodTy ty = split ty
454 split (FunTy arg res) = case tcSplitPredTy_maybe arg of
456 Nothing -> panic "splitMethodTy"
457 split (NoteTy n ty) = split ty
458 split (UsageTy _ ty) = split ty
459 split _ = panic "splitMethodTy"
461 tcSplitDFunTy :: Type -> ([TyVar], [SourceType], Class, [Type])
462 -- Split the type of a dictionary function
464 = case tcSplitSigmaTy ty of { (tvs, theta, tau) ->
465 case tcSplitPredTy_maybe tau of { Just (ClassP clas tys) ->
466 (tvs, theta, clas, tys) }}
470 %************************************************************************
472 \subsection{Predicate types}
474 %************************************************************************
476 "Predicates" are particular source types, namelyClassP or IParams
479 isPred :: SourceType -> Bool
480 isPred (ClassP _ _) = True
481 isPred (IParam _ _) = True
482 isPred (NType _ _) = False
484 isPredTy :: Type -> Bool
485 isPredTy (NoteTy _ ty) = isPredTy ty
486 isPredTy (UsageTy _ ty) = isPredTy ty
487 isPredTy (SourceTy sty) = isPred sty
490 tcSplitPredTy_maybe :: Type -> Maybe PredType
491 -- Returns Just for predicates only
492 tcSplitPredTy_maybe (NoteTy _ ty) = tcSplitPredTy_maybe ty
493 tcSplitPredTy_maybe (UsageTy _ ty) = tcSplitPredTy_maybe ty
494 tcSplitPredTy_maybe (SourceTy p) | isPred p = Just p
495 tcSplitPredTy_maybe other = Nothing
497 predTyUnique :: PredType -> Unique
498 predTyUnique (IParam n _) = getUnique (ipNameName n)
499 predTyUnique (ClassP clas tys) = getUnique clas
501 predHasFDs :: PredType -> Bool
502 -- True if the predicate has functional depenencies;
503 -- I.e. should participate in improvement
504 predHasFDs (IParam _ _) = True
505 predHasFDs (ClassP cls _) = classHasFDs cls
507 mkPredName :: Unique -> SrcLoc -> SourceType -> Name
508 mkPredName uniq loc (ClassP cls tys) = mkLocalName uniq (mkDictOcc (getOccName cls)) loc
509 mkPredName uniq loc (IParam ip ty) = mkLocalName uniq (getOccName (ipNameName ip)) loc
513 --------------------- Dictionary types ---------------------------------
516 mkClassPred clas tys = UASSERT2( not (any isUTy tys), ppr clas <+> fsep (map pprType tys) )
519 isClassPred :: SourceType -> Bool
520 isClassPred (ClassP clas tys) = True
521 isClassPred other = False
523 isTyVarClassPred (ClassP clas tys) = all tcIsTyVarTy tys
524 isTyVarClassPred other = False
526 getClassPredTys_maybe :: SourceType -> Maybe (Class, [Type])
527 getClassPredTys_maybe (ClassP clas tys) = Just (clas, tys)
528 getClassPredTys_maybe _ = Nothing
530 getClassPredTys :: PredType -> (Class, [Type])
531 getClassPredTys (ClassP clas tys) = (clas, tys)
533 mkDictTy :: Class -> [Type] -> Type
534 mkDictTy clas tys = UASSERT2( not (any isUTy tys), ppr clas <+> fsep (map pprType tys) )
535 mkPredTy (ClassP clas tys)
537 isDictTy :: Type -> Bool
538 isDictTy (SourceTy p) = isClassPred p
539 isDictTy (NoteTy _ ty) = isDictTy ty
540 isDictTy (UsageTy _ ty) = isDictTy ty
541 isDictTy other = False
544 --------------------- Implicit parameters ---------------------------------
547 isIPPred :: SourceType -> Bool
548 isIPPred (IParam _ _) = True
549 isIPPred other = False
551 inheritablePred :: PredType -> Bool
552 -- Can be inherited by a context. For example, consider
553 -- f x = let g y = (?v, y+x)
554 -- in (g 3 with ?v = 8,
556 -- The point is that g's type must be quantifed over ?v:
557 -- g :: (?v :: a) => a -> a
558 -- but it doesn't need to be quantified over the Num a dictionary
559 -- which can be free in g's rhs, and shared by both calls to g
560 inheritablePred (ClassP _ _) = True
561 inheritablePred other = False
565 %************************************************************************
567 \subsection{Comparison}
569 %************************************************************************
571 Comparison, taking note of newtypes, predicates, etc,
572 But ignoring usage types
575 tcEqType :: Type -> Type -> Bool
576 tcEqType ty1 ty2 = case ty1 `tcCmpType` ty2 of { EQ -> True; other -> False }
578 tcEqTypes :: [Type] -> [Type] -> Bool
579 tcEqTypes ty1 ty2 = case ty1 `tcCmpTypes` ty2 of { EQ -> True; other -> False }
581 tcEqPred :: PredType -> PredType -> Bool
582 tcEqPred p1 p2 = case p1 `tcCmpPred` p2 of { EQ -> True; other -> False }
585 tcCmpType :: Type -> Type -> Ordering
586 tcCmpType ty1 ty2 = cmpTy emptyVarEnv ty1 ty2
588 tcCmpTypes tys1 tys2 = cmpTys emptyVarEnv tys1 tys2
590 tcCmpPred p1 p2 = cmpSourceTy emptyVarEnv p1 p2
592 cmpTys env tys1 tys2 = cmpList (cmpTy env) tys1 tys2
595 cmpTy :: TyVarEnv TyVar -> Type -> Type -> Ordering
596 -- The "env" maps type variables in ty1 to type variables in ty2
597 -- So when comparing for-alls.. (forall tv1 . t1) (forall tv2 . t2)
598 -- we in effect substitute tv2 for tv1 in t1 before continuing
600 -- Look through NoteTy and UsageTy
601 cmpTy env (NoteTy _ ty1) ty2 = cmpTy env ty1 ty2
602 cmpTy env ty1 (NoteTy _ ty2) = cmpTy env ty1 ty2
603 cmpTy env (UsageTy _ ty1) ty2 = cmpTy env ty1 ty2
604 cmpTy env ty1 (UsageTy _ ty2) = cmpTy env ty1 ty2
606 -- Deal with equal constructors
607 cmpTy env (TyVarTy tv1) (TyVarTy tv2) = case lookupVarEnv env tv1 of
608 Just tv1a -> tv1a `compare` tv2
609 Nothing -> tv1 `compare` tv2
611 cmpTy env (SourceTy p1) (SourceTy p2) = cmpSourceTy env p1 p2
612 cmpTy env (AppTy f1 a1) (AppTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
613 cmpTy env (FunTy f1 a1) (FunTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
614 cmpTy env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
615 cmpTy env (ForAllTy tv1 t1) (ForAllTy tv2 t2) = cmpTy (extendVarEnv env tv1 tv2) t1 t2
617 -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy < SourceTy
618 cmpTy env (AppTy _ _) (TyVarTy _) = GT
620 cmpTy env (FunTy _ _) (TyVarTy _) = GT
621 cmpTy env (FunTy _ _) (AppTy _ _) = GT
623 cmpTy env (TyConApp _ _) (TyVarTy _) = GT
624 cmpTy env (TyConApp _ _) (AppTy _ _) = GT
625 cmpTy env (TyConApp _ _) (FunTy _ _) = GT
627 cmpTy env (ForAllTy _ _) (TyVarTy _) = GT
628 cmpTy env (ForAllTy _ _) (AppTy _ _) = GT
629 cmpTy env (ForAllTy _ _) (FunTy _ _) = GT
630 cmpTy env (ForAllTy _ _) (TyConApp _ _) = GT
632 cmpTy env (SourceTy _) t2 = GT
638 cmpSourceTy :: TyVarEnv TyVar -> SourceType -> SourceType -> Ordering
639 cmpSourceTy env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` (cmpTy env ty1 ty2)
640 -- Compare types as well as names for implicit parameters
641 -- This comparison is used exclusively (I think) for the
642 -- finite map built in TcSimplify
643 cmpSourceTy env (IParam _ _) sty = LT
645 cmpSourceTy env (ClassP _ _) (IParam _ _) = GT
646 cmpSourceTy env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` (cmpTys env tys1 tys2)
647 cmpSourceTy env (ClassP _ _) (NType _ _) = LT
649 cmpSourceTy env (NType tc1 tys1) (NType tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
650 cmpSourceTy env (NType _ _) sty = GT
653 PredTypes are used as a FM key in TcSimplify,
654 so we take the easy path and make them an instance of Ord
657 instance Eq SourceType where { (==) = tcEqPred }
658 instance Ord SourceType where { compare = tcCmpPred }
662 %************************************************************************
664 \subsection{Predicates}
666 %************************************************************************
668 isSigmaTy returns true of any qualified type. It doesn't *necessarily* have
670 f :: (?x::Int) => Int -> Int
673 isSigmaTy :: Type -> Bool
674 isSigmaTy (ForAllTy tyvar ty) = True
675 isSigmaTy (FunTy a b) = isPredTy a
676 isSigmaTy (NoteTy n ty) = isSigmaTy ty
677 isSigmaTy (UsageTy _ ty) = isSigmaTy ty
680 isOverloadedTy :: Type -> Bool
681 isOverloadedTy (ForAllTy tyvar ty) = isOverloadedTy ty
682 isOverloadedTy (FunTy a b) = isPredTy a
683 isOverloadedTy (NoteTy n ty) = isOverloadedTy ty
684 isOverloadedTy (UsageTy _ ty) = isOverloadedTy ty
685 isOverloadedTy _ = False
689 isFloatTy = is_tc floatTyConKey
690 isDoubleTy = is_tc doubleTyConKey
691 isForeignPtrTy = is_tc foreignPtrTyConKey
692 isIntegerTy = is_tc integerTyConKey
693 isIntTy = is_tc intTyConKey
694 isAddrTy = is_tc addrTyConKey
695 isBoolTy = is_tc boolTyConKey
696 isUnitTy = is_tc unitTyConKey
698 is_tc :: Unique -> Type -> Bool
699 -- Newtypes are opaque to this
700 is_tc uniq ty = case tcSplitTyConApp_maybe ty of
701 Just (tc, _) -> uniq == getUnique tc
706 %************************************************************************
710 %************************************************************************
713 hoistForAllTys :: Type -> Type
714 -- Used for user-written type signatures only
715 -- Move all the foralls and constraints to the top
716 -- e.g. T -> forall a. a ==> forall a. T -> a
717 -- T -> (?x::Int) -> Int ==> (?x::Int) -> T -> Int
719 -- We want to 'look through' type synonyms when doing this
720 -- so it's better done on the Type than the HsType
723 = case hoist ty ty of
724 (tvs, theta, body) -> mkForAllTys tvs (mkFunTys theta body)
726 hoist orig_ty (ForAllTy tv ty) = case hoist ty ty of
727 (tvs,theta,tau) -> (tv:tvs,theta,tau)
728 hoist orig_ty (FunTy arg res)
729 | isPredTy arg = case hoist res res of
730 (tvs,theta,tau) -> (tvs,arg:theta,tau)
731 | otherwise = case hoist res res of
732 (tvs,theta,tau) -> (tvs,theta,mkFunTy arg tau)
734 hoist orig_ty (NoteTy _ ty) = hoist orig_ty ty
735 hoist orig_ty (UsageTy _ ty) = hoist orig_ty ty
736 hoist orig_ty ty = ([], [], orig_ty)
741 deNoteType :: Type -> Type
742 -- Remove synonyms, but not source types
743 deNoteType ty@(TyVarTy tyvar) = ty
744 deNoteType (TyConApp tycon tys) = TyConApp tycon (map deNoteType tys)
745 deNoteType (SourceTy p) = SourceTy (deNoteSourceType p)
746 deNoteType (NoteTy _ ty) = deNoteType ty
747 deNoteType (AppTy fun arg) = AppTy (deNoteType fun) (deNoteType arg)
748 deNoteType (FunTy fun arg) = FunTy (deNoteType fun) (deNoteType arg)
749 deNoteType (ForAllTy tv ty) = ForAllTy tv (deNoteType ty)
750 deNoteType (UsageTy u ty) = UsageTy u (deNoteType ty)
752 deNoteSourceType :: SourceType -> SourceType
753 deNoteSourceType (ClassP c tys) = ClassP c (map deNoteType tys)
754 deNoteSourceType (IParam n ty) = IParam n (deNoteType ty)
755 deNoteSourceType (NType tc tys) = NType tc (map deNoteType tys)
758 Find the free names of a type, including the type constructors and classes it mentions
759 This is used in the front end of the compiler
762 namesOfType :: Type -> NameSet
763 namesOfType (TyVarTy tv) = unitNameSet (getName tv)
764 namesOfType (TyConApp tycon tys) = unitNameSet (getName tycon) `unionNameSets` namesOfTypes tys
765 namesOfType (NoteTy (SynNote ty1) ty2) = namesOfType ty1
766 namesOfType (NoteTy other_note ty2) = namesOfType ty2
767 namesOfType (SourceTy (IParam n ty)) = namesOfType ty
768 namesOfType (SourceTy (ClassP cl tys)) = unitNameSet (getName cl) `unionNameSets` namesOfTypes tys
769 namesOfType (SourceTy (NType tc tys)) = unitNameSet (getName tc) `unionNameSets` namesOfTypes tys
770 namesOfType (FunTy arg res) = namesOfType arg `unionNameSets` namesOfType res
771 namesOfType (AppTy fun arg) = namesOfType fun `unionNameSets` namesOfType arg
772 namesOfType (ForAllTy tyvar ty) = namesOfType ty `delFromNameSet` getName tyvar
773 namesOfType (UsageTy u ty) = namesOfType u `unionNameSets` namesOfType ty
775 namesOfTypes tys = foldr (unionNameSets . namesOfType) emptyNameSet tys
777 namesOfDFunHead :: Type -> NameSet
778 -- Find the free type constructors and classes
779 -- of the head of the dfun instance type
780 -- The 'dfun_head_type' is because of
781 -- instance Foo a => Baz T where ...
782 -- The decl is an orphan if Baz and T are both not locally defined,
783 -- even if Foo *is* locally defined
784 namesOfDFunHead dfun_ty = case tcSplitSigmaTy dfun_ty of
785 (tvs,_,head_ty) -> delListFromNameSet (namesOfType head_ty)
790 %************************************************************************
792 \subsection[TysWiredIn-ext-type]{External types}
794 %************************************************************************
796 The compiler's foreign function interface supports the passing of a
797 restricted set of types as arguments and results (the restricting factor
801 isFFIArgumentTy :: DynFlags -> Safety -> Type -> Bool
802 -- Checks for valid argument type for a 'foreign import'
803 isFFIArgumentTy dflags safety ty
804 = checkRepTyCon (legalOutgoingTyCon dflags safety) ty
806 isFFIExternalTy :: Type -> Bool
807 -- Types that are allowed as arguments of a 'foreign export'
808 isFFIExternalTy ty = checkRepTyCon legalFEArgTyCon ty
810 isFFIImportResultTy :: DynFlags -> Type -> Bool
811 isFFIImportResultTy dflags ty
812 = checkRepTyCon (legalFIResultTyCon dflags) ty
814 isFFIExportResultTy :: Type -> Bool
815 isFFIExportResultTy ty = checkRepTyCon legalFEResultTyCon ty
817 isFFIDynArgumentTy :: Type -> Bool
818 -- The argument type of a foreign import dynamic must be Ptr, FunPtr, Addr,
819 -- or a newtype of either.
820 isFFIDynArgumentTy = checkRepTyCon (\tc -> tc == ptrTyCon || tc == funPtrTyCon || tc == addrTyCon)
822 isFFIDynResultTy :: Type -> Bool
823 -- The result type of a foreign export dynamic must be Ptr, FunPtr, Addr,
824 -- or a newtype of either.
825 isFFIDynResultTy = checkRepTyCon (\tc -> tc == ptrTyCon || tc == funPtrTyCon || tc == addrTyCon)
827 isFFILabelTy :: Type -> Bool
828 -- The type of a foreign label must be Ptr, FunPtr, Addr,
829 -- or a newtype of either.
830 isFFILabelTy = checkRepTyCon (\tc -> tc == ptrTyCon || tc == funPtrTyCon || tc == addrTyCon)
832 checkRepTyCon :: (TyCon -> Bool) -> Type -> Bool
833 -- Look through newtypes
834 -- Non-recursive ones are transparent to splitTyConApp,
835 -- but recursive ones aren't; hence the splitNewType_maybe
836 checkRepTyCon check_tc ty
837 | Just ty' <- splitNewType_maybe ty = checkRepTyCon check_tc ty'
838 | Just (tc,_) <- splitTyConApp_maybe ty = check_tc tc
842 ----------------------------------------------
843 These chaps do the work; they are not exported
844 ----------------------------------------------
847 legalFEArgTyCon :: TyCon -> Bool
848 -- It's illegal to return foreign objects and (mutable)
849 -- bytearrays from a _ccall_ / foreign declaration
850 -- (or be passed them as arguments in foreign exported functions).
852 | getUnique tc `elem` [ foreignObjTyConKey, foreignPtrTyConKey,
853 byteArrayTyConKey, mutableByteArrayTyConKey ]
855 -- It's also illegal to make foreign exports that take unboxed
856 -- arguments. The RTS API currently can't invoke such things. --SDM 7/2000
858 = boxedMarshalableTyCon tc
860 legalFIResultTyCon :: DynFlags -> TyCon -> Bool
861 legalFIResultTyCon dflags tc
862 | getUnique tc `elem`
863 [ foreignObjTyConKey, foreignPtrTyConKey,
864 byteArrayTyConKey, mutableByteArrayTyConKey ] = False
865 | tc == unitTyCon = True
866 | otherwise = marshalableTyCon dflags tc
868 legalFEResultTyCon :: TyCon -> Bool
869 legalFEResultTyCon tc
870 | getUnique tc `elem`
871 [ foreignObjTyConKey, foreignPtrTyConKey,
872 byteArrayTyConKey, mutableByteArrayTyConKey ] = False
873 | tc == unitTyCon = True
874 | otherwise = boxedMarshalableTyCon tc
876 legalOutgoingTyCon :: DynFlags -> Safety -> TyCon -> Bool
877 -- Checks validity of types going from Haskell -> external world
878 legalOutgoingTyCon dflags safety tc
879 | playSafe safety && getUnique tc `elem` [byteArrayTyConKey, mutableByteArrayTyConKey]
882 = marshalableTyCon dflags tc
884 marshalableTyCon dflags tc
885 = (dopt Opt_GlasgowExts dflags && isUnLiftedTyCon tc)
886 || boxedMarshalableTyCon tc
888 boxedMarshalableTyCon tc
889 = getUnique tc `elem` [ intTyConKey, int8TyConKey, int16TyConKey
890 , int32TyConKey, int64TyConKey
891 , wordTyConKey, word8TyConKey, word16TyConKey
892 , word32TyConKey, word64TyConKey
893 , floatTyConKey, doubleTyConKey
894 , addrTyConKey, ptrTyConKey, funPtrTyConKey
895 , charTyConKey, foreignObjTyConKey
898 , byteArrayTyConKey, mutableByteArrayTyConKey
904 %************************************************************************
906 \subsection{Unification with an explicit substitution}
908 %************************************************************************
910 (allDistinctTyVars tys tvs) = True
912 all the types tys are type variables,
913 distinct from each other and from tvs.
915 This is useful when checking that unification hasn't unified signature
916 type variables. For example, if the type sig is
917 f :: forall a b. a -> b -> b
918 we want to check that 'a' and 'b' havn't
919 (a) been unified with a non-tyvar type
920 (b) been unified with each other (all distinct)
921 (c) been unified with a variable free in the environment
924 allDistinctTyVars :: [Type] -> TyVarSet -> Bool
926 allDistinctTyVars [] acc
928 allDistinctTyVars (ty:tys) acc
929 = case tcGetTyVar_maybe ty of
930 Nothing -> False -- (a)
931 Just tv | tv `elemVarSet` acc -> False -- (b) or (c)
932 | otherwise -> allDistinctTyVars tys (acc `extendVarSet` tv)
936 %************************************************************************
938 \subsection{Unification with an explicit substitution}
940 %************************************************************************
942 Unify types with an explicit substitution and no monad.
943 Ignore usage annotations.
947 = (TyVarSet, -- Set of template tyvars
948 TyVarSubstEnv) -- Not necessarily idempotent
950 unifyTysX :: TyVarSet -- Template tyvars
953 -> Maybe TyVarSubstEnv
954 unifyTysX tmpl_tyvars ty1 ty2
955 = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
957 unifyExtendTysX :: TyVarSet -- Template tyvars
958 -> TyVarSubstEnv -- Substitution to start with
961 -> Maybe TyVarSubstEnv -- Extended substitution
962 unifyExtendTysX tmpl_tyvars subst ty1 ty2
963 = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, subst)
965 unifyTyListsX :: TyVarSet -> [Type] -> [Type]
966 -> Maybe TyVarSubstEnv
967 unifyTyListsX tmpl_tyvars tys1 tys2
968 = uTyListsX tys1 tys2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
973 -> (MySubst -> Maybe result)
977 uTysX (NoteTy _ ty1) ty2 k subst = uTysX ty1 ty2 k subst
978 uTysX ty1 (NoteTy _ ty2) k subst = uTysX ty1 ty2 k subst
980 -- Variables; go for uVar
981 uTysX (TyVarTy tyvar1) (TyVarTy tyvar2) k subst
984 uTysX (TyVarTy tyvar1) ty2 k subst@(tmpls,_)
985 | tyvar1 `elemVarSet` tmpls
986 = uVarX tyvar1 ty2 k subst
987 uTysX ty1 (TyVarTy tyvar2) k subst@(tmpls,_)
988 | tyvar2 `elemVarSet` tmpls
989 = uVarX tyvar2 ty1 k subst
992 uTysX (SourceTy (IParam n1 t1)) (SourceTy (IParam n2 t2)) k subst
993 | n1 == n2 = uTysX t1 t2 k subst
994 uTysX (SourceTy (ClassP c1 tys1)) (SourceTy (ClassP c2 tys2)) k subst
995 | c1 == c2 = uTyListsX tys1 tys2 k subst
996 uTysX (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) k subst
997 | tc1 == tc2 = uTyListsX tys1 tys2 k subst
999 -- Functions; just check the two parts
1000 uTysX (FunTy fun1 arg1) (FunTy fun2 arg2) k subst
1001 = uTysX fun1 fun2 (uTysX arg1 arg2 k) subst
1003 -- Type constructors must match
1004 uTysX (TyConApp con1 tys1) (TyConApp con2 tys2) k subst
1005 | (con1 == con2 && equalLength tys1 tys2)
1006 = uTyListsX tys1 tys2 k subst
1008 -- Applications need a bit of care!
1009 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
1010 -- NB: we've already dealt with type variables and Notes,
1011 -- so if one type is an App the other one jolly well better be too
1012 uTysX (AppTy s1 t1) ty2 k subst
1013 = case tcSplitAppTy_maybe ty2 of
1014 Just (s2, t2) -> uTysX s1 s2 (uTysX t1 t2 k) subst
1015 Nothing -> Nothing -- Fail
1017 uTysX ty1 (AppTy s2 t2) k subst
1018 = case tcSplitAppTy_maybe ty1 of
1019 Just (s1, t1) -> uTysX s1 s2 (uTysX t1 t2 k) subst
1020 Nothing -> Nothing -- Fail
1022 -- Not expecting for-alls in unification
1024 uTysX (ForAllTy _ _) ty2 k subst = panic "Unify.uTysX subst:ForAllTy (1st arg)"
1025 uTysX ty1 (ForAllTy _ _) k subst = panic "Unify.uTysX subst:ForAllTy (2nd arg)"
1029 uTysX (UsageTy _ t1) t2 k subst = uTysX t1 t2 k subst
1030 uTysX t1 (UsageTy _ t2) k subst = uTysX t1 t2 k subst
1032 -- Anything else fails
1033 uTysX ty1 ty2 k subst = Nothing
1036 uTyListsX [] [] k subst = k subst
1037 uTyListsX (ty1:tys1) (ty2:tys2) k subst = uTysX ty1 ty2 (uTyListsX tys1 tys2 k) subst
1038 uTyListsX tys1 tys2 k subst = Nothing -- Fail if the lists are different lengths
1042 -- Invariant: tv1 is a unifiable variable
1043 uVarX tv1 ty2 k subst@(tmpls, env)
1044 = case lookupSubstEnv env tv1 of
1045 Just (DoneTy ty1) -> -- Already bound
1046 uTysX ty1 ty2 k subst
1048 Nothing -- Not already bound
1049 | typeKind ty2 `eqKind` tyVarKind tv1
1050 && occur_check_ok ty2
1051 -> -- No kind mismatch nor occur check
1052 UASSERT( not (isUTy ty2) )
1053 k (tmpls, extendSubstEnv env tv1 (DoneTy ty2))
1055 | otherwise -> Nothing -- Fail if kind mis-match or occur check
1057 occur_check_ok ty = all occur_check_ok_tv (varSetElems (tyVarsOfType ty))
1058 occur_check_ok_tv tv | tv1 == tv = False
1059 | otherwise = case lookupSubstEnv env tv of
1061 Just (DoneTy ty) -> occur_check_ok ty
1066 %************************************************************************
1068 \subsection{Matching on types}
1070 %************************************************************************
1072 Matching is a {\em unidirectional} process, matching a type against a
1073 template (which is just a type with type variables in it). The
1074 matcher assumes that there are no repeated type variables in the
1075 template, so that it simply returns a mapping of type variables to
1076 types. It also fails on nested foralls.
1078 @matchTys@ matches corresponding elements of a list of templates and
1079 types. It and @matchTy@ both ignore usage annotations, unlike the
1080 main function @match@.
1083 matchTy :: TyVarSet -- Template tyvars
1085 -> Type -- Proposed instance of template
1086 -> Maybe TyVarSubstEnv -- Matching substitution
1089 matchTys :: TyVarSet -- Template tyvars
1090 -> [Type] -- Templates
1091 -> [Type] -- Proposed instance of template
1092 -> Maybe (TyVarSubstEnv, -- Matching substitution
1093 [Type]) -- Left over instance types
1095 matchTy tmpls ty1 ty2 = match ty1 ty2 tmpls (\ senv -> Just senv) emptySubstEnv
1097 matchTys tmpls tys1 tys2 = match_list tys1 tys2 tmpls
1098 (\ (senv,tys) -> Just (senv,tys))
1102 @match@ is the main function. It takes a flag indicating whether
1103 usage annotations are to be respected.
1106 match :: Type -> Type -- Current match pair
1107 -> TyVarSet -- Template vars
1108 -> (TyVarSubstEnv -> Maybe result) -- Continuation
1109 -> TyVarSubstEnv -- Current subst
1112 -- When matching against a type variable, see if the variable
1113 -- has already been bound. If so, check that what it's bound to
1114 -- is the same as ty; if not, bind it and carry on.
1116 match (TyVarTy v) ty tmpls k senv
1117 | v `elemVarSet` tmpls
1118 = -- v is a template variable
1119 case lookupSubstEnv senv v of
1120 Nothing -> UASSERT( not (isUTy ty) )
1121 k (extendSubstEnv senv v (DoneTy ty))
1122 Just (DoneTy ty') | ty' `tcEqType` ty -> k senv -- Succeeds
1123 | otherwise -> Nothing -- Fails
1126 = -- v is not a template variable; ty had better match
1127 -- Can't use (==) because types differ
1128 case tcGetTyVar_maybe ty of
1129 Just v' | v == v' -> k senv -- Success
1130 other -> Nothing -- Failure
1131 -- This tcGetTyVar_maybe is *required* because it must strip Notes.
1132 -- I guess the reason the Note-stripping case is *last* rather than first
1133 -- is to preserve type synonyms etc., so I'm not moving it to the
1134 -- top; but this means that (without the deNotetype) a type
1135 -- variable may not match the pattern (TyVarTy v') as one would
1136 -- expect, due to an intervening Note. KSW 2000-06.
1139 match (SourceTy (IParam n1 t1)) (SourceTy (IParam n2 t2)) tmpls k senv
1140 | n1 == n2 = match t1 t2 tmpls k senv
1141 match (SourceTy (ClassP c1 tys1)) (SourceTy (ClassP c2 tys2)) tmpls k senv
1142 | c1 == c2 = match_list_exactly tys1 tys2 tmpls k senv
1143 match (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) tmpls k senv
1144 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1146 -- Functions; just check the two parts
1147 match (FunTy arg1 res1) (FunTy arg2 res2) tmpls k senv
1148 = match arg1 arg2 tmpls (match res1 res2 tmpls k) senv
1150 match (AppTy fun1 arg1) ty2 tmpls k senv
1151 = case tcSplitAppTy_maybe ty2 of
1152 Just (fun2,arg2) -> match fun1 fun2 tmpls (match arg1 arg2 tmpls k) senv
1153 Nothing -> Nothing -- Fail
1155 match (TyConApp tc1 tys1) (TyConApp tc2 tys2) tmpls k senv
1156 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1158 -- Newtypes are opaque; other source types should not happen
1159 match (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) tmpls k senv
1160 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1162 match (UsageTy _ ty1) ty2 tmpls k senv = match ty1 ty2 tmpls k senv
1163 match ty1 (UsageTy _ ty2) tmpls k senv = match ty1 ty2 tmpls k senv
1165 -- With type synonyms, we have to be careful for the exact
1166 -- same reasons as in the unifier. Please see the
1167 -- considerable commentary there before changing anything
1168 -- here! (WDP 95/05)
1169 match (NoteTy n1 ty1) ty2 tmpls k senv = match ty1 ty2 tmpls k senv
1170 match ty1 (NoteTy n2 ty2) tmpls k senv = match ty1 ty2 tmpls k senv
1173 match _ _ _ _ _ = Nothing
1175 match_list_exactly tys1 tys2 tmpls k senv
1176 = match_list tys1 tys2 tmpls k' senv
1178 k' (senv', tys2') | null tys2' = k senv' -- Succeed
1179 | otherwise = Nothing -- Fail
1181 match_list [] tys2 tmpls k senv = k (senv, tys2)
1182 match_list (ty1:tys1) [] tmpls k senv = Nothing -- Not enough arg tys => failure
1183 match_list (ty1:tys1) (ty2:tys2) tmpls k senv
1184 = match ty1 ty2 tmpls (match_list tys1 tys2 tmpls k) senv