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, TcRhoType, TcTauType, TcPredType, TcThetaType,
21 TcTyVar, TcTyVarSet, TcKind,
23 --------------------------------
25 TyVarDetails(..), isUserTyVar, isSkolemTyVar, isExistentialTyVar,
28 --------------------------------
32 --------------------------------
34 -- These are important because they do not look through newtypes
35 tcSplitForAllTys, tcSplitPhiTy,
36 tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy,
37 tcSplitTyConApp, tcSplitTyConApp_maybe, tcTyConAppTyCon, tcTyConAppArgs,
38 tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, 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,
48 isTauTy, tcIsTyVarTy, tcIsForAllTy,
51 ---------------------------------
52 -- Misc type manipulators
53 deNoteType, classesOfTheta,
54 tyClsNamesOfType, tyClsNamesOfDFunHead,
57 ---------------------------------
59 getClassPredTys_maybe, getClassPredTys,
60 isClassPred, isTyVarClassPred,
61 mkDictTy, tcSplitPredTy_maybe,
62 isPredTy, isDictTy, tcSplitDFunTy, predTyUnique,
63 mkClassPred, isInheritablePred, isLinearPred, isIPPred, mkPredName,
65 ---------------------------------
66 -- Foreign import and export
67 isFFIArgumentTy, -- :: DynFlags -> Safety -> Type -> Bool
68 isFFIImportResultTy, -- :: DynFlags -> Type -> Bool
69 isFFIExportResultTy, -- :: Type -> Bool
70 isFFIExternalTy, -- :: Type -> Bool
71 isFFIDynArgumentTy, -- :: Type -> Bool
72 isFFIDynResultTy, -- :: Type -> Bool
73 isFFILabelTy, -- :: Type -> Bool
74 isFFIDotnetTy, -- :: DynFlags -> Type -> Bool
75 isFFIDotnetObjTy, -- :: Type -> Bool
76 isFFITy, -- :: Type -> Bool
78 toDNType, -- :: Type -> DNType
80 ---------------------------------
81 -- Unifier and matcher
82 unifyTysX, unifyTyListsX, unifyExtendTyListsX,
83 matchTy, matchTys, match,
85 --------------------------------
86 -- Rexported from Type
87 Kind, -- Stuff to do with kinds is insensitive to pre/post Tc
88 unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds,
89 isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind,
90 isArgTypeKind, isSubKind, defaultKind,
92 Type, PredType(..), ThetaType,
93 mkForAllTy, mkForAllTys,
94 mkFunTy, mkFunTys, zipFunTys,
95 mkTyConApp, mkGenTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
96 mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy, mkPredTys,
98 isUnLiftedType, -- Source types are always lifted
99 isUnboxedTupleType, -- Ditto
102 tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
103 tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars,
106 tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
108 pprKind, pprParendKind,
109 pprType, pprParendType,
110 pprPred, pprTheta, pprThetaArrow, pprClassPred
114 #include "HsVersions.h"
117 import TypeRep ( Type(..), TyNote(..), funTyCon ) -- friend
119 import Type ( -- Re-exports
120 tyVarsOfType, tyVarsOfTypes, tyVarsOfPred,
121 tyVarsOfTheta, Kind, Type, PredType(..),
122 ThetaType, unliftedTypeKind,
123 liftedTypeKind, openTypeKind, mkArrowKind,
124 isLiftedTypeKind, isUnliftedTypeKind,
126 mkArrowKinds, mkForAllTy, mkForAllTys,
127 defaultKind, isArgTypeKind, isOpenTypeKind,
128 mkFunTy, mkFunTys, zipFunTys,
129 mkTyConApp, mkGenTyConApp, mkAppTy,
130 mkAppTys, mkSynTy, applyTy, applyTys,
131 mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy,
132 mkPredTys, isUnLiftedType,
133 isUnboxedTupleType, isPrimitiveType,
135 tidyTopType, tidyType, tidyPred, tidyTypes,
136 tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
137 tidyTyVarBndr, tidyOpenTyVar,
141 pprKind, pprParendKind,
142 pprType, pprParendType,
143 pprPred, pprTheta, pprThetaArrow, pprClassPred
145 import TyCon ( TyCon, isUnLiftedTyCon, tyConUnique )
146 import Class ( Class )
147 import Var ( TyVar, tyVarKind, tcTyVarDetails )
148 import ForeignCall ( Safety, playSafe, DNType(..) )
153 import CmdLineOpts ( DynFlags, DynFlag( Opt_GlasgowExts ), dopt )
154 import Name ( Name, NamedThing(..), mkInternalName, getSrcLoc )
156 import OccName ( OccName, mkDictOcc )
157 import PrelNames -- Lots (e.g. in isFFIArgumentTy)
158 import TysWiredIn ( unitTyCon, charTyCon, listTyCon )
159 import BasicTypes ( IPName(..), ipNameName )
160 import Unique ( Unique, Uniquable(..) )
161 import SrcLoc ( SrcLoc )
162 import Util ( cmpList, thenCmp, equalLength, snocView )
163 import Maybes ( maybeToBool, expectJust )
168 %************************************************************************
172 %************************************************************************
174 The type checker divides the generic Type world into the
175 following more structured beasts:
177 sigma ::= forall tyvars. phi
178 -- A sigma type is a qualified type
180 -- Note that even if 'tyvars' is empty, theta
181 -- may not be: e.g. (?x::Int) => Int
183 -- Note that 'sigma' is in prenex form:
184 -- all the foralls are at the front.
185 -- A 'phi' type has no foralls to the right of
193 -- A 'tau' type has no quantification anywhere
194 -- Note that the args of a type constructor must be taus
196 | tycon tau_1 .. tau_n
200 -- In all cases, a (saturated) type synonym application is legal,
201 -- provided it expands to the required form.
204 type TcType = Type -- A TcType can have mutable type variables
205 -- Invariant on ForAllTy in TcTypes:
207 -- a cannot occur inside a MutTyVar in T; that is,
208 -- T is "flattened" before quantifying over a
210 type TcPredType = PredType
211 type TcThetaType = ThetaType
212 type TcSigmaType = TcType
213 type TcRhoType = TcType
214 type TcTauType = TcType
220 %************************************************************************
222 \subsection{TyVarDetails}
224 %************************************************************************
226 TyVarDetails gives extra info about type variables, used during type
227 checking. It's attached to mutable type variables only.
228 It's knot-tied back to Var.lhs. There is no reason in principle
229 why Var.lhs shouldn't actually have the definition, but it "belongs" here.
232 type TcTyVar = TyVar -- Used only during type inference
235 = SigTv -- Introduced when instantiating a type signature,
236 -- prior to checking that the defn of a fn does
237 -- have the expected type. Should not be instantiated.
238 -- f :: forall a. a -> a
240 -- When checking e, with expected type (a->a), we
241 -- should not instantiate a
243 | ClsTv -- Scoped type variable introduced by a class decl
244 -- class C a where ...
246 | InstTv -- Ditto, but instance decl
248 | PatSigTv -- Scoped type variable, introduced by a pattern
249 -- type signature \ x::a -> e
251 | ExistTv -- An existential type variable bound by a pattern for
252 -- a data constructor with an existential type. E.g.
253 -- data T = forall a. Eq a => MkT a
255 -- The pattern MkT x will allocate an existential type
256 -- variable for 'a'. We distinguish these from all others
257 -- on one place, namely InstEnv.lookupInstEnv.
259 | VanillaTv -- Everything else
261 isUserTyVar :: TcTyVar -> Bool -- Avoid unifying these if possible
262 isUserTyVar tv = case tcTyVarDetails tv of
266 isSkolemTyVar :: TcTyVar -> Bool
267 isSkolemTyVar tv = case tcTyVarDetails tv of
274 isExistentialTyVar :: TcTyVar -> Bool
275 isExistentialTyVar tv = case tcTyVarDetails tv of
279 tyVarBindingInfo :: TcTyVar -> SDoc -- Used in checkSigTyVars
281 = sep [ptext SLIT("is bound by the") <+> details (tcTyVarDetails tv),
282 ptext SLIT("at") <+> ppr (getSrcLoc tv)]
284 details SigTv = ptext SLIT("type signature")
285 details ClsTv = ptext SLIT("class declaration")
286 details InstTv = ptext SLIT("instance declaration")
287 details PatSigTv = ptext SLIT("pattern type signature")
288 details ExistTv = ptext SLIT("existential constructor")
289 details VanillaTv = ptext SLIT("//vanilla//") -- Ditto
293 type TcTyVarSet = TyVarSet
296 %************************************************************************
298 \subsection{Tau, sigma and rho}
300 %************************************************************************
303 mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkPhiTy theta tau)
305 mkPhiTy :: [PredType] -> Type -> Type
306 mkPhiTy theta ty = foldr (\p r -> FunTy (mkPredTy p) r) ty theta
309 @isTauTy@ tests for nested for-alls.
312 isTauTy :: Type -> Bool
313 isTauTy (TyVarTy v) = True
314 isTauTy (TyConApp _ tys) = all isTauTy tys
315 isTauTy (NewTcApp _ tys) = all isTauTy tys
316 isTauTy (AppTy a b) = isTauTy a && isTauTy b
317 isTauTy (FunTy a b) = isTauTy a && isTauTy b
318 isTauTy (PredTy p) = True -- Don't look through source types
319 isTauTy (NoteTy _ ty) = isTauTy ty
320 isTauTy other = False
324 getDFunTyKey :: Type -> OccName -- Get some string from a type, to be used to
325 -- construct a dictionary function name
326 getDFunTyKey (TyVarTy tv) = getOccName tv
327 getDFunTyKey (TyConApp tc _) = getOccName tc
328 getDFunTyKey (NewTcApp tc _) = getOccName tc
329 getDFunTyKey (AppTy fun _) = getDFunTyKey fun
330 getDFunTyKey (NoteTy _ t) = getDFunTyKey t
331 getDFunTyKey (FunTy arg _) = getOccName funTyCon
332 getDFunTyKey (ForAllTy _ t) = getDFunTyKey t
333 getDFunTyKey ty = pprPanic "getDFunTyKey" (pprType ty)
334 -- PredTy shouldn't happen
338 %************************************************************************
340 \subsection{Expanding and splitting}
342 %************************************************************************
344 These tcSplit functions are like their non-Tc analogues, but
345 a) they do not look through newtypes
346 b) they do not look through PredTys
347 c) [future] they ignore usage-type annotations
349 However, they are non-monadic and do not follow through mutable type
350 variables. It's up to you to make sure this doesn't matter.
353 tcSplitForAllTys :: Type -> ([TyVar], Type)
354 tcSplitForAllTys ty = split ty ty []
356 split orig_ty (ForAllTy tv ty) tvs = split ty ty (tv:tvs)
357 split orig_ty (NoteTy n ty) tvs = split orig_ty ty tvs
358 split orig_ty t tvs = (reverse tvs, orig_ty)
360 tcIsForAllTy (ForAllTy tv ty) = True
361 tcIsForAllTy (NoteTy n ty) = tcIsForAllTy ty
362 tcIsForAllTy t = False
364 tcSplitPhiTy :: Type -> ([PredType], Type)
365 tcSplitPhiTy ty = split ty ty []
367 split orig_ty (FunTy arg res) ts = case tcSplitPredTy_maybe arg of
368 Just p -> split res res (p:ts)
369 Nothing -> (reverse ts, orig_ty)
370 split orig_ty (NoteTy n ty) ts = split orig_ty ty ts
371 split orig_ty ty ts = (reverse ts, orig_ty)
373 tcSplitSigmaTy ty = case tcSplitForAllTys ty of
374 (tvs, rho) -> case tcSplitPhiTy rho of
375 (theta, tau) -> (tvs, theta, tau)
377 tcTyConAppTyCon :: Type -> TyCon
378 tcTyConAppTyCon ty = fst (tcSplitTyConApp ty)
380 tcTyConAppArgs :: Type -> [Type]
381 tcTyConAppArgs ty = snd (tcSplitTyConApp ty)
383 tcSplitTyConApp :: Type -> (TyCon, [Type])
384 tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of
386 Nothing -> pprPanic "tcSplitTyConApp" (pprType ty)
388 tcSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
389 tcSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
390 tcSplitTyConApp_maybe (NewTcApp tc tys) = Just (tc, tys)
391 tcSplitTyConApp_maybe (FunTy arg res) = Just (funTyCon, [arg,res])
392 tcSplitTyConApp_maybe (NoteTy n ty) = tcSplitTyConApp_maybe ty
393 -- Newtypes are opaque, so they may be split
394 -- However, predicates are not treated
395 -- as tycon applications by the type checker
396 tcSplitTyConApp_maybe other = Nothing
398 tcSplitFunTys :: Type -> ([Type], Type)
399 tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
401 Just (arg,res) -> (arg:args, res')
403 (args,res') = tcSplitFunTys res
405 tcSplitFunTy_maybe :: Type -> Maybe (Type, Type)
406 tcSplitFunTy_maybe (FunTy arg res) = Just (arg, res)
407 tcSplitFunTy_maybe (NoteTy n ty) = tcSplitFunTy_maybe ty
408 tcSplitFunTy_maybe other = Nothing
410 tcFunArgTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> arg }
411 tcFunResultTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> res }
414 tcSplitAppTy_maybe :: Type -> Maybe (Type, Type)
415 tcSplitAppTy_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [ty1], ty2)
416 tcSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
417 tcSplitAppTy_maybe (NoteTy n ty) = tcSplitAppTy_maybe ty
418 tcSplitAppTy_maybe (TyConApp tc tys) = case snocView tys of
419 Just (tys', ty') -> Just (TyConApp tc tys', ty')
421 tcSplitAppTy_maybe (NewTcApp tc tys) = case snocView tys of
422 Just (tys', ty') -> Just (NewTcApp tc tys', ty')
424 tcSplitAppTy_maybe other = Nothing
426 tcSplitAppTy ty = case tcSplitAppTy_maybe ty of
428 Nothing -> pprPanic "tcSplitAppTy" (pprType ty)
430 tcSplitAppTys :: Type -> (Type, [Type])
434 go ty args = case tcSplitAppTy_maybe ty of
435 Just (ty', arg) -> go ty' (arg:args)
438 tcGetTyVar_maybe :: Type -> Maybe TyVar
439 tcGetTyVar_maybe (TyVarTy tv) = Just tv
440 tcGetTyVar_maybe (NoteTy _ t) = tcGetTyVar_maybe t
441 tcGetTyVar_maybe other = Nothing
443 tcGetTyVar :: String -> Type -> TyVar
444 tcGetTyVar msg ty = expectJust msg (tcGetTyVar_maybe ty)
446 tcIsTyVarTy :: Type -> Bool
447 tcIsTyVarTy ty = maybeToBool (tcGetTyVar_maybe ty)
450 The type of a method for class C is always of the form:
451 Forall a1..an. C a1..an => sig_ty
452 where sig_ty is the type given by the method's signature, and thus in general
453 is a ForallTy. At the point that splitMethodTy is called, it is expected
454 that the outer Forall has already been stripped off. splitMethodTy then
455 returns (C a1..an, sig_ty') where sig_ty' is sig_ty with any Notes stripped off.
458 tcSplitMethodTy :: Type -> (PredType, Type)
459 tcSplitMethodTy ty = split ty
461 split (FunTy arg res) = case tcSplitPredTy_maybe arg of
463 Nothing -> panic "splitMethodTy"
464 split (NoteTy n ty) = split ty
465 split _ = panic "splitMethodTy"
467 tcSplitDFunTy :: Type -> ([TyVar], [PredType], Class, [Type])
468 -- Split the type of a dictionary function
470 = case tcSplitSigmaTy ty of { (tvs, theta, tau) ->
471 case tcSplitPredTy_maybe tau of { Just (ClassP clas tys) ->
472 (tvs, theta, clas, tys) }}
475 (allDistinctTyVars tys tvs) = True
477 all the types tys are type variables,
478 distinct from each other and from tvs.
480 This is useful when checking that unification hasn't unified signature
481 type variables. For example, if the type sig is
482 f :: forall a b. a -> b -> b
483 we want to check that 'a' and 'b' havn't
484 (a) been unified with a non-tyvar type
485 (b) been unified with each other (all distinct)
486 (c) been unified with a variable free in the environment
489 allDistinctTyVars :: [Type] -> TyVarSet -> Bool
491 allDistinctTyVars [] acc
493 allDistinctTyVars (ty:tys) acc
494 = case tcGetTyVar_maybe ty of
495 Nothing -> False -- (a)
496 Just tv | tv `elemVarSet` acc -> False -- (b) or (c)
497 | otherwise -> allDistinctTyVars tys (acc `extendVarSet` tv)
501 %************************************************************************
503 \subsection{Predicate types}
505 %************************************************************************
508 tcSplitPredTy_maybe :: Type -> Maybe PredType
509 -- Returns Just for predicates only
510 tcSplitPredTy_maybe (NoteTy _ ty) = tcSplitPredTy_maybe ty
511 tcSplitPredTy_maybe (PredTy p) = Just p
512 tcSplitPredTy_maybe other = Nothing
514 predTyUnique :: PredType -> Unique
515 predTyUnique (IParam n _) = getUnique (ipNameName n)
516 predTyUnique (ClassP clas tys) = getUnique clas
518 mkPredName :: Unique -> SrcLoc -> PredType -> Name
519 mkPredName uniq loc (ClassP cls tys) = mkInternalName uniq (mkDictOcc (getOccName cls)) loc
520 mkPredName uniq loc (IParam ip ty) = mkInternalName uniq (getOccName (ipNameName ip)) loc
524 --------------------- Dictionary types ---------------------------------
527 mkClassPred clas tys = ClassP clas tys
529 isClassPred :: PredType -> Bool
530 isClassPred (ClassP clas tys) = True
531 isClassPred other = False
533 isTyVarClassPred (ClassP clas tys) = all tcIsTyVarTy tys
534 isTyVarClassPred other = False
536 getClassPredTys_maybe :: PredType -> Maybe (Class, [Type])
537 getClassPredTys_maybe (ClassP clas tys) = Just (clas, tys)
538 getClassPredTys_maybe _ = Nothing
540 getClassPredTys :: PredType -> (Class, [Type])
541 getClassPredTys (ClassP clas tys) = (clas, tys)
543 mkDictTy :: Class -> [Type] -> Type
544 mkDictTy clas tys = mkPredTy (ClassP clas tys)
546 isDictTy :: Type -> Bool
547 isDictTy (PredTy p) = isClassPred p
548 isDictTy (NoteTy _ ty) = isDictTy ty
549 isDictTy other = False
552 --------------------- Implicit parameters ---------------------------------
555 isIPPred :: PredType -> Bool
556 isIPPred (IParam _ _) = True
557 isIPPred other = False
559 isInheritablePred :: PredType -> Bool
560 -- Can be inherited by a context. For example, consider
561 -- f x = let g y = (?v, y+x)
562 -- in (g 3 with ?v = 8,
564 -- The point is that g's type must be quantifed over ?v:
565 -- g :: (?v :: a) => a -> a
566 -- but it doesn't need to be quantified over the Num a dictionary
567 -- which can be free in g's rhs, and shared by both calls to g
568 isInheritablePred (ClassP _ _) = True
569 isInheritablePred other = False
571 isLinearPred :: TcPredType -> Bool
572 isLinearPred (IParam (Linear n) _) = True
573 isLinearPred other = False
577 %************************************************************************
579 \subsection{Comparison}
581 %************************************************************************
583 Comparison, taking note of newtypes, predicates, etc,
586 tcEqType :: Type -> Type -> Bool
587 tcEqType ty1 ty2 = case ty1 `tcCmpType` ty2 of { EQ -> True; other -> False }
589 tcEqTypes :: [Type] -> [Type] -> Bool
590 tcEqTypes ty1 ty2 = case ty1 `tcCmpTypes` ty2 of { EQ -> True; other -> False }
592 tcEqPred :: PredType -> PredType -> Bool
593 tcEqPred p1 p2 = case p1 `tcCmpPred` p2 of { EQ -> True; other -> False }
596 tcCmpType :: Type -> Type -> Ordering
597 tcCmpType ty1 ty2 = cmpTy emptyVarEnv ty1 ty2
599 tcCmpTypes tys1 tys2 = cmpTys emptyVarEnv tys1 tys2
601 tcCmpPred p1 p2 = cmpPredTy emptyVarEnv p1 p2
603 cmpTys env tys1 tys2 = cmpList (cmpTy env) tys1 tys2
606 cmpTy :: TyVarEnv TyVar -> Type -> Type -> Ordering
607 -- The "env" maps type variables in ty1 to type variables in ty2
608 -- So when comparing for-alls.. (forall tv1 . t1) (forall tv2 . t2)
609 -- we in effect substitute tv2 for tv1 in t1 before continuing
611 -- Look through NoteTy
612 cmpTy env (NoteTy _ ty1) ty2 = cmpTy env ty1 ty2
613 cmpTy env ty1 (NoteTy _ ty2) = cmpTy env ty1 ty2
615 -- Deal with equal constructors
616 cmpTy env (TyVarTy tv1) (TyVarTy tv2) = case lookupVarEnv env tv1 of
617 Just tv1a -> tv1a `compare` tv2
618 Nothing -> tv1 `compare` tv2
620 cmpTy env (PredTy p1) (PredTy p2) = cmpPredTy env p1 p2
621 cmpTy env (AppTy f1 a1) (AppTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
622 cmpTy env (FunTy f1 a1) (FunTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
623 cmpTy env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
624 cmpTy env (NewTcApp tc1 tys1) (NewTcApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
625 cmpTy env (ForAllTy tv1 t1) (ForAllTy tv2 t2) = cmpTy (extendVarEnv env tv1 tv2) t1 t2
627 -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < NewTcApp < ForAllTy < PredTy
628 cmpTy env (AppTy _ _) (TyVarTy _) = GT
630 cmpTy env (FunTy _ _) (TyVarTy _) = GT
631 cmpTy env (FunTy _ _) (AppTy _ _) = GT
633 cmpTy env (TyConApp _ _) (TyVarTy _) = GT
634 cmpTy env (TyConApp _ _) (AppTy _ _) = GT
635 cmpTy env (TyConApp _ _) (FunTy _ _) = GT
637 cmpTy env (NewTcApp _ _) (TyVarTy _) = GT
638 cmpTy env (NewTcApp _ _) (AppTy _ _) = GT
639 cmpTy env (NewTcApp _ _) (FunTy _ _) = GT
640 cmpTy env (NewTcApp _ _) (TyConApp _ _) = GT
642 cmpTy env (ForAllTy _ _) (TyVarTy _) = GT
643 cmpTy env (ForAllTy _ _) (AppTy _ _) = GT
644 cmpTy env (ForAllTy _ _) (FunTy _ _) = GT
645 cmpTy env (ForAllTy _ _) (TyConApp _ _) = GT
646 cmpTy env (ForAllTy _ _) (NewTcApp _ _) = GT
648 cmpTy env (PredTy _) t2 = GT
654 cmpPredTy :: TyVarEnv TyVar -> PredType -> PredType -> Ordering
655 cmpPredTy env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` (cmpTy env ty1 ty2)
656 -- Compare types as well as names for implicit parameters
657 -- This comparison is used exclusively (I think) for the
658 -- finite map built in TcSimplify
659 cmpPredTy env (IParam _ _) (ClassP _ _) = LT
660 cmpPredTy env (ClassP _ _) (IParam _ _) = GT
661 cmpPredTy env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` (cmpTys env tys1 tys2)
664 PredTypes are used as a FM key in TcSimplify,
665 so we take the easy path and make them an instance of Ord
668 instance Eq PredType where { (==) = tcEqPred }
669 instance Ord PredType where { compare = tcCmpPred }
673 %************************************************************************
675 \subsection{Predicates}
677 %************************************************************************
679 isSigmaTy returns true of any qualified type. It doesn't *necessarily* have
681 f :: (?x::Int) => Int -> Int
684 isSigmaTy :: Type -> Bool
685 isSigmaTy (ForAllTy tyvar ty) = True
686 isSigmaTy (FunTy a b) = isPredTy a
687 isSigmaTy (NoteTy n ty) = isSigmaTy ty
690 isOverloadedTy :: Type -> Bool
691 isOverloadedTy (ForAllTy tyvar ty) = isOverloadedTy ty
692 isOverloadedTy (FunTy a b) = isPredTy a
693 isOverloadedTy (NoteTy n ty) = isOverloadedTy ty
694 isOverloadedTy _ = False
696 isPredTy :: Type -> Bool -- Belongs in TcType because it does
697 -- not look through newtypes, or predtypes (of course)
698 isPredTy (NoteTy _ ty) = isPredTy ty
699 isPredTy (PredTy sty) = True
704 isFloatTy = is_tc floatTyConKey
705 isDoubleTy = is_tc doubleTyConKey
706 isIntegerTy = is_tc integerTyConKey
707 isIntTy = is_tc intTyConKey
708 isAddrTy = is_tc addrTyConKey
709 isBoolTy = is_tc boolTyConKey
710 isUnitTy = is_tc unitTyConKey
712 is_tc :: Unique -> Type -> Bool
713 -- Newtypes are opaque to this
714 is_tc uniq ty = case tcSplitTyConApp_maybe ty of
715 Just (tc, _) -> uniq == getUnique tc
720 %************************************************************************
724 %************************************************************************
727 deNoteType :: Type -> Type
728 -- Remove synonyms, but not predicate types
729 deNoteType ty@(TyVarTy tyvar) = ty
730 deNoteType (TyConApp tycon tys) = TyConApp tycon (map deNoteType tys)
731 deNoteType (NewTcApp tycon tys) = NewTcApp tycon (map deNoteType tys)
732 deNoteType (PredTy p) = PredTy (deNotePredType p)
733 deNoteType (NoteTy _ ty) = deNoteType ty
734 deNoteType (AppTy fun arg) = AppTy (deNoteType fun) (deNoteType arg)
735 deNoteType (FunTy fun arg) = FunTy (deNoteType fun) (deNoteType arg)
736 deNoteType (ForAllTy tv ty) = ForAllTy tv (deNoteType ty)
738 deNotePredType :: PredType -> PredType
739 deNotePredType (ClassP c tys) = ClassP c (map deNoteType tys)
740 deNotePredType (IParam n ty) = IParam n (deNoteType ty)
743 Find the free tycons and classes of a type. This is used in the front
747 tyClsNamesOfType :: Type -> NameSet
748 tyClsNamesOfType (TyVarTy tv) = emptyNameSet
749 tyClsNamesOfType (TyConApp tycon tys) = unitNameSet (getName tycon) `unionNameSets` tyClsNamesOfTypes tys
750 tyClsNamesOfType (NewTcApp tycon tys) = unitNameSet (getName tycon) `unionNameSets` tyClsNamesOfTypes tys
751 tyClsNamesOfType (NoteTy (SynNote ty1) ty2) = tyClsNamesOfType ty1
752 tyClsNamesOfType (NoteTy other_note ty2) = tyClsNamesOfType ty2
753 tyClsNamesOfType (PredTy (IParam n ty)) = tyClsNamesOfType ty
754 tyClsNamesOfType (PredTy (ClassP cl tys)) = unitNameSet (getName cl) `unionNameSets` tyClsNamesOfTypes tys
755 tyClsNamesOfType (FunTy arg res) = tyClsNamesOfType arg `unionNameSets` tyClsNamesOfType res
756 tyClsNamesOfType (AppTy fun arg) = tyClsNamesOfType fun `unionNameSets` tyClsNamesOfType arg
757 tyClsNamesOfType (ForAllTy tyvar ty) = tyClsNamesOfType ty
759 tyClsNamesOfTypes tys = foldr (unionNameSets . tyClsNamesOfType) emptyNameSet tys
761 tyClsNamesOfDFunHead :: Type -> NameSet
762 -- Find the free type constructors and classes
763 -- of the head of the dfun instance type
764 -- The 'dfun_head_type' is because of
765 -- instance Foo a => Baz T where ...
766 -- The decl is an orphan if Baz and T are both not locally defined,
767 -- even if Foo *is* locally defined
768 tyClsNamesOfDFunHead dfun_ty
769 = case tcSplitSigmaTy dfun_ty of
770 (tvs,_,head_ty) -> tyClsNamesOfType head_ty
772 classesOfTheta :: ThetaType -> [Class]
773 -- Looks just for ClassP things; maybe it should check
774 classesOfTheta preds = [ c | ClassP c _ <- preds ]
778 %************************************************************************
780 \subsection[TysWiredIn-ext-type]{External types}
782 %************************************************************************
784 The compiler's foreign function interface supports the passing of a
785 restricted set of types as arguments and results (the restricting factor
789 isFFITy :: Type -> Bool
790 -- True for any TyCon that can possibly be an arg or result of an FFI call
791 isFFITy ty = checkRepTyCon legalFFITyCon ty
793 isFFIArgumentTy :: DynFlags -> Safety -> Type -> Bool
794 -- Checks for valid argument type for a 'foreign import'
795 isFFIArgumentTy dflags safety ty
796 = checkRepTyCon (legalOutgoingTyCon dflags safety) ty
798 isFFIExternalTy :: Type -> Bool
799 -- Types that are allowed as arguments of a 'foreign export'
800 isFFIExternalTy ty = checkRepTyCon legalFEArgTyCon ty
802 isFFIImportResultTy :: DynFlags -> Type -> Bool
803 isFFIImportResultTy dflags ty
804 = checkRepTyCon (legalFIResultTyCon dflags) ty
806 isFFIExportResultTy :: Type -> Bool
807 isFFIExportResultTy ty = checkRepTyCon legalFEResultTyCon ty
809 isFFIDynArgumentTy :: Type -> Bool
810 -- The argument type of a foreign import dynamic must be Ptr, FunPtr, Addr,
811 -- or a newtype of either.
812 isFFIDynArgumentTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey, addrTyConKey]
814 isFFIDynResultTy :: Type -> Bool
815 -- The result type of a foreign export dynamic must be Ptr, FunPtr, Addr,
816 -- or a newtype of either.
817 isFFIDynResultTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey, addrTyConKey]
819 isFFILabelTy :: Type -> Bool
820 -- The type of a foreign label must be Ptr, FunPtr, Addr,
821 -- or a newtype of either.
822 isFFILabelTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey, addrTyConKey]
824 isFFIDotnetTy :: DynFlags -> Type -> Bool
825 isFFIDotnetTy dflags ty
826 = checkRepTyCon (\ tc -> not (isByteArrayLikeTyCon tc) &&
827 (legalFIResultTyCon dflags tc ||
828 isFFIDotnetObjTy ty || isStringTy ty)) ty
830 -- Support String as an argument or result from a .NET FFI call.
832 case tcSplitTyConApp_maybe (repType ty) of
835 case tcSplitTyConApp_maybe (repType arg_ty) of
836 Just (cc,[]) -> cc == charTyCon
840 -- Support String as an argument or result from a .NET FFI call.
841 isFFIDotnetObjTy ty =
843 (_, t_ty) = tcSplitForAllTys ty
845 case tcSplitTyConApp_maybe (repType t_ty) of
846 Just (tc, [arg_ty]) | getName tc == objectTyConName -> True
849 toDNType :: Type -> DNType
851 | isStringTy ty = DNString
852 | isFFIDotnetObjTy ty = DNObject
853 | Just (tc,argTys) <- tcSplitTyConApp_maybe ty =
854 case lookup (getUnique tc) dn_assoc of
857 | tc `hasKey` ioTyConKey -> toDNType (head argTys)
858 | otherwise -> pprPanic ("toDNType: unsupported .NET type") (pprType ty <+> parens (hcat (map pprType argTys)) <+> ppr tc)
860 dn_assoc :: [ (Unique, DNType) ]
861 dn_assoc = [ (unitTyConKey, DNUnit)
862 , (intTyConKey, DNInt)
863 , (int8TyConKey, DNInt8)
864 , (int16TyConKey, DNInt16)
865 , (int32TyConKey, DNInt32)
866 , (int64TyConKey, DNInt64)
867 , (wordTyConKey, DNInt)
868 , (word8TyConKey, DNWord8)
869 , (word16TyConKey, DNWord16)
870 , (word32TyConKey, DNWord32)
871 , (word64TyConKey, DNWord64)
872 , (floatTyConKey, DNFloat)
873 , (doubleTyConKey, DNDouble)
874 , (addrTyConKey, DNPtr)
875 , (ptrTyConKey, DNPtr)
876 , (funPtrTyConKey, DNPtr)
877 , (charTyConKey, DNChar)
878 , (boolTyConKey, DNBool)
881 checkRepTyCon :: (TyCon -> Bool) -> Type -> Bool
882 -- Look through newtypes
883 -- Non-recursive ones are transparent to splitTyConApp,
884 -- but recursive ones aren't. Manuel had:
885 -- newtype T = MkT (Ptr T)
886 -- and wanted it to work...
887 checkRepTyCon check_tc ty
888 | Just (tc,_) <- splitTyConApp_maybe (repType ty) = check_tc tc
891 checkRepTyConKey :: [Unique] -> Type -> Bool
892 -- Like checkRepTyCon, but just looks at the TyCon key
893 checkRepTyConKey keys
894 = checkRepTyCon (\tc -> tyConUnique tc `elem` keys)
897 ----------------------------------------------
898 These chaps do the work; they are not exported
899 ----------------------------------------------
902 legalFEArgTyCon :: TyCon -> Bool
903 -- It's illegal to return foreign objects and (mutable)
904 -- bytearrays from a _ccall_ / foreign declaration
905 -- (or be passed them as arguments in foreign exported functions).
907 | isByteArrayLikeTyCon tc
909 -- It's also illegal to make foreign exports that take unboxed
910 -- arguments. The RTS API currently can't invoke such things. --SDM 7/2000
912 = boxedMarshalableTyCon tc
914 legalFIResultTyCon :: DynFlags -> TyCon -> Bool
915 legalFIResultTyCon dflags tc
916 | isByteArrayLikeTyCon tc = False
917 | tc == unitTyCon = True
918 | otherwise = marshalableTyCon dflags tc
920 legalFEResultTyCon :: TyCon -> Bool
921 legalFEResultTyCon tc
922 | isByteArrayLikeTyCon tc = False
923 | tc == unitTyCon = True
924 | otherwise = boxedMarshalableTyCon tc
926 legalOutgoingTyCon :: DynFlags -> Safety -> TyCon -> Bool
927 -- Checks validity of types going from Haskell -> external world
928 legalOutgoingTyCon dflags safety tc
929 | playSafe safety && isByteArrayLikeTyCon tc
932 = marshalableTyCon dflags tc
934 legalFFITyCon :: TyCon -> Bool
935 -- True for any TyCon that can possibly be an arg or result of an FFI call
937 = isUnLiftedTyCon tc || boxedMarshalableTyCon tc || tc == unitTyCon
939 marshalableTyCon dflags tc
940 = (dopt Opt_GlasgowExts dflags && isUnLiftedTyCon tc)
941 || boxedMarshalableTyCon tc
943 boxedMarshalableTyCon tc
944 = getUnique tc `elem` [ intTyConKey, int8TyConKey, int16TyConKey
945 , int32TyConKey, int64TyConKey
946 , wordTyConKey, word8TyConKey, word16TyConKey
947 , word32TyConKey, word64TyConKey
948 , floatTyConKey, doubleTyConKey
949 , addrTyConKey, ptrTyConKey, funPtrTyConKey
952 , byteArrayTyConKey, mutableByteArrayTyConKey
956 isByteArrayLikeTyCon :: TyCon -> Bool
957 isByteArrayLikeTyCon tc =
958 getUnique tc `elem` [byteArrayTyConKey, mutableByteArrayTyConKey]
962 %************************************************************************
964 \subsection{Unification with an explicit substitution}
966 %************************************************************************
968 Unify types with an explicit substitution and no monad.
972 = (TyVarSet, -- Set of template tyvars
973 TyVarSubstEnv) -- Not necessarily idempotent
975 unifyTysX :: TyVarSet -- Template tyvars
978 -> Maybe TyVarSubstEnv
979 unifyTysX tmpl_tyvars ty1 ty2
980 = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
983 :: TyVarSet -- Template tyvars
984 -> TyVarSubstEnv -- Substitution to start with
987 -> Maybe TyVarSubstEnv -- Extended substitution
988 unifyExtendTyListsX tmpl_tyvars subst tys1 tys2
989 = uTyListsX tys1 tys2 (\(_,s) -> Just s) (tmpl_tyvars, subst)
991 unifyTyListsX :: TyVarSet -> [Type] -> [Type]
992 -> Maybe TyVarSubstEnv
993 unifyTyListsX tmpl_tyvars tys1 tys2
994 = uTyListsX tys1 tys2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
999 -> (MySubst -> Maybe result)
1003 uTysX (NoteTy _ ty1) ty2 k subst = uTysX ty1 ty2 k subst
1004 uTysX ty1 (NoteTy _ ty2) k subst = uTysX ty1 ty2 k subst
1006 -- Variables; go for uVar
1007 uTysX (TyVarTy tyvar1) (TyVarTy tyvar2) k subst
1010 uTysX (TyVarTy tyvar1) ty2 k subst@(tmpls,_)
1011 | tyvar1 `elemVarSet` tmpls
1012 = uVarX tyvar1 ty2 k subst
1013 uTysX ty1 (TyVarTy tyvar2) k subst@(tmpls,_)
1014 | tyvar2 `elemVarSet` tmpls
1015 = uVarX tyvar2 ty1 k subst
1018 uTysX (PredTy (IParam n1 t1)) (PredTy (IParam n2 t2)) k subst
1019 | n1 == n2 = uTysX t1 t2 k subst
1020 uTysX (PredTy (ClassP c1 tys1)) (PredTy (ClassP c2 tys2)) k subst
1021 | c1 == c2 = uTyListsX tys1 tys2 k subst
1023 -- Functions; just check the two parts
1024 uTysX (FunTy fun1 arg1) (FunTy fun2 arg2) k subst
1025 = uTysX fun1 fun2 (uTysX arg1 arg2 k) subst
1027 -- Type constructors must match
1028 uTysX (NewTcApp tc1 tys1) (NewTcApp tc2 tys2) k subst
1029 | tc1 == tc2 = uTyListsX tys1 tys2 k subst
1030 uTysX (TyConApp con1 tys1) (TyConApp con2 tys2) k subst
1031 | (con1 == con2 && equalLength tys1 tys2)
1032 = uTyListsX tys1 tys2 k subst
1034 -- Applications need a bit of care!
1035 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
1036 -- NB: we've already dealt with type variables and Notes,
1037 -- so if one type is an App the other one jolly well better be too
1038 uTysX (AppTy s1 t1) ty2 k subst
1039 = case tcSplitAppTy_maybe ty2 of
1040 Just (s2, t2) -> uTysX s1 s2 (uTysX t1 t2 k) subst
1041 Nothing -> Nothing -- Fail
1043 uTysX ty1 (AppTy s2 t2) k subst
1044 = case tcSplitAppTy_maybe ty1 of
1045 Just (s1, t1) -> uTysX s1 s2 (uTysX t1 t2 k) subst
1046 Nothing -> Nothing -- Fail
1048 -- Not expecting for-alls in unification
1050 uTysX (ForAllTy _ _) ty2 k subst = panic "Unify.uTysX subst:ForAllTy (1st arg)"
1051 uTysX ty1 (ForAllTy _ _) k subst = panic "Unify.uTysX subst:ForAllTy (2nd arg)"
1054 -- Anything else fails
1055 uTysX ty1 ty2 k subst = Nothing
1058 uTyListsX [] [] k subst = k subst
1059 uTyListsX (ty1:tys1) (ty2:tys2) k subst = uTysX ty1 ty2 (uTyListsX tys1 tys2 k) subst
1060 uTyListsX tys1 tys2 k subst = Nothing -- Fail if the lists are different lengths
1064 -- Invariant: tv1 is a unifiable variable
1065 uVarX tv1 ty2 k subst@(tmpls, env)
1066 = case lookupSubstEnv env tv1 of
1067 Just (DoneTy ty1) -> -- Already bound
1068 uTysX ty1 ty2 k subst
1070 Nothing -- Not already bound
1071 | typeKind ty2 == tyVarKind tv1
1072 && occur_check_ok ty2
1073 -> -- No kind mismatch nor occur check
1074 k (tmpls, extendSubstEnv env tv1 (DoneTy ty2))
1076 | otherwise -> Nothing -- Fail if kind mis-match or occur check
1078 occur_check_ok ty = all occur_check_ok_tv (varSetElems (tyVarsOfType ty))
1079 occur_check_ok_tv tv | tv1 == tv = False
1080 | otherwise = case lookupSubstEnv env tv of
1082 Just (DoneTy ty) -> occur_check_ok ty
1087 %************************************************************************
1089 \subsection{Matching on types}
1091 %************************************************************************
1093 Matching is a {\em unidirectional} process, matching a type against a
1094 template (which is just a type with type variables in it). The
1095 matcher assumes that there are no repeated type variables in the
1096 template, so that it simply returns a mapping of type variables to
1097 types. It also fails on nested foralls.
1099 @matchTys@ matches corresponding elements of a list of templates and
1100 types. It and @matchTy@ both ignore usage annotations, unlike the
1101 main function @match@.
1104 matchTy :: TyVarSet -- Template tyvars
1106 -> Type -- Proposed instance of template
1107 -> Maybe TyVarSubstEnv -- Matching substitution
1110 matchTys :: TyVarSet -- Template tyvars
1111 -> [Type] -- Templates
1112 -> [Type] -- Proposed instance of template
1113 -> Maybe (TyVarSubstEnv, -- Matching substitution
1114 [Type]) -- Left over instance types
1116 matchTy tmpls ty1 ty2 = match ty1 ty2 tmpls (\ senv -> Just senv) emptySubstEnv
1118 matchTys tmpls tys1 tys2 = match_list tys1 tys2 tmpls
1119 (\ (senv,tys) -> Just (senv,tys))
1123 @match@ is the main function. It takes a flag indicating whether
1124 usage annotations are to be respected.
1127 match :: Type -> Type -- Current match pair
1128 -> TyVarSet -- Template vars
1129 -> (TyVarSubstEnv -> Maybe result) -- Continuation
1130 -> TyVarSubstEnv -- Current subst
1133 -- When matching against a type variable, see if the variable
1134 -- has already been bound. If so, check that what it's bound to
1135 -- is the same as ty; if not, bind it and carry on.
1137 match (TyVarTy v) ty tmpls k senv
1138 | v `elemVarSet` tmpls
1139 = -- v is a template variable
1140 case lookupSubstEnv senv v of
1141 Nothing | typeKind ty `isSubKind` tyVarKind v
1142 -- We do a kind check, just as in the uVarX above
1143 -- The kind check is needed to avoid bogus matches
1144 -- of (a b) with (c d), where the kinds don't match
1145 -- An occur check isn't needed when matching.
1146 -> k (extendSubstEnv senv v (DoneTy ty))
1148 | otherwise -> Nothing -- Fails
1150 Just (DoneTy ty') | ty' `tcEqType` ty -> k senv -- Succeeds
1151 | otherwise -> Nothing -- Fails
1154 = -- v is not a template variable; ty had better match
1155 -- Can't use (==) because types differ
1156 case tcGetTyVar_maybe ty of
1157 Just v' | v == v' -> k senv -- Success
1158 other -> Nothing -- Failure
1159 -- This tcGetTyVar_maybe is *required* because it must strip Notes.
1160 -- I guess the reason the Note-stripping case is *last* rather than first
1161 -- is to preserve type synonyms etc., so I'm not moving it to the
1162 -- top; but this means that (without the deNotetype) a type
1163 -- variable may not match the pattern (TyVarTy v') as one would
1164 -- expect, due to an intervening Note. KSW 2000-06.
1167 match (PredTy (IParam n1 t1)) (PredTy (IParam n2 t2)) tmpls k senv
1168 | n1 == n2 = match t1 t2 tmpls k senv
1169 match (PredTy (ClassP c1 tys1)) (PredTy (ClassP c2 tys2)) tmpls k senv
1170 | c1 == c2 = match_list_exactly tys1 tys2 tmpls k senv
1172 -- Functions; just check the two parts
1173 match (FunTy arg1 res1) (FunTy arg2 res2) tmpls k senv
1174 = match arg1 arg2 tmpls (match res1 res2 tmpls k) senv
1176 -- If the template is an application, try to make the
1177 -- thing we are matching look like an application
1178 match (AppTy fun1 arg1) ty2 tmpls k senv
1179 = case tcSplitAppTy_maybe ty2 of
1180 Just (fun2,arg2) -> match fun1 fun2 tmpls (match arg1 arg2 tmpls k) senv
1181 Nothing -> Nothing -- Fail
1183 -- Newtypes are opaque; predicate types should not happen
1184 match (NewTcApp tc1 tys1) (NewTcApp tc2 tys2) tmpls k senv
1185 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1186 match (TyConApp tc1 tys1) (TyConApp tc2 tys2) tmpls k senv
1187 | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1189 -- With type synonyms, we have to be careful for the exact
1190 -- same reasons as in the unifier. Please see the
1191 -- considerable commentary there before changing anything
1192 -- here! (WDP 95/05)
1193 match (NoteTy n1 ty1) ty2 tmpls k senv = match ty1 ty2 tmpls k senv
1194 match ty1 (NoteTy n2 ty2) tmpls k senv = match ty1 ty2 tmpls k senv
1197 match _ _ _ _ _ = Nothing
1199 match_list_exactly tys1 tys2 tmpls k senv
1200 = match_list tys1 tys2 tmpls k' senv
1202 k' (senv', tys2') | null tys2' = k senv' -- Succeed
1203 | otherwise = Nothing -- Fail
1205 match_list [] tys2 tmpls k senv = k (senv, tys2)
1206 match_list (ty1:tys1) [] tmpls k senv = Nothing -- Not enough arg tys => failure
1207 match_list (ty1:tys1) (ty2:tys2) tmpls k senv
1208 = match ty1 ty2 tmpls (match_list tys1 tys2 tmpls k) senv