2 #include "HsVersions.h"
5 GenType(..), Type(..), TauType(..),
6 mkTyVarTy, getTyVar, getTyVar_maybe, isTyVarTy,
7 mkAppTy, mkAppTys, splitAppTy,
8 mkFunTy, mkFunTys, splitFunTy, getFunTy_maybe,
9 mkTyConTy, getTyCon_maybe, applyTyCon,
11 mkForAllTy, mkForAllTys, getForAllTy_maybe, splitForAllTy,
12 mkForAllUsageTy, getForAllUsageTy,
17 RhoType(..), SigmaType(..), ThetaType(..),
20 mkSigmaTy, splitSigmaTy,
22 maybeAppTyCon, getAppTyCon,
23 maybeAppDataTyCon, getAppDataTyCon,
26 matchTy, matchTys, eqTy, eqSimpleTy, eqSimpleTheta,
28 instantiateTy,instantiateUsage,
32 tyVarsOfType, tyVarsOfTypes, getTypeKind
38 import IdLoop -- for paranoia checking
39 import TyLoop -- for paranoia checking
40 import PrelLoop -- for paranoia checking
43 import Class ( getClassSig, getClassOpLocalType, GenClass{-instances-} )
44 import Kind ( mkBoxedTypeKind, resultKind )
45 import TyCon ( mkFunTyCon, mkTupleTyCon, isFunTyCon, isPrimTyCon,
46 getTyConKind, getTyConDataCons, TyCon )
47 import TyVar ( getTyVarKind, GenTyVar{-instances-}, GenTyVarSet(..),
48 emptyTyVarSet, unionTyVarSets, minusTyVarSet,
49 singletonTyVarSet, nullTyVarEnv, lookupTyVarEnv,
50 addOneToTyVarEnv, TyVarEnv(..) )
51 import Usage ( usageOmega, GenUsage, Usage(..), UVar(..), UVarEnv(..),
52 nullUVarEnv, addOneToUVarEnv, lookupUVarEnv, eqUVar,
56 import Util ( thenCmp, zipEqual, panic, panic#, assertPanic,
65 type Type = GenType TyVar UVar -- Used after typechecker
67 data GenType tyvar uvar -- Parameterised over type and usage variables
74 | TyConTy -- Constants of a specified kind
76 (GenUsage uvar) -- Usage gives uvar of the full application,
77 -- iff the full application is of kind Type
78 -- c.f. the Usage field in TyVars
80 | SynTy -- Synonyms must be saturated, and contain their expansion
81 TyCon -- Must be a SynTyCon
83 (GenType tyvar uvar) -- Expansion!
87 (GenType tyvar uvar) -- TypeKind
90 uvar -- Quantify over this
91 [uvar] -- Bounds; the quantified var must be
92 -- less than or equal to all these
95 -- Two special cases that save a *lot* of administrative
98 | FunTy -- BoxedTypeKind
99 (GenType tyvar uvar) -- Both args are of TypeKind
105 (GenType tyvar uvar) -- Arg has kind TypeKind
112 type ThetaType = [(Class, Type)]
113 type SigmaType = Type
119 Removes just the top level of any abbreviations.
122 expandTy :: Type -> Type -- Restricted to Type due to Dict expansion
124 expandTy (FunTy t1 t2 u) = AppTy (AppTy (TyConTy mkFunTyCon u) t1) t2
125 expandTy (SynTy _ _ t) = expandTy t
126 expandTy (DictTy clas ty u)
127 = case all_arg_tys of
129 [arg_ty] -> expandTy arg_ty -- just the <whatever> itself
131 -- The extra expandTy is to make sure that
132 -- the result isn't still a dict, which it might be
133 -- if the original guy was a dict with one superdict and
136 other -> ASSERT(not (null all_arg_tys))
137 foldl AppTy (TyConTy (mkTupleTyCon (length all_arg_tys)) u) all_arg_tys
140 -- Note: length of all_arg_tys can be 0 if the class is
141 -- _CCallable, _CReturnable (and anything else
142 -- *really weird* that the user writes).
144 (tyvar, super_classes, ops) = getClassSig clas
145 super_dict_tys = map mk_super_ty super_classes
146 class_op_tys = map mk_op_ty ops
147 all_arg_tys = super_dict_tys ++ class_op_tys
148 mk_super_ty sc = DictTy sc ty usageOmega
149 mk_op_ty op = instantiateTy [(tyvar,ty)] (getClassOpLocalType op)
154 Simple construction and analysis functions
155 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
157 mkTyVarTy :: t -> GenType t u
159 -- could we use something for (map mkTyVarTy blahs) ?? WDP
161 getTyVar :: String -> GenType t u -> t
162 getTyVar msg (TyVarTy tv) = tv
163 getTyVar msg (SynTy _ _ t) = getTyVar msg t
164 getTyVar msg other = error ("getTyVar" ++ msg)
166 getTyVar_maybe :: GenType t u -> Maybe t
167 getTyVar_maybe (TyVarTy tv) = Just tv
168 getTyVar_maybe (SynTy _ _ t) = getTyVar_maybe t
169 getTyVar_maybe other = Nothing
171 isTyVarTy :: GenType t u -> Bool
172 isTyVarTy (TyVarTy tv) = True
173 isTyVarTy (SynTy _ _ t) = isTyVarTy t
174 isTyVarTy other = False
180 mkAppTys :: GenType t u -> [GenType t u] -> GenType t u
181 mkAppTys t ts = foldl AppTy t ts
183 splitAppTy :: GenType t u -> (GenType t u, [GenType t u])
184 splitAppTy t = go t []
186 go (AppTy t arg) ts = go t (arg:ts)
187 go (FunTy fun arg u) ts = (TyConTy mkFunTyCon u, fun:arg:ts)
188 go (SynTy _ _ t) ts = go t ts
193 -- NB mkFunTy, mkFunTys puts in Omega usages, for now at least
194 mkFunTy arg res = FunTy arg res usageOmega
196 mkFunTys :: [GenType t u] -> GenType t u -> GenType t u
197 mkFunTys ts t = foldr (\ f a -> FunTy f a usageOmega) t ts
199 getFunTy_maybe :: GenType t u -> Maybe (GenType t u, GenType t u)
200 getFunTy_maybe (FunTy arg result _) = Just (arg,result)
201 getFunTy_maybe (AppTy (AppTy (TyConTy tycon _) arg) res)
202 | isFunTyCon tycon = Just (arg, res)
203 getFunTy_maybe (SynTy _ _ t) = getFunTy_maybe t
204 getFunTy_maybe other = Nothing
206 splitFunTy :: GenType t u -> ([GenType t u], GenType t u)
207 splitFunTy t = go t []
209 go (FunTy arg res _) ts = go res (arg:ts)
210 go (AppTy (AppTy (TyConTy tycon _) arg) res) ts
220 -- NB applyTyCon puts in usageOmega, for now at least
221 mkTyConTy tycon = TyConTy tycon usageOmega
223 applyTyCon :: TyCon -> [GenType t u] -> GenType t u
224 applyTyCon tycon tys = foldl AppTy (TyConTy tycon usageOmega) tys
226 getTyCon_maybe :: GenType t u -> Maybe TyCon
227 getTyCon_maybe (TyConTy tycon _) = Just tycon
228 getTyCon_maybe (SynTy _ _ t) = getTyCon_maybe t
229 getTyCon_maybe other_ty = Nothing
233 mkSynTy syn_tycon tys
234 = SynTy syn_tycon tys (panic "Type.mkSynTy:expansion")
240 isTauTy :: GenType t u -> Bool
241 isTauTy (TyVarTy v) = True
242 isTauTy (TyConTy _ _) = True
243 isTauTy (AppTy a b) = isTauTy a && isTauTy b
244 isTauTy (FunTy a b _) = isTauTy a && isTauTy b
245 isTauTy (SynTy _ _ ty) = isTauTy ty
246 isTauTy other = False
251 NB mkRhoTy and mkDictTy put in usageOmega, for now at least
254 mkDictTy :: Class -> GenType t u -> GenType t u
255 mkDictTy clas ty = DictTy clas ty usageOmega
257 mkRhoTy :: [(Class, GenType t u)] -> GenType t u -> GenType t u
259 foldr (\(c,t) r -> FunTy (DictTy c t usageOmega) r usageOmega) ty theta
261 splitRhoTy :: GenType t u -> ([(Class,GenType t u)], GenType t u)
265 go (FunTy (DictTy c t _) r _) ts = go r ((c,t):ts)
266 go (AppTy (AppTy (TyConTy tycon _) (DictTy c t _)) r) ts
269 go (SynTy _ _ t) ts = go t ts
270 go t ts = (reverse ts, t)
277 mkForAllTy = ForAllTy
279 mkForAllTys :: [t] -> GenType t u -> GenType t u
280 mkForAllTys tyvars ty = foldr ForAllTy ty tyvars
282 getForAllTy_maybe :: GenType t u -> Maybe (t,GenType t u)
283 getForAllTy_maybe (SynTy _ _ t) = getForAllTy_maybe t
284 getForAllTy_maybe (ForAllTy tyvar t) = Just(tyvar,t)
285 getForAllTy_maybe _ = Nothing
287 splitForAllTy :: GenType t u-> ([t], GenType t u)
288 splitForAllTy t = go t []
290 go (ForAllTy tv t) tvs = go t (tv:tvs)
291 go (SynTy _ _ t) tvs = go t tvs
292 go t tvs = (reverse tvs, t)
296 mkForAllUsageTy :: u -> [u] -> GenType t u -> GenType t u
297 mkForAllUsageTy = ForAllUsageTy
299 getForAllUsageTy :: GenType t u -> Maybe (u,[u],GenType t u)
300 getForAllUsageTy (ForAllUsageTy uvar bounds t) = Just(uvar,bounds,t)
301 getForAllUsageTy (SynTy _ _ t) = getForAllUsageTy t
302 getForAllUsageTy _ = Nothing
305 Applied tycons (includes FunTyCons)
306 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
309 :: GenType tyvar uvar
310 -> Maybe (TyCon, -- the type constructor
311 [GenType tyvar uvar]) -- types to which it is applied
314 = case (getTyCon_maybe app_ty) of
316 Just tycon -> Just (tycon, arg_tys)
318 (app_ty, arg_tys) = splitAppTy ty
322 :: GenType tyvar uvar
323 -> (TyCon, -- the type constructor
324 [GenType tyvar uvar]) -- types to which it is applied
327 = case maybeAppTyCon ty of
330 Nothing -> panic "Type.getAppTyCon" -- (ppr PprShowAll ty)
334 Applied data tycons (give back constrs)
335 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
338 :: GenType tyvar uvar
339 -> Maybe (TyCon, -- the type constructor
340 [GenType tyvar uvar], -- types to which it is applied
341 [Id]) -- its family of data-constructors
344 = case (getTyCon_maybe app_ty) of
346 Just tycon | isFunTyCon tycon
349 -> Just (tycon, arg_tys, getTyConDataCons tycon)
351 (app_ty, arg_tys) = splitAppTy ty
355 :: GenType tyvar uvar
356 -> (TyCon, -- the type constructor
357 [GenType tyvar uvar], -- types to which it is applied
358 [Id]) -- its family of data-constructors
361 = case maybeAppDataTyCon ty of
364 Nothing -> panic "Type.getAppDataTyCon" -- (ppr PprShowAll ty)
368 maybeBoxedPrimType :: Type -> Maybe (Id, Type)
370 maybeBoxedPrimType ty
371 = case (maybeAppDataTyCon ty) of -- Data type,
372 Just (tycon, tys_applied, [data_con]) -- with exactly one constructor
373 -> case (getInstantiatedDataConSig data_con tys_applied) of
374 (_, [data_con_arg_ty], _) -- Applied to exactly one type,
375 | isPrimType data_con_arg_ty -- which is primitive
376 -> Just (data_con, data_con_arg_ty)
377 other_cases -> Nothing
378 other_cases -> Nothing
382 splitSigmaTy :: GenType t u -> ([t], [(Class,GenType t u)], GenType t u)
386 (tyvars,rho) = splitForAllTy ty
387 (theta,tau) = splitRhoTy rho
389 mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkRhoTy theta tau)
393 Finding the kind of a type
394 ~~~~~~~~~~~~~~~~~~~~~~~~~~
396 getTypeKind :: GenType (GenTyVar any) u -> Kind
397 getTypeKind (TyVarTy tyvar) = getTyVarKind tyvar
398 getTypeKind (TyConTy tycon usage) = getTyConKind tycon
399 getTypeKind (SynTy _ _ ty) = getTypeKind ty
400 getTypeKind (FunTy fun arg _) = mkBoxedTypeKind
401 getTypeKind (DictTy clas arg _) = mkBoxedTypeKind
402 getTypeKind (AppTy fun arg) = resultKind (getTypeKind fun)
403 getTypeKind (ForAllTy _ _) = mkBoxedTypeKind
404 getTypeKind (ForAllUsageTy _ _ _) = mkBoxedTypeKind
408 Free variables of a type
409 ~~~~~~~~~~~~~~~~~~~~~~~~
411 tyVarsOfType :: GenType (GenTyVar flexi) uvar -> GenTyVarSet flexi
413 tyVarsOfType (TyVarTy tv) = singletonTyVarSet tv
414 tyVarsOfType (TyConTy tycon usage) = emptyTyVarSet
415 tyVarsOfType (SynTy _ tys ty) = tyVarsOfTypes tys
416 tyVarsOfType (FunTy arg res _) = tyVarsOfType arg `unionTyVarSets` tyVarsOfType res
417 tyVarsOfType (AppTy fun arg) = tyVarsOfType fun `unionTyVarSets` tyVarsOfType arg
418 tyVarsOfType (DictTy clas ty _) = tyVarsOfType ty
419 tyVarsOfType (ForAllTy tyvar ty) = tyVarsOfType ty `minusTyVarSet` singletonTyVarSet tyvar
420 tyVarsOfType (ForAllUsageTy _ _ ty) = tyVarsOfType ty
422 tyVarsOfTypes :: [GenType (GenTyVar flexi) uvar] -> GenTyVarSet flexi
423 tyVarsOfTypes tys = foldr (unionTyVarSets.tyVarsOfType) emptyTyVarSet tys
430 applyTy :: Eq t => GenType t u -> GenType t u -> GenType t u
431 applyTy (SynTy _ _ fun) arg = applyTy fun arg
432 applyTy (ForAllTy tv ty) arg = instantiateTy [(tv,arg)] ty
433 applyTy other arg = panic "applyTy"
435 instantiateTy :: Eq t => [(t, GenType t u)] -> GenType t u -> GenType t u
436 instantiateTy tenv ty
439 go (TyVarTy tv) = case [ty | (tv',ty) <- tenv, tv==tv'] of
442 go ty@(TyConTy tycon usage) = ty
443 go (SynTy tycon tys ty) = SynTy tycon (map go tys) (go ty)
444 go (FunTy arg res usage) = FunTy (go arg) (go res) usage
445 go (AppTy fun arg) = AppTy (go fun) (go arg)
446 go (DictTy clas ty usage) = DictTy clas (go ty) usage
447 go (ForAllTy tv ty) = ASSERT(null tv_bound)
450 tv_bound = [() | (tv',_) <- tenv, tv==tv']
452 go (ForAllUsageTy uvar bds ty) = ForAllUsageTy uvar bds (go ty)
455 :: Ord3 u => [(u, GenType t u')] -> GenType t u -> GenType t u'
456 instantiateUsage = error "instantiateUsage: not implemented"
460 isPrimType :: GenType tyvar uvar -> Bool
461 isPrimType (AppTy ty _) = isPrimType ty
462 isPrimType (SynTy _ _ ty) = isPrimType ty
463 isPrimType (TyConTy tycon _) = isPrimTyCon tycon
467 %************************************************************************
469 \subsection{Matching on types}
471 %************************************************************************
473 Matching is a {\em unidirectional} process, matching a type against a
474 template (which is just a type with type variables in it). The
475 matcher assumes that there are no repeated type variables in the
476 template, so that it simply returns a mapping of type variables to
477 types. It also fails on nested foralls.
479 @matchTys@ matches corresponding elements of a list of templates and
483 matchTy :: GenType t1 u1 -- Template
484 -> GenType t2 u2 -- Proposed instance of template
485 -> Maybe [(t1,GenType t2 u2)] -- Matching substitution
487 matchTys :: [GenType t1 u1] -- Templates
488 -> [GenType t2 u2] -- Proposed instance of template
489 -> Maybe [(t1,GenType t2 u2)] -- Matching substitution
491 matchTy ty1 ty2 = match [] [] ty1 ty2
492 matchTys tys1 tys2 = match' [] (zipEqual tys1 tys2)
495 @match@ is the main function.
498 match :: [(t1, GenType t2 u2)] -- r, the accumulating result
499 -> [(GenType t1 u1, GenType t2 u2)] -- w, the work list
500 -> GenType t1 u1 -> GenType t2 u2 -- Current match pair
501 -> Maybe [(t1, GenType t2 u2)]
503 match r w (TyVarTy v) ty = match' ((v,ty) : r) w
504 match r w (FunTy fun1 arg1 _) (FunTy fun2 arg2 _) = match r ((fun1,fun2):w) arg1 arg2
505 match r w (AppTy fun1 arg1) (AppTy fun2 arg2) = match r ((fun1,fun2):w) arg1 arg2
506 match r w (TyConTy con1 _) (TyConTy con2 _) | con1 == con2 = match' r w
507 match r w (DictTy clas1 ty1 _) (DictTy clas2 ty2 _) | clas1 == clas2 = match r w ty1 ty2
508 match r w (SynTy _ _ ty1) ty2 = match r w ty1 ty2
509 match r w ty1 (SynTy _ _ ty2) = match r w ty1 ty2
511 -- With type synonyms, we have to be careful for the exact
512 -- same reasons as in the unifier. Please see the
513 -- considerable commentary there before changing anything
517 match _ _ _ _ = Nothing
520 match' r ((ty1,ty2):w) = match r w ty1 ty2
523 %************************************************************************
525 \subsection{Equality on types}
527 %************************************************************************
529 The functions eqSimpleTy and eqSimpleTheta are polymorphic in the types t
530 and u, but ONLY WORK FOR SIMPLE TYPES (ie. they panic if they see
531 dictionaries or polymorphic types). The function eqTy has a more
532 specific type, but does the `right thing' for all types.
535 eqSimpleTheta :: (Eq t,Eq u) =>
536 [(Class,GenType t u)] -> [(Class,GenType t u)] -> Bool
538 eqSimpleTheta [] [] = True
539 eqSimpleTheta ((c1,t1):th1) ((c2,t2):th2) =
540 c1==c2 && t1 `eqSimpleTy` t2 && th1 `eqSimpleTheta` th2
541 eqSimpleTheta other1 other2 = False
545 eqSimpleTy :: (Eq t,Eq u) => GenType t u -> GenType t u -> Bool
547 (TyVarTy tv1) `eqSimpleTy` (TyVarTy tv2) =
549 (AppTy f1 a1) `eqSimpleTy` (AppTy f2 a2) =
550 f1 `eqSimpleTy` f2 && a1 `eqSimpleTy` a2
551 (TyConTy tc1 u1) `eqSimpleTy` (TyConTy tc2 u2) =
552 tc1 == tc2 && u1 == u2
554 (FunTy f1 a1 u1) `eqSimpleTy` (FunTy f2 a2 u2) =
555 f1 `eqSimpleTy` f2 && a1 `eqSimpleTy` a2 && u1 == u2
556 (FunTy f1 a1 u1) `eqSimpleTy` t2 =
557 -- Expand t1 just in case t2 matches that version
558 (AppTy (AppTy (TyConTy mkFunTyCon u1) f1) a1) `eqSimpleTy` t2
559 t1 `eqSimpleTy` (FunTy f2 a2 u2) =
560 -- Expand t2 just in case t1 matches that version
561 t1 `eqSimpleTy` (AppTy (AppTy (TyConTy mkFunTyCon u2) f2) a2)
563 (SynTy tc1 ts1 t1) `eqSimpleTy` (SynTy tc2 ts2 t2) =
564 (tc1 == tc2 && and (zipWith eqSimpleTy ts1 ts2) && length ts1 == length ts2)
565 || t1 `eqSimpleTy` t2
566 (SynTy _ _ t1) `eqSimpleTy` t2 =
567 t1 `eqSimpleTy` t2 -- Expand the abbrevation and try again
568 t1 `eqSimpleTy` (SynTy _ _ t2) =
569 t1 `eqSimpleTy` t2 -- Expand the abbrevation and try again
571 (DictTy _ _ _) `eqSimpleTy` _ = panic "eqSimpleTy: got DictTy"
572 _ `eqSimpleTy` (DictTy _ _ _) = panic "eqSimpleTy: got DictTy"
574 (ForAllTy _ _) `eqSimpleTy` _ = panic "eqSimpleTy: got ForAllTy"
575 _ `eqSimpleTy` (ForAllTy _ _) = panic "eqSimpleTy: got ForAllTy"
577 (ForAllUsageTy _ _ _) `eqSimpleTy` _ = panic "eqSimpleTy: got ForAllUsageTy"
578 _ `eqSimpleTy` (ForAllUsageTy _ _ _) = panic "eqSimpleTy: got ForAllUsageTy"
580 _ `eqSimpleTy` _ = False
583 Types are ordered so we can sort on types in the renamer etc. DNT: Since
584 this class is also used in CoreLint and other such places, we DO expand out
585 Fun/Syn/Dict types (if necessary).
588 eqTy :: Type -> Type -> Bool
591 eq nullTyVarEnv nullUVarEnv t1 t2
593 eq tve uve (TyVarTy tv1) (TyVarTy tv2) =
595 case (lookupTyVarEnv tve tv1) of
598 eq tve uve (AppTy f1 a1) (AppTy f2 a2) =
599 eq tve uve f1 f2 && eq tve uve a1 a2
600 eq tve uve (TyConTy tc1 u1) (TyConTy tc2 u2) =
601 tc1 == tc2 && eqUsage uve u1 u2
603 eq tve uve (FunTy f1 a1 u1) (FunTy f2 a2 u2) =
604 eq tve uve f1 f2 && eq tve uve a1 a2 && eqUsage uve u1 u2
605 eq tve uve (FunTy f1 a1 u1) t2 =
606 -- Expand t1 just in case t2 matches that version
607 eq tve uve (AppTy (AppTy (TyConTy mkFunTyCon u1) f1) a1) t2
608 eq tve uve t1 (FunTy f2 a2 u2) =
609 -- Expand t2 just in case t1 matches that version
610 eq tve uve t1 (AppTy (AppTy (TyConTy mkFunTyCon u2) f2) a2)
612 eq tve uve (DictTy c1 t1 u1) (DictTy c2 t2 u2) =
613 c1 == c2 && eq tve uve t1 t2 && eqUsage uve u1 u2
614 eq tve uve t1@(DictTy _ _ _) t2 =
615 eq tve uve (expandTy t1) t2 -- Expand the dictionary and try again
616 eq tve uve t1 t2@(DictTy _ _ _) =
617 eq tve uve t1 (expandTy t2) -- Expand the dictionary and try again
619 eq tve uve (SynTy tc1 ts1 t1) (SynTy tc2 ts2 t2) =
620 (tc1 == tc2 && and (zipWith (eq tve uve) ts1 ts2) && length ts1 == length ts2)
622 eq tve uve (SynTy _ _ t1) t2 =
623 eq tve uve t1 t2 -- Expand the abbrevation and try again
624 eq tve uve t1 (SynTy _ _ t2) =
625 eq tve uve t1 t2 -- Expand the abbrevation and try again
627 eq tve uve (ForAllTy tv1 t1) (ForAllTy tv2 t2) =
628 eq (addOneToTyVarEnv tve tv1 tv2) uve t1 t2
629 eq tve uve (ForAllUsageTy u1 b1 t1) (ForAllUsageTy u2 b2 t2) =
630 eqBounds uve b1 b2 && eq tve (addOneToUVarEnv uve u1 u2) t1 t2
634 eqBounds uve [] [] = True
635 eqBounds uve (u1:b1) (u2:b2) = eqUVar uve u1 u2 && eqBounds uve b1 b2
636 eqBounds uve _ _ = False