s/Invisible/Inferred/g s/Visible/Required/g
[ghc.git] / compiler / iface / IfaceType.hs
1 {-
2 (c) The University of Glasgow 2006
3 (c) The GRASP/AQUA Project, Glasgow University, 1993-1998
4
5
6 This module defines interface types and binders
7 -}
8
9 {-# LANGUAGE CPP, FlexibleInstances #-}
10 -- FlexibleInstances for Binary (DefMethSpec IfaceType)
11
12 module IfaceType (
13 IfExtName, IfLclName,
14
15 IfaceType(..), IfacePredType, IfaceKind, IfaceCoercion(..),
16 IfaceUnivCoProv(..),
17 IfaceTyCon(..), IfaceTyConInfo(..),
18 IfaceTyLit(..), IfaceTcArgs(..),
19 IfaceContext, IfaceBndr(..), IfaceOneShot(..), IfaceLamBndr,
20 IfaceTvBndr, IfaceIdBndr, IfaceTyConBinder,
21 IfaceForAllBndr, ArgFlag(..),
22
23 ifConstraintKind, ifTyConBinderTyVar, ifTyConBinderName,
24
25 -- Equality testing
26 IfRnEnv2, emptyIfRnEnv2, eqIfaceType, eqIfaceTypes,
27 eqIfaceTcArgs, eqIfaceTvBndrs, isIfaceLiftedTypeKind,
28
29 -- Conversion from Type -> IfaceType
30 toIfaceType, toIfaceTypes, toIfaceKind, toIfaceTyVar,
31 toIfaceContext, toIfaceBndr, toIfaceIdBndr,
32 toIfaceTyCon, toIfaceTyCon_name,
33 toIfaceTcArgs, toIfaceTvBndr, toIfaceTvBndrs,
34 toIfaceForAllBndr,
35
36 -- Conversion from IfaceTcArgs -> IfaceType
37 tcArgsIfaceTypes,
38
39 -- Conversion from Coercion -> IfaceCoercion
40 toIfaceCoercion,
41
42 -- Printing
43 pprIfaceType, pprParendIfaceType,
44 pprIfaceContext, pprIfaceContextArr,
45 pprIfaceIdBndr, pprIfaceLamBndr, pprIfaceTvBndr, pprIfaceTyConBinders,
46 pprIfaceBndrs, pprIfaceTcArgs, pprParendIfaceTcArgs,
47 pprIfaceForAllPart, pprIfaceForAll, pprIfaceSigmaType,
48 pprIfaceCoercion, pprParendIfaceCoercion,
49 splitIfaceSigmaTy, pprIfaceTypeApp, pprUserIfaceForAll,
50
51 suppressIfaceInvisibles,
52 stripIfaceInvisVars,
53 stripInvisArgs,
54 substIfaceType, substIfaceTyVar, substIfaceTcArgs, mkIfaceTySubst,
55 eqIfaceTvBndr
56 ) where
57
58 #include "HsVersions.h"
59
60 import Coercion
61 import DataCon ( isTupleDataCon )
62 import TcType
63 import DynFlags
64 import TyCoRep -- needs to convert core types to iface types
65 import TyCon hiding ( pprPromotionQuote )
66 import CoAxiom
67 import Id
68 import Var
69 -- import RnEnv( FastStringEnv, mkFsEnv, lookupFsEnv )
70 import TysWiredIn
71 import TysPrim
72 import PrelNames
73 import Name
74 import BasicTypes
75 import Binary
76 import Outputable
77 import FastString
78 import UniqSet
79 import VarEnv
80 import UniqFM
81 import Util
82
83 {-
84 ************************************************************************
85 * *
86 Local (nested) binders
87 * *
88 ************************************************************************
89 -}
90
91 type IfLclName = FastString -- A local name in iface syntax
92
93 type IfExtName = Name -- An External or WiredIn Name can appear in IfaceSyn
94 -- (However Internal or System Names never should)
95
96 data IfaceBndr -- Local (non-top-level) binders
97 = IfaceIdBndr {-# UNPACK #-} !IfaceIdBndr
98 | IfaceTvBndr {-# UNPACK #-} !IfaceTvBndr
99
100 type IfaceIdBndr = (IfLclName, IfaceType)
101 type IfaceTvBndr = (IfLclName, IfaceKind)
102
103 ifaceTvBndrName :: IfaceTvBndr -> IfLclName
104 ifaceTvBndrName (n,_) = n
105
106 type IfaceLamBndr = (IfaceBndr, IfaceOneShot)
107
108 data IfaceOneShot -- See Note [Preserve OneShotInfo] in CoreTicy
109 = IfaceNoOneShot -- and Note [The oneShot function] in MkId
110 | IfaceOneShot
111
112
113 {-
114 %************************************************************************
115 %* *
116 IfaceType
117 %* *
118 %************************************************************************
119 -}
120
121 -------------------------------
122 type IfaceKind = IfaceType
123
124 data IfaceType -- A kind of universal type, used for types and kinds
125 = IfaceTyVar IfLclName -- Type/coercion variable only, not tycon
126 | IfaceLitTy IfaceTyLit
127 | IfaceAppTy IfaceType IfaceType
128 | IfaceFunTy IfaceType IfaceType
129 | IfaceDFunTy IfaceType IfaceType
130 | IfaceForAllTy IfaceForAllBndr IfaceType
131 | IfaceTyConApp IfaceTyCon IfaceTcArgs -- Not necessarily saturated
132 -- Includes newtypes, synonyms, tuples
133 | IfaceCastTy IfaceType IfaceCoercion
134 | IfaceCoercionTy IfaceCoercion
135 | IfaceTupleTy -- Saturated tuples (unsaturated ones use IfaceTyConApp)
136 TupleSort IfaceTyConInfo -- A bit like IfaceTyCon
137 IfaceTcArgs -- arity = length args
138 -- For promoted data cons, the kind args are omitted
139
140 type IfacePredType = IfaceType
141 type IfaceContext = [IfacePredType]
142
143 data IfaceTyLit
144 = IfaceNumTyLit Integer
145 | IfaceStrTyLit FastString
146 deriving (Eq)
147
148 type IfaceTyConBinder = TyVarBndr IfaceTvBndr TyConBndrVis
149 type IfaceForAllBndr = TyVarBndr IfaceTvBndr ArgFlag
150
151 -- See Note [Suppressing invisible arguments]
152 -- We use a new list type (rather than [(IfaceType,Bool)], because
153 -- it'll be more compact and faster to parse in interface
154 -- files. Rather than two bytes and two decisions (nil/cons, and
155 -- type/kind) there'll just be one.
156 data IfaceTcArgs
157 = ITC_Nil
158 | ITC_Vis IfaceType IfaceTcArgs -- "Vis" means show when pretty-printing
159 | ITC_Invis IfaceKind IfaceTcArgs -- "Invis" means don't show when pretty-printing
160 -- except with -fprint-explicit-kinds
161
162 -- Encodes type constructors, kind constructors,
163 -- coercion constructors, the lot.
164 -- We have to tag them in order to pretty print them
165 -- properly.
166 data IfaceTyCon = IfaceTyCon { ifaceTyConName :: IfExtName
167 , ifaceTyConInfo :: IfaceTyConInfo }
168 deriving (Eq)
169
170 data IfaceTyConInfo -- Used to guide pretty-printing
171 -- and to disambiguate D from 'D (they share a name)
172 = NoIfaceTyConInfo
173 | IfacePromotedDataCon
174 deriving (Eq)
175
176 data IfaceCoercion
177 = IfaceReflCo Role IfaceType
178 | IfaceFunCo Role IfaceCoercion IfaceCoercion
179 | IfaceTyConAppCo Role IfaceTyCon [IfaceCoercion]
180 | IfaceAppCo IfaceCoercion IfaceCoercion
181 | IfaceForAllCo IfaceTvBndr IfaceCoercion IfaceCoercion
182 | IfaceCoVarCo IfLclName
183 | IfaceAxiomInstCo IfExtName BranchIndex [IfaceCoercion]
184 | IfaceUnivCo IfaceUnivCoProv Role IfaceType IfaceType
185 | IfaceSymCo IfaceCoercion
186 | IfaceTransCo IfaceCoercion IfaceCoercion
187 | IfaceNthCo Int IfaceCoercion
188 | IfaceLRCo LeftOrRight IfaceCoercion
189 | IfaceInstCo IfaceCoercion IfaceCoercion
190 | IfaceCoherenceCo IfaceCoercion IfaceCoercion
191 | IfaceKindCo IfaceCoercion
192 | IfaceSubCo IfaceCoercion
193 | IfaceAxiomRuleCo IfLclName [IfaceCoercion]
194
195 data IfaceUnivCoProv
196 = IfaceUnsafeCoerceProv
197 | IfacePhantomProv IfaceCoercion
198 | IfaceProofIrrelProv IfaceCoercion
199 | IfacePluginProv String
200
201 -- this constant is needed for dealing with pretty-printing classes
202 ifConstraintKind :: IfaceKind
203 ifConstraintKind = IfaceTyConApp (IfaceTyCon { ifaceTyConName = getName constraintKindTyCon
204 , ifaceTyConInfo = NoIfaceTyConInfo })
205 ITC_Nil
206
207 {-
208 %************************************************************************
209 %* *
210 Functions over IFaceTypes
211 * *
212 ************************************************************************
213 -}
214
215 eqIfaceTvBndr :: IfaceTvBndr -> IfaceTvBndr -> Bool
216 eqIfaceTvBndr (occ1, _) (occ2, _) = occ1 == occ2
217
218 isIfaceLiftedTypeKind :: IfaceKind -> Bool
219 isIfaceLiftedTypeKind (IfaceTyConApp tc ITC_Nil)
220 = isLiftedTypeKindTyConName (ifaceTyConName tc)
221 isIfaceLiftedTypeKind (IfaceTyConApp tc
222 (ITC_Vis (IfaceTyConApp ptr_rep_lifted ITC_Nil) ITC_Nil))
223 = ifaceTyConName tc == tYPETyConName
224 && ifaceTyConName ptr_rep_lifted `hasKey` ptrRepLiftedDataConKey
225 isIfaceLiftedTypeKind _ = False
226
227 splitIfaceSigmaTy :: IfaceType -> ([IfaceForAllBndr], [IfacePredType], IfaceType)
228 -- Mainly for printing purposes
229 splitIfaceSigmaTy ty
230 = (bndrs, theta, tau)
231 where
232 (bndrs, rho) = split_foralls ty
233 (theta, tau) = split_rho rho
234
235 split_foralls (IfaceForAllTy bndr ty)
236 = case split_foralls ty of { (bndrs, rho) -> (bndr:bndrs, rho) }
237 split_foralls rho = ([], rho)
238
239 split_rho (IfaceDFunTy ty1 ty2)
240 = case split_rho ty2 of { (ps, tau) -> (ty1:ps, tau) }
241 split_rho tau = ([], tau)
242
243 suppressIfaceInvisibles :: DynFlags -> [IfaceTyConBinder] -> [a] -> [a]
244 suppressIfaceInvisibles dflags tys xs
245 | gopt Opt_PrintExplicitKinds dflags = xs
246 | otherwise = suppress tys xs
247 where
248 suppress _ [] = []
249 suppress [] a = a
250 suppress (k:ks) a@(_:xs)
251 | isInvisibleTyConBinder k = suppress ks xs
252 | otherwise = a
253
254 stripIfaceInvisVars :: DynFlags -> [IfaceTyConBinder] -> [IfaceTyConBinder]
255 stripIfaceInvisVars dflags tyvars
256 | gopt Opt_PrintExplicitKinds dflags = tyvars
257 | otherwise = filterOut isInvisibleTyConBinder tyvars
258
259 -- | Extract a IfaceTvBndr from a IfaceTyConBinder
260 ifTyConBinderTyVar :: IfaceTyConBinder -> IfaceTvBndr
261 ifTyConBinderTyVar = binderVar
262
263 -- | Extract the variable name from a IfaceTyConBinder
264 ifTyConBinderName :: IfaceTyConBinder -> IfLclName
265 ifTyConBinderName tcb = ifaceTvBndrName (ifTyConBinderTyVar tcb)
266
267 ifTyVarsOfType :: IfaceType -> UniqSet IfLclName
268 ifTyVarsOfType ty
269 = case ty of
270 IfaceTyVar v -> unitUniqSet v
271 IfaceAppTy fun arg
272 -> ifTyVarsOfType fun `unionUniqSets` ifTyVarsOfType arg
273 IfaceFunTy arg res
274 -> ifTyVarsOfType arg `unionUniqSets` ifTyVarsOfType res
275 IfaceDFunTy arg res
276 -> ifTyVarsOfType arg `unionUniqSets` ifTyVarsOfType res
277 IfaceForAllTy bndr ty
278 -> let (free, bound) = ifTyVarsOfForAllBndr bndr in
279 delListFromUniqSet (ifTyVarsOfType ty) bound `unionUniqSets` free
280 IfaceTyConApp _ args -> ifTyVarsOfArgs args
281 IfaceLitTy _ -> emptyUniqSet
282 IfaceCastTy ty co
283 -> ifTyVarsOfType ty `unionUniqSets` ifTyVarsOfCoercion co
284 IfaceCoercionTy co -> ifTyVarsOfCoercion co
285 IfaceTupleTy _ _ args -> ifTyVarsOfArgs args
286
287 ifTyVarsOfForAllBndr :: IfaceForAllBndr
288 -> ( UniqSet IfLclName -- names used free in the binder
289 , [IfLclName] ) -- names bound by this binder
290 ifTyVarsOfForAllBndr (TvBndr (name, kind) _) = (ifTyVarsOfType kind, [name])
291
292 ifTyVarsOfArgs :: IfaceTcArgs -> UniqSet IfLclName
293 ifTyVarsOfArgs args = argv emptyUniqSet args
294 where
295 argv vs (ITC_Vis t ts) = argv (vs `unionUniqSets` (ifTyVarsOfType t)) ts
296 argv vs (ITC_Invis k ks) = argv (vs `unionUniqSets` (ifTyVarsOfType k)) ks
297 argv vs ITC_Nil = vs
298
299 ifTyVarsOfCoercion :: IfaceCoercion -> UniqSet IfLclName
300 ifTyVarsOfCoercion = go
301 where
302 go (IfaceReflCo _ ty) = ifTyVarsOfType ty
303 go (IfaceFunCo _ c1 c2) = go c1 `unionUniqSets` go c2
304 go (IfaceTyConAppCo _ _ cos) = ifTyVarsOfCoercions cos
305 go (IfaceAppCo c1 c2) = go c1 `unionUniqSets` go c2
306 go (IfaceForAllCo (bound, _) kind_co co)
307 = go co `delOneFromUniqSet` bound `unionUniqSets` go kind_co
308 go (IfaceCoVarCo cv) = unitUniqSet cv
309 go (IfaceAxiomInstCo _ _ cos) = ifTyVarsOfCoercions cos
310 go (IfaceUnivCo p _ ty1 ty2) = go_prov p `unionUniqSets`
311 ifTyVarsOfType ty1 `unionUniqSets`
312 ifTyVarsOfType ty2
313 go (IfaceSymCo co) = go co
314 go (IfaceTransCo c1 c2) = go c1 `unionUniqSets` go c2
315 go (IfaceNthCo _ co) = go co
316 go (IfaceLRCo _ co) = go co
317 go (IfaceInstCo c1 c2) = go c1 `unionUniqSets` go c2
318 go (IfaceCoherenceCo c1 c2) = go c1 `unionUniqSets` go c2
319 go (IfaceKindCo co) = go co
320 go (IfaceSubCo co) = go co
321 go (IfaceAxiomRuleCo rule cos)
322 = unionManyUniqSets
323 [ unitUniqSet rule
324 , ifTyVarsOfCoercions cos ]
325
326 go_prov IfaceUnsafeCoerceProv = emptyUniqSet
327 go_prov (IfacePhantomProv co) = go co
328 go_prov (IfaceProofIrrelProv co) = go co
329 go_prov (IfacePluginProv _) = emptyUniqSet
330
331 ifTyVarsOfCoercions :: [IfaceCoercion] -> UniqSet IfLclName
332 ifTyVarsOfCoercions = foldr (unionUniqSets . ifTyVarsOfCoercion) emptyUniqSet
333
334 {-
335 Substitutions on IfaceType. This is only used during pretty-printing to construct
336 the result type of a GADT, and does not deal with binders (eg IfaceForAll), so
337 it doesn't need fancy capture stuff.
338 -}
339
340 type IfaceTySubst = FastStringEnv IfaceType
341
342 mkIfaceTySubst :: [IfaceTvBndr] -> [IfaceType] -> IfaceTySubst
343 mkIfaceTySubst tvs tys = mkFsEnv $ zipWithEqual "mkIfaceTySubst" (\(fs,_) ty -> (fs,ty)) tvs tys
344
345 substIfaceType :: IfaceTySubst -> IfaceType -> IfaceType
346 substIfaceType env ty
347 = go ty
348 where
349 go (IfaceTyVar tv) = substIfaceTyVar env tv
350 go (IfaceAppTy t1 t2) = IfaceAppTy (go t1) (go t2)
351 go (IfaceFunTy t1 t2) = IfaceFunTy (go t1) (go t2)
352 go (IfaceDFunTy t1 t2) = IfaceDFunTy (go t1) (go t2)
353 go ty@(IfaceLitTy {}) = ty
354 go (IfaceTyConApp tc tys) = IfaceTyConApp tc (substIfaceTcArgs env tys)
355 go (IfaceTupleTy s i tys) = IfaceTupleTy s i (substIfaceTcArgs env tys)
356 go (IfaceForAllTy {}) = pprPanic "substIfaceType" (ppr ty)
357 go (IfaceCastTy ty co) = IfaceCastTy (go ty) (go_co co)
358 go (IfaceCoercionTy co) = IfaceCoercionTy (go_co co)
359
360 go_co (IfaceReflCo r ty) = IfaceReflCo r (go ty)
361 go_co (IfaceFunCo r c1 c2) = IfaceFunCo r (go_co c1) (go_co c2)
362 go_co (IfaceTyConAppCo r tc cos) = IfaceTyConAppCo r tc (go_cos cos)
363 go_co (IfaceAppCo c1 c2) = IfaceAppCo (go_co c1) (go_co c2)
364 go_co (IfaceForAllCo {}) = pprPanic "substIfaceCoercion" (ppr ty)
365 go_co (IfaceCoVarCo cv) = IfaceCoVarCo cv
366 go_co (IfaceAxiomInstCo a i cos) = IfaceAxiomInstCo a i (go_cos cos)
367 go_co (IfaceUnivCo prov r t1 t2) = IfaceUnivCo (go_prov prov) r (go t1) (go t2)
368 go_co (IfaceSymCo co) = IfaceSymCo (go_co co)
369 go_co (IfaceTransCo co1 co2) = IfaceTransCo (go_co co1) (go_co co2)
370 go_co (IfaceNthCo n co) = IfaceNthCo n (go_co co)
371 go_co (IfaceLRCo lr co) = IfaceLRCo lr (go_co co)
372 go_co (IfaceInstCo c1 c2) = IfaceInstCo (go_co c1) (go_co c2)
373 go_co (IfaceCoherenceCo c1 c2) = IfaceCoherenceCo (go_co c1) (go_co c2)
374 go_co (IfaceKindCo co) = IfaceKindCo (go_co co)
375 go_co (IfaceSubCo co) = IfaceSubCo (go_co co)
376 go_co (IfaceAxiomRuleCo n cos) = IfaceAxiomRuleCo n (go_cos cos)
377
378 go_cos = map go_co
379
380 go_prov IfaceUnsafeCoerceProv = IfaceUnsafeCoerceProv
381 go_prov (IfacePhantomProv co) = IfacePhantomProv (go_co co)
382 go_prov (IfaceProofIrrelProv co) = IfaceProofIrrelProv (go_co co)
383 go_prov (IfacePluginProv str) = IfacePluginProv str
384
385 substIfaceTcArgs :: IfaceTySubst -> IfaceTcArgs -> IfaceTcArgs
386 substIfaceTcArgs env args
387 = go args
388 where
389 go ITC_Nil = ITC_Nil
390 go (ITC_Vis ty tys) = ITC_Vis (substIfaceType env ty) (go tys)
391 go (ITC_Invis ty tys) = ITC_Invis (substIfaceType env ty) (go tys)
392
393 substIfaceTyVar :: IfaceTySubst -> IfLclName -> IfaceType
394 substIfaceTyVar env tv
395 | Just ty <- lookupFsEnv env tv = ty
396 | otherwise = IfaceTyVar tv
397
398 {-
399 ************************************************************************
400 * *
401 Equality over IfaceTypes
402 * *
403 ************************************************************************
404
405 Note [No kind check in ifaces]
406 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
407 We check iface types for equality only when checking the consistency
408 between two user-written signatures. In these cases, there is no possibility
409 for a kind mismatch. So we omit the kind check (which would be impossible to
410 write, anyway.)
411
412 -}
413
414 -- Like an RnEnv2, but mapping from FastString to deBruijn index
415 -- DeBruijn; see eqTypeX
416 type BoundVar = Int
417 data IfRnEnv2
418 = IRV2 { ifenvL :: UniqFM BoundVar -- from FastString
419 , ifenvR :: UniqFM BoundVar
420 , ifenv_next :: BoundVar
421 }
422
423 emptyIfRnEnv2 :: IfRnEnv2
424 emptyIfRnEnv2 = IRV2 { ifenvL = emptyUFM
425 , ifenvR = emptyUFM
426 , ifenv_next = 0 }
427
428 rnIfOccL :: IfRnEnv2 -> IfLclName -> Maybe BoundVar
429 rnIfOccL env = lookupUFM (ifenvL env)
430
431 rnIfOccR :: IfRnEnv2 -> IfLclName -> Maybe BoundVar
432 rnIfOccR env = lookupUFM (ifenvR env)
433
434 extendIfRnEnv2 :: IfRnEnv2 -> IfLclName -> IfLclName -> IfRnEnv2
435 extendIfRnEnv2 IRV2 { ifenvL = lenv
436 , ifenvR = renv
437 , ifenv_next = n } tv1 tv2
438 = IRV2 { ifenvL = addToUFM lenv tv1 n
439 , ifenvR = addToUFM renv tv2 n
440 , ifenv_next = n + 1
441 }
442
443 -- See Note [No kind check in ifaces]
444 eqIfaceType :: IfRnEnv2 -> IfaceType -> IfaceType -> Bool
445 eqIfaceType env (IfaceTyVar tv1) (IfaceTyVar tv2) =
446 case (rnIfOccL env tv1, rnIfOccR env tv2) of
447 (Just v1, Just v2) -> v1 == v2
448 (Nothing, Nothing) -> tv1 == tv2
449 _ -> False
450 eqIfaceType _ (IfaceLitTy l1) (IfaceLitTy l2) = l1 == l2
451 eqIfaceType env (IfaceAppTy t11 t12) (IfaceAppTy t21 t22)
452 = eqIfaceType env t11 t21 && eqIfaceType env t12 t22
453 eqIfaceType env (IfaceFunTy t11 t12) (IfaceFunTy t21 t22)
454 = eqIfaceType env t11 t21 && eqIfaceType env t12 t22
455 eqIfaceType env (IfaceDFunTy t11 t12) (IfaceDFunTy t21 t22)
456 = eqIfaceType env t11 t21 && eqIfaceType env t12 t22
457 eqIfaceType env (IfaceForAllTy bndr1 t1) (IfaceForAllTy bndr2 t2)
458 = eqIfaceForAllBndr env bndr1 bndr2 (\env' -> eqIfaceType env' t1 t2)
459 eqIfaceType env (IfaceTyConApp tc1 tys1) (IfaceTyConApp tc2 tys2)
460 = tc1 == tc2 && eqIfaceTcArgs env tys1 tys2
461 eqIfaceType env (IfaceTupleTy s1 tc1 tys1) (IfaceTupleTy s2 tc2 tys2)
462 = s1 == s2 && tc1 == tc2 && eqIfaceTcArgs env tys1 tys2
463 eqIfaceType env (IfaceCastTy t1 _) (IfaceCastTy t2 _)
464 = eqIfaceType env t1 t2
465 eqIfaceType _ (IfaceCoercionTy {}) (IfaceCoercionTy {})
466 = True
467 eqIfaceType _ _ _ = False
468
469 eqIfaceTypes :: IfRnEnv2 -> [IfaceType] -> [IfaceType] -> Bool
470 eqIfaceTypes env tys1 tys2 = and (zipWith (eqIfaceType env) tys1 tys2)
471
472 eqIfaceForAllBndr :: IfRnEnv2 -> IfaceForAllBndr -> IfaceForAllBndr
473 -> (IfRnEnv2 -> Bool) -- continuation
474 -> Bool
475 eqIfaceForAllBndr env (TvBndr (tv1, k1) vis1) (TvBndr (tv2, k2) vis2) k
476 = eqIfaceType env k1 k2 && vis1 == vis2 &&
477 k (extendIfRnEnv2 env tv1 tv2)
478
479 eqIfaceTcArgs :: IfRnEnv2 -> IfaceTcArgs -> IfaceTcArgs -> Bool
480 eqIfaceTcArgs _ ITC_Nil ITC_Nil = True
481 eqIfaceTcArgs env (ITC_Vis ty1 tys1) (ITC_Vis ty2 tys2)
482 = eqIfaceType env ty1 ty2 && eqIfaceTcArgs env tys1 tys2
483 eqIfaceTcArgs env (ITC_Invis ty1 tys1) (ITC_Invis ty2 tys2)
484 = eqIfaceType env ty1 ty2 && eqIfaceTcArgs env tys1 tys2
485 eqIfaceTcArgs _ _ _ = False
486
487 -- | Similar to 'eqTyVarBndrs', checks that tyvar lists
488 -- are the same length and have matching kinds; if so, extend the
489 -- 'IfRnEnv2'. Returns 'Nothing' if they don't match.
490 eqIfaceTvBndrs :: IfRnEnv2 -> [IfaceTvBndr] -> [IfaceTvBndr] -> Maybe IfRnEnv2
491 eqIfaceTvBndrs env [] [] = Just env
492 eqIfaceTvBndrs env ((tv1, k1):tvs1) ((tv2, k2):tvs2)
493 | eqIfaceType env k1 k2
494 = eqIfaceTvBndrs (extendIfRnEnv2 env tv1 tv2) tvs1 tvs2
495 eqIfaceTvBndrs _ _ _ = Nothing
496
497 {-
498 ************************************************************************
499 * *
500 Functions over IFaceTcArgs
501 * *
502 ************************************************************************
503 -}
504
505 stripInvisArgs :: DynFlags -> IfaceTcArgs -> IfaceTcArgs
506 stripInvisArgs dflags tys
507 | gopt Opt_PrintExplicitKinds dflags = tys
508 | otherwise = suppress_invis tys
509 where
510 suppress_invis c
511 = case c of
512 ITC_Invis _ ts -> suppress_invis ts
513 _ -> c
514
515 toIfaceTcArgs :: TyCon -> [Type] -> IfaceTcArgs
516 -- See Note [Suppressing invisible arguments]
517 toIfaceTcArgs tc ty_args
518 = go (mkEmptyTCvSubst in_scope) (tyConKind tc) ty_args
519 where
520 in_scope = mkInScopeSet (tyCoVarsOfTypes ty_args)
521
522 go _ _ [] = ITC_Nil
523 go env ty ts
524 | Just ty' <- coreView ty
525 = go env ty' ts
526 go env (ForAllTy (TvBndr tv vis) res) (t:ts)
527 | isVisibleArgFlag vis = ITC_Vis t' ts'
528 | otherwise = ITC_Invis t' ts'
529 where
530 t' = toIfaceType t
531 ts' = go (extendTvSubst env tv t) res ts
532
533 go env (FunTy _ res) (t:ts) -- No type-class args in tycon apps
534 = ITC_Vis (toIfaceType t) (go env res ts)
535
536 go env (TyVarTy tv) ts
537 | Just ki <- lookupTyVar env tv = go env ki ts
538 go env kind (t:ts) = WARN( True, ppr tc $$ ppr (tyConKind tc) $$ ppr ty_args )
539 ITC_Vis (toIfaceType t) (go env kind ts) -- Ill-kinded
540
541 tcArgsIfaceTypes :: IfaceTcArgs -> [IfaceType]
542 tcArgsIfaceTypes ITC_Nil = []
543 tcArgsIfaceTypes (ITC_Invis t ts) = t : tcArgsIfaceTypes ts
544 tcArgsIfaceTypes (ITC_Vis t ts) = t : tcArgsIfaceTypes ts
545
546 {-
547 Note [Suppressing invisible arguments]
548 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
549 We use the IfaceTcArgs to specify which of the arguments to a type
550 constructor should be displayed when pretty-printing, under
551 the control of -fprint-explicit-kinds.
552 See also Type.filterOutInvisibleTypes.
553 For example, given
554 T :: forall k. (k->*) -> k -> * -- Ordinary kind polymorphism
555 'Just :: forall k. k -> 'Maybe k -- Promoted
556 we want
557 T * Tree Int prints as T Tree Int
558 'Just * prints as Just *
559
560
561 ************************************************************************
562 * *
563 Pretty-printing
564 * *
565 ************************************************************************
566 -}
567
568 pprIfaceInfixApp :: (TyPrec -> a -> SDoc) -> TyPrec -> SDoc -> a -> a -> SDoc
569 pprIfaceInfixApp pp p pp_tc ty1 ty2
570 = maybeParen p FunPrec $
571 sep [pp FunPrec ty1, pprInfixVar True pp_tc <+> pp FunPrec ty2]
572
573 pprIfacePrefixApp :: TyPrec -> SDoc -> [SDoc] -> SDoc
574 pprIfacePrefixApp p pp_fun pp_tys
575 | null pp_tys = pp_fun
576 | otherwise = maybeParen p TyConPrec $
577 hang pp_fun 2 (sep pp_tys)
578
579 -- ----------------------------- Printing binders ------------------------------------
580
581 instance Outputable IfaceBndr where
582 ppr (IfaceIdBndr bndr) = pprIfaceIdBndr bndr
583 ppr (IfaceTvBndr bndr) = char '@' <+> pprIfaceTvBndr bndr
584
585 pprIfaceBndrs :: [IfaceBndr] -> SDoc
586 pprIfaceBndrs bs = sep (map ppr bs)
587
588 pprIfaceLamBndr :: IfaceLamBndr -> SDoc
589 pprIfaceLamBndr (b, IfaceNoOneShot) = ppr b
590 pprIfaceLamBndr (b, IfaceOneShot) = ppr b <> text "[OneShot]"
591
592 pprIfaceIdBndr :: (IfLclName, IfaceType) -> SDoc
593 pprIfaceIdBndr (name, ty) = parens (ppr name <+> dcolon <+> ppr ty)
594
595 pprIfaceTvBndr :: IfaceTvBndr -> SDoc
596 pprIfaceTvBndr (tv, ki)
597 | isIfaceLiftedTypeKind ki = ppr tv
598 | otherwise = parens (ppr tv <+> dcolon <+> ppr ki)
599
600 pprIfaceTyConBinders :: [IfaceTyConBinder] -> SDoc
601 pprIfaceTyConBinders = sep . map go
602 where
603 go tcb = pprIfaceTvBndr (ifTyConBinderTyVar tcb)
604
605 instance Binary IfaceBndr where
606 put_ bh (IfaceIdBndr aa) = do
607 putByte bh 0
608 put_ bh aa
609 put_ bh (IfaceTvBndr ab) = do
610 putByte bh 1
611 put_ bh ab
612 get bh = do
613 h <- getByte bh
614 case h of
615 0 -> do aa <- get bh
616 return (IfaceIdBndr aa)
617 _ -> do ab <- get bh
618 return (IfaceTvBndr ab)
619
620 instance Binary IfaceOneShot where
621 put_ bh IfaceNoOneShot = do
622 putByte bh 0
623 put_ bh IfaceOneShot = do
624 putByte bh 1
625 get bh = do
626 h <- getByte bh
627 case h of
628 0 -> do return IfaceNoOneShot
629 _ -> do return IfaceOneShot
630
631 -- ----------------------------- Printing IfaceType ------------------------------------
632
633 ---------------------------------
634 instance Outputable IfaceType where
635 ppr ty = pprIfaceType ty
636
637 pprIfaceType, pprParendIfaceType ::IfaceType -> SDoc
638 pprIfaceType = ppr_ty TopPrec
639 pprParendIfaceType = ppr_ty TyConPrec
640
641 ppr_ty :: TyPrec -> IfaceType -> SDoc
642 ppr_ty _ (IfaceTyVar tyvar) = ppr tyvar
643 ppr_ty ctxt_prec (IfaceTyConApp tc tys) = sdocWithDynFlags (pprTyTcApp ctxt_prec tc tys)
644 ppr_ty _ (IfaceTupleTy s i tys) = pprTuple s i tys
645 ppr_ty _ (IfaceLitTy n) = ppr_tylit n
646 -- Function types
647 ppr_ty ctxt_prec (IfaceFunTy ty1 ty2)
648 = -- We don't want to lose synonyms, so we mustn't use splitFunTys here.
649 maybeParen ctxt_prec FunPrec $
650 sep [ppr_ty FunPrec ty1, sep (ppr_fun_tail ty2)]
651 where
652 ppr_fun_tail (IfaceFunTy ty1 ty2)
653 = (arrow <+> ppr_ty FunPrec ty1) : ppr_fun_tail ty2
654 ppr_fun_tail other_ty
655 = [arrow <+> pprIfaceType other_ty]
656
657 ppr_ty ctxt_prec (IfaceAppTy ty1 ty2)
658 = maybeParen ctxt_prec TyConPrec $
659 ppr_ty FunPrec ty1 <+> pprParendIfaceType ty2
660
661 ppr_ty ctxt_prec (IfaceCastTy ty co)
662 = maybeParen ctxt_prec FunPrec $
663 sep [ppr_ty FunPrec ty, text "`cast`", ppr_co FunPrec co]
664
665 ppr_ty ctxt_prec (IfaceCoercionTy co)
666 = ppr_co ctxt_prec co
667
668 ppr_ty ctxt_prec ty
669 = maybeParen ctxt_prec FunPrec (ppr_iface_sigma_type True ty)
670
671 instance Outputable IfaceTcArgs where
672 ppr tca = pprIfaceTcArgs tca
673
674 pprIfaceTcArgs, pprParendIfaceTcArgs :: IfaceTcArgs -> SDoc
675 pprIfaceTcArgs = ppr_tc_args TopPrec
676 pprParendIfaceTcArgs = ppr_tc_args TyConPrec
677
678 ppr_tc_args :: TyPrec -> IfaceTcArgs -> SDoc
679 ppr_tc_args ctx_prec args
680 = let pprTys t ts = ppr_ty ctx_prec t <+> ppr_tc_args ctx_prec ts
681 in case args of
682 ITC_Nil -> empty
683 ITC_Vis t ts -> pprTys t ts
684 ITC_Invis t ts -> pprTys t ts
685
686 -------------------
687 ppr_iface_sigma_type :: Bool -> IfaceType -> SDoc
688 ppr_iface_sigma_type show_foralls_unconditionally ty
689 = ppr_iface_forall_part show_foralls_unconditionally tvs theta (ppr tau)
690 where
691 (tvs, theta, tau) = splitIfaceSigmaTy ty
692
693 -------------------
694 pprIfaceForAllPart :: [IfaceForAllBndr] -> [IfaceType] -> SDoc -> SDoc
695 pprIfaceForAllPart tvs ctxt sdoc = ppr_iface_forall_part False tvs ctxt sdoc
696
697 pprIfaceForAllCoPart :: [(IfLclName, IfaceCoercion)] -> SDoc -> SDoc
698 pprIfaceForAllCoPart tvs sdoc = sep [ pprIfaceForAllCo tvs
699 , sdoc ]
700
701 ppr_iface_forall_part :: Outputable a
702 => Bool -> [IfaceForAllBndr] -> [a] -> SDoc -> SDoc
703 ppr_iface_forall_part show_foralls_unconditionally tvs ctxt sdoc
704 = sep [ if show_foralls_unconditionally
705 then pprIfaceForAll tvs
706 else pprUserIfaceForAll tvs
707 , pprIfaceContextArr ctxt
708 , sdoc]
709
710 -- | Render the "forall ... ." or "forall ... ->" bit of a type.
711 pprIfaceForAll :: [IfaceForAllBndr] -> SDoc
712 pprIfaceForAll [] = empty
713 pprIfaceForAll bndrs@(TvBndr _ vis : _)
714 = add_separator (text "forall" <+> doc) <+> pprIfaceForAll bndrs'
715 where
716 (bndrs', doc) = ppr_itv_bndrs bndrs vis
717
718 add_separator stuff = case vis of
719 Required -> stuff <+> arrow
720 _inv -> stuff <> dot
721
722
723 -- | Render the ... in @(forall ... .)@ or @(forall ... ->)@.
724 -- Returns both the list of not-yet-rendered binders and the doc.
725 -- No anonymous binders here!
726 ppr_itv_bndrs :: [IfaceForAllBndr]
727 -> ArgFlag -- ^ visibility of the first binder in the list
728 -> ([IfaceForAllBndr], SDoc)
729 ppr_itv_bndrs all_bndrs@(bndr@(TvBndr _ vis) : bndrs) vis1
730 | vis `sameVis` vis1 = let (bndrs', doc) = ppr_itv_bndrs bndrs vis1 in
731 (bndrs', pprIfaceForAllBndr bndr <+> doc)
732 | otherwise = (all_bndrs, empty)
733 ppr_itv_bndrs [] _ = ([], empty)
734
735 pprIfaceForAllCo :: [(IfLclName, IfaceCoercion)] -> SDoc
736 pprIfaceForAllCo [] = empty
737 pprIfaceForAllCo tvs = text "forall" <+> pprIfaceForAllCoBndrs tvs <> dot
738
739 pprIfaceForAllCoBndrs :: [(IfLclName, IfaceCoercion)] -> SDoc
740 pprIfaceForAllCoBndrs bndrs = hsep $ map pprIfaceForAllCoBndr bndrs
741
742 pprIfaceForAllBndr :: IfaceForAllBndr -> SDoc
743 pprIfaceForAllBndr (TvBndr tv Inferred) = sdocWithDynFlags $ \dflags ->
744 if gopt Opt_PrintExplicitForalls dflags
745 then braces $ pprIfaceTvBndr tv
746 else pprIfaceTvBndr tv
747 pprIfaceForAllBndr (TvBndr tv _) = pprIfaceTvBndr tv
748
749 pprIfaceForAllCoBndr :: (IfLclName, IfaceCoercion) -> SDoc
750 pprIfaceForAllCoBndr (tv, kind_co)
751 = parens (ppr tv <+> dcolon <+> pprIfaceCoercion kind_co)
752
753 pprIfaceSigmaType :: IfaceType -> SDoc
754 pprIfaceSigmaType ty = ppr_iface_sigma_type False ty
755
756 pprUserIfaceForAll :: [IfaceForAllBndr] -> SDoc
757 pprUserIfaceForAll tvs
758 = sdocWithDynFlags $ \dflags ->
759 ppWhen (any tv_has_kind_var tvs || gopt Opt_PrintExplicitForalls dflags) $
760 pprIfaceForAll tvs
761 where
762 tv_has_kind_var bndr
763 = not (isEmptyUniqSet (fst (ifTyVarsOfForAllBndr bndr)))
764
765 -------------------
766
767 -- See equivalent function in TyCoRep.hs
768 pprIfaceTyList :: TyPrec -> IfaceType -> IfaceType -> SDoc
769 -- Given a type-level list (t1 ': t2), see if we can print
770 -- it in list notation [t1, ...].
771 -- Precondition: Opt_PrintExplicitKinds is off
772 pprIfaceTyList ctxt_prec ty1 ty2
773 = case gather ty2 of
774 (arg_tys, Nothing)
775 -> char '\'' <> brackets (fsep (punctuate comma
776 (map (ppr_ty TopPrec) (ty1:arg_tys))))
777 (arg_tys, Just tl)
778 -> maybeParen ctxt_prec FunPrec $ hang (ppr_ty FunPrec ty1)
779 2 (fsep [ colon <+> ppr_ty FunPrec ty | ty <- arg_tys ++ [tl]])
780 where
781 gather :: IfaceType -> ([IfaceType], Maybe IfaceType)
782 -- (gather ty) = (tys, Nothing) means ty is a list [t1, .., tn]
783 -- = (tys, Just tl) means ty is of form t1:t2:...tn:tl
784 gather (IfaceTyConApp tc tys)
785 | tcname == consDataConName
786 , (ITC_Invis _ (ITC_Vis ty1 (ITC_Vis ty2 ITC_Nil))) <- tys
787 , (args, tl) <- gather ty2
788 = (ty1:args, tl)
789 | tcname == nilDataConName
790 = ([], Nothing)
791 where tcname = ifaceTyConName tc
792 gather ty = ([], Just ty)
793
794 pprIfaceTypeApp :: IfaceTyCon -> IfaceTcArgs -> SDoc
795 pprIfaceTypeApp tc args = sdocWithDynFlags (pprTyTcApp TopPrec tc args)
796
797 pprTyTcApp :: TyPrec -> IfaceTyCon -> IfaceTcArgs -> DynFlags -> SDoc
798 pprTyTcApp ctxt_prec tc tys dflags
799 | ifaceTyConName tc `hasKey` ipClassKey
800 , ITC_Vis (IfaceLitTy (IfaceStrTyLit n)) (ITC_Vis ty ITC_Nil) <- tys
801 = char '?' <> ftext n <> text "::" <> ppr_ty TopPrec ty
802
803 | ifaceTyConName tc == consDataConName
804 , not (gopt Opt_PrintExplicitKinds dflags)
805 , ITC_Invis _ (ITC_Vis ty1 (ITC_Vis ty2 ITC_Nil)) <- tys
806 = pprIfaceTyList ctxt_prec ty1 ty2
807
808 | ifaceTyConName tc == tYPETyConName
809 , ITC_Vis (IfaceTyConApp ptr_rep ITC_Nil) ITC_Nil <- tys
810 , ifaceTyConName ptr_rep `hasKey` ptrRepLiftedDataConKey
811 = char '*'
812
813 | ifaceTyConName tc == tYPETyConName
814 , ITC_Vis (IfaceTyConApp ptr_rep ITC_Nil) ITC_Nil <- tys
815 , ifaceTyConName ptr_rep `hasKey` ptrRepUnliftedDataConKey
816 = char '#'
817
818 | otherwise
819 = ppr_iface_tc_app ppr_ty ctxt_prec tc tys_wo_kinds
820 where
821 tys_wo_kinds = tcArgsIfaceTypes $ stripInvisArgs dflags tys
822
823 pprIfaceCoTcApp :: TyPrec -> IfaceTyCon -> [IfaceCoercion] -> SDoc
824 pprIfaceCoTcApp ctxt_prec tc tys = ppr_iface_tc_app ppr_co ctxt_prec tc tys
825
826 ppr_iface_tc_app :: (TyPrec -> a -> SDoc) -> TyPrec -> IfaceTyCon -> [a] -> SDoc
827 ppr_iface_tc_app pp _ tc [ty]
828 | n == listTyConName = pprPromotionQuote tc <> brackets (pp TopPrec ty)
829 | n == parrTyConName = pprPromotionQuote tc <> paBrackets (pp TopPrec ty)
830 where
831 n = ifaceTyConName tc
832
833 ppr_iface_tc_app pp ctxt_prec tc tys
834 | not (isSymOcc (nameOccName tc_name))
835 = pprIfacePrefixApp ctxt_prec (ppr tc) (map (pp TyConPrec) tys)
836
837 | [ty1,ty2] <- tys -- Infix, two arguments;
838 -- we know nothing of precedence though
839 = pprIfaceInfixApp pp ctxt_prec (ppr tc) ty1 ty2
840
841 | tc_name == starKindTyConName || tc_name == unliftedTypeKindTyConName
842 || tc_name == unicodeStarKindTyConName
843 = ppr tc -- Do not wrap *, # in parens
844
845 | otherwise
846 = pprIfacePrefixApp ctxt_prec (parens (ppr tc)) (map (pp TyConPrec) tys)
847 where
848 tc_name = ifaceTyConName tc
849
850 pprTuple :: TupleSort -> IfaceTyConInfo -> IfaceTcArgs -> SDoc
851 pprTuple sort info args
852 = -- drop the RuntimeRep vars.
853 -- See Note [Unboxed tuple RuntimeRep vars] in TyCon
854 let tys = tcArgsIfaceTypes args
855 args' = case sort of
856 UnboxedTuple -> drop (length tys `div` 2) tys
857 _ -> tys
858 in
859 pprPromotionQuoteI info <>
860 tupleParens sort (pprWithCommas pprIfaceType args')
861
862 ppr_tylit :: IfaceTyLit -> SDoc
863 ppr_tylit (IfaceNumTyLit n) = integer n
864 ppr_tylit (IfaceStrTyLit n) = text (show n)
865
866 pprIfaceCoercion, pprParendIfaceCoercion :: IfaceCoercion -> SDoc
867 pprIfaceCoercion = ppr_co TopPrec
868 pprParendIfaceCoercion = ppr_co TyConPrec
869
870 ppr_co :: TyPrec -> IfaceCoercion -> SDoc
871 ppr_co _ (IfaceReflCo r ty) = angleBrackets (ppr ty) <> ppr_role r
872 ppr_co ctxt_prec (IfaceFunCo r co1 co2)
873 = maybeParen ctxt_prec FunPrec $
874 sep (ppr_co FunPrec co1 : ppr_fun_tail co2)
875 where
876 ppr_fun_tail (IfaceFunCo r co1 co2)
877 = (arrow <> ppr_role r <+> ppr_co FunPrec co1) : ppr_fun_tail co2
878 ppr_fun_tail other_co
879 = [arrow <> ppr_role r <+> pprIfaceCoercion other_co]
880
881 ppr_co _ (IfaceTyConAppCo r tc cos)
882 = parens (pprIfaceCoTcApp TopPrec tc cos) <> ppr_role r
883 ppr_co ctxt_prec (IfaceAppCo co1 co2)
884 = maybeParen ctxt_prec TyConPrec $
885 ppr_co FunPrec co1 <+> pprParendIfaceCoercion co2
886 ppr_co ctxt_prec co@(IfaceForAllCo {})
887 = maybeParen ctxt_prec FunPrec (pprIfaceForAllCoPart tvs (pprIfaceCoercion inner_co))
888 where
889 (tvs, inner_co) = split_co co
890
891 split_co (IfaceForAllCo (name, _) kind_co co')
892 = let (tvs, co'') = split_co co' in ((name,kind_co):tvs,co'')
893 split_co co' = ([], co')
894
895 ppr_co _ (IfaceCoVarCo covar) = ppr covar
896
897 ppr_co ctxt_prec (IfaceUnivCo IfaceUnsafeCoerceProv r ty1 ty2)
898 = maybeParen ctxt_prec TyConPrec $
899 text "UnsafeCo" <+> ppr r <+>
900 pprParendIfaceType ty1 <+> pprParendIfaceType ty2
901
902 ppr_co _ (IfaceUnivCo _ _ ty1 ty2)
903 = angleBrackets ( ppr ty1 <> comma <+> ppr ty2 )
904
905 ppr_co ctxt_prec (IfaceInstCo co ty)
906 = maybeParen ctxt_prec TyConPrec $
907 text "Inst" <+> pprParendIfaceCoercion co
908 <+> pprParendIfaceCoercion ty
909
910 ppr_co ctxt_prec (IfaceAxiomRuleCo tc cos)
911 = maybeParen ctxt_prec TyConPrec $ ppr tc <+> parens (interpp'SP cos)
912
913 ppr_co ctxt_prec co
914 = ppr_special_co ctxt_prec doc cos
915 where (doc, cos) = case co of
916 { IfaceAxiomInstCo n i cos -> (ppr n <> brackets (ppr i), cos)
917 ; IfaceSymCo co -> (text "Sym", [co])
918 ; IfaceTransCo co1 co2 -> (text "Trans", [co1,co2])
919 ; IfaceNthCo d co -> (text "Nth:" <> int d,
920 [co])
921 ; IfaceLRCo lr co -> (ppr lr, [co])
922 ; IfaceSubCo co -> (text "Sub", [co])
923 ; _ -> panic "pprIfaceCo" }
924
925 ppr_special_co :: TyPrec -> SDoc -> [IfaceCoercion] -> SDoc
926 ppr_special_co ctxt_prec doc cos
927 = maybeParen ctxt_prec TyConPrec
928 (sep [doc, nest 4 (sep (map pprParendIfaceCoercion cos))])
929
930 ppr_role :: Role -> SDoc
931 ppr_role r = underscore <> pp_role
932 where pp_role = case r of
933 Nominal -> char 'N'
934 Representational -> char 'R'
935 Phantom -> char 'P'
936
937 -------------------
938 instance Outputable IfaceTyCon where
939 ppr tc = pprPromotionQuote tc <> ppr (ifaceTyConName tc)
940
941 pprPromotionQuote :: IfaceTyCon -> SDoc
942 pprPromotionQuote tc = pprPromotionQuoteI (ifaceTyConInfo tc)
943
944 pprPromotionQuoteI :: IfaceTyConInfo -> SDoc
945 pprPromotionQuoteI NoIfaceTyConInfo = empty
946 pprPromotionQuoteI IfacePromotedDataCon = char '\''
947
948 instance Outputable IfaceCoercion where
949 ppr = pprIfaceCoercion
950
951 instance Binary IfaceTyCon where
952 put_ bh (IfaceTyCon n i) = put_ bh n >> put_ bh i
953
954 get bh = do n <- get bh
955 i <- get bh
956 return (IfaceTyCon n i)
957
958 instance Binary IfaceTyConInfo where
959 put_ bh NoIfaceTyConInfo = putByte bh 0
960 put_ bh IfacePromotedDataCon = putByte bh 1
961
962 get bh =
963 do i <- getByte bh
964 case i of
965 0 -> return NoIfaceTyConInfo
966 _ -> return IfacePromotedDataCon
967
968 instance Outputable IfaceTyLit where
969 ppr = ppr_tylit
970
971 instance Binary IfaceTyLit where
972 put_ bh (IfaceNumTyLit n) = putByte bh 1 >> put_ bh n
973 put_ bh (IfaceStrTyLit n) = putByte bh 2 >> put_ bh n
974
975 get bh =
976 do tag <- getByte bh
977 case tag of
978 1 -> do { n <- get bh
979 ; return (IfaceNumTyLit n) }
980 2 -> do { n <- get bh
981 ; return (IfaceStrTyLit n) }
982 _ -> panic ("get IfaceTyLit " ++ show tag)
983
984 instance Binary IfaceTcArgs where
985 put_ bh tk =
986 case tk of
987 ITC_Vis t ts -> putByte bh 0 >> put_ bh t >> put_ bh ts
988 ITC_Invis t ts -> putByte bh 1 >> put_ bh t >> put_ bh ts
989 ITC_Nil -> putByte bh 2
990
991 get bh =
992 do c <- getByte bh
993 case c of
994 0 -> do
995 t <- get bh
996 ts <- get bh
997 return $! ITC_Vis t ts
998 1 -> do
999 t <- get bh
1000 ts <- get bh
1001 return $! ITC_Invis t ts
1002 2 -> return ITC_Nil
1003 _ -> panic ("get IfaceTcArgs " ++ show c)
1004
1005 -------------------
1006 pprIfaceContextArr :: Outputable a => [a] -> SDoc
1007 -- Prints "(C a, D b) =>", including the arrow
1008 pprIfaceContextArr [] = empty
1009 pprIfaceContextArr preds = pprIfaceContext preds <+> darrow
1010
1011 pprIfaceContext :: Outputable a => [a] -> SDoc
1012 pprIfaceContext [] = parens empty
1013 pprIfaceContext [pred] = ppr pred -- No parens
1014 pprIfaceContext preds = parens (fsep (punctuate comma (map ppr preds)))
1015
1016 instance Binary IfaceType where
1017 put_ bh (IfaceForAllTy aa ab) = do
1018 putByte bh 0
1019 put_ bh aa
1020 put_ bh ab
1021 put_ bh (IfaceTyVar ad) = do
1022 putByte bh 1
1023 put_ bh ad
1024 put_ bh (IfaceAppTy ae af) = do
1025 putByte bh 2
1026 put_ bh ae
1027 put_ bh af
1028 put_ bh (IfaceFunTy ag ah) = do
1029 putByte bh 3
1030 put_ bh ag
1031 put_ bh ah
1032 put_ bh (IfaceDFunTy ag ah) = do
1033 putByte bh 4
1034 put_ bh ag
1035 put_ bh ah
1036 put_ bh (IfaceTyConApp tc tys)
1037 = do { putByte bh 5; put_ bh tc; put_ bh tys }
1038 put_ bh (IfaceCastTy a b)
1039 = do { putByte bh 6; put_ bh a; put_ bh b }
1040 put_ bh (IfaceCoercionTy a)
1041 = do { putByte bh 7; put_ bh a }
1042 put_ bh (IfaceTupleTy s i tys)
1043 = do { putByte bh 8; put_ bh s; put_ bh i; put_ bh tys }
1044 put_ bh (IfaceLitTy n)
1045 = do { putByte bh 9; put_ bh n }
1046
1047 get bh = do
1048 h <- getByte bh
1049 case h of
1050 0 -> do aa <- get bh
1051 ab <- get bh
1052 return (IfaceForAllTy aa ab)
1053 1 -> do ad <- get bh
1054 return (IfaceTyVar ad)
1055 2 -> do ae <- get bh
1056 af <- get bh
1057 return (IfaceAppTy ae af)
1058 3 -> do ag <- get bh
1059 ah <- get bh
1060 return (IfaceFunTy ag ah)
1061 4 -> do ag <- get bh
1062 ah <- get bh
1063 return (IfaceDFunTy ag ah)
1064 5 -> do { tc <- get bh; tys <- get bh
1065 ; return (IfaceTyConApp tc tys) }
1066 6 -> do { a <- get bh; b <- get bh
1067 ; return (IfaceCastTy a b) }
1068 7 -> do { a <- get bh
1069 ; return (IfaceCoercionTy a) }
1070
1071 8 -> do { s <- get bh; i <- get bh; tys <- get bh
1072 ; return (IfaceTupleTy s i tys) }
1073 _ -> do n <- get bh
1074 return (IfaceLitTy n)
1075
1076 instance Binary IfaceCoercion where
1077 put_ bh (IfaceReflCo a b) = do
1078 putByte bh 1
1079 put_ bh a
1080 put_ bh b
1081 put_ bh (IfaceFunCo a b c) = do
1082 putByte bh 2
1083 put_ bh a
1084 put_ bh b
1085 put_ bh c
1086 put_ bh (IfaceTyConAppCo a b c) = do
1087 putByte bh 3
1088 put_ bh a
1089 put_ bh b
1090 put_ bh c
1091 put_ bh (IfaceAppCo a b) = do
1092 putByte bh 4
1093 put_ bh a
1094 put_ bh b
1095 put_ bh (IfaceForAllCo a b c) = do
1096 putByte bh 5
1097 put_ bh a
1098 put_ bh b
1099 put_ bh c
1100 put_ bh (IfaceCoVarCo a) = do
1101 putByte bh 6
1102 put_ bh a
1103 put_ bh (IfaceAxiomInstCo a b c) = do
1104 putByte bh 7
1105 put_ bh a
1106 put_ bh b
1107 put_ bh c
1108 put_ bh (IfaceUnivCo a b c d) = do
1109 putByte bh 8
1110 put_ bh a
1111 put_ bh b
1112 put_ bh c
1113 put_ bh d
1114 put_ bh (IfaceSymCo a) = do
1115 putByte bh 9
1116 put_ bh a
1117 put_ bh (IfaceTransCo a b) = do
1118 putByte bh 10
1119 put_ bh a
1120 put_ bh b
1121 put_ bh (IfaceNthCo a b) = do
1122 putByte bh 11
1123 put_ bh a
1124 put_ bh b
1125 put_ bh (IfaceLRCo a b) = do
1126 putByte bh 12
1127 put_ bh a
1128 put_ bh b
1129 put_ bh (IfaceInstCo a b) = do
1130 putByte bh 13
1131 put_ bh a
1132 put_ bh b
1133 put_ bh (IfaceCoherenceCo a b) = do
1134 putByte bh 14
1135 put_ bh a
1136 put_ bh b
1137 put_ bh (IfaceKindCo a) = do
1138 putByte bh 15
1139 put_ bh a
1140 put_ bh (IfaceSubCo a) = do
1141 putByte bh 16
1142 put_ bh a
1143 put_ bh (IfaceAxiomRuleCo a b) = do
1144 putByte bh 17
1145 put_ bh a
1146 put_ bh b
1147
1148 get bh = do
1149 tag <- getByte bh
1150 case tag of
1151 1 -> do a <- get bh
1152 b <- get bh
1153 return $ IfaceReflCo a b
1154 2 -> do a <- get bh
1155 b <- get bh
1156 c <- get bh
1157 return $ IfaceFunCo a b c
1158 3 -> do a <- get bh
1159 b <- get bh
1160 c <- get bh
1161 return $ IfaceTyConAppCo a b c
1162 4 -> do a <- get bh
1163 b <- get bh
1164 return $ IfaceAppCo a b
1165 5 -> do a <- get bh
1166 b <- get bh
1167 c <- get bh
1168 return $ IfaceForAllCo a b c
1169 6 -> do a <- get bh
1170 return $ IfaceCoVarCo a
1171 7 -> do a <- get bh
1172 b <- get bh
1173 c <- get bh
1174 return $ IfaceAxiomInstCo a b c
1175 8 -> do a <- get bh
1176 b <- get bh
1177 c <- get bh
1178 d <- get bh
1179 return $ IfaceUnivCo a b c d
1180 9 -> do a <- get bh
1181 return $ IfaceSymCo a
1182 10-> do a <- get bh
1183 b <- get bh
1184 return $ IfaceTransCo a b
1185 11-> do a <- get bh
1186 b <- get bh
1187 return $ IfaceNthCo a b
1188 12-> do a <- get bh
1189 b <- get bh
1190 return $ IfaceLRCo a b
1191 13-> do a <- get bh
1192 b <- get bh
1193 return $ IfaceInstCo a b
1194 14-> do a <- get bh
1195 b <- get bh
1196 return $ IfaceCoherenceCo a b
1197 15-> do a <- get bh
1198 return $ IfaceKindCo a
1199 16-> do a <- get bh
1200 return $ IfaceSubCo a
1201 17-> do a <- get bh
1202 b <- get bh
1203 return $ IfaceAxiomRuleCo a b
1204 _ -> panic ("get IfaceCoercion " ++ show tag)
1205
1206 instance Binary IfaceUnivCoProv where
1207 put_ bh IfaceUnsafeCoerceProv = putByte bh 1
1208 put_ bh (IfacePhantomProv a) = do
1209 putByte bh 2
1210 put_ bh a
1211 put_ bh (IfaceProofIrrelProv a) = do
1212 putByte bh 3
1213 put_ bh a
1214 put_ bh (IfacePluginProv a) = do
1215 putByte bh 4
1216 put_ bh a
1217
1218 get bh = do
1219 tag <- getByte bh
1220 case tag of
1221 1 -> return $ IfaceUnsafeCoerceProv
1222 2 -> do a <- get bh
1223 return $ IfacePhantomProv a
1224 3 -> do a <- get bh
1225 return $ IfaceProofIrrelProv a
1226 4 -> do a <- get bh
1227 return $ IfacePluginProv a
1228 _ -> panic ("get IfaceUnivCoProv " ++ show tag)
1229
1230
1231 instance Binary (DefMethSpec IfaceType) where
1232 put_ bh VanillaDM = putByte bh 0
1233 put_ bh (GenericDM t) = putByte bh 1 >> put_ bh t
1234 get bh = do
1235 h <- getByte bh
1236 case h of
1237 0 -> return VanillaDM
1238 _ -> do { t <- get bh; return (GenericDM t) }
1239
1240 {-
1241 ************************************************************************
1242 * *
1243 Conversion from Type to IfaceType
1244 * *
1245 ************************************************************************
1246 -}
1247
1248 ----------------
1249 toIfaceTvBndr :: TyVar -> IfaceTvBndr
1250 toIfaceTvBndr tyvar = ( occNameFS (getOccName tyvar)
1251 , toIfaceKind (tyVarKind tyvar)
1252 )
1253
1254 toIfaceIdBndr :: Id -> (IfLclName, IfaceType)
1255 toIfaceIdBndr id = (occNameFS (getOccName id), toIfaceType (idType id))
1256
1257 toIfaceTvBndrs :: [TyVar] -> [IfaceTvBndr]
1258 toIfaceTvBndrs = map toIfaceTvBndr
1259
1260 toIfaceBndr :: Var -> IfaceBndr
1261 toIfaceBndr var
1262 | isId var = IfaceIdBndr (toIfaceIdBndr var)
1263 | otherwise = IfaceTvBndr (toIfaceTvBndr var)
1264
1265 toIfaceKind :: Type -> IfaceType
1266 toIfaceKind = toIfaceType
1267
1268 ---------------------
1269 toIfaceType :: Type -> IfaceType
1270 -- Synonyms are retained in the interface type
1271 toIfaceType (TyVarTy tv) = IfaceTyVar (toIfaceTyVar tv)
1272 toIfaceType (AppTy t1 t2) = IfaceAppTy (toIfaceType t1) (toIfaceType t2)
1273 toIfaceType (LitTy n) = IfaceLitTy (toIfaceTyLit n)
1274 toIfaceType (ForAllTy b t) = IfaceForAllTy (toIfaceForAllBndr b) (toIfaceType t)
1275 toIfaceType (FunTy t1 t2)
1276 | isPredTy t1 = IfaceDFunTy (toIfaceType t1) (toIfaceType t2)
1277 | otherwise = IfaceFunTy (toIfaceType t1) (toIfaceType t2)
1278 toIfaceType (CastTy ty co) = IfaceCastTy (toIfaceType ty) (toIfaceCoercion co)
1279 toIfaceType (CoercionTy co) = IfaceCoercionTy (toIfaceCoercion co)
1280
1281 toIfaceType (TyConApp tc tys) -- Look for the two sorts of saturated tuple
1282 | Just sort <- tyConTuple_maybe tc
1283 , n_tys == arity
1284 = IfaceTupleTy sort NoIfaceTyConInfo (toIfaceTcArgs tc tys)
1285
1286 | Just dc <- isPromotedDataCon_maybe tc
1287 , isTupleDataCon dc
1288 , n_tys == 2*arity
1289 = IfaceTupleTy BoxedTuple IfacePromotedDataCon (toIfaceTcArgs tc (drop arity tys))
1290
1291 | otherwise
1292 = IfaceTyConApp (toIfaceTyCon tc) (toIfaceTcArgs tc tys)
1293 where
1294 arity = tyConArity tc
1295 n_tys = length tys
1296
1297 toIfaceTyVar :: TyVar -> FastString
1298 toIfaceTyVar = occNameFS . getOccName
1299
1300 toIfaceCoVar :: CoVar -> FastString
1301 toIfaceCoVar = occNameFS . getOccName
1302
1303 toIfaceForAllBndr :: TyVarBinder -> IfaceForAllBndr
1304 toIfaceForAllBndr (TvBndr v vis) = TvBndr (toIfaceTvBndr v) vis
1305
1306 ----------------
1307 toIfaceTyCon :: TyCon -> IfaceTyCon
1308 toIfaceTyCon tc
1309 = IfaceTyCon tc_name info
1310 where
1311 tc_name = tyConName tc
1312 info | isPromotedDataCon tc = IfacePromotedDataCon
1313 | otherwise = NoIfaceTyConInfo
1314
1315 toIfaceTyCon_name :: Name -> IfaceTyCon
1316 toIfaceTyCon_name n = IfaceTyCon n NoIfaceTyConInfo
1317 -- Used for the "rough-match" tycon stuff,
1318 -- where pretty-printing is not an issue
1319
1320 toIfaceTyLit :: TyLit -> IfaceTyLit
1321 toIfaceTyLit (NumTyLit x) = IfaceNumTyLit x
1322 toIfaceTyLit (StrTyLit x) = IfaceStrTyLit x
1323
1324 ----------------
1325 toIfaceTypes :: [Type] -> [IfaceType]
1326 toIfaceTypes ts = map toIfaceType ts
1327
1328 ----------------
1329 toIfaceContext :: ThetaType -> IfaceContext
1330 toIfaceContext = toIfaceTypes
1331
1332 ----------------
1333 toIfaceCoercion :: Coercion -> IfaceCoercion
1334 toIfaceCoercion (Refl r ty) = IfaceReflCo r (toIfaceType ty)
1335 toIfaceCoercion (TyConAppCo r tc cos)
1336 | tc `hasKey` funTyConKey
1337 , [arg,res] <- cos = IfaceFunCo r (toIfaceCoercion arg) (toIfaceCoercion res)
1338 | otherwise = IfaceTyConAppCo r (toIfaceTyCon tc)
1339 (map toIfaceCoercion cos)
1340 toIfaceCoercion (AppCo co1 co2) = IfaceAppCo (toIfaceCoercion co1)
1341 (toIfaceCoercion co2)
1342 toIfaceCoercion (ForAllCo tv k co) = IfaceForAllCo (toIfaceTvBndr tv)
1343 (toIfaceCoercion k)
1344 (toIfaceCoercion co)
1345 toIfaceCoercion (CoVarCo cv) = IfaceCoVarCo (toIfaceCoVar cv)
1346 toIfaceCoercion (AxiomInstCo con ind cos)
1347 = IfaceAxiomInstCo (coAxiomName con) ind
1348 (map toIfaceCoercion cos)
1349 toIfaceCoercion (UnivCo p r t1 t2) = IfaceUnivCo (toIfaceUnivCoProv p) r
1350 (toIfaceType t1)
1351 (toIfaceType t2)
1352 toIfaceCoercion (SymCo co) = IfaceSymCo (toIfaceCoercion co)
1353 toIfaceCoercion (TransCo co1 co2) = IfaceTransCo (toIfaceCoercion co1)
1354 (toIfaceCoercion co2)
1355 toIfaceCoercion (NthCo d co) = IfaceNthCo d (toIfaceCoercion co)
1356 toIfaceCoercion (LRCo lr co) = IfaceLRCo lr (toIfaceCoercion co)
1357 toIfaceCoercion (InstCo co arg) = IfaceInstCo (toIfaceCoercion co)
1358 (toIfaceCoercion arg)
1359 toIfaceCoercion (CoherenceCo c1 c2) = IfaceCoherenceCo (toIfaceCoercion c1)
1360 (toIfaceCoercion c2)
1361 toIfaceCoercion (KindCo c) = IfaceKindCo (toIfaceCoercion c)
1362 toIfaceCoercion (SubCo co) = IfaceSubCo (toIfaceCoercion co)
1363 toIfaceCoercion (AxiomRuleCo co cs) = IfaceAxiomRuleCo (coaxrName co)
1364 (map toIfaceCoercion cs)
1365
1366 toIfaceUnivCoProv :: UnivCoProvenance -> IfaceUnivCoProv
1367 toIfaceUnivCoProv UnsafeCoerceProv = IfaceUnsafeCoerceProv
1368 toIfaceUnivCoProv (PhantomProv co) = IfacePhantomProv (toIfaceCoercion co)
1369 toIfaceUnivCoProv (ProofIrrelProv co) = IfaceProofIrrelProv (toIfaceCoercion co)
1370 toIfaceUnivCoProv (PluginProv str) = IfacePluginProv str
1371 toIfaceUnivCoProv (HoleProv h) = pprPanic "toIfaceUnivCoProv hit a hole" (ppr h)