never executed always true always false
1
2 {-# LANGUAGE DeriveDataTypeable #-}
3
4 {-# OPTIONS_HADDOCK not-home #-}
5
6 {-
7 (c) The University of Glasgow 2006
8 (c) The GRASP/AQUA Project, Glasgow University, 1998
9 \section[GHC.Core.TyCo.Rep]{Type and Coercion - friends' interface}
10
11 Note [The Type-related module hierarchy]
12 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
13 GHC.Core.Class
14 GHC.Core.Coercion.Axiom
15 GHC.Core.TyCon imports GHC.Core.{Class, Coercion.Axiom}
16 GHC.Core.TyCo.Rep imports GHC.Core.{Class, Coercion.Axiom, TyCon}
17 GHC.Core.TyCo.Ppr imports GHC.Core.TyCo.Rep
18 GHC.Core.TyCo.FVs imports GHC.Core.TyCo.Rep
19 GHC.Core.TyCo.Subst imports GHC.Core.TyCo.{Rep, FVs, Ppr}
20 GHC.Core.TyCo.Tidy imports GHC.Core.TyCo.{Rep, FVs}
21 GHC.Builtin.Types.Prim imports GHC.Core.TyCo.Rep ( including mkTyConTy )
22 GHC.Core.Coercion imports GHC.Core.Type
23 -}
24
25 -- We expose the relevant stuff from this module via the Type module
26 module GHC.Core.TyCo.Rep (
27
28 -- * Types
29 Type(..),
30
31 TyLit(..),
32 KindOrType, Kind,
33 KnotTied,
34 PredType, ThetaType, -- Synonyms
35 ArgFlag(..), AnonArgFlag(..),
36
37 -- * Coercions
38 Coercion(..),
39 UnivCoProvenance(..),
40 CoercionHole(..), coHoleCoVar, setCoHoleCoVar,
41 CoercionN, CoercionR, CoercionP, KindCoercion,
42 MCoercion(..), MCoercionR, MCoercionN,
43
44 -- * Functions over types
45 mkTyConTy_, mkTyVarTy, mkTyVarTys,
46 mkTyCoVarTy, mkTyCoVarTys,
47 mkFunTy, mkVisFunTy, mkInvisFunTy, mkVisFunTys,
48 mkForAllTy, mkForAllTys, mkInvisForAllTys,
49 mkPiTy, mkPiTys,
50 mkFunTyMany,
51 mkScaledFunTy,
52 mkVisFunTyMany, mkVisFunTysMany,
53 mkInvisFunTyMany, mkInvisFunTysMany,
54 nonDetCmpTyLit, cmpTyLit,
55
56 -- * Functions over binders
57 TyCoBinder(..), TyCoVarBinder, TyBinder,
58 binderVar, binderVars, binderType, binderArgFlag,
59 delBinderVar,
60 isInvisibleArgFlag, isVisibleArgFlag,
61 isInvisibleBinder, isVisibleBinder,
62 isTyBinder, isNamedBinder,
63
64 -- * Functions over coercions
65 pickLR,
66
67 -- ** Analyzing types
68 TyCoFolder(..), foldTyCo,
69
70 -- * Sizes
71 typeSize, coercionSize, provSize,
72
73 -- * Multiplicities
74 Scaled(..), scaledMult, scaledThing, mapScaledType, Mult
75 ) where
76
77 import GHC.Prelude
78
79 import {-# SOURCE #-} GHC.Core.TyCo.Ppr ( pprType, pprCo, pprTyLit )
80
81 -- Transitively pulls in a LOT of stuff, better to break the loop
82
83 -- friends:
84 import GHC.Iface.Type
85 import GHC.Types.Var
86 import GHC.Types.Var.Set
87 import GHC.Core.TyCon
88 import GHC.Core.Coercion.Axiom
89
90 -- others
91 import {-# SOURCE #-} GHC.Builtin.Types ( manyDataConTy )
92 import GHC.Types.Basic ( LeftOrRight(..), pickLR )
93 import GHC.Types.Unique ( Uniquable(..) )
94 import GHC.Utils.Outputable
95 import GHC.Data.FastString
96 import GHC.Utils.Misc
97 import GHC.Utils.Panic
98
99 -- libraries
100 import qualified Data.Data as Data hiding ( TyCon )
101 import Data.IORef ( IORef ) -- for CoercionHole
102
103 {- **********************************************************************
104 * *
105 Type
106 * *
107 ********************************************************************** -}
108
109 -- | The key representation of types within the compiler
110
111 type KindOrType = Type -- See Note [Arguments to type constructors]
112
113 -- | The key type representing kinds in the compiler.
114 type Kind = Type
115
116 -- If you edit this type, you may need to update the GHC formalism
117 -- See Note [GHC Formalism] in GHC.Core.Lint
118 data Type
119 -- See Note [Non-trivial definitional equality]
120 = TyVarTy Var -- ^ Vanilla type or kind variable (*never* a coercion variable)
121
122 | AppTy
123 Type
124 Type -- ^ Type application to something other than a 'TyCon'. Parameters:
125 --
126 -- 1) Function: must /not/ be a 'TyConApp' or 'CastTy',
127 -- must be another 'AppTy', or 'TyVarTy'
128 -- See Note [Respecting definitional equality] \(EQ1) about the
129 -- no 'CastTy' requirement
130 --
131 -- 2) Argument type
132
133 | TyConApp
134 TyCon
135 [KindOrType] -- ^ Application of a 'TyCon', including newtypes /and/ synonyms.
136 -- Invariant: saturated applications of 'FunTyCon' must
137 -- use 'FunTy' and saturated synonyms must use their own
138 -- constructors. However, /unsaturated/ 'FunTyCon's
139 -- do appear as 'TyConApp's.
140 -- Parameters:
141 --
142 -- 1) Type constructor being applied to.
143 --
144 -- 2) Type arguments. Might not have enough type arguments
145 -- here to saturate the constructor.
146 -- Even type synonyms are not necessarily saturated;
147 -- for example unsaturated type synonyms
148 -- can appear as the right hand side of a type synonym.
149
150 | ForAllTy
151 {-# UNPACK #-} !TyCoVarBinder
152 Type -- ^ A Π type.
153 -- INVARIANT: If the binder is a coercion variable, it must
154 -- be mentioned in the Type. See
155 -- Note [Unused coercion variable in ForAllTy]
156
157 | FunTy -- ^ FUN m t1 t2 Very common, so an important special case
158 -- See Note [Function types]
159 { ft_af :: AnonArgFlag -- Is this (->) or (=>)?
160 , ft_mult :: Mult -- Multiplicity
161 , ft_arg :: Type -- Argument type
162 , ft_res :: Type } -- Result type
163
164 | LitTy TyLit -- ^ Type literals are similar to type constructors.
165
166 | CastTy
167 Type
168 KindCoercion -- ^ A kind cast. The coercion is always nominal.
169 -- INVARIANT: The cast is never reflexive \(EQ2)
170 -- INVARIANT: The Type is not a CastTy (use TransCo instead) \(EQ3)
171 -- INVARIANT: The Type is not a ForAllTy over a tyvar \(EQ4)
172 -- See Note [Respecting definitional equality]
173
174 | CoercionTy
175 Coercion -- ^ Injection of a Coercion into a type
176 -- This should only ever be used in the RHS of an AppTy,
177 -- in the list of a TyConApp, when applying a promoted
178 -- GADT data constructor
179
180 deriving Data.Data
181
182 instance Outputable Type where
183 ppr = pprType
184
185 -- NOTE: Other parts of the code assume that type literals do not contain
186 -- types or type variables.
187 data TyLit
188 = NumTyLit Integer
189 | StrTyLit FastString
190 | CharTyLit Char
191 deriving (Eq, Data.Data)
192
193 -- Non-determinism arises due to uniqCompareFS
194 nonDetCmpTyLit :: TyLit -> TyLit -> Ordering
195 nonDetCmpTyLit = cmpTyLitWith NonDetFastString
196
197 -- Slower than nonDetCmpTyLit but deterministic
198 cmpTyLit :: TyLit -> TyLit -> Ordering
199 cmpTyLit = cmpTyLitWith LexicalFastString
200
201 {-# INLINE cmpTyLitWith #-}
202 cmpTyLitWith :: Ord r => (FastString -> r) -> TyLit -> TyLit -> Ordering
203 cmpTyLitWith _ (NumTyLit x) (NumTyLit y) = compare x y
204 cmpTyLitWith w (StrTyLit x) (StrTyLit y) = compare (w x) (w y)
205 cmpTyLitWith _ (CharTyLit x) (CharTyLit y) = compare x y
206 cmpTyLitWith _ a b = compare (tag a) (tag b)
207 where
208 tag :: TyLit -> Int
209 tag NumTyLit{} = 0
210 tag StrTyLit{} = 1
211 tag CharTyLit{} = 2
212
213 instance Outputable TyLit where
214 ppr = pprTyLit
215
216 {- Note [Function types]
217 ~~~~~~~~~~~~~~~~~~~~~~~~
218 FFunTy is the constructor for a function type. Lots of things to say
219 about it!
220
221 * FFunTy is the data constructor, meaning "full function type".
222
223 * The function type constructor (->) has kind
224 (->) :: forall {r1} {r2}. TYPE r1 -> TYPE r2 -> Type LiftedRep
225 mkTyConApp ensure that we convert a saturated application
226 TyConApp (->) [r1,r2,t1,t2] into FunTy t1 t2
227 dropping the 'r1' and 'r2' arguments; they are easily recovered
228 from 't1' and 't2'.
229
230 * For the time being its RuntimeRep quantifiers are left
231 inferred. This is to allow for it to evolve.
232
233 * The ft_af field says whether or not this is an invisible argument
234 VisArg: t1 -> t2 Ordinary function type
235 InvisArg: t1 => t2 t1 is guaranteed to be a predicate type,
236 i.e. t1 :: Constraint
237 See Note [Types for coercions, predicates, and evidence]
238
239 This visibility info makes no difference in Core; it matters
240 only when we regard the type as a Haskell source type.
241
242 * FunTy is a (unidirectional) pattern synonym that allows
243 positional pattern matching (FunTy arg res), ignoring the
244 ArgFlag.
245 -}
246
247 {- -----------------------
248 Commented out until the pattern match
249 checker can handle it; see #16185
250
251 For now we use the CPP macro #define FunTy FFunTy _
252 (see HsVersions.h) to allow pattern matching on a
253 (positional) FunTy constructor.
254
255 {-# COMPLETE FunTy, TyVarTy, AppTy, TyConApp
256 , ForAllTy, LitTy, CastTy, CoercionTy :: Type #-}
257
258 -- | 'FunTy' is a (uni-directional) pattern synonym for the common
259 -- case where we want to match on the argument/result type, but
260 -- ignoring the AnonArgFlag
261 pattern FunTy :: Type -> Type -> Type
262 pattern FunTy arg res <- FFunTy { ft_arg = arg, ft_res = res }
263
264 End of commented out block
265 ---------------------------------- -}
266
267 {- Note [Types for coercions, predicates, and evidence]
268 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
269 We treat differently:
270
271 (a) Predicate types
272 Test: isPredTy
273 Binders: DictIds
274 Kind: Constraint
275 Examples: (Eq a), and (a ~ b)
276
277 (b) Coercion types are primitive, unboxed equalities
278 Test: isCoVarTy
279 Binders: CoVars (can appear in coercions)
280 Kind: TYPE (TupleRep [])
281 Examples: (t1 ~# t2) or (t1 ~R# t2)
282
283 (c) Evidence types is the type of evidence manipulated by
284 the type constraint solver.
285 Test: isEvVarType
286 Binders: EvVars
287 Kind: Constraint or TYPE (TupleRep [])
288 Examples: all coercion types and predicate types
289
290 Coercion types and predicate types are mutually exclusive,
291 but evidence types are a superset of both.
292
293 When treated as a user type,
294
295 - Predicates (of kind Constraint) are invisible and are
296 implicitly instantiated
297
298 - Coercion types, and non-pred evidence types (i.e. not
299 of kind Constrain), are just regular old types, are
300 visible, and are not implicitly instantiated.
301
302 In a FunTy { ft_af = InvisArg }, the argument type is always
303 a Predicate type.
304
305 Note [Weird typing rule for ForAllTy]
306 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
307 Here are the typing rules for ForAllTy:
308
309 tyvar : Type
310 inner : TYPE r
311 tyvar does not occur in r
312 ------------------------------------
313 ForAllTy (Bndr tyvar vis) inner : TYPE r
314
315 inner : TYPE r
316 ------------------------------------
317 ForAllTy (Bndr covar vis) inner : Type
318
319 Note that the kind of the result depends on whether the binder is a
320 tyvar or a covar. The kind of a forall-over-tyvar is the same as
321 the kind of the inner type. This is because quantification over types
322 is erased before runtime. By contrast, the kind of a forall-over-covar
323 is always Type, because a forall-over-covar is compiled into a function
324 taking a 0-bit-wide erased coercion argument.
325
326 Because the tyvar form above includes r in its result, we must
327 be careful not to let any variables escape -- thus the last premise
328 of the rule above.
329
330 Note [Constraints in kinds]
331 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
332 Do we allow a type constructor to have a kind like
333 S :: Eq a => a -> Type
334
335 No, we do not. Doing so would mean would need a TyConApp like
336 S @k @(d :: Eq k) (ty :: k)
337 and we have no way to build, or decompose, evidence like
338 (d :: Eq k) at the type level.
339
340 But we admit one exception: equality. We /do/ allow, say,
341 MkT :: (a ~ b) => a -> b -> Type a b
342
343 Why? Because we can, without much difficulty. Moreover
344 we can promote a GADT data constructor (see TyCon
345 Note [Promoted data constructors]), like
346 data GT a b where
347 MkGT : a -> a -> GT a a
348 so programmers might reasonably expect to be able to
349 promote MkT as well.
350
351 How does this work?
352
353 * In GHC.Tc.Validity.checkConstraintsOK we reject kinds that
354 have constraints other than (a~b) and (a~~b).
355
356 * In Inst.tcInstInvisibleTyBinder we instantiate a call
357 of MkT by emitting
358 [W] co :: alpha ~# beta
359 and producing the elaborated term
360 MkT @alpha @beta (Eq# alpha beta co)
361 We don't generate a boxed "Wanted"; we generate only a
362 regular old /unboxed/ primitive-equality Wanted, and build
363 the box on the spot.
364
365 * How can we get such a MkT? By promoting a GADT-style data
366 constructor
367 data T a b where
368 MkT :: (a~b) => a -> b -> T a b
369 See DataCon.mkPromotedDataCon
370 and Note [Promoted data constructors] in GHC.Core.TyCon
371
372 * We support both homogeneous (~) and heterogeneous (~~)
373 equality. (See Note [The equality types story]
374 in GHC.Builtin.Types.Prim for a primer on these equality types.)
375
376 * How do we prevent a MkT having an illegal constraint like
377 Eq a? We check for this at use-sites; see GHC.Tc.Gen.HsType.tcTyVar,
378 specifically dc_theta_illegal_constraint.
379
380 * Notice that nothing special happens if
381 K :: (a ~# b) => blah
382 because (a ~# b) is not a predicate type, and is never
383 implicitly instantiated. (Mind you, it's not clear how you
384 could creates a type constructor with such a kind.) See
385 Note [Types for coercions, predicates, and evidence]
386
387 * The existence of promoted MkT with an equality-constraint
388 argument is the (only) reason that the AnonTCB constructor
389 of TyConBndrVis carries an AnonArgFlag (VisArg/InvisArg).
390 For example, when we promote the data constructor
391 MkT :: forall a b. (a~b) => a -> b -> T a b
392 we get a PromotedDataCon with tyConBinders
393 Bndr (a :: Type) (NamedTCB Inferred)
394 Bndr (b :: Type) (NamedTCB Inferred)
395 Bndr (_ :: a ~ b) (AnonTCB InvisArg)
396 Bndr (_ :: a) (AnonTCB VisArg))
397 Bndr (_ :: b) (AnonTCB VisArg))
398
399 * One might reasonably wonder who *unpacks* these boxes once they are
400 made. After all, there is no type-level `case` construct. The
401 surprising answer is that no one ever does. Instead, if a GADT
402 constructor is used on the left-hand side of a type family equation,
403 that occurrence forces GHC to unify the types in question. For
404 example:
405
406 data G a where
407 MkG :: G Bool
408
409 type family F (x :: G a) :: a where
410 F MkG = False
411
412 When checking the LHS `F MkG`, GHC sees the MkG constructor and then must
413 unify F's implicit parameter `a` with Bool. This succeeds, making the equation
414
415 F Bool (MkG @Bool <Bool>) = False
416
417 Note that we never need unpack the coercion. This is because type
418 family equations are *not* parametric in their kind variables. That
419 is, we could have just said
420
421 type family H (x :: G a) :: a where
422 H _ = False
423
424 The presence of False on the RHS also forces `a` to become Bool,
425 giving us
426
427 H Bool _ = False
428
429 The fact that any of this works stems from the lack of phase
430 separation between types and kinds (unlike the very present phase
431 separation between terms and types).
432
433 Once we have the ability to pattern-match on types below top-level,
434 this will no longer cut it, but it seems fine for now.
435
436
437 Note [Arguments to type constructors]
438 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
439 Because of kind polymorphism, in addition to type application we now
440 have kind instantiation. We reuse the same notations to do so.
441
442 For example:
443
444 Just (* -> *) Maybe
445 Right * Nat Zero
446
447 are represented by:
448
449 TyConApp (PromotedDataCon Just) [* -> *, Maybe]
450 TyConApp (PromotedDataCon Right) [*, Nat, (PromotedDataCon Zero)]
451
452 Important note: Nat is used as a *kind* and not as a type. This can be
453 confusing, since type-level Nat and kind-level Nat are identical. We
454 use the kind of (PromotedDataCon Right) to know if its arguments are
455 kinds or types.
456
457 This kind instantiation only happens in TyConApp currently.
458
459 Note [Non-trivial definitional equality]
460 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
461 Is Int |> <*> the same as Int? YES! In order to reduce headaches,
462 we decide that any reflexive casts in types are just ignored.
463 (Indeed they must be. See Note [Respecting definitional equality].)
464 More generally, the `eqType` function, which defines Core's type equality
465 relation, ignores casts and coercion arguments, as long as the
466 two types have the same kind. This allows us to be a little sloppier
467 in keeping track of coercions, which is a good thing. It also means
468 that eqType does not depend on eqCoercion, which is also a good thing.
469
470 Why is this sensible? That is, why is something different than α-equivalence
471 appropriate for the implementation of eqType?
472
473 Anything smaller than ~ and homogeneous is an appropriate definition for
474 equality. The type safety of FC depends only on ~. Let's say η : τ ~ σ. Any
475 expression of type τ can be transmuted to one of type σ at any point by
476 casting. The same is true of expressions of type σ. So in some sense, τ and σ
477 are interchangeable.
478
479 But let's be more precise. If we examine the typing rules of FC (say, those in
480 https://richarde.dev/papers/2015/equalities/equalities.pdf)
481 there are several places where the same metavariable is used in two different
482 premises to a rule. (For example, see Ty_App.) There is an implicit equality
483 check here. What definition of equality should we use? By convention, we use
484 α-equivalence. Take any rule with one (or more) of these implicit equality
485 checks. Then there is an admissible rule that uses ~ instead of the implicit
486 check, adding in casts as appropriate.
487
488 The only problem here is that ~ is heterogeneous. To make the kinds work out
489 in the admissible rule that uses ~, it is necessary to homogenize the
490 coercions. That is, if we have η : (τ : κ1) ~ (σ : κ2), then we don't use η;
491 we use η |> kind η, which is homogeneous.
492
493 The effect of this all is that eqType, the implementation of the implicit
494 equality check, can use any homogeneous relation that is smaller than ~, as
495 those rules must also be admissible.
496
497 A more drawn out argument around all of this is presented in Section 7.2 of
498 Richard E's thesis (http://richarde.dev/papers/2016/thesis/eisenberg-thesis.pdf).
499
500 What would go wrong if we insisted on the casts matching? See the beginning of
501 Section 8 in the unpublished paper above. Theoretically, nothing at all goes
502 wrong. But in practical terms, getting the coercions right proved to be
503 nightmarish. And types would explode: during kind-checking, we often produce
504 reflexive kind coercions. When we try to cast by these, mkCastTy just discards
505 them. But if we used an eqType that distinguished between Int and Int |> <*>,
506 then we couldn't discard -- the output of kind-checking would be enormous,
507 and we would need enormous casts with lots of CoherenceCo's to straighten
508 them out.
509
510 Would anything go wrong if eqType looked through type families? No, not at
511 all. But that makes eqType rather hard to implement.
512
513 Thus, the guideline for eqType is that it should be the largest
514 easy-to-implement relation that is still smaller than ~ and homogeneous. The
515 precise choice of relation is somewhat incidental, as long as the smart
516 constructors and destructors in Type respect whatever relation is chosen.
517
518 Another helpful principle with eqType is this:
519
520 (EQ) If (t1 `eqType` t2) then I can replace t1 by t2 anywhere.
521
522 This principle also tells us that eqType must relate only types with the
523 same kinds.
524
525 Interestingly, it must be the case that the free variables of t1 and t2
526 might be different, even if t1 `eqType` t2. A simple example of this is
527 if we have both cv1 :: k1 ~ k2 and cv2 :: k1 ~ k2 in the environment.
528 Then t1 = t |> cv1 and t2 = t |> cv2 are eqType; yet cv1 is in the free
529 vars of t1 and cv2 is in the free vars of t2. Unless we choose to implement
530 eqType to be just α-equivalence, this wrinkle around free variables
531 remains.
532
533 Yet not all is lost: we can say that any two equal types share the same
534 *relevant* free variables. Here, a relevant variable is a shallow
535 free variable (see Note [Shallow and deep free variables] in GHC.Core.TyCo.FVs)
536 that does not appear within a coercion. Note that type variables can
537 appear within coercions (in, say, a Refl node), but that coercion variables
538 cannot appear outside a coercion. We do not (yet) have a function to
539 extract relevant free variables, but it would not be hard to write if
540 the need arises.
541
542 Besides eqType, another equality relation that upholds the (EQ) property above
543 is /typechecker equality/, which is implemented as
544 GHC.Tc.Utils.TcType.tcEqType. See
545 Note [Typechecker equality vs definitional equality] in GHC.Tc.Utils.TcType for
546 what the difference between eqType and tcEqType is.
547
548 Note [Respecting definitional equality]
549 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
550 Note [Non-trivial definitional equality] introduces the property (EQ).
551 How is this upheld?
552
553 Any function that pattern matches on all the constructors will have to
554 consider the possibility of CastTy. Presumably, those functions will handle
555 CastTy appropriately and we'll be OK.
556
557 More dangerous are the splitXXX functions. Let's focus on splitTyConApp.
558 We don't want it to fail on (T a b c |> co). Happily, if we have
559 (T a b c |> co) `eqType` (T d e f)
560 then co must be reflexive. Why? eqType checks that the kinds are equal, as
561 well as checking that (a `eqType` d), (b `eqType` e), and (c `eqType` f).
562 By the kind check, we know that (T a b c |> co) and (T d e f) have the same
563 kind. So the only way that co could be non-reflexive is for (T a b c) to have
564 a different kind than (T d e f). But because T's kind is closed (all tycon kinds
565 are closed), the only way for this to happen is that one of the arguments has
566 to differ, leading to a contradiction. Thus, co is reflexive.
567
568 Accordingly, by eliminating reflexive casts, splitTyConApp need not worry
569 about outermost casts to uphold (EQ). Eliminating reflexive casts is done
570 in mkCastTy. This is (EQ1) below.
571
572 Unforunately, that's not the end of the story. Consider comparing
573 (T a b c) =? (T a b |> (co -> <Type>)) (c |> co)
574 These two types have the same kind (Type), but the left type is a TyConApp
575 while the right type is not. To handle this case, we say that the right-hand
576 type is ill-formed, requiring an AppTy never to have a casted TyConApp
577 on its left. It is easy enough to pull around the coercions to maintain
578 this invariant, as done in Type.mkAppTy. In the example above, trying to
579 form the right-hand type will instead yield (T a b (c |> co |> sym co) |> <Type>).
580 Both the casts there are reflexive and will be dropped. Huzzah.
581
582 This idea of pulling coercions to the right works for splitAppTy as well.
583
584 However, there is one hiccup: it's possible that a coercion doesn't relate two
585 Pi-types. For example, if we have @type family Fun a b where Fun a b = a -> b@,
586 then we might have (T :: Fun Type Type) and (T |> axFun) Int. That axFun can't
587 be pulled to the right. But we don't need to pull it: (T |> axFun) Int is not
588 `eqType` to any proper TyConApp -- thus, leaving it where it is doesn't violate
589 our (EQ) property.
590
591 In order to detect reflexive casts reliably, we must make sure not
592 to have nested casts: we update (t |> co1 |> co2) to (t |> (co1 `TransCo` co2)).
593 This is (EQ2) below.
594
595 One other troublesome case is ForAllTy. See Note [Weird typing rule for ForAllTy].
596 The kind of the body is the same as the kind of the ForAllTy. Accordingly,
597
598 ForAllTy tv (ty |> co) and (ForAllTy tv ty) |> co
599
600 are `eqType`. But only the first can be split by splitForAllTy. So we forbid
601 the second form, instead pushing the coercion inside to get the first form.
602 This is done in mkCastTy.
603
604 In sum, in order to uphold (EQ), we need the following invariants:
605
606 (EQ1) No decomposable CastTy to the left of an AppTy, where a decomposable
607 cast is one that relates either a FunTy to a FunTy or a
608 ForAllTy to a ForAllTy.
609 (EQ2) No reflexive casts in CastTy.
610 (EQ3) No nested CastTys.
611 (EQ4) No CastTy over (ForAllTy (Bndr tyvar vis) body).
612 See Note [Weird typing rule for ForAllTy]
613
614 These invariants are all documented above, in the declaration for Type.
615
616 Note [Equality on FunTys]
617 ~~~~~~~~~~~~~~~~~~~~~~~~~
618 A (FunTy vis mult arg res) is just an abbreviation for a
619 TyConApp funTyCon [mult, arg_rep, res_rep, arg, res]
620 where
621 arg :: TYPE arg_rep
622 res :: TYPE res_rep
623 Note that the vis field of a FunTy appears nowhere in the
624 equivalent TyConApp. In Core, this is OK, because we no longer
625 care about the visibility of the argument in a FunTy
626 (the vis distinguishes between arg -> res and arg => res).
627 In the type-checker, we are careful not to decompose FunTys
628 with an invisible argument. See also Note [Decomposing fat arrow c=>t]
629 in GHC.Core.Type.
630
631 In order to compare FunTys while respecting how they could
632 expand into TyConApps, we must check
633 the kinds of the arg and the res.
634
635 Note [Unused coercion variable in ForAllTy]
636 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
637 Suppose we have
638 \(co:t1 ~ t2). e
639
640 What type should we give to this expression?
641 (1) forall (co:t1 ~ t2) -> t
642 (2) (t1 ~ t2) -> t
643
644 If co is used in t, (1) should be the right choice.
645 if co is not used in t, we would like to have (1) and (2) equivalent.
646
647 However, we want to keep eqType simple and don't want eqType (1) (2) to return
648 True in any case.
649
650 We decide to always construct (2) if co is not used in t.
651
652 Thus in mkLamType, we check whether the variable is a coercion
653 variable (of type (t1 ~# t2), and whether it is un-used in the
654 body. If so, it returns a FunTy instead of a ForAllTy.
655
656 There are cases we want to skip the check. For example, the check is
657 unnecessary when it is known from the context that the input variable
658 is a type variable. In those cases, we use mkForAllTy.
659
660 Note [Weird typing rule for ForAllTy]
661 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
662 Here is the (truncated) typing rule for the dependent ForAllTy:
663
664 inner : TYPE r
665 tyvar is not free in r
666 ----------------------------------------
667 ForAllTy (Bndr tyvar vis) inner : TYPE r
668
669 Note that the kind of `inner` is the kind of the overall ForAllTy. This is
670 necessary because every ForAllTy over a type variable is erased at runtime.
671 Thus the runtime representation of a ForAllTy (as encoded, via TYPE rep, in
672 the kind) must be the same as the representation of the body. We must check
673 for skolem-escape, though. The skolem-escape would prevent a definition like
674
675 undefined :: forall (r :: RuntimeRep) (a :: TYPE r). a
676
677 because the type's kind (TYPE r) mentions the out-of-scope r. Luckily, the real
678 type of undefined is
679
680 undefined :: forall (r :: RuntimeRep) (a :: TYPE r). HasCallStack => a
681
682 and that HasCallStack constraint neatly sidesteps the potential skolem-escape
683 problem.
684
685 If the bound variable is a coercion variable:
686
687 inner : TYPE r
688 covar is free in inner
689 ------------------------------------
690 ForAllTy (Bndr covar vis) inner : Type
691
692 Here, the kind of the ForAllTy is just Type, because coercion abstractions
693 are *not* erased. The "covar is free in inner" premise is solely to maintain
694 the representation invariant documented in
695 Note [Unused coercion variable in ForAllTy]. Though there is surface similarity
696 between this free-var check and the one in the tyvar rule, these two restrictions
697 are truly unrelated.
698
699 -}
700
701 -- | A type labeled 'KnotTied' might have knot-tied tycons in it. See
702 -- Note [Type checking recursive type and class declarations] in
703 -- "GHC.Tc.TyCl"
704 type KnotTied ty = ty
705
706 {- **********************************************************************
707 * *
708 TyCoBinder and ArgFlag
709 * *
710 ********************************************************************** -}
711
712 -- | A 'TyCoBinder' represents an argument to a function. TyCoBinders can be
713 -- dependent ('Named') or nondependent ('Anon'). They may also be visible or
714 -- not. See Note [TyCoBinders]
715 data TyCoBinder
716 = Named TyCoVarBinder -- A type-lambda binder
717 | Anon AnonArgFlag (Scaled Type) -- A term-lambda binder. Type here can be CoercionTy.
718 -- Visibility is determined by the AnonArgFlag
719 deriving Data.Data
720
721 instance Outputable TyCoBinder where
722 ppr (Anon af ty) = ppr af <+> ppr ty
723 ppr (Named (Bndr v Required)) = ppr v
724 -- See Note [Explicit Case Statement for Specificity]
725 ppr (Named (Bndr v (Invisible spec))) = case spec of
726 SpecifiedSpec -> char '@' <> ppr v
727 InferredSpec -> braces (ppr v)
728
729
730 -- | 'TyBinder' is like 'TyCoBinder', but there can only be 'TyVarBinder'
731 -- in the 'Named' field.
732 type TyBinder = TyCoBinder
733
734 -- | Remove the binder's variable from the set, if the binder has
735 -- a variable.
736 delBinderVar :: VarSet -> TyCoVarBinder -> VarSet
737 delBinderVar vars (Bndr tv _) = vars `delVarSet` tv
738
739 -- | Does this binder bind an invisible argument?
740 isInvisibleBinder :: TyCoBinder -> Bool
741 isInvisibleBinder (Named (Bndr _ vis)) = isInvisibleArgFlag vis
742 isInvisibleBinder (Anon InvisArg _) = True
743 isInvisibleBinder (Anon VisArg _) = False
744
745 -- | Does this binder bind a visible argument?
746 isVisibleBinder :: TyCoBinder -> Bool
747 isVisibleBinder = not . isInvisibleBinder
748
749 isNamedBinder :: TyCoBinder -> Bool
750 isNamedBinder (Named {}) = True
751 isNamedBinder (Anon {}) = False
752
753 -- | If its a named binder, is the binder a tyvar?
754 -- Returns True for nondependent binder.
755 -- This check that we're really returning a *Ty*Binder (as opposed to a
756 -- coercion binder). That way, if/when we allow coercion quantification
757 -- in more places, we'll know we missed updating some function.
758 isTyBinder :: TyCoBinder -> Bool
759 isTyBinder (Named bnd) = isTyVarBinder bnd
760 isTyBinder _ = True
761
762 {- Note [TyCoBinders]
763 ~~~~~~~~~~~~~~~~~~~
764 A ForAllTy contains a TyCoVarBinder. But a type can be decomposed
765 to a telescope consisting of a [TyCoBinder]
766
767 A TyCoBinder represents the type of binders -- that is, the type of an
768 argument to a Pi-type. GHC Core currently supports two different
769 Pi-types:
770
771 * A non-dependent function type,
772 written with ->, e.g. ty1 -> ty2
773 represented as FunTy ty1 ty2. These are
774 lifted to Coercions with the corresponding FunCo.
775
776 * A dependent compile-time-only polytype,
777 written with forall, e.g. forall (a:*). ty
778 represented as ForAllTy (Bndr a v) ty
779
780 Both Pi-types classify terms/types that take an argument. In other
781 words, if `x` is either a function or a polytype, `x arg` makes sense
782 (for an appropriate `arg`).
783
784
785 Note [VarBndrs, TyCoVarBinders, TyConBinders, and visibility]
786 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
787 * A ForAllTy (used for both types and kinds) contains a TyCoVarBinder.
788 Each TyCoVarBinder
789 Bndr a tvis
790 is equipped with tvis::ArgFlag, which says whether or not arguments
791 for this binder should be visible (explicit) in source Haskell.
792
793 * A TyCon contains a list of TyConBinders. Each TyConBinder
794 Bndr a cvis
795 is equipped with cvis::TyConBndrVis, which says whether or not type
796 and kind arguments for this TyCon should be visible (explicit) in
797 source Haskell.
798
799 This table summarises the visibility rules:
800 ---------------------------------------------------------------------------------------
801 | Occurrences look like this
802 | GHC displays type as in Haskell source code
803 |--------------------------------------------------------------------------------------
804 | Bndr a tvis :: TyCoVarBinder, in the binder of ForAllTy for a term
805 | tvis :: ArgFlag
806 | tvis = Inferred: f :: forall {a}. type Arg not allowed: f
807 f :: forall {co}. type Arg not allowed: f
808 | tvis = Specified: f :: forall a. type Arg optional: f or f @Int
809 | tvis = Required: T :: forall k -> type Arg required: T *
810 | This last form is illegal in terms: See Note [No Required TyCoBinder in terms]
811 |
812 | Bndr k cvis :: TyConBinder, in the TyConBinders of a TyCon
813 | cvis :: TyConBndrVis
814 | cvis = AnonTCB: T :: kind -> kind Required: T *
815 | cvis = NamedTCB Inferred: T :: forall {k}. kind Arg not allowed: T
816 | T :: forall {co}. kind Arg not allowed: T
817 | cvis = NamedTCB Specified: T :: forall k. kind Arg not allowed[1]: T
818 | cvis = NamedTCB Required: T :: forall k -> kind Required: T *
819 ---------------------------------------------------------------------------------------
820
821 [1] In types, in the Specified case, it would make sense to allow
822 optional kind applications, thus (T @*), but we have not
823 yet implemented that
824
825 ---- In term declarations ----
826
827 * Inferred. Function defn, with no signature: f1 x = x
828 We infer f1 :: forall {a}. a -> a, with 'a' Inferred
829 It's Inferred because it doesn't appear in any
830 user-written signature for f1
831
832 * Specified. Function defn, with signature (implicit forall):
833 f2 :: a -> a; f2 x = x
834 So f2 gets the type f2 :: forall a. a -> a, with 'a' Specified
835 even though 'a' is not bound in the source code by an explicit forall
836
837 * Specified. Function defn, with signature (explicit forall):
838 f3 :: forall a. a -> a; f3 x = x
839 So f3 gets the type f3 :: forall a. a -> a, with 'a' Specified
840
841 * Inferred. Function defn, with signature (explicit forall), marked as inferred:
842 f4 :: forall {a}. a -> a; f4 x = x
843 So f4 gets the type f4 :: forall {a}. a -> a, with 'a' Inferred
844 It's Inferred because the user marked it as such, even though it does appear
845 in the user-written signature for f4
846
847 * Inferred/Specified. Function signature with inferred kind polymorphism.
848 f5 :: a b -> Int
849 So 'f5' gets the type f5 :: forall {k} (a:k->*) (b:k). a b -> Int
850 Here 'k' is Inferred (it's not mentioned in the type),
851 but 'a' and 'b' are Specified.
852
853 * Specified. Function signature with explicit kind polymorphism
854 f6 :: a (b :: k) -> Int
855 This time 'k' is Specified, because it is mentioned explicitly,
856 so we get f6 :: forall (k:*) (a:k->*) (b:k). a b -> Int
857
858 * Similarly pattern synonyms:
859 Inferred - from inferred types (e.g. no pattern type signature)
860 - or from inferred kind polymorphism
861
862 ---- In type declarations ----
863
864 * Inferred (k)
865 data T1 a b = MkT1 (a b)
866 Here T1's kind is T1 :: forall {k:*}. (k->*) -> k -> *
867 The kind variable 'k' is Inferred, since it is not mentioned
868
869 Note that 'a' and 'b' correspond to /Anon/ TyCoBinders in T1's kind,
870 and Anon binders don't have a visibility flag. (Or you could think
871 of Anon having an implicit Required flag.)
872
873 * Specified (k)
874 data T2 (a::k->*) b = MkT (a b)
875 Here T's kind is T :: forall (k:*). (k->*) -> k -> *
876 The kind variable 'k' is Specified, since it is mentioned in
877 the signature.
878
879 * Required (k)
880 data T k (a::k->*) b = MkT (a b)
881 Here T's kind is T :: forall k:* -> (k->*) -> k -> *
882 The kind is Required, since it bound in a positional way in T's declaration
883 Every use of T must be explicitly applied to a kind
884
885 * Inferred (k1), Specified (k)
886 data T a b (c :: k) = MkT (a b) (Proxy c)
887 Here T's kind is T :: forall {k1:*} (k:*). (k1->*) -> k1 -> k -> *
888 So 'k' is Specified, because it appears explicitly,
889 but 'k1' is Inferred, because it does not
890
891 Generally, in the list of TyConBinders for a TyCon,
892
893 * Inferred arguments always come first
894 * Specified, Anon and Required can be mixed
895
896 e.g.
897 data Foo (a :: Type) :: forall b. (a -> b -> Type) -> Type where ...
898
899 Here Foo's TyConBinders are
900 [Required 'a', Specified 'b', Anon]
901 and its kind prints as
902 Foo :: forall a -> forall b. (a -> b -> Type) -> Type
903
904 See also Note [Required, Specified, and Inferred for types] in GHC.Tc.TyCl
905
906 ---- Printing -----
907
908 We print forall types with enough syntax to tell you their visibility
909 flag. But this is not source Haskell, and these types may not all
910 be parsable.
911
912 Specified: a list of Specified binders is written between `forall` and `.`:
913 const :: forall a b. a -> b -> a
914
915 Inferred: like Specified, but every binder is written in braces:
916 f :: forall {k} (a:k). S k a -> Int
917
918 Required: binders are put between `forall` and `->`:
919 T :: forall k -> *
920
921 ---- Other points -----
922
923 * In classic Haskell, all named binders (that is, the type variables in
924 a polymorphic function type f :: forall a. a -> a) have been Inferred.
925
926 * Inferred variables correspond to "generalized" variables from the
927 Visible Type Applications paper (ESOP'16).
928
929 Note [No Required TyCoBinder in terms]
930 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
931 We don't allow Required foralls for term variables, including pattern
932 synonyms and data constructors. Why? Because then an application
933 would need a /compulsory/ type argument (possibly without an "@"?),
934 thus (f Int); and we don't have concrete syntax for that.
935
936 We could change this decision, but Required, Named TyCoBinders are rare
937 anyway. (Most are Anons.)
938
939 However the type of a term can (just about) have a required quantifier;
940 see Note [Required quantifiers in the type of a term] in GHC.Tc.Gen.Expr.
941 -}
942
943
944 {- **********************************************************************
945 * *
946 PredType
947 * *
948 ********************************************************************** -}
949
950
951 -- | A type of the form @p@ of constraint kind represents a value whose type is
952 -- the Haskell predicate @p@, where a predicate is what occurs before
953 -- the @=>@ in a Haskell type.
954 --
955 -- We use 'PredType' as documentation to mark those types that we guarantee to
956 -- have this kind.
957 --
958 -- It can be expanded into its representation, but:
959 --
960 -- * The type checker must treat it as opaque
961 --
962 -- * The rest of the compiler treats it as transparent
963 --
964 -- Consider these examples:
965 --
966 -- > f :: (Eq a) => a -> Int
967 -- > g :: (?x :: Int -> Int) => a -> Int
968 -- > h :: (r\l) => {r} => {l::Int | r}
969 --
970 -- Here the @Eq a@ and @?x :: Int -> Int@ and @r\l@ are all called \"predicates\"
971 type PredType = Type
972
973 -- | A collection of 'PredType's
974 type ThetaType = [PredType]
975
976 {-
977 (We don't support TREX records yet, but the setup is designed
978 to expand to allow them.)
979
980 A Haskell qualified type, such as that for f,g,h above, is
981 represented using
982 * a FunTy for the double arrow
983 * with a type of kind Constraint as the function argument
984
985 The predicate really does turn into a real extra argument to the
986 function. If the argument has type (p :: Constraint) then the predicate p is
987 represented by evidence of type p.
988
989
990 %************************************************************************
991 %* *
992 Simple constructors
993 %* *
994 %************************************************************************
995
996 These functions are here so that they can be used by GHC.Builtin.Types.Prim,
997 which in turn is imported by Type
998 -}
999
1000 mkTyVarTy :: TyVar -> Type
1001 mkTyVarTy v = assertPpr (isTyVar v) (ppr v <+> dcolon <+> ppr (tyVarKind v)) $
1002 TyVarTy v
1003
1004 mkTyVarTys :: [TyVar] -> [Type]
1005 mkTyVarTys = map mkTyVarTy -- a common use of mkTyVarTy
1006
1007 mkTyCoVarTy :: TyCoVar -> Type
1008 mkTyCoVarTy v
1009 | isTyVar v
1010 = TyVarTy v
1011 | otherwise
1012 = CoercionTy (CoVarCo v)
1013
1014 mkTyCoVarTys :: [TyCoVar] -> [Type]
1015 mkTyCoVarTys = map mkTyCoVarTy
1016
1017 infixr 3 `mkFunTy`, `mkVisFunTy`, `mkInvisFunTy`, `mkVisFunTyMany`,
1018 `mkInvisFunTyMany` -- Associates to the right
1019
1020 mkFunTy :: AnonArgFlag -> Mult -> Type -> Type -> Type
1021 mkFunTy af mult arg res = FunTy { ft_af = af
1022 , ft_mult = mult
1023 , ft_arg = arg
1024 , ft_res = res }
1025
1026 mkScaledFunTy :: AnonArgFlag -> Scaled Type -> Type -> Type
1027 mkScaledFunTy af (Scaled mult arg) res = mkFunTy af mult arg res
1028
1029 mkVisFunTy, mkInvisFunTy :: Mult -> Type -> Type -> Type
1030 mkVisFunTy = mkFunTy VisArg
1031 mkInvisFunTy = mkFunTy InvisArg
1032
1033 mkFunTyMany :: AnonArgFlag -> Type -> Type -> Type
1034 mkFunTyMany af = mkFunTy af manyDataConTy
1035
1036 -- | Special, common, case: Arrow type with mult Many
1037 mkVisFunTyMany :: Type -> Type -> Type
1038 mkVisFunTyMany = mkVisFunTy manyDataConTy
1039
1040 mkInvisFunTyMany :: Type -> Type -> Type
1041 mkInvisFunTyMany = mkInvisFunTy manyDataConTy
1042
1043 -- | Make nested arrow types
1044 mkVisFunTys :: [Scaled Type] -> Type -> Type
1045 mkVisFunTys tys ty = foldr (mkScaledFunTy VisArg) ty tys
1046
1047 mkVisFunTysMany :: [Type] -> Type -> Type
1048 mkVisFunTysMany tys ty = foldr mkVisFunTyMany ty tys
1049
1050 mkInvisFunTysMany :: [Type] -> Type -> Type
1051 mkInvisFunTysMany tys ty = foldr mkInvisFunTyMany ty tys
1052
1053 -- | Like 'mkTyCoForAllTy', but does not check the occurrence of the binder
1054 -- See Note [Unused coercion variable in ForAllTy]
1055 mkForAllTy :: TyCoVar -> ArgFlag -> Type -> Type
1056 mkForAllTy tv vis ty = ForAllTy (Bndr tv vis) ty
1057
1058 -- | Wraps foralls over the type using the provided 'TyCoVar's from left to right
1059 mkForAllTys :: [TyCoVarBinder] -> Type -> Type
1060 mkForAllTys tyvars ty = foldr ForAllTy ty tyvars
1061
1062 -- | Wraps foralls over the type using the provided 'InvisTVBinder's from left to right
1063 mkInvisForAllTys :: [InvisTVBinder] -> Type -> Type
1064 mkInvisForAllTys tyvars ty = foldr ForAllTy ty $ tyVarSpecToBinders tyvars
1065
1066 mkPiTy :: TyCoBinder -> Type -> Type
1067 mkPiTy (Anon af ty1) ty2 = mkScaledFunTy af ty1 ty2
1068 mkPiTy (Named (Bndr tv vis)) ty = mkForAllTy tv vis ty
1069
1070 mkPiTys :: [TyCoBinder] -> Type -> Type
1071 mkPiTys tbs ty = foldr mkPiTy ty tbs
1072
1073 -- | Create a nullary 'TyConApp'. In general you should rather use
1074 -- 'GHC.Core.Type.mkTyConTy'. This merely exists to break the import cycle
1075 -- between 'GHC.Core.TyCon' and this module.
1076 mkTyConTy_ :: TyCon -> Type
1077 mkTyConTy_ tycon = TyConApp tycon []
1078
1079 {-
1080 %************************************************************************
1081 %* *
1082 Coercions
1083 %* *
1084 %************************************************************************
1085 -}
1086
1087 -- | A 'Coercion' is concrete evidence of the equality/convertibility
1088 -- of two types.
1089
1090 -- If you edit this type, you may need to update the GHC formalism
1091 -- See Note [GHC Formalism] in GHC.Core.Lint
1092 data Coercion
1093 -- Each constructor has a "role signature", indicating the way roles are
1094 -- propagated through coercions.
1095 -- - P, N, and R stand for coercions of the given role
1096 -- - e stands for a coercion of a specific unknown role
1097 -- (think "role polymorphism")
1098 -- - "e" stands for an explicit role parameter indicating role e.
1099 -- - _ stands for a parameter that is not a Role or Coercion.
1100
1101 -- These ones mirror the shape of types
1102 = -- Refl :: _ -> N
1103 -- A special case reflexivity for a very common case: Nominal reflexivity
1104 -- If you need Representational, use (GRefl Representational ty MRefl)
1105 -- not (SubCo (Refl ty))
1106 Refl Type -- See Note [Refl invariant]
1107
1108 -- GRefl :: "e" -> _ -> Maybe N -> e
1109 -- See Note [Generalized reflexive coercion]
1110 | GRefl Role Type MCoercionN -- See Note [Refl invariant]
1111 -- Use (Refl ty), not (GRefl Nominal ty MRefl)
1112 -- Use (GRefl Representational _ _), not (SubCo (GRefl Nominal _ _))
1113
1114 -- These ones simply lift the correspondingly-named
1115 -- Type constructors into Coercions
1116
1117 -- TyConAppCo :: "e" -> _ -> ?? -> e
1118 -- See Note [TyConAppCo roles]
1119 | TyConAppCo Role TyCon [Coercion] -- lift TyConApp
1120 -- The TyCon is never a synonym;
1121 -- we expand synonyms eagerly
1122 -- But it can be a type function
1123 -- TyCon is never a saturated (->); use FunCo instead
1124
1125 | AppCo Coercion CoercionN -- lift AppTy
1126 -- AppCo :: e -> N -> e
1127
1128 -- See Note [Forall coercions]
1129 | ForAllCo TyCoVar KindCoercion Coercion
1130 -- ForAllCo :: _ -> N -> e -> e
1131
1132 | FunCo Role CoercionN Coercion Coercion -- lift FunTy
1133 -- FunCo :: "e" -> N -> e -> e -> e
1134 -- Note: why doesn't FunCo have a AnonArgFlag, like FunTy?
1135 -- Because the AnonArgFlag has no impact on Core; it is only
1136 -- there to guide implicit instantiation of Haskell source
1137 -- types, and that is irrelevant for coercions, which are
1138 -- Core-only.
1139
1140 -- These are special
1141 | CoVarCo CoVar -- :: _ -> (N or R)
1142 -- result role depends on the tycon of the variable's type
1143
1144 -- AxiomInstCo :: e -> _ -> ?? -> e
1145 | AxiomInstCo (CoAxiom Branched) BranchIndex [Coercion]
1146 -- See also [CoAxiom index]
1147 -- The coercion arguments always *precisely* saturate
1148 -- arity of (that branch of) the CoAxiom. If there are
1149 -- any left over, we use AppCo.
1150 -- See [Coercion axioms applied to coercions]
1151 -- The roles of the argument coercions are determined
1152 -- by the cab_roles field of the relevant branch of the CoAxiom
1153
1154 | AxiomRuleCo CoAxiomRule [Coercion]
1155 -- AxiomRuleCo is very like AxiomInstCo, but for a CoAxiomRule
1156 -- The number coercions should match exactly the expectations
1157 -- of the CoAxiomRule (i.e., the rule is fully saturated).
1158
1159 | UnivCo UnivCoProvenance Role Type Type
1160 -- :: _ -> "e" -> _ -> _ -> e
1161
1162 | SymCo Coercion -- :: e -> e
1163 | TransCo Coercion Coercion -- :: e -> e -> e
1164
1165 | NthCo Role Int Coercion -- Zero-indexed; decomposes (T t0 ... tn)
1166 -- :: "e" -> _ -> e0 -> e (inverse of TyConAppCo, see Note [TyConAppCo roles])
1167 -- Using NthCo on a ForAllCo gives an N coercion always
1168 -- See Note [NthCo and newtypes]
1169 --
1170 -- Invariant: (NthCo r i co), it is always the case that r = role of (Nth i co)
1171 -- That is: the role of the entire coercion is redundantly cached here.
1172 -- See Note [NthCo Cached Roles]
1173
1174 | LRCo LeftOrRight CoercionN -- Decomposes (t_left t_right)
1175 -- :: _ -> N -> N
1176 | InstCo Coercion CoercionN
1177 -- :: e -> N -> e
1178 -- See Note [InstCo roles]
1179
1180 -- Extract a kind coercion from a (heterogeneous) type coercion
1181 -- NB: all kind coercions are Nominal
1182 | KindCo Coercion
1183 -- :: e -> N
1184
1185 | SubCo CoercionN -- Turns a ~N into a ~R
1186 -- :: N -> R
1187
1188 | HoleCo CoercionHole -- ^ See Note [Coercion holes]
1189 -- Only present during typechecking
1190 deriving Data.Data
1191
1192 type CoercionN = Coercion -- always nominal
1193 type CoercionR = Coercion -- always representational
1194 type CoercionP = Coercion -- always phantom
1195 type KindCoercion = CoercionN -- always nominal
1196
1197 instance Outputable Coercion where
1198 ppr = pprCo
1199
1200 -- | A semantically more meaningful type to represent what may or may not be a
1201 -- useful 'Coercion'.
1202 data MCoercion
1203 = MRefl
1204 -- A trivial Reflexivity coercion
1205 | MCo Coercion
1206 -- Other coercions
1207 deriving Data.Data
1208 type MCoercionR = MCoercion
1209 type MCoercionN = MCoercion
1210
1211 instance Outputable MCoercion where
1212 ppr MRefl = text "MRefl"
1213 ppr (MCo co) = text "MCo" <+> ppr co
1214
1215 {- Note [Refl invariant]
1216 ~~~~~~~~~~~~~~~~~~~~~~~~
1217 Invariant 1: Refl lifting
1218 Refl (similar for GRefl r ty MRefl) is always lifted as far as possible.
1219 For example
1220 (Refl T) (Refl a) (Refl b) is normalised (by mkAPpCo) to (Refl (T a b)).
1221
1222 You might think that a consequences is:
1223 Every identity coercion has Refl at the root
1224
1225 But that's not quite true because of coercion variables. Consider
1226 g where g :: Int~Int
1227 Left h where h :: Maybe Int ~ Maybe Int
1228 etc. So the consequence is only true of coercions that
1229 have no coercion variables.
1230
1231 Invariant 2: TyConAppCo
1232 An application of (Refl T) to some coercions, at least one of which is
1233 NOT the identity, is normalised to TyConAppCo. (They may not be
1234 fully saturated however.) TyConAppCo coercions (like all coercions
1235 other than Refl) are NEVER the identity.
1236
1237 Note [Generalized reflexive coercion]
1238 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1239 GRefl is a generalized reflexive coercion (see #15192). It wraps a kind
1240 coercion, which might be reflexive (MRefl) or any coercion (MCo co). The typing
1241 rules for GRefl:
1242
1243 ty : k1
1244 ------------------------------------
1245 GRefl r ty MRefl: ty ~r ty
1246
1247 ty : k1 co :: k1 ~ k2
1248 ------------------------------------
1249 GRefl r ty (MCo co) : ty ~r ty |> co
1250
1251 Consider we have
1252
1253 g1 :: s ~r t
1254 s :: k1
1255 g2 :: k1 ~ k2
1256
1257 and we want to construct a coercions co which has type
1258
1259 (s |> g2) ~r t
1260
1261 We can define
1262
1263 co = Sym (GRefl r s g2) ; g1
1264
1265 It is easy to see that
1266
1267 Refl == GRefl Nominal ty MRefl :: ty ~n ty
1268
1269 A nominal reflexive coercion is quite common, so we keep the special form Refl to
1270 save allocation.
1271
1272 Note [Coercion axioms applied to coercions]
1273 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1274 The reason coercion axioms can be applied to coercions and not just
1275 types is to allow for better optimization. There are some cases where
1276 we need to be able to "push transitivity inside" an axiom in order to
1277 expose further opportunities for optimization.
1278
1279 For example, suppose we have
1280
1281 C a : t[a] ~ F a
1282 g : b ~ c
1283
1284 and we want to optimize
1285
1286 sym (C b) ; t[g] ; C c
1287
1288 which has the kind
1289
1290 F b ~ F c
1291
1292 (stopping through t[b] and t[c] along the way).
1293
1294 We'd like to optimize this to just F g -- but how? The key is
1295 that we need to allow axioms to be instantiated by *coercions*,
1296 not just by types. Then we can (in certain cases) push
1297 transitivity inside the axiom instantiations, and then react
1298 opposite-polarity instantiations of the same axiom. In this
1299 case, e.g., we match t[g] against the LHS of (C c)'s kind, to
1300 obtain the substitution a |-> g (note this operation is sort
1301 of the dual of lifting!) and hence end up with
1302
1303 C g : t[b] ~ F c
1304
1305 which indeed has the same kind as t[g] ; C c.
1306
1307 Now we have
1308
1309 sym (C b) ; C g
1310
1311 which can be optimized to F g.
1312
1313 Note [CoAxiom index]
1314 ~~~~~~~~~~~~~~~~~~~~
1315 A CoAxiom has 1 or more branches. Each branch has contains a list
1316 of the free type variables in that branch, the LHS type patterns,
1317 and the RHS type for that branch. When we apply an axiom to a list
1318 of coercions, we must choose which branch of the axiom we wish to
1319 use, as the different branches may have different numbers of free
1320 type variables. (The number of type patterns is always the same
1321 among branches, but that doesn't quite concern us here.)
1322
1323 The Int in the AxiomInstCo constructor is the 0-indexed number
1324 of the chosen branch.
1325
1326 Note [Forall coercions]
1327 ~~~~~~~~~~~~~~~~~~~~~~~
1328 Constructing coercions between forall-types can be a bit tricky,
1329 because the kinds of the bound tyvars can be different.
1330
1331 The typing rule is:
1332
1333
1334 kind_co : k1 ~ k2
1335 tv1:k1 |- co : t1 ~ t2
1336 -------------------------------------------------------------------
1337 ForAllCo tv1 kind_co co : all tv1:k1. t1 ~
1338 all tv1:k2. (t2[tv1 |-> tv1 |> sym kind_co])
1339
1340 First, the TyCoVar stored in a ForAllCo is really an optimisation: this field
1341 should be a Name, as its kind is redundant. Thinking of the field as a Name
1342 is helpful in understanding what a ForAllCo means.
1343 The kind of TyCoVar always matches the left-hand kind of the coercion.
1344
1345 The idea is that kind_co gives the two kinds of the tyvar. See how, in the
1346 conclusion, tv1 is assigned kind k1 on the left but kind k2 on the right.
1347
1348 Of course, a type variable can't have different kinds at the same time. So,
1349 we arbitrarily prefer the first kind when using tv1 in the inner coercion
1350 co, which shows that t1 equals t2.
1351
1352 The last wrinkle is that we need to fix the kinds in the conclusion. In
1353 t2, tv1 is assumed to have kind k1, but it has kind k2 in the conclusion of
1354 the rule. So we do a kind-fixing substitution, replacing (tv1:k1) with
1355 (tv1:k2) |> sym kind_co. This substitution is slightly bizarre, because it
1356 mentions the same name with different kinds, but it *is* well-kinded, noting
1357 that `(tv1:k2) |> sym kind_co` has kind k1.
1358
1359 This all really would work storing just a Name in the ForAllCo. But we can't
1360 add Names to, e.g., VarSets, and there generally is just an impedance mismatch
1361 in a bunch of places. So we use tv1. When we need tv2, we can use
1362 setTyVarKind.
1363
1364 Note [Predicate coercions]
1365 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1366 Suppose we have
1367 g :: a~b
1368 How can we coerce between types
1369 ([c]~a) => [a] -> c
1370 and
1371 ([c]~b) => [b] -> c
1372 where the equality predicate *itself* differs?
1373
1374 Answer: we simply treat (~) as an ordinary type constructor, so these
1375 types really look like
1376
1377 ((~) [c] a) -> [a] -> c
1378 ((~) [c] b) -> [b] -> c
1379
1380 So the coercion between the two is obviously
1381
1382 ((~) [c] g) -> [g] -> c
1383
1384 Another way to see this to say that we simply collapse predicates to
1385 their representation type (see Type.coreView and Type.predTypeRep).
1386
1387 This collapse is done by mkPredCo; there is no PredCo constructor
1388 in Coercion. This is important because we need Nth to work on
1389 predicates too:
1390 Nth 1 ((~) [c] g) = g
1391 See Simplify.simplCoercionF, which generates such selections.
1392
1393 Note [Roles]
1394 ~~~~~~~~~~~~
1395 Roles are a solution to the GeneralizedNewtypeDeriving problem, articulated
1396 in #1496. The full story is in docs/core-spec/core-spec.pdf. Also, see
1397 https://gitlab.haskell.org/ghc/ghc/wikis/roles-implementation
1398
1399 Here is one way to phrase the problem:
1400
1401 Given:
1402 newtype Age = MkAge Int
1403 type family F x
1404 type instance F Age = Bool
1405 type instance F Int = Char
1406
1407 This compiles down to:
1408 axAge :: Age ~ Int
1409 axF1 :: F Age ~ Bool
1410 axF2 :: F Int ~ Char
1411
1412 Then, we can make:
1413 (sym (axF1) ; F axAge ; axF2) :: Bool ~ Char
1414
1415 Yikes!
1416
1417 The solution is _roles_, as articulated in "Generative Type Abstraction and
1418 Type-level Computation" (POPL 2010), available at
1419 http://www.seas.upenn.edu/~sweirich/papers/popl163af-weirich.pdf
1420
1421 The specification for roles has evolved somewhat since that paper. For the
1422 current full details, see the documentation in docs/core-spec. Here are some
1423 highlights.
1424
1425 We label every equality with a notion of type equivalence, of which there are
1426 three options: Nominal, Representational, and Phantom. A ground type is
1427 nominally equivalent only with itself. A newtype (which is considered a ground
1428 type in Haskell) is representationally equivalent to its representation.
1429 Anything is "phantomly" equivalent to anything else. We use "N", "R", and "P"
1430 to denote the equivalences.
1431
1432 The axioms above would be:
1433 axAge :: Age ~R Int
1434 axF1 :: F Age ~N Bool
1435 axF2 :: F Age ~N Char
1436
1437 Then, because transitivity applies only to coercions proving the same notion
1438 of equivalence, the above construction is impossible.
1439
1440 However, there is still an escape hatch: we know that any two types that are
1441 nominally equivalent are representationally equivalent as well. This is what
1442 the form SubCo proves -- it "demotes" a nominal equivalence into a
1443 representational equivalence. So, it would seem the following is possible:
1444
1445 sub (sym axF1) ; F axAge ; sub axF2 :: Bool ~R Char -- WRONG
1446
1447 What saves us here is that the arguments to a type function F, lifted into a
1448 coercion, *must* prove nominal equivalence. So, (F axAge) is ill-formed, and
1449 we are safe.
1450
1451 Roles are attached to parameters to TyCons. When lifting a TyCon into a
1452 coercion (through TyConAppCo), we need to ensure that the arguments to the
1453 TyCon respect their roles. For example:
1454
1455 data T a b = MkT a (F b)
1456
1457 If we know that a1 ~R a2, then we know (T a1 b) ~R (T a2 b). But, if we know
1458 that b1 ~R b2, we know nothing about (T a b1) and (T a b2)! This is because
1459 the type function F branches on b's *name*, not representation. So, we say
1460 that 'a' has role Representational and 'b' has role Nominal. The third role,
1461 Phantom, is for parameters not used in the type's definition. Given the
1462 following definition
1463
1464 data Q a = MkQ Int
1465
1466 the Phantom role allows us to say that (Q Bool) ~R (Q Char), because we
1467 can construct the coercion Bool ~P Char (using UnivCo).
1468
1469 See the paper cited above for more examples and information.
1470
1471 Note [TyConAppCo roles]
1472 ~~~~~~~~~~~~~~~~~~~~~~~
1473 The TyConAppCo constructor has a role parameter, indicating the role at
1474 which the coercion proves equality. The choice of this parameter affects
1475 the required roles of the arguments of the TyConAppCo. To help explain
1476 it, assume the following definition:
1477
1478 type instance F Int = Bool -- Axiom axF : F Int ~N Bool
1479 newtype Age = MkAge Int -- Axiom axAge : Age ~R Int
1480 data Foo a = MkFoo a -- Role on Foo's parameter is Representational
1481
1482 TyConAppCo Nominal Foo axF : Foo (F Int) ~N Foo Bool
1483 For (TyConAppCo Nominal) all arguments must have role Nominal. Why?
1484 So that Foo Age ~N Foo Int does *not* hold.
1485
1486 TyConAppCo Representational Foo (SubCo axF) : Foo (F Int) ~R Foo Bool
1487 TyConAppCo Representational Foo axAge : Foo Age ~R Foo Int
1488 For (TyConAppCo Representational), all arguments must have the roles
1489 corresponding to the result of tyConRoles on the TyCon. This is the
1490 whole point of having roles on the TyCon to begin with. So, we can
1491 have Foo Age ~R Foo Int, if Foo's parameter has role R.
1492
1493 If a Representational TyConAppCo is over-saturated (which is otherwise fine),
1494 the spill-over arguments must all be at Nominal. This corresponds to the
1495 behavior for AppCo.
1496
1497 TyConAppCo Phantom Foo (UnivCo Phantom Int Bool) : Foo Int ~P Foo Bool
1498 All arguments must have role Phantom. This one isn't strictly
1499 necessary for soundness, but this choice removes ambiguity.
1500
1501 The rules here dictate the roles of the parameters to mkTyConAppCo
1502 (should be checked by Lint).
1503
1504 Note [NthCo and newtypes]
1505 ~~~~~~~~~~~~~~~~~~~~~~~~~
1506 Suppose we have
1507
1508 newtype N a = MkN Int
1509 type role N representational
1510
1511 This yields axiom
1512
1513 NTCo:N :: forall a. N a ~R Int
1514
1515 We can then build
1516
1517 co :: forall a b. N a ~R N b
1518 co = NTCo:N a ; sym (NTCo:N b)
1519
1520 for any `a` and `b`. Because of the role annotation on N, if we use
1521 NthCo, we'll get out a representational coercion. That is:
1522
1523 NthCo r 0 co :: forall a b. a ~R b
1524
1525 Yikes! Clearly, this is terrible. The solution is simple: forbid
1526 NthCo to be used on newtypes if the internal coercion is representational.
1527
1528 This is not just some corner case discovered by a segfault somewhere;
1529 it was discovered in the proof of soundness of roles and described
1530 in the "Safe Coercions" paper (ICFP '14).
1531
1532 Note [NthCo Cached Roles]
1533 ~~~~~~~~~~~~~~~~~~~~~~~~~
1534 Why do we cache the role of NthCo in the NthCo constructor?
1535 Because computing role(Nth i co) involves figuring out that
1536
1537 co :: T tys1 ~ T tys2
1538
1539 using coercionKind, and finding (coercionRole co), and then looking
1540 at the tyConRoles of T. Avoiding bad asymptotic behaviour here means
1541 we have to compute the kind and role of a coercion simultaneously,
1542 which makes the code complicated and inefficient.
1543
1544 This only happens for NthCo. Caching the role solves the problem, and
1545 allows coercionKind and coercionRole to be simple.
1546
1547 See #11735
1548
1549 Note [InstCo roles]
1550 ~~~~~~~~~~~~~~~~~~~
1551 Here is (essentially) the typing rule for InstCo:
1552
1553 g :: (forall a. t1) ~r (forall a. t2)
1554 w :: s1 ~N s2
1555 ------------------------------- InstCo
1556 InstCo g w :: (t1 [a |-> s1]) ~r (t2 [a |-> s2])
1557
1558 Note that the Coercion w *must* be nominal. This is necessary
1559 because the variable a might be used in a "nominal position"
1560 (that is, a place where role inference would require a nominal
1561 role) in t1 or t2. If we allowed w to be representational, we
1562 could get bogus equalities.
1563
1564 A more nuanced treatment might be able to relax this condition
1565 somewhat, by checking if t1 and/or t2 use their bound variables
1566 in nominal ways. If not, having w be representational is OK.
1567
1568
1569 %************************************************************************
1570 %* *
1571 UnivCoProvenance
1572 %* *
1573 %************************************************************************
1574
1575 A UnivCo is a coercion whose proof does not directly express its role
1576 and kind (indeed for some UnivCos, like PluginProv, there /is/ no proof).
1577
1578 The different kinds of UnivCo are described by UnivCoProvenance. Really
1579 each is entirely separate, but they all share the need to represent their
1580 role and kind, which is done in the UnivCo constructor.
1581
1582 -}
1583
1584 -- | For simplicity, we have just one UnivCo that represents a coercion from
1585 -- some type to some other type, with (in general) no restrictions on the
1586 -- type. The UnivCoProvenance specifies more exactly what the coercion really
1587 -- is and why a program should (or shouldn't!) trust the coercion.
1588 -- It is reasonable to consider each constructor of 'UnivCoProvenance'
1589 -- as a totally independent coercion form; their only commonality is
1590 -- that they don't tell you what types they coercion between. (That info
1591 -- is in the 'UnivCo' constructor of 'Coercion'.
1592 data UnivCoProvenance
1593 = PhantomProv KindCoercion -- ^ See Note [Phantom coercions]. Only in Phantom
1594 -- roled coercions
1595
1596 | ProofIrrelProv KindCoercion -- ^ From the fact that any two coercions are
1597 -- considered equivalent. See Note [ProofIrrelProv].
1598 -- Can be used in Nominal or Representational coercions
1599
1600 | PluginProv String -- ^ From a plugin, which asserts that this coercion
1601 -- is sound. The string is for the use of the plugin.
1602
1603 | CorePrepProv -- See Note [Unsafe coercions] in GHC.Core.CoreToStg.Prep
1604 Bool -- True <=> the UnivCo must be homogeneously kinded
1605 -- False <=> allow hetero-kinded, e.g. Int ~ Int#
1606
1607 deriving Data.Data
1608
1609 instance Outputable UnivCoProvenance where
1610 ppr (PhantomProv _) = text "(phantom)"
1611 ppr (ProofIrrelProv _) = text "(proof irrel.)"
1612 ppr (PluginProv str) = parens (text "plugin" <+> brackets (text str))
1613 ppr (CorePrepProv _) = text "(CorePrep)"
1614
1615 -- | A coercion to be filled in by the type-checker. See Note [Coercion holes]
1616 data CoercionHole
1617 = CoercionHole { ch_co_var :: CoVar
1618 -- See Note [CoercionHoles and coercion free variables]
1619
1620 , ch_ref :: IORef (Maybe Coercion)
1621 }
1622
1623 coHoleCoVar :: CoercionHole -> CoVar
1624 coHoleCoVar = ch_co_var
1625
1626 setCoHoleCoVar :: CoercionHole -> CoVar -> CoercionHole
1627 setCoHoleCoVar h cv = h { ch_co_var = cv }
1628
1629 instance Data.Data CoercionHole where
1630 -- don't traverse?
1631 toConstr _ = abstractConstr "CoercionHole"
1632 gunfold _ _ = error "gunfold"
1633 dataTypeOf _ = mkNoRepType "CoercionHole"
1634
1635 instance Outputable CoercionHole where
1636 ppr (CoercionHole { ch_co_var = cv }) = braces (ppr cv)
1637
1638 instance Uniquable CoercionHole where
1639 getUnique (CoercionHole { ch_co_var = cv }) = getUnique cv
1640
1641 {- Note [Phantom coercions]
1642 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1643 Consider
1644 data T a = T1 | T2
1645 Then we have
1646 T s ~R T t
1647 for any old s,t. The witness for this is (TyConAppCo T Rep co),
1648 where (co :: s ~P t) is a phantom coercion built with PhantomProv.
1649 The role of the UnivCo is always Phantom. The Coercion stored is the
1650 (nominal) kind coercion between the types
1651 kind(s) ~N kind (t)
1652
1653 Note [Coercion holes]
1654 ~~~~~~~~~~~~~~~~~~~~~~~~
1655 During typechecking, constraint solving for type classes works by
1656 - Generate an evidence Id, d7 :: Num a
1657 - Wrap it in a Wanted constraint, [W] d7 :: Num a
1658 - Use the evidence Id where the evidence is needed
1659 - Solve the constraint later
1660 - When solved, add an enclosing let-binding let d7 = .... in ....
1661 which actually binds d7 to the (Num a) evidence
1662
1663 For equality constraints we use a different strategy. See Note [The
1664 equality types story] in GHC.Builtin.Types.Prim for background on equality constraints.
1665 - For /boxed/ equality constraints, (t1 ~N t2) and (t1 ~R t2), it's just
1666 like type classes above. (Indeed, boxed equality constraints *are* classes.)
1667 - But for /unboxed/ equality constraints (t1 ~R# t2) and (t1 ~N# t2)
1668 we use a different plan
1669
1670 For unboxed equalities:
1671 - Generate a CoercionHole, a mutable variable just like a unification
1672 variable
1673 - Wrap the CoercionHole in a Wanted constraint; see GHC.Tc.Utils.TcEvDest
1674 - Use the CoercionHole in a Coercion, via HoleCo
1675 - Solve the constraint later
1676 - When solved, fill in the CoercionHole by side effect, instead of
1677 doing the let-binding thing
1678
1679 The main reason for all this is that there may be no good place to let-bind
1680 the evidence for unboxed equalities:
1681
1682 - We emit constraints for kind coercions, to be used to cast a
1683 type's kind. These coercions then must be used in types. Because
1684 they might appear in a top-level type, there is no place to bind
1685 these (unlifted) coercions in the usual way.
1686
1687 - A coercion for (forall a. t1) ~ (forall a. t2) will look like
1688 forall a. (coercion for t1~t2)
1689 But the coercion for (t1~t2) may mention 'a', and we don't have
1690 let-bindings within coercions. We could add them, but coercion
1691 holes are easier.
1692
1693 - Moreover, nothing is lost from the lack of let-bindings. For
1694 dictionaries want to achieve sharing to avoid recomoputing the
1695 dictionary. But coercions are entirely erased, so there's little
1696 benefit to sharing. Indeed, even if we had a let-binding, we
1697 always inline types and coercions at every use site and drop the
1698 binding.
1699
1700 Other notes about HoleCo:
1701
1702 * INVARIANT: CoercionHole and HoleCo are used only during type checking,
1703 and should never appear in Core. Just like unification variables; a Type
1704 can contain a TcTyVar, but only during type checking. If, one day, we
1705 use type-level information to separate out forms that can appear during
1706 type-checking vs forms that can appear in core proper, holes in Core will
1707 be ruled out.
1708
1709 * See Note [CoercionHoles and coercion free variables]
1710
1711 * Coercion holes can be compared for equality like other coercions:
1712 by looking at the types coerced.
1713
1714
1715 Note [CoercionHoles and coercion free variables]
1716 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1717 Why does a CoercionHole contain a CoVar, as well as reference to
1718 fill in? Because we want to treat that CoVar as a free variable of
1719 the coercion. See #14584, and Note [What prevents a
1720 constraint from floating] in GHC.Tc.Solver, item (4):
1721
1722 forall k. [W] co1 :: t1 ~# t2 |> co2
1723 [W] co2 :: k ~# *
1724
1725 Here co2 is a CoercionHole. But we /must/ know that it is free in
1726 co1, because that's all that stops it floating outside the
1727 implication.
1728
1729
1730 Note [ProofIrrelProv]
1731 ~~~~~~~~~~~~~~~~~~~~~
1732 A ProofIrrelProv is a coercion between coercions. For example:
1733
1734 data G a where
1735 MkG :: G Bool
1736
1737 In core, we get
1738
1739 G :: * -> *
1740 MkG :: forall (a :: *). (a ~ Bool) -> G a
1741
1742 Now, consider 'MkG -- that is, MkG used in a type -- and suppose we want
1743 a proof that ('MkG a1 co1) ~ ('MkG a2 co2). This will have to be
1744
1745 TyConAppCo Nominal MkG [co3, co4]
1746 where
1747 co3 :: co1 ~ co2
1748 co4 :: a1 ~ a2
1749
1750 Note that
1751 co1 :: a1 ~ Bool
1752 co2 :: a2 ~ Bool
1753
1754 Here,
1755 co3 = UnivCo (ProofIrrelProv co5) Nominal (CoercionTy co1) (CoercionTy co2)
1756 where
1757 co5 :: (a1 ~ Bool) ~ (a2 ~ Bool)
1758 co5 = TyConAppCo Nominal (~#) [<*>, <*>, co4, <Bool>]
1759 -}
1760
1761
1762 {- *********************************************************************
1763 * *
1764 foldType and foldCoercion
1765 * *
1766 ********************************************************************* -}
1767
1768 {- Note [foldType]
1769 ~~~~~~~~~~~~~~~~~~
1770 foldType is a bit more powerful than perhaps it looks:
1771
1772 * You can fold with an accumulating parameter, via
1773 TyCoFolder env (Endo a)
1774 Recall newtype Endo a = Endo (a->a)
1775
1776 * You can fold monadically with a monad M, via
1777 TyCoFolder env (M a)
1778 provided you have
1779 instance .. => Monoid (M a)
1780
1781 Note [mapType vs foldType]
1782 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1783 We define foldType here, but mapType in module Type. Why?
1784
1785 * foldType is used in GHC.Core.TyCo.FVs for finding free variables.
1786 It's a very simple function that analyses a type,
1787 but does not construct one.
1788
1789 * mapType constructs new types, and so it needs to call
1790 the "smart constructors", mkAppTy, mkCastTy, and so on.
1791 These are sophisticated functions, and can't be defined
1792 here in GHC.Core.TyCo.Rep.
1793
1794 Note [Specialising foldType]
1795 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1796 We inline foldType at every call site (there are not many), so that it
1797 becomes specialised for the particular monoid *and* TyCoFolder at
1798 that site. This is just for efficiency, but walking over types is
1799 done a *lot* in GHC, so worth optimising.
1800
1801 We were worried that
1802 TyCoFolder env (Endo a)
1803 might not eta-expand. Recall newtype Endo a = Endo (a->a).
1804
1805 In particular, given
1806 fvs :: Type -> TyCoVarSet
1807 fvs ty = appEndo (foldType tcf emptyVarSet ty) emptyVarSet
1808
1809 tcf :: TyCoFolder enf (Endo a)
1810 tcf = TyCoFolder { tcf_tyvar = do_tv, ... }
1811 where
1812 do_tvs is tv = Endo do_it
1813 where
1814 do_it acc | tv `elemVarSet` is = acc
1815 | tv `elemVarSet` acc = acc
1816 | otherwise = acc `extendVarSet` tv
1817
1818
1819 we want to end up with
1820 fvs ty = go emptyVarSet ty emptyVarSet
1821 where
1822 go env (TyVarTy tv) acc = acc `extendVarSet` tv
1823 ..etc..
1824
1825 And indeed this happens.
1826 - Selections from 'tcf' are done at compile time
1827 - 'go' is nicely eta-expanded.
1828
1829 We were also worried about
1830 deep_fvs :: Type -> TyCoVarSet
1831 deep_fvs ty = appEndo (foldType deep_tcf emptyVarSet ty) emptyVarSet
1832
1833 deep_tcf :: TyCoFolder enf (Endo a)
1834 deep_tcf = TyCoFolder { tcf_tyvar = do_tv, ... }
1835 where
1836 do_tvs is tv = Endo do_it
1837 where
1838 do_it acc | tv `elemVarSet` is = acc
1839 | tv `elemVarSet` acc = acc
1840 | otherwise = deep_fvs (varType tv)
1841 `unionVarSet` acc
1842 `extendVarSet` tv
1843
1844 Here deep_fvs and deep_tcf are mutually recursive, unlike fvs and tcf.
1845 But, amazingly, we get good code here too. GHC is careful not to makr
1846 TyCoFolder data constructor for deep_tcf as a loop breaker, so the
1847 record selections still cancel. And eta expansion still happens too.
1848 -}
1849
1850 data TyCoFolder env a
1851 = TyCoFolder
1852 { tcf_view :: Type -> Maybe Type -- Optional "view" function
1853 -- E.g. expand synonyms
1854 , tcf_tyvar :: env -> TyVar -> a
1855 , tcf_covar :: env -> CoVar -> a
1856 , tcf_hole :: env -> CoercionHole -> a
1857 -- ^ What to do with coercion holes.
1858 -- See Note [Coercion holes] in "GHC.Core.TyCo.Rep".
1859
1860 , tcf_tycobinder :: env -> TyCoVar -> ArgFlag -> env
1861 -- ^ The returned env is used in the extended scope
1862 }
1863
1864 {-# INLINE foldTyCo #-} -- See Note [Specialising foldType]
1865 foldTyCo :: Monoid a => TyCoFolder env a -> env
1866 -> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
1867 foldTyCo (TyCoFolder { tcf_view = view
1868 , tcf_tyvar = tyvar
1869 , tcf_tycobinder = tycobinder
1870 , tcf_covar = covar
1871 , tcf_hole = cohole }) env
1872 = (go_ty env, go_tys env, go_co env, go_cos env)
1873 where
1874 go_ty env ty | Just ty' <- view ty = go_ty env ty'
1875 go_ty env (TyVarTy tv) = tyvar env tv
1876 go_ty env (AppTy t1 t2) = go_ty env t1 `mappend` go_ty env t2
1877 go_ty _ (LitTy {}) = mempty
1878 go_ty env (CastTy ty co) = go_ty env ty `mappend` go_co env co
1879 go_ty env (CoercionTy co) = go_co env co
1880 go_ty env (FunTy _ w arg res) = go_ty env w `mappend` go_ty env arg `mappend` go_ty env res
1881 go_ty env (TyConApp _ tys) = go_tys env tys
1882 go_ty env (ForAllTy (Bndr tv vis) inner)
1883 = let !env' = tycobinder env tv vis -- Avoid building a thunk here
1884 in go_ty env (varType tv) `mappend` go_ty env' inner
1885
1886 -- Explicit recursion because using foldr builds a local
1887 -- loop (with env free) and I'm not confident it'll be
1888 -- lambda lifted in the end
1889 go_tys _ [] = mempty
1890 go_tys env (t:ts) = go_ty env t `mappend` go_tys env ts
1891
1892 go_cos _ [] = mempty
1893 go_cos env (c:cs) = go_co env c `mappend` go_cos env cs
1894
1895 go_co env (Refl ty) = go_ty env ty
1896 go_co env (GRefl _ ty MRefl) = go_ty env ty
1897 go_co env (GRefl _ ty (MCo co)) = go_ty env ty `mappend` go_co env co
1898 go_co env (TyConAppCo _ _ args) = go_cos env args
1899 go_co env (AppCo c1 c2) = go_co env c1 `mappend` go_co env c2
1900 go_co env (FunCo _ cw c1 c2) = go_co env cw `mappend`
1901 go_co env c1 `mappend`
1902 go_co env c2
1903 go_co env (CoVarCo cv) = covar env cv
1904 go_co env (AxiomInstCo _ _ args) = go_cos env args
1905 go_co env (HoleCo hole) = cohole env hole
1906 go_co env (UnivCo p _ t1 t2) = go_prov env p `mappend` go_ty env t1
1907 `mappend` go_ty env t2
1908 go_co env (SymCo co) = go_co env co
1909 go_co env (TransCo c1 c2) = go_co env c1 `mappend` go_co env c2
1910 go_co env (AxiomRuleCo _ cos) = go_cos env cos
1911 go_co env (NthCo _ _ co) = go_co env co
1912 go_co env (LRCo _ co) = go_co env co
1913 go_co env (InstCo co arg) = go_co env co `mappend` go_co env arg
1914 go_co env (KindCo co) = go_co env co
1915 go_co env (SubCo co) = go_co env co
1916 go_co env (ForAllCo tv kind_co co)
1917 = go_co env kind_co `mappend` go_ty env (varType tv)
1918 `mappend` go_co env' co
1919 where
1920 env' = tycobinder env tv Inferred
1921
1922 go_prov env (PhantomProv co) = go_co env co
1923 go_prov env (ProofIrrelProv co) = go_co env co
1924 go_prov _ (PluginProv _) = mempty
1925 go_prov _ (CorePrepProv _) = mempty
1926
1927 {- *********************************************************************
1928 * *
1929 typeSize, coercionSize
1930 * *
1931 ********************************************************************* -}
1932
1933 -- NB: We put typeSize/coercionSize here because they are mutually
1934 -- recursive, and have the CPR property. If we have mutual
1935 -- recursion across a hi-boot file, we don't get the CPR property
1936 -- and these functions allocate a tremendous amount of rubbish.
1937 -- It's not critical (because typeSize is really only used in
1938 -- debug mode, but I tripped over an example (T5642) in which
1939 -- typeSize was one of the biggest single allocators in all of GHC.
1940 -- And it's easy to fix, so I did.
1941
1942 -- NB: typeSize does not respect `eqType`, in that two types that
1943 -- are `eqType` may return different sizes. This is OK, because this
1944 -- function is used only in reporting, not decision-making.
1945
1946 typeSize :: Type -> Int
1947 typeSize (LitTy {}) = 1
1948 typeSize (TyVarTy {}) = 1
1949 typeSize (AppTy t1 t2) = typeSize t1 + typeSize t2
1950 typeSize (FunTy _ _ t1 t2) = typeSize t1 + typeSize t2
1951 typeSize (ForAllTy (Bndr tv _) t) = typeSize (varType tv) + typeSize t
1952 typeSize (TyConApp _ ts) = 1 + sum (map typeSize ts)
1953 typeSize (CastTy ty co) = typeSize ty + coercionSize co
1954 typeSize (CoercionTy co) = coercionSize co
1955
1956 coercionSize :: Coercion -> Int
1957 coercionSize (Refl ty) = typeSize ty
1958 coercionSize (GRefl _ ty MRefl) = typeSize ty
1959 coercionSize (GRefl _ ty (MCo co)) = 1 + typeSize ty + coercionSize co
1960 coercionSize (TyConAppCo _ _ args) = 1 + sum (map coercionSize args)
1961 coercionSize (AppCo co arg) = coercionSize co + coercionSize arg
1962 coercionSize (ForAllCo _ h co) = 1 + coercionSize co + coercionSize h
1963 coercionSize (FunCo _ w co1 co2) = 1 + coercionSize co1 + coercionSize co2
1964 + coercionSize w
1965 coercionSize (CoVarCo _) = 1
1966 coercionSize (HoleCo _) = 1
1967 coercionSize (AxiomInstCo _ _ args) = 1 + sum (map coercionSize args)
1968 coercionSize (UnivCo p _ t1 t2) = 1 + provSize p + typeSize t1 + typeSize t2
1969 coercionSize (SymCo co) = 1 + coercionSize co
1970 coercionSize (TransCo co1 co2) = 1 + coercionSize co1 + coercionSize co2
1971 coercionSize (NthCo _ _ co) = 1 + coercionSize co
1972 coercionSize (LRCo _ co) = 1 + coercionSize co
1973 coercionSize (InstCo co arg) = 1 + coercionSize co + coercionSize arg
1974 coercionSize (KindCo co) = 1 + coercionSize co
1975 coercionSize (SubCo co) = 1 + coercionSize co
1976 coercionSize (AxiomRuleCo _ cs) = 1 + sum (map coercionSize cs)
1977
1978 provSize :: UnivCoProvenance -> Int
1979 provSize (PhantomProv co) = 1 + coercionSize co
1980 provSize (ProofIrrelProv co) = 1 + coercionSize co
1981 provSize (PluginProv _) = 1
1982 provSize (CorePrepProv _) = 1
1983
1984 {-
1985 ************************************************************************
1986 * *
1987 Multiplicities
1988 * *
1989 ************************************************************************
1990
1991 These definitions are here to avoid module loops, and to keep
1992 GHC.Core.Multiplicity above this module.
1993
1994 -}
1995
1996 -- | A shorthand for data with an attached 'Mult' element (the multiplicity).
1997 data Scaled a = Scaled !Mult a
1998 deriving (Data.Data)
1999 -- You might think that this would be a natural candidate for
2000 -- Functor, Traversable but Krzysztof says (!3674) "it was too easy
2001 -- to accidentally lift functions (substitutions, zonking etc.) from
2002 -- Type -> Type to Scaled Type -> Scaled Type, ignoring
2003 -- multiplicities and causing bugs". So we don't.
2004 --
2005 -- Being strict in a is worse for performance, so we are only strict on the
2006 -- Mult part of scaled.
2007
2008
2009 instance (Outputable a) => Outputable (Scaled a) where
2010 ppr (Scaled _cnt t) = ppr t
2011 -- Do not print the multiplicity here because it tends to be too verbose
2012
2013 scaledMult :: Scaled a -> Mult
2014 scaledMult (Scaled m _) = m
2015
2016 scaledThing :: Scaled a -> a
2017 scaledThing (Scaled _ t) = t
2018
2019 -- | Apply a function to both the Mult and the Type in a 'Scaled Type'
2020 mapScaledType :: (Type -> Type) -> Scaled Type -> Scaled Type
2021 mapScaledType f (Scaled m t) = Scaled (f m) (f t)
2022
2023 {- |
2024 Mult is a type alias for Type.
2025
2026 Mult must contain Type because multiplicity variables are mere type variables
2027 (of kind Multiplicity) in Haskell. So the simplest implementation is to make
2028 Mult be Type.
2029
2030 Multiplicities can be formed with:
2031 - One: GHC.Types.One (= oneDataCon)
2032 - Many: GHC.Types.Many (= manyDataCon)
2033 - Multiplication: GHC.Types.MultMul (= multMulTyCon)
2034
2035 So that Mult feels a bit more structured, we provide pattern synonyms and smart
2036 constructors for these.
2037 -}
2038 type Mult = Type