af05d5c1f8dbedcf6c653eff3c0d2ea4312a1ce9
[ghc.git] / compiler / types / Coercion.hs
1 -- (c) The University of Glasgow 2006
2
3 {-# LANGUAGE CPP, DeriveDataTypeable #-}
4
5 -- | Module for (a) type kinds and (b) type coercions,
6 -- as used in System FC. See 'CoreSyn.Expr' for
7 -- more on System FC and how coercions fit into it.
8 --
9 module Coercion (
10 -- * Main data type
11 Coercion(..), Var, CoVar,
12 LeftOrRight(..), pickLR,
13 Role(..), ltRole,
14
15 -- ** Functions over coercions
16 coVarKind, coVarRole,
17 coercionType, coercionKind, coercionKinds, isReflCo,
18 isReflCo_maybe, coercionRole, coercionKindRole,
19 mkCoercionType,
20
21 -- ** Constructing coercions
22 mkReflCo, mkCoVarCo,
23 mkAxInstCo, mkUnbranchedAxInstCo, mkAxInstLHS, mkAxInstRHS,
24 mkUnbranchedAxInstRHS,
25 mkPiCo, mkPiCos, mkCoCast,
26 mkSymCo, mkTransCo, mkNthCo, mkNthCoRole, mkLRCo,
27 mkInstCo, mkAppCo, mkAppCoFlexible, mkTyConAppCo, mkFunCo,
28 mkForAllCo, mkUnsafeCo, mkUnivCo, mkSubCo, mkPhantomCo,
29 mkNewTypeCo, downgradeRole,
30 mkAxiomRuleCo,
31
32 -- ** Decomposition
33 instNewTyCon_maybe,
34
35 NormaliseStepper, NormaliseStepResult(..), composeSteppers,
36 modifyStepResultCo, unwrapNewTypeStepper,
37 topNormaliseNewType_maybe, topNormaliseTypeX_maybe,
38
39 decomposeCo, getCoVar_maybe,
40 splitAppCo_maybe,
41 splitForAllCo_maybe,
42 nthRole, tyConRolesX,
43 setNominalRole_maybe,
44
45 -- ** Coercion variables
46 mkCoVar, isCoVar, isCoVarType, coVarName, setCoVarName, setCoVarUnique,
47
48 -- ** Free variables
49 tyCoVarsOfCo, tyCoVarsOfCos, coVarsOfCo, coercionSize,
50
51 -- ** Substitution
52 CvSubstEnv, emptyCvSubstEnv,
53 CvSubst(..), emptyCvSubst, Coercion.lookupTyVar, lookupCoVar,
54 isEmptyCvSubst, zapCvSubstEnv, getCvInScope,
55 substCo, substCos, substCoVar, substCoVars,
56 substCoWithTy, substCoWithTys,
57 cvTvSubst, tvCvSubst, mkCvSubst, zipOpenCvSubst,
58 substTy, extendTvSubst,
59 extendCvSubstAndInScope, extendTvSubstAndInScope,
60 substTyVarBndr, substCoVarBndr,
61
62 -- ** Lifting
63 liftCoMatch, liftCoSubstTyVar, liftCoSubstWith,
64
65 -- ** Comparison
66 coreEqCoercion, coreEqCoercion2,
67
68 -- ** Forcing evaluation of coercions
69 seqCo,
70
71 -- * Pretty-printing
72 pprCo, pprParendCo,
73 pprCoAxiom, pprCoAxBranch, pprCoAxBranchHdr,
74
75 -- * Tidying
76 tidyCo, tidyCos,
77
78 -- * Other
79 applyCo,
80 ) where
81
82 #include "HsVersions.h"
83
84 import Unify ( MatchEnv(..), matchList )
85 import TypeRep
86 import qualified Type
87 import Type hiding( substTy, substTyVarBndr, extendTvSubst )
88 import TyCon
89 import CoAxiom
90 import Var
91 import VarEnv
92 import VarSet
93 import Binary
94 import Maybes ( orElse )
95 import Name ( Name, NamedThing(..), nameUnique, nameModule, getSrcSpan )
96 import OccName ( parenSymOcc )
97 import Util
98 import BasicTypes
99 import Outputable
100 import Unique
101 import Pair
102 import SrcLoc
103 import PrelNames ( funTyConKey, eqPrimTyConKey, eqReprPrimTyConKey )
104 #if __GLASGOW_HASKELL__ < 709
105 import Control.Applicative hiding ( empty )
106 import Data.Traversable (traverse, sequenceA)
107 #endif
108 import FastString
109 import ListSetOps
110
111 import qualified Data.Data as Data hiding ( TyCon )
112 import Control.Arrow ( first )
113
114 {-
115 ************************************************************************
116 * *
117 Coercions
118 * *
119 ************************************************************************
120 -}
121
122 -- | A 'Coercion' is concrete evidence of the equality/convertibility
123 -- of two types.
124
125 -- If you edit this type, you may need to update the GHC formalism
126 -- See Note [GHC Formalism] in coreSyn/CoreLint.hs
127 data Coercion
128 -- Each constructor has a "role signature", indicating the way roles are
129 -- propagated through coercions. P, N, and R stand for coercions of the
130 -- given role. e stands for a coercion of a specific unknown role (think
131 -- "role polymorphism"). "e" stands for an explicit role parameter
132 -- indicating role e. _ stands for a parameter that is not a Role or
133 -- Coercion.
134
135 -- These ones mirror the shape of types
136 = -- Refl :: "e" -> _ -> e
137 Refl Role Type -- See Note [Refl invariant]
138 -- Invariant: applications of (Refl T) to a bunch of identity coercions
139 -- always show up as Refl.
140 -- For example (Refl T) (Refl a) (Refl b) shows up as (Refl (T a b)).
141
142 -- Applications of (Refl T) to some coercions, at least one of
143 -- which is NOT the identity, show up as TyConAppCo.
144 -- (They may not be fully saturated however.)
145 -- ConAppCo coercions (like all coercions other than Refl)
146 -- are NEVER the identity.
147
148 -- Use (Refl Representational _), not (SubCo (Refl Nominal _))
149
150 -- These ones simply lift the correspondingly-named
151 -- Type constructors into Coercions
152
153 -- TyConAppCo :: "e" -> _ -> ?? -> e
154 -- See Note [TyConAppCo roles]
155 | TyConAppCo Role TyCon [Coercion] -- lift TyConApp
156 -- The TyCon is never a synonym;
157 -- we expand synonyms eagerly
158 -- But it can be a type function
159
160 | AppCo Coercion Coercion -- lift AppTy
161 -- AppCo :: e -> N -> e
162
163 -- See Note [Forall coercions]
164 | ForAllCo TyVar Coercion -- forall a. g
165 -- :: _ -> e -> e
166
167 -- These are special
168 | CoVarCo CoVar -- :: _ -> (N or R)
169 -- result role depends on the tycon of the variable's type
170
171 -- AxiomInstCo :: e -> _ -> [N] -> e
172 | AxiomInstCo (CoAxiom Branched) BranchIndex [Coercion]
173 -- See also [CoAxiom index]
174 -- The coercion arguments always *precisely* saturate
175 -- arity of (that branch of) the CoAxiom. If there are
176 -- any left over, we use AppCo. See
177 -- See [Coercion axioms applied to coercions]
178
179 -- see Note [UnivCo]
180 | UnivCo FastString Role Type Type -- :: "e" -> _ -> _ -> e
181 -- the FastString is just a note for provenance
182 | SymCo Coercion -- :: e -> e
183 | TransCo Coercion Coercion -- :: e -> e -> e
184
185 -- The number of types and coercions should match exactly the expectations
186 -- of the CoAxiomRule (i.e., the rule is fully saturated).
187 | AxiomRuleCo CoAxiomRule [Type] [Coercion]
188
189 -- These are destructors
190
191 | NthCo Int Coercion -- Zero-indexed; decomposes (T t0 ... tn)
192 -- and (F t0 ... tn), assuming F is injective.
193 -- :: _ -> e -> ?? (inverse of TyConAppCo, see Note [TyConAppCo roles])
194 -- See Note [NthCo and newtypes]
195
196 | LRCo LeftOrRight Coercion -- Decomposes (t_left t_right)
197 -- :: _ -> N -> N
198 | InstCo Coercion Type
199 -- :: e -> _ -> e
200
201 | SubCo Coercion -- Turns a ~N into a ~R
202 -- :: N -> R
203 deriving (Data.Data, Data.Typeable)
204
205 -- If you edit this type, you may need to update the GHC formalism
206 -- See Note [GHC Formalism] in coreSyn/CoreLint.hs
207 data LeftOrRight = CLeft | CRight
208 deriving( Eq, Data.Data, Data.Typeable )
209
210 instance Binary LeftOrRight where
211 put_ bh CLeft = putByte bh 0
212 put_ bh CRight = putByte bh 1
213
214 get bh = do { h <- getByte bh
215 ; case h of
216 0 -> return CLeft
217 _ -> return CRight }
218
219 pickLR :: LeftOrRight -> (a,a) -> a
220 pickLR CLeft (l,_) = l
221 pickLR CRight (_,r) = r
222
223 {-
224 Note [Refl invariant]
225 ~~~~~~~~~~~~~~~~~~~~~
226 Coercions have the following invariant
227 Refl is always lifted as far as possible.
228
229 You might think that a consequencs is:
230 Every identity coercions has Refl at the root
231
232 But that's not quite true because of coercion variables. Consider
233 g where g :: Int~Int
234 Left h where h :: Maybe Int ~ Maybe Int
235 etc. So the consequence is only true of coercions that
236 have no coercion variables.
237
238 Note [Coercion axioms applied to coercions]
239 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
240 The reason coercion axioms can be applied to coercions and not just
241 types is to allow for better optimization. There are some cases where
242 we need to be able to "push transitivity inside" an axiom in order to
243 expose further opportunities for optimization.
244
245 For example, suppose we have
246
247 C a : t[a] ~ F a
248 g : b ~ c
249
250 and we want to optimize
251
252 sym (C b) ; t[g] ; C c
253
254 which has the kind
255
256 F b ~ F c
257
258 (stopping through t[b] and t[c] along the way).
259
260 We'd like to optimize this to just F g -- but how? The key is
261 that we need to allow axioms to be instantiated by *coercions*,
262 not just by types. Then we can (in certain cases) push
263 transitivity inside the axiom instantiations, and then react
264 opposite-polarity instantiations of the same axiom. In this
265 case, e.g., we match t[g] against the LHS of (C c)'s kind, to
266 obtain the substitution a |-> g (note this operation is sort
267 of the dual of lifting!) and hence end up with
268
269 C g : t[b] ~ F c
270
271 which indeed has the same kind as t[g] ; C c.
272
273 Now we have
274
275 sym (C b) ; C g
276
277 which can be optimized to F g.
278
279 Note [CoAxiom index]
280 ~~~~~~~~~~~~~~~~~~~~
281 A CoAxiom has 1 or more branches. Each branch has contains a list
282 of the free type variables in that branch, the LHS type patterns,
283 and the RHS type for that branch. When we apply an axiom to a list
284 of coercions, we must choose which branch of the axiom we wish to
285 use, as the different branches may have different numbers of free
286 type variables. (The number of type patterns is always the same
287 among branches, but that doesn't quite concern us here.)
288
289 The Int in the AxiomInstCo constructor is the 0-indexed number
290 of the chosen branch.
291
292 Note [Forall coercions]
293 ~~~~~~~~~~~~~~~~~~~~~~~
294 Constructing coercions between forall-types can be a bit tricky.
295 Currently, the situation is as follows:
296
297 ForAllCo TyVar Coercion
298
299 represents a coercion between polymorphic types, with the rule
300
301 v : k g : t1 ~ t2
302 ----------------------------------------------
303 ForAllCo v g : (all v:k . t1) ~ (all v:k . t2)
304
305 Note that it's only necessary to coerce between polymorphic types
306 where the type variables have identical kinds, because equality on
307 kinds is trivial.
308
309 Note [Predicate coercions]
310 ~~~~~~~~~~~~~~~~~~~~~~~~~~
311 Suppose we have
312 g :: a~b
313 How can we coerce between types
314 ([c]~a) => [a] -> c
315 and
316 ([c]~b) => [b] -> c
317 where the equality predicate *itself* differs?
318
319 Answer: we simply treat (~) as an ordinary type constructor, so these
320 types really look like
321
322 ((~) [c] a) -> [a] -> c
323 ((~) [c] b) -> [b] -> c
324
325 So the coercion between the two is obviously
326
327 ((~) [c] g) -> [g] -> c
328
329 Another way to see this to say that we simply collapse predicates to
330 their representation type (see Type.coreView and Type.predTypeRep).
331
332 This collapse is done by mkPredCo; there is no PredCo constructor
333 in Coercion. This is important because we need Nth to work on
334 predicates too:
335 Nth 1 ((~) [c] g) = g
336 See Simplify.simplCoercionF, which generates such selections.
337
338 Note [Kind coercions]
339 ~~~~~~~~~~~~~~~~~~~~~
340 Suppose T :: * -> *, and g :: A ~ B
341 Then the coercion
342 TyConAppCo T [g] T g : T A ~ T B
343
344 Now suppose S :: forall k. k -> *, and g :: A ~ B
345 Then the coercion
346 TyConAppCo S [Refl *, g] T <*> g : T * A ~ T * B
347
348 Notice that the arguments to TyConAppCo are coercions, but the first
349 represents a *kind* coercion. Now, we don't allow any non-trivial kind
350 coercions, so it's an invariant that any such kind coercions are Refl.
351 Lint checks this.
352
353 However it's inconvenient to insist that these kind coercions are always
354 *structurally* (Refl k), because the key function exprIsConApp_maybe
355 pushes coercions into constructor arguments, so
356 C k ty e |> g
357 may turn into
358 C (Nth 0 g) ....
359 Now (Nth 0 g) will optimise to Refl, but perhaps not instantly.
360
361 Note [Roles]
362 ~~~~~~~~~~~~
363 Roles are a solution to the GeneralizedNewtypeDeriving problem, articulated
364 in Trac #1496. The full story is in docs/core-spec/core-spec.pdf. Also, see
365 http://ghc.haskell.org/trac/ghc/wiki/RolesImplementation
366
367 Here is one way to phrase the problem:
368
369 Given:
370 newtype Age = MkAge Int
371 type family F x
372 type instance F Age = Bool
373 type instance F Int = Char
374
375 This compiles down to:
376 axAge :: Age ~ Int
377 axF1 :: F Age ~ Bool
378 axF2 :: F Int ~ Char
379
380 Then, we can make:
381 (sym (axF1) ; F axAge ; axF2) :: Bool ~ Char
382
383 Yikes!
384
385 The solution is _roles_, as articulated in "Generative Type Abstraction and
386 Type-level Computation" (POPL 2010), available at
387 http://www.seas.upenn.edu/~sweirich/papers/popl163af-weirich.pdf
388
389 The specification for roles has evolved somewhat since that paper. For the
390 current full details, see the documentation in docs/core-spec. Here are some
391 highlights.
392
393 We label every equality with a notion of type equivalence, of which there are
394 three options: Nominal, Representational, and Phantom. A ground type is
395 nominally equivalent only with itself. A newtype (which is considered a ground
396 type in Haskell) is representationally equivalent to its representation.
397 Anything is "phantomly" equivalent to anything else. We use "N", "R", and "P"
398 to denote the equivalences.
399
400 The axioms above would be:
401 axAge :: Age ~R Int
402 axF1 :: F Age ~N Bool
403 axF2 :: F Age ~N Char
404
405 Then, because transitivity applies only to coercions proving the same notion
406 of equivalence, the above construction is impossible.
407
408 However, there is still an escape hatch: we know that any two types that are
409 nominally equivalent are representationally equivalent as well. This is what
410 the form SubCo proves -- it "demotes" a nominal equivalence into a
411 representational equivalence. So, it would seem the following is possible:
412
413 sub (sym axF1) ; F axAge ; sub axF2 :: Bool ~R Char -- WRONG
414
415 What saves us here is that the arguments to a type function F, lifted into a
416 coercion, *must* prove nominal equivalence. So, (F axAge) is ill-formed, and
417 we are safe.
418
419 Roles are attached to parameters to TyCons. When lifting a TyCon into a
420 coercion (through TyConAppCo), we need to ensure that the arguments to the
421 TyCon respect their roles. For example:
422
423 data T a b = MkT a (F b)
424
425 If we know that a1 ~R a2, then we know (T a1 b) ~R (T a2 b). But, if we know
426 that b1 ~R b2, we know nothing about (T a b1) and (T a b2)! This is because
427 the type function F branches on b's *name*, not representation. So, we say
428 that 'a' has role Representational and 'b' has role Nominal. The third role,
429 Phantom, is for parameters not used in the type's definition. Given the
430 following definition
431
432 data Q a = MkQ Int
433
434 the Phantom role allows us to say that (Q Bool) ~R (Q Char), because we
435 can construct the coercion Bool ~P Char (using UnivCo).
436
437 See the paper cited above for more examples and information.
438
439 Note [UnivCo]
440 ~~~~~~~~~~~~~
441 The UnivCo ("universal coercion") serves two rather separate functions:
442 - the implementation for unsafeCoerce#
443 - placeholder for phantom parameters in a TyConAppCo
444
445 At Representational, it asserts that two (possibly unrelated)
446 types have the same representation and can be casted to one another.
447 This form is necessary for unsafeCoerce#.
448
449 For optimisation purposes, it is convenient to allow UnivCo to appear
450 at Nominal role. If we have
451
452 data Foo a = MkFoo (F a) -- F is a type family
453
454 and we want an unsafe coercion from Foo Int to Foo Bool, then it would
455 be nice to have (TyConAppCo Foo (UnivCo Nominal Int Bool)). So, we allow
456 Nominal UnivCo's.
457
458 At Phantom role, it is used as an argument to TyConAppCo in the place
459 of a phantom parameter (a type parameter unused in the type definition).
460
461 For example:
462
463 data Q a = MkQ Int
464
465 We want a coercion for (Q Bool) ~R (Q Char).
466
467 (TyConAppCo Representational Q [UnivCo Phantom Bool Char]) does the trick.
468
469 Note [TyConAppCo roles]
470 ~~~~~~~~~~~~~~~~~~~~~~~
471 The TyConAppCo constructor has a role parameter, indicating the role at
472 which the coercion proves equality. The choice of this parameter affects
473 the required roles of the arguments of the TyConAppCo. To help explain
474 it, assume the following definition:
475
476 type instance F Int = Bool -- Axiom axF : F Int ~N Bool
477 newtype Age = MkAge Int -- Axiom axAge : Age ~R Int
478 data Foo a = MkFoo a -- Role on Foo's parameter is Representational
479
480 TyConAppCo Nominal Foo axF : Foo (F Int) ~N Foo Bool
481 For (TyConAppCo Nominal) all arguments must have role Nominal. Why?
482 So that Foo Age ~N Foo Int does *not* hold.
483
484 TyConAppCo Representational Foo (SubCo axF) : Foo (F Int) ~R Foo Bool
485 TyConAppCo Representational Foo axAge : Foo Age ~R Foo Int
486 For (TyConAppCo Representational), all arguments must have the roles
487 corresponding to the result of tyConRoles on the TyCon. This is the
488 whole point of having roles on the TyCon to begin with. So, we can
489 have Foo Age ~R Foo Int, if Foo's parameter has role R.
490
491 If a Representational TyConAppCo is over-saturated (which is otherwise fine),
492 the spill-over arguments must all be at Nominal. This corresponds to the
493 behavior for AppCo.
494
495 TyConAppCo Phantom Foo (UnivCo Phantom Int Bool) : Foo Int ~P Foo Bool
496 All arguments must have role Phantom. This one isn't strictly
497 necessary for soundness, but this choice removes ambiguity.
498
499 The rules here dictate the roles of the parameters to mkTyConAppCo
500 (should be checked by Lint).
501
502 Note [NthCo and newtypes]
503 ~~~~~~~~~~~~~~~~~~~~~~~~~
504 Suppose we have
505
506 newtype N a = MkN Int
507 type role N representational
508
509 This yields axiom
510
511 NTCo:N :: forall a. N a ~R Int
512
513 We can then build
514
515 co :: forall a b. N a ~R N b
516 co = NTCo:N a ; sym (NTCo:N b)
517
518 for any `a` and `b`. Because of the role annotation on N, if we use
519 NthCo, we'll get out a representational coercion. That is:
520
521 NthCo 0 co :: forall a b. a ~R b
522
523 Yikes! Clearly, this is terrible. The solution is simple: forbid
524 NthCo to be used on newtypes if the internal coercion is representational.
525
526 This is not just some corner case discovered by a segfault somewhere;
527 it was discovered in the proof of soundness of roles and described
528 in the "Safe Coercions" paper (ICFP '14).
529
530 ************************************************************************
531 * *
532 \subsection{Coercion variables}
533 * *
534 ************************************************************************
535 -}
536
537 coVarName :: CoVar -> Name
538 coVarName = varName
539
540 setCoVarUnique :: CoVar -> Unique -> CoVar
541 setCoVarUnique = setVarUnique
542
543 setCoVarName :: CoVar -> Name -> CoVar
544 setCoVarName = setVarName
545
546 isCoVar :: Var -> Bool
547 isCoVar v = isCoVarType (varType v)
548
549 isCoVarType :: Type -> Bool
550 isCoVarType ty -- Tests for t1 ~# t2, the unboxed equality
551 = case splitTyConApp_maybe ty of
552 Just (tc,tys) -> (tc `hasKey` eqPrimTyConKey || tc `hasKey` eqReprPrimTyConKey)
553 && tys `lengthAtLeast` 2
554 Nothing -> False
555
556 tyCoVarsOfCo :: Coercion -> VarSet
557 -- Extracts type and coercion variables from a coercion
558 tyCoVarsOfCo (Refl _ ty) = tyVarsOfType ty
559 tyCoVarsOfCo (TyConAppCo _ _ cos) = tyCoVarsOfCos cos
560 tyCoVarsOfCo (AppCo co1 co2) = tyCoVarsOfCo co1 `unionVarSet` tyCoVarsOfCo co2
561 tyCoVarsOfCo (ForAllCo tv co) = tyCoVarsOfCo co `delVarSet` tv
562 tyCoVarsOfCo (CoVarCo v) = unitVarSet v
563 tyCoVarsOfCo (AxiomInstCo _ _ cos) = tyCoVarsOfCos cos
564 tyCoVarsOfCo (UnivCo _ _ ty1 ty2) = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2
565 tyCoVarsOfCo (SymCo co) = tyCoVarsOfCo co
566 tyCoVarsOfCo (TransCo co1 co2) = tyCoVarsOfCo co1 `unionVarSet` tyCoVarsOfCo co2
567 tyCoVarsOfCo (NthCo _ co) = tyCoVarsOfCo co
568 tyCoVarsOfCo (LRCo _ co) = tyCoVarsOfCo co
569 tyCoVarsOfCo (InstCo co ty) = tyCoVarsOfCo co `unionVarSet` tyVarsOfType ty
570 tyCoVarsOfCo (SubCo co) = tyCoVarsOfCo co
571 tyCoVarsOfCo (AxiomRuleCo _ ts cs) = tyVarsOfTypes ts `unionVarSet` tyCoVarsOfCos cs
572
573 tyCoVarsOfCos :: [Coercion] -> VarSet
574 tyCoVarsOfCos = mapUnionVarSet tyCoVarsOfCo
575
576 coVarsOfCo :: Coercion -> VarSet
577 -- Extract *coerction* variables only. Tiresome to repeat the code, but easy.
578 coVarsOfCo (Refl _ _) = emptyVarSet
579 coVarsOfCo (TyConAppCo _ _ cos) = coVarsOfCos cos
580 coVarsOfCo (AppCo co1 co2) = coVarsOfCo co1 `unionVarSet` coVarsOfCo co2
581 coVarsOfCo (ForAllCo _ co) = coVarsOfCo co
582 coVarsOfCo (CoVarCo v) = unitVarSet v
583 coVarsOfCo (AxiomInstCo _ _ cos) = coVarsOfCos cos
584 coVarsOfCo (UnivCo _ _ _ _) = emptyVarSet
585 coVarsOfCo (SymCo co) = coVarsOfCo co
586 coVarsOfCo (TransCo co1 co2) = coVarsOfCo co1 `unionVarSet` coVarsOfCo co2
587 coVarsOfCo (NthCo _ co) = coVarsOfCo co
588 coVarsOfCo (LRCo _ co) = coVarsOfCo co
589 coVarsOfCo (InstCo co _) = coVarsOfCo co
590 coVarsOfCo (SubCo co) = coVarsOfCo co
591 coVarsOfCo (AxiomRuleCo _ _ cos) = coVarsOfCos cos
592
593 coVarsOfCos :: [Coercion] -> VarSet
594 coVarsOfCos = mapUnionVarSet coVarsOfCo
595
596 coercionSize :: Coercion -> Int
597 coercionSize (Refl _ ty) = typeSize ty
598 coercionSize (TyConAppCo _ _ cos) = 1 + sum (map coercionSize cos)
599 coercionSize (AppCo co1 co2) = coercionSize co1 + coercionSize co2
600 coercionSize (ForAllCo _ co) = 1 + coercionSize co
601 coercionSize (CoVarCo _) = 1
602 coercionSize (AxiomInstCo _ _ cos) = 1 + sum (map coercionSize cos)
603 coercionSize (UnivCo _ _ ty1 ty2) = typeSize ty1 + typeSize ty2
604 coercionSize (SymCo co) = 1 + coercionSize co
605 coercionSize (TransCo co1 co2) = 1 + coercionSize co1 + coercionSize co2
606 coercionSize (NthCo _ co) = 1 + coercionSize co
607 coercionSize (LRCo _ co) = 1 + coercionSize co
608 coercionSize (InstCo co ty) = 1 + coercionSize co + typeSize ty
609 coercionSize (SubCo co) = 1 + coercionSize co
610 coercionSize (AxiomRuleCo _ tys cos) = 1 + sum (map typeSize tys)
611 + sum (map coercionSize cos)
612
613 {-
614 ************************************************************************
615 * *
616 Tidying coercions
617 * *
618 ************************************************************************
619 -}
620
621 tidyCo :: TidyEnv -> Coercion -> Coercion
622 tidyCo env@(_, subst) co
623 = go co
624 where
625 go (Refl r ty) = Refl r (tidyType env ty)
626 go (TyConAppCo r tc cos) = let args = map go cos
627 in args `seqList` TyConAppCo r tc args
628 go (AppCo co1 co2) = (AppCo $! go co1) $! go co2
629 go (ForAllCo tv co) = ForAllCo tvp $! (tidyCo envp co)
630 where
631 (envp, tvp) = tidyTyVarBndr env tv
632 go (CoVarCo cv) = case lookupVarEnv subst cv of
633 Nothing -> CoVarCo cv
634 Just cv' -> CoVarCo cv'
635 go (AxiomInstCo con ind cos) = let args = tidyCos env cos
636 in args `seqList` AxiomInstCo con ind args
637 go (UnivCo s r ty1 ty2) = (UnivCo s r $! tidyType env ty1) $! tidyType env ty2
638 go (SymCo co) = SymCo $! go co
639 go (TransCo co1 co2) = (TransCo $! go co1) $! go co2
640 go (NthCo d co) = NthCo d $! go co
641 go (LRCo lr co) = LRCo lr $! go co
642 go (InstCo co ty) = (InstCo $! go co) $! tidyType env ty
643 go (SubCo co) = SubCo $! go co
644
645 go (AxiomRuleCo ax tys cos) = let tys1 = map (tidyType env) tys
646 cos1 = tidyCos env cos
647 in tys1 `seqList` cos1 `seqList`
648 AxiomRuleCo ax tys1 cos1
649
650
651 tidyCos :: TidyEnv -> [Coercion] -> [Coercion]
652 tidyCos env = map (tidyCo env)
653
654 {-
655 ************************************************************************
656 * *
657 Pretty-printing coercions
658 * *
659 ************************************************************************
660
661 @pprCo@ is the standard @Coercion@ printer; the overloaded @ppr@
662 function is defined to use this. @pprParendCo@ is the same, except it
663 puts parens around the type, except for the atomic cases.
664 @pprParendCo@ works just by setting the initial context precedence
665 very high.
666 -}
667
668 instance Outputable Coercion where
669 ppr = pprCo
670
671 pprCo, pprParendCo :: Coercion -> SDoc
672 pprCo co = ppr_co TopPrec co
673 pprParendCo co = ppr_co TyConPrec co
674
675 ppr_co :: TyPrec -> Coercion -> SDoc
676 ppr_co _ (Refl r ty) = angleBrackets (ppr ty) <> ppr_role r
677
678 ppr_co p co@(TyConAppCo _ tc [_,_])
679 | tc `hasKey` funTyConKey = ppr_fun_co p co
680
681 ppr_co _ (TyConAppCo r tc cos) = pprTcApp TyConPrec ppr_co tc cos <> ppr_role r
682 ppr_co p (AppCo co1 co2) = maybeParen p TyConPrec $
683 pprCo co1 <+> ppr_co TyConPrec co2
684 ppr_co p co@(ForAllCo {}) = ppr_forall_co p co
685 ppr_co _ (CoVarCo cv) = parenSymOcc (getOccName cv) (ppr cv)
686 ppr_co p (AxiomInstCo con index cos)
687 = pprPrefixApp p (ppr (getName con) <> brackets (ppr index))
688 (map (ppr_co TyConPrec) cos)
689
690 ppr_co p co@(TransCo {}) = maybeParen p FunPrec $
691 case trans_co_list co [] of
692 [] -> panic "ppr_co"
693 (co:cos) -> sep ( ppr_co FunPrec co
694 : [ char ';' <+> ppr_co FunPrec co | co <- cos])
695 ppr_co p (InstCo co ty) = maybeParen p TyConPrec $
696 pprParendCo co <> ptext (sLit "@") <> pprType ty
697
698 ppr_co p (UnivCo s r ty1 ty2) = pprPrefixApp p (ptext (sLit "UnivCo") <+> ftext s <+> ppr r)
699 [pprParendType ty1, pprParendType ty2]
700 ppr_co p (SymCo co) = pprPrefixApp p (ptext (sLit "Sym")) [pprParendCo co]
701 ppr_co p (NthCo n co) = pprPrefixApp p (ptext (sLit "Nth:") <> int n) [pprParendCo co]
702 ppr_co p (LRCo sel co) = pprPrefixApp p (ppr sel) [pprParendCo co]
703 ppr_co p (SubCo co) = pprPrefixApp p (ptext (sLit "Sub")) [pprParendCo co]
704 ppr_co p (AxiomRuleCo co ts cs) = maybeParen p TopPrec $
705 ppr_axiom_rule_co co ts cs
706
707 ppr_axiom_rule_co :: CoAxiomRule -> [Type] -> [Coercion] -> SDoc
708 ppr_axiom_rule_co co ts ps = ppr (coaxrName co) <> ppTs ts $$ nest 2 (ppPs ps)
709 where
710 ppTs [] = Outputable.empty
711 ppTs [t] = ptext (sLit "@") <> ppr_type TopPrec t
712 ppTs ts = ptext (sLit "@") <>
713 parens (hsep $ punctuate comma $ map pprType ts)
714
715 ppPs [] = Outputable.empty
716 ppPs [p] = pprParendCo p
717 ppPs (p : ps) = ptext (sLit "(") <+> pprCo p $$
718 vcat [ ptext (sLit ",") <+> pprCo q | q <- ps ] $$
719 ptext (sLit ")")
720
721
722
723 ppr_role :: Role -> SDoc
724 ppr_role r = underscore <> pp_role
725 where pp_role = case r of
726 Nominal -> char 'N'
727 Representational -> char 'R'
728 Phantom -> char 'P'
729
730 trans_co_list :: Coercion -> [Coercion] -> [Coercion]
731 trans_co_list (TransCo co1 co2) cos = trans_co_list co1 (trans_co_list co2 cos)
732 trans_co_list co cos = co : cos
733
734 instance Outputable LeftOrRight where
735 ppr CLeft = ptext (sLit "Left")
736 ppr CRight = ptext (sLit "Right")
737
738 ppr_fun_co :: TyPrec -> Coercion -> SDoc
739 ppr_fun_co p co = pprArrowChain p (split co)
740 where
741 split :: Coercion -> [SDoc]
742 split (TyConAppCo _ f [arg,res])
743 | f `hasKey` funTyConKey
744 = ppr_co FunPrec arg : split res
745 split co = [ppr_co TopPrec co]
746
747 ppr_forall_co :: TyPrec -> Coercion -> SDoc
748 ppr_forall_co p ty
749 = maybeParen p FunPrec $
750 sep [pprForAll tvs, ppr_co TopPrec rho]
751 where
752 (tvs, rho) = split1 [] ty
753 split1 tvs (ForAllCo tv ty) = split1 (tv:tvs) ty
754 split1 tvs ty = (reverse tvs, ty)
755
756 pprCoAxiom :: CoAxiom br -> SDoc
757 pprCoAxiom ax@(CoAxiom { co_ax_branches = branches })
758 = hang (text "axiom" <+> ppr ax <+> dcolon)
759 2 (vcat (map (ppr_co_ax_branch (const ppr) ax) $ fromBranches branches))
760
761 pprCoAxBranch :: CoAxiom br -> CoAxBranch -> SDoc
762 pprCoAxBranch = ppr_co_ax_branch pprRhs
763 where
764 pprRhs fam_tc (TyConApp tycon _)
765 | isDataFamilyTyCon fam_tc
766 = pprDataCons tycon
767 pprRhs _ rhs = ppr rhs
768
769 pprCoAxBranchHdr :: CoAxiom br -> BranchIndex -> SDoc
770 pprCoAxBranchHdr ax index = pprCoAxBranch ax (coAxiomNthBranch ax index)
771
772 ppr_co_ax_branch :: (TyCon -> Type -> SDoc) -> CoAxiom br -> CoAxBranch -> SDoc
773 ppr_co_ax_branch ppr_rhs
774 (CoAxiom { co_ax_tc = fam_tc, co_ax_name = name })
775 (CoAxBranch { cab_tvs = tvs
776 , cab_lhs = lhs
777 , cab_rhs = rhs
778 , cab_loc = loc })
779 = foldr1 (flip hangNotEmpty 2)
780 [ pprUserForAll tvs
781 , pprTypeApp fam_tc lhs <+> equals <+> ppr_rhs fam_tc rhs
782 , text "-- Defined" <+> pprLoc loc ]
783 where
784 pprLoc loc
785 | isGoodSrcSpan loc
786 = text "at" <+> ppr (srcSpanStart loc)
787
788 | otherwise
789 = text "in" <+>
790 quotes (ppr (nameModule name))
791
792 {-
793 ************************************************************************
794 * *
795 Functions over Kinds
796 * *
797 ************************************************************************
798 -}
799
800 -- | This breaks a 'Coercion' with type @T A B C ~ T D E F@ into
801 -- a list of 'Coercion's of kinds @A ~ D@, @B ~ E@ and @E ~ F@. Hence:
802 --
803 -- > decomposeCo 3 c = [nth 0 c, nth 1 c, nth 2 c]
804 decomposeCo :: Arity -> Coercion -> [Coercion]
805 decomposeCo arity co
806 = [mkNthCo n co | n <- [0..(arity-1)] ]
807 -- Remember, Nth is zero-indexed
808
809 -- | Attempts to obtain the type variable underlying a 'Coercion'
810 getCoVar_maybe :: Coercion -> Maybe CoVar
811 getCoVar_maybe (CoVarCo cv) = Just cv
812 getCoVar_maybe _ = Nothing
813
814 -- first result has role equal to input; second result is Nominal
815 splitAppCo_maybe :: Coercion -> Maybe (Coercion, Coercion)
816 -- ^ Attempt to take a coercion application apart.
817 splitAppCo_maybe (AppCo co1 co2) = Just (co1, co2)
818 splitAppCo_maybe (TyConAppCo r tc cos)
819 | mightBeUnsaturatedTyCon tc || cos `lengthExceeds` tyConArity tc
820 , Just (cos', co') <- snocView cos
821 , Just co'' <- setNominalRole_maybe co'
822 = Just (mkTyConAppCo r tc cos', co'') -- Never create unsaturated type family apps!
823 -- Use mkTyConAppCo to preserve the invariant
824 -- that identity coercions are always represented by Refl
825 splitAppCo_maybe (Refl r ty)
826 | Just (ty1, ty2) <- splitAppTy_maybe ty
827 = Just (Refl r ty1, Refl Nominal ty2)
828 splitAppCo_maybe _ = Nothing
829
830 splitForAllCo_maybe :: Coercion -> Maybe (TyVar, Coercion)
831 splitForAllCo_maybe (ForAllCo tv co) = Just (tv, co)
832 splitForAllCo_maybe _ = Nothing
833
834 -------------------------------------------------------
835 -- and some coercion kind stuff
836
837 coVarKind :: CoVar -> (Type,Type)
838 coVarKind cv
839 | Just (tc, [_kind,ty1,ty2]) <- splitTyConApp_maybe (varType cv)
840 = ASSERT(tc `hasKey` eqPrimTyConKey || tc `hasKey` eqReprPrimTyConKey)
841 (ty1,ty2)
842 | otherwise = panic "coVarKind, non coercion variable"
843
844 coVarRole :: CoVar -> Role
845 coVarRole cv
846 | tc `hasKey` eqPrimTyConKey
847 = Nominal
848 | tc `hasKey` eqReprPrimTyConKey
849 = Representational
850 | otherwise
851 = pprPanic "coVarRole: unknown tycon" (ppr cv)
852
853 where
854 tc = case tyConAppTyCon_maybe (varType cv) of
855 Just tc0 -> tc0
856 Nothing -> pprPanic "coVarRole: not tyconapp" (ppr cv)
857
858 -- | Makes a coercion type from two types: the types whose equality
859 -- is proven by the relevant 'Coercion'
860 mkCoercionType :: Role -> Type -> Type -> Type
861 mkCoercionType Nominal = mkPrimEqPred
862 mkCoercionType Representational = mkReprPrimEqPred
863 mkCoercionType Phantom = panic "mkCoercionType"
864
865 isReflCo :: Coercion -> Bool
866 isReflCo (Refl {}) = True
867 isReflCo _ = False
868
869 isReflCo_maybe :: Coercion -> Maybe Type
870 isReflCo_maybe (Refl _ ty) = Just ty
871 isReflCo_maybe _ = Nothing
872
873 {-
874 ************************************************************************
875 * *
876 Building coercions
877 * *
878 ************************************************************************
879
880 Note [Role twiddling functions]
881 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
882
883 There are a plethora of functions for twiddling roles:
884
885 mkSubCo: Requires a nominal input coercion and always produces a
886 representational output. This is used when you (the programmer) are sure you
887 know exactly that role you have and what you want.
888
889 downgradeRole_maybe: This function takes both the input role and the output role
890 as parameters. (The *output* role comes first!) It can only *downgrade* a
891 role -- that is, change it from N to R or P, or from R to P. This one-way
892 behavior is why there is the "_maybe". If an upgrade is requested, this
893 function produces Nothing. This is used when you need to change the role of a
894 coercion, but you're not sure (as you're writing the code) of which roles are
895 involved.
896
897 This function could have been written using coercionRole to ascertain the role
898 of the input. But, that function is recursive, and the caller of downgradeRole_maybe
899 often knows the input role. So, this is more efficient.
900
901 downgradeRole: This is just like downgradeRole_maybe, but it panics if the conversion
902 isn't a downgrade.
903
904 setNominalRole_maybe: This is the only function that can *upgrade* a coercion. The result
905 (if it exists) is always Nominal. The input can be at any role. It works on a
906 "best effort" basis, as it should never be strictly necessary to upgrade a coercion
907 during compilation. It is currently only used within GHC in splitAppCo_maybe. In order
908 to be a proper inverse of mkAppCo, the second coercion that splitAppCo_maybe returns
909 must be nominal. But, it's conceivable that splitAppCo_maybe is operating over a
910 TyConAppCo that uses a representational coercion. Hence the need for setNominalRole_maybe.
911 splitAppCo_maybe, in turn, is used only within coercion optimization -- thus, it is
912 not absolutely critical that setNominalRole_maybe be complete.
913
914 Note that setNominalRole_maybe will never upgrade a phantom UnivCo. Phantom
915 UnivCos are perfectly type-safe, whereas representational and nominal ones are
916 not. Indeed, `unsafeCoerce` is implemented via a representational UnivCo.
917 (Nominal ones are no worse than representational ones, so this function *will*
918 change a UnivCo Representational to a UnivCo Nominal.)
919
920 Conal Elliott also came across a need for this function while working with the GHC
921 API, as he was decomposing Core casts. The Core casts use representational coercions,
922 as they must, but his use case required nominal coercions (he was building a GADT).
923 So, that's why this function is exported from this module.
924
925 One might ask: shouldn't downgradeRole_maybe just use setNominalRole_maybe as appropriate?
926 I (Richard E.) have decided not to do this, because upgrading a role is bizarre and
927 a caller should have to ask for this behavior explicitly.
928 -}
929
930 mkCoVarCo :: CoVar -> Coercion
931 -- cv :: s ~# t
932 mkCoVarCo cv
933 | ty1 `eqType` ty2 = Refl (coVarRole cv) ty1
934 | otherwise = CoVarCo cv
935 where
936 (ty1, ty2) = ASSERT( isCoVar cv ) coVarKind cv
937
938 mkReflCo :: Role -> Type -> Coercion
939 mkReflCo = Refl
940
941 mkAxInstCo :: Role -> CoAxiom br -> BranchIndex -> [Type] -> Coercion
942 -- mkAxInstCo can legitimately be called over-staturated;
943 -- i.e. with more type arguments than the coercion requires
944 mkAxInstCo role ax index tys
945 | arity == n_tys = downgradeRole role ax_role $ AxiomInstCo ax_br index rtys
946 | otherwise = ASSERT( arity < n_tys )
947 downgradeRole role ax_role $
948 foldl AppCo (AxiomInstCo ax_br index (take arity rtys))
949 (drop arity rtys)
950 where
951 n_tys = length tys
952 ax_br = toBranchedAxiom ax
953 branch = coAxiomNthBranch ax_br index
954 arity = length $ coAxBranchTyVars branch
955 arg_roles = coAxBranchRoles branch
956 rtys = zipWith mkReflCo (arg_roles ++ repeat Nominal) tys
957 ax_role = coAxiomRole ax
958
959 -- to be used only with unbranched axioms
960 mkUnbranchedAxInstCo :: Role -> CoAxiom Unbranched -> [Type] -> Coercion
961 mkUnbranchedAxInstCo role ax tys
962 = mkAxInstCo role ax 0 tys
963
964 mkAxInstLHS, mkAxInstRHS :: CoAxiom br -> BranchIndex -> [Type] -> Type
965 -- Instantiate the axiom with specified types,
966 -- returning the instantiated RHS
967 -- A companion to mkAxInstCo:
968 -- mkAxInstRhs ax index tys = snd (coercionKind (mkAxInstCo ax index tys))
969 mkAxInstLHS ax index tys
970 | CoAxBranch { cab_tvs = tvs, cab_lhs = lhs } <- coAxiomNthBranch ax index
971 , (tys1, tys2) <- splitAtList tvs tys
972 = ASSERT( tvs `equalLength` tys1 )
973 mkTyConApp (coAxiomTyCon ax) (substTysWith tvs tys1 lhs ++ tys2)
974
975 mkAxInstRHS ax index tys
976 | CoAxBranch { cab_tvs = tvs, cab_rhs = rhs } <- coAxiomNthBranch ax index
977 , (tys1, tys2) <- splitAtList tvs tys
978 = ASSERT( tvs `equalLength` tys1 )
979 mkAppTys (substTyWith tvs tys1 rhs) tys2
980
981 mkUnbranchedAxInstRHS :: CoAxiom Unbranched -> [Type] -> Type
982 mkUnbranchedAxInstRHS ax = mkAxInstRHS ax 0
983
984 -- | Apply a 'Coercion' to another 'Coercion'.
985 -- The second coercion must be Nominal, unless the first is Phantom.
986 -- If the first is Phantom, then the second can be either Phantom or Nominal.
987 mkAppCo :: Coercion -> Coercion -> Coercion
988 mkAppCo co1 co2 = mkAppCoFlexible co1 Nominal co2
989 -- Note, mkAppCo is careful to maintain invariants regarding
990 -- where Refl constructors appear; see the comments in the definition
991 -- of Coercion and the Note [Refl invariant] in types/TypeRep.hs.
992
993 -- | Apply a 'Coercion' to another 'Coercion'.
994 -- The second 'Coercion's role is given, making this more flexible than
995 -- 'mkAppCo'.
996 mkAppCoFlexible :: Coercion -> Role -> Coercion -> Coercion
997 mkAppCoFlexible (Refl r ty1) _ (Refl _ ty2)
998 = Refl r (mkAppTy ty1 ty2)
999 mkAppCoFlexible (Refl r ty1) r2 co2
1000 | Just (tc, tys) <- splitTyConApp_maybe ty1
1001 -- Expand type synonyms; a TyConAppCo can't have a type synonym (Trac #9102)
1002 = TyConAppCo r tc (zip_roles (tyConRolesX r tc) tys)
1003 where
1004 zip_roles (r1:_) [] = [downgradeRole r1 r2 co2]
1005 zip_roles (r1:rs) (ty1:tys) = mkReflCo r1 ty1 : zip_roles rs tys
1006 zip_roles _ _ = panic "zip_roles" -- but the roles are infinite...
1007 mkAppCoFlexible (TyConAppCo r tc cos) r2 co
1008 = case r of
1009 Nominal -> ASSERT( r2 == Nominal )
1010 TyConAppCo Nominal tc (cos ++ [co])
1011 Representational -> TyConAppCo Representational tc (cos ++ [co'])
1012 where new_role = (tyConRolesX Representational tc) !! (length cos)
1013 co' = downgradeRole new_role r2 co
1014 Phantom -> TyConAppCo Phantom tc (cos ++ [mkPhantomCo co])
1015
1016 mkAppCoFlexible co1 _r2 co2 = ASSERT( _r2 == Nominal )
1017 AppCo co1 co2
1018
1019
1020 -- | Applies multiple 'Coercion's to another 'Coercion', from left to right.
1021 -- See also 'mkAppCo'.
1022 mkAppCos :: Coercion -> [Coercion] -> Coercion
1023 mkAppCos co1 cos = foldl mkAppCo co1 cos
1024
1025 -- | Apply a type constructor to a list of coercions. It is the
1026 -- caller's responsibility to get the roles correct on argument coercions.
1027 mkTyConAppCo :: Role -> TyCon -> [Coercion] -> Coercion
1028 mkTyConAppCo r tc cos
1029 -- Expand type synonyms
1030 | Just (tv_co_prs, rhs_ty, leftover_cos) <- expandSynTyCon_maybe tc cos
1031 = mkAppCos (liftCoSubst r tv_co_prs rhs_ty) leftover_cos
1032
1033 | Just tys <- traverse isReflCo_maybe cos
1034 = Refl r (mkTyConApp tc tys) -- See Note [Refl invariant]
1035
1036 | otherwise = TyConAppCo r tc cos
1037
1038 -- | Make a function 'Coercion' between two other 'Coercion's
1039 mkFunCo :: Role -> Coercion -> Coercion -> Coercion
1040 mkFunCo r co1 co2 = mkTyConAppCo r funTyCon [co1, co2]
1041
1042 -- | Make a 'Coercion' which binds a variable within an inner 'Coercion'
1043 mkForAllCo :: Var -> Coercion -> Coercion
1044 -- note that a TyVar should be used here, not a CoVar (nor a TcTyVar)
1045 mkForAllCo tv (Refl r ty) = ASSERT( isTyVar tv ) Refl r (mkForAllTy tv ty)
1046 mkForAllCo tv co = ASSERT( isTyVar tv ) ForAllCo tv co
1047
1048 -------------------------------
1049
1050 -- | Create a symmetric version of the given 'Coercion' that asserts
1051 -- equality between the same types but in the other "direction", so
1052 -- a kind of @t1 ~ t2@ becomes the kind @t2 ~ t1@.
1053 mkSymCo :: Coercion -> Coercion
1054
1055 -- Do a few simple optimizations, but don't bother pushing occurrences
1056 -- of symmetry to the leaves; the optimizer will take care of that.
1057 mkSymCo co@(Refl {}) = co
1058 mkSymCo (UnivCo s r ty1 ty2) = UnivCo s r ty2 ty1
1059 mkSymCo (SymCo co) = co
1060 mkSymCo co = SymCo co
1061
1062 -- | Create a new 'Coercion' by composing the two given 'Coercion's transitively.
1063 mkTransCo :: Coercion -> Coercion -> Coercion
1064 mkTransCo (Refl {}) co = co
1065 mkTransCo co (Refl {}) = co
1066 mkTransCo co1 co2 = TransCo co1 co2
1067
1068 -- the Role is the desired one. It is the caller's responsibility to make
1069 -- sure this request is reasonable
1070 mkNthCoRole :: Role -> Int -> Coercion -> Coercion
1071 mkNthCoRole role n co
1072 = downgradeRole role nth_role $ nth_co
1073 where
1074 nth_co = mkNthCo n co
1075 nth_role = coercionRole nth_co
1076
1077 mkNthCo :: Int -> Coercion -> Coercion
1078 mkNthCo n (Refl r ty) = ASSERT( ok_tc_app ty n )
1079 Refl r' (tyConAppArgN n ty)
1080 where tc = tyConAppTyCon ty
1081 r' = nthRole r tc n
1082 mkNthCo n co = ASSERT( ok_tc_app _ty1 n && ok_tc_app _ty2 n )
1083 NthCo n co
1084 where
1085 Pair _ty1 _ty2 = coercionKind co
1086
1087
1088 mkLRCo :: LeftOrRight -> Coercion -> Coercion
1089 mkLRCo lr (Refl eq ty) = Refl eq (pickLR lr (splitAppTy ty))
1090 mkLRCo lr co = LRCo lr co
1091
1092 ok_tc_app :: Type -> Int -> Bool
1093 ok_tc_app ty n = case splitTyConApp_maybe ty of
1094 Just (_, tys) -> tys `lengthExceeds` n
1095 Nothing -> False
1096
1097 -- | Instantiates a 'Coercion' with a 'Type' argument.
1098 mkInstCo :: Coercion -> Type -> Coercion
1099 mkInstCo co ty = InstCo co ty
1100
1101 -- | Manufacture an unsafe coercion from thin air.
1102 -- Currently (May 14) this is used only to implement the
1103 -- @unsafeCoerce#@ primitive. Optimise by pushing
1104 -- down through type constructors.
1105 mkUnsafeCo :: Type -> Type -> Coercion
1106 mkUnsafeCo = mkUnivCo (fsLit "mkUnsafeCo") Representational
1107
1108 mkUnivCo :: FastString -> Role -> Type -> Type -> Coercion
1109 mkUnivCo prov role ty1 ty2
1110 | ty1 `eqType` ty2 = Refl role ty1
1111 | otherwise = UnivCo prov role ty1 ty2
1112
1113 mkAxiomRuleCo :: CoAxiomRule -> [Type] -> [Coercion] -> Coercion
1114 mkAxiomRuleCo = AxiomRuleCo
1115
1116 -- input coercion is Nominal; see also Note [Role twiddling functions]
1117 mkSubCo :: Coercion -> Coercion
1118 mkSubCo (Refl Nominal ty) = Refl Representational ty
1119 mkSubCo (TyConAppCo Nominal tc cos)
1120 = TyConAppCo Representational tc (applyRoles tc cos)
1121 mkSubCo (UnivCo s Nominal ty1 ty2) = UnivCo s Representational ty1 ty2
1122 mkSubCo co = ASSERT2( coercionRole co == Nominal, ppr co <+> ppr (coercionRole co) )
1123 SubCo co
1124
1125 -- only *downgrades* a role. See Note [Role twiddling functions]
1126 downgradeRole_maybe :: Role -- desired role
1127 -> Role -- current role
1128 -> Coercion
1129 -> Maybe Coercion
1130 -- In (downgradeRole_maybe dr cr co) it's a precondition that
1131 -- cr = coercionRole co
1132 downgradeRole_maybe Representational Nominal co = Just (mkSubCo co)
1133 downgradeRole_maybe Nominal Representational _ = Nothing
1134 downgradeRole_maybe Phantom Phantom co = Just co
1135 downgradeRole_maybe Phantom _ co = Just (mkPhantomCo co)
1136 downgradeRole_maybe _ Phantom _ = Nothing
1137 downgradeRole_maybe _ _ co = Just co
1138
1139 -- panics if the requested conversion is not a downgrade.
1140 -- See also Note [Role twiddling functions]
1141 downgradeRole :: Role -- desired role
1142 -> Role -- current role
1143 -> Coercion -> Coercion
1144 downgradeRole r1 r2 co
1145 = case downgradeRole_maybe r1 r2 co of
1146 Just co' -> co'
1147 Nothing -> pprPanic "downgradeRole" (ppr co)
1148
1149 -- Converts a coercion to be nominal, if possible.
1150 -- See also Note [Role twiddling functions]
1151 setNominalRole_maybe :: Coercion -> Maybe Coercion
1152 setNominalRole_maybe co
1153 | Nominal <- coercionRole co = Just co
1154 setNominalRole_maybe (SubCo co) = Just co
1155 setNominalRole_maybe (Refl _ ty) = Just $ Refl Nominal ty
1156 setNominalRole_maybe (TyConAppCo Representational tc coes)
1157 = do { cos' <- mapM setNominalRole_maybe coes
1158 ; return $ TyConAppCo Nominal tc cos' }
1159 setNominalRole_maybe (UnivCo s Representational ty1 ty2) = Just $ UnivCo s Nominal ty1 ty2
1160 -- We do *not* promote UnivCo Phantom, as that's unsafe.
1161 -- UnivCo Nominal is no more unsafe than UnivCo Representational
1162 setNominalRole_maybe (TransCo co1 co2)
1163 = TransCo <$> setNominalRole_maybe co1 <*> setNominalRole_maybe co2
1164 setNominalRole_maybe (AppCo co1 co2)
1165 = AppCo <$> setNominalRole_maybe co1 <*> pure co2
1166 setNominalRole_maybe (ForAllCo tv co)
1167 = ForAllCo tv <$> setNominalRole_maybe co
1168 setNominalRole_maybe (NthCo n co)
1169 = NthCo n <$> setNominalRole_maybe co
1170 setNominalRole_maybe (InstCo co ty)
1171 = InstCo <$> setNominalRole_maybe co <*> pure ty
1172 setNominalRole_maybe _ = Nothing
1173
1174 -- takes any coercion and turns it into a Phantom coercion
1175 mkPhantomCo :: Coercion -> Coercion
1176 mkPhantomCo co
1177 | Just ty <- isReflCo_maybe co = Refl Phantom ty
1178 | Pair ty1 ty2 <- coercionKind co = UnivCo (fsLit "mkPhantomCo") Phantom ty1 ty2
1179 -- don't optimise here... wait for OptCoercion
1180
1181 -- All input coercions are assumed to be Nominal,
1182 -- or, if Role is Phantom, the Coercion can be Phantom, too.
1183 applyRole :: Role -> Coercion -> Coercion
1184 applyRole Nominal = id
1185 applyRole Representational = mkSubCo
1186 applyRole Phantom = mkPhantomCo
1187
1188 -- Convert args to a TyConAppCo Nominal to the same TyConAppCo Representational
1189 applyRoles :: TyCon -> [Coercion] -> [Coercion]
1190 applyRoles tc cos
1191 = zipWith applyRole (tyConRolesX Representational tc) cos
1192
1193 -- the Role parameter is the Role of the TyConAppCo
1194 -- defined here because this is intimiately concerned with the implementation
1195 -- of TyConAppCo
1196 tyConRolesX :: Role -> TyCon -> [Role]
1197 tyConRolesX Representational tc = tyConRoles tc ++ repeat Nominal
1198 tyConRolesX role _ = repeat role
1199
1200 nthRole :: Role -> TyCon -> Int -> Role
1201 nthRole Nominal _ _ = Nominal
1202 nthRole Phantom _ _ = Phantom
1203 nthRole Representational tc n
1204 = (tyConRolesX Representational tc) !! n
1205
1206 ltRole :: Role -> Role -> Bool
1207 -- Is one role "less" than another?
1208 -- Nominal < Representational < Phantom
1209 ltRole Phantom _ = False
1210 ltRole Representational Phantom = True
1211 ltRole Representational _ = False
1212 ltRole Nominal Nominal = False
1213 ltRole Nominal _ = True
1214
1215 -- See note [Newtype coercions] in TyCon
1216 -- | Create a coercion constructor (axiom) suitable for the given
1217 -- newtype 'TyCon'. The 'Name' should be that of a new coercion
1218 -- 'CoAxiom', the 'TyVar's the arguments expected by the @newtype@ and
1219 -- the type the appropriate right hand side of the @newtype@, with
1220 -- the free variables a subset of those 'TyVar's.
1221 mkNewTypeCo :: Name -> TyCon -> [TyVar] -> [Role] -> Type -> CoAxiom Unbranched
1222 mkNewTypeCo name tycon tvs roles rhs_ty
1223 = CoAxiom { co_ax_unique = nameUnique name
1224 , co_ax_name = name
1225 , co_ax_implicit = True -- See Note [Implicit axioms] in TyCon
1226 , co_ax_role = Representational
1227 , co_ax_tc = tycon
1228 , co_ax_branches = unbranched branch }
1229 where branch = CoAxBranch { cab_loc = getSrcSpan name
1230 , cab_tvs = tvs
1231 , cab_lhs = mkTyVarTys tvs
1232 , cab_roles = roles
1233 , cab_rhs = rhs_ty
1234 , cab_incomps = [] }
1235
1236 mkPiCos :: Role -> [Var] -> Coercion -> Coercion
1237 mkPiCos r vs co = foldr (mkPiCo r) co vs
1238
1239 mkPiCo :: Role -> Var -> Coercion -> Coercion
1240 mkPiCo r v co | isTyVar v = mkForAllCo v co
1241 | otherwise = mkFunCo r (mkReflCo r (varType v)) co
1242
1243 -- The first coercion *must* be Nominal.
1244 mkCoCast :: Coercion -> Coercion -> Coercion
1245 -- (mkCoCast (c :: s1 ~# t1) (g :: (s1 ~# t1) ~# (s2 ~# t2)
1246 mkCoCast c g
1247 = mkSymCo g1 `mkTransCo` c `mkTransCo` g2
1248 where
1249 -- g :: (s1 ~# s2) ~# (t1 ~# t2)
1250 -- g1 :: s1 ~# t1
1251 -- g2 :: s2 ~# t2
1252 [_reflk, g1, g2] = decomposeCo 3 g
1253 -- Remember, (~#) :: forall k. k -> k -> *
1254 -- so it takes *three* arguments, not two
1255
1256 {-
1257 ************************************************************************
1258 * *
1259 Newtypes
1260 * *
1261 ************************************************************************
1262 -}
1263
1264 -- | If @co :: T ts ~ rep_ty@ then:
1265 --
1266 -- > instNewTyCon_maybe T ts = Just (rep_ty, co)
1267 --
1268 -- Checks for a newtype, and for being saturated
1269 instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, Coercion)
1270 instNewTyCon_maybe tc tys
1271 | Just (tvs, ty, co_tc) <- unwrapNewTyConEtad_maybe tc -- Check for newtype
1272 , tvs `leLength` tys -- Check saturated enough
1273 = Just ( applyTysX tvs ty tys
1274 , mkUnbranchedAxInstCo Representational co_tc tys)
1275 | otherwise
1276 = Nothing
1277
1278 {-
1279 ************************************************************************
1280 * *
1281 Type normalisation
1282 * *
1283 ************************************************************************
1284 -}
1285
1286 -- | A function to check if we can reduce a type by one step. Used
1287 -- with 'topNormaliseTypeX_maybe'.
1288 type NormaliseStepper = RecTcChecker
1289 -> TyCon -- tc
1290 -> [Type] -- tys
1291 -> NormaliseStepResult
1292
1293 -- | The result of stepping in a normalisation function.
1294 -- See 'topNormaliseTypeX_maybe'.
1295 data NormaliseStepResult
1296 = NS_Done -- ^ Nothing more to do
1297 | NS_Abort -- ^ Utter failure. The outer function should fail too.
1298 | NS_Step RecTcChecker Type Coercion -- ^ We stepped, yielding new bits;
1299 -- ^ co :: old type ~ new type
1300
1301 modifyStepResultCo :: (Coercion -> Coercion)
1302 -> NormaliseStepResult -> NormaliseStepResult
1303 modifyStepResultCo f (NS_Step rec_nts ty co) = NS_Step rec_nts ty (f co)
1304 modifyStepResultCo _ result = result
1305
1306 -- | Try one stepper and then try the next,
1307 -- if the first doesn't make progress.
1308 -- So if it returns NS_Done, it means that both steppers are satisfied
1309 composeSteppers :: NormaliseStepper -> NormaliseStepper
1310 -> NormaliseStepper
1311 composeSteppers step1 step2 rec_nts tc tys
1312 = case step1 rec_nts tc tys of
1313 success@(NS_Step {}) -> success
1314 NS_Done -> step2 rec_nts tc tys
1315 NS_Abort -> NS_Abort
1316
1317 -- | A 'NormaliseStepper' that unwraps newtypes, careful not to fall into
1318 -- a loop. If it would fall into a loop, it produces 'NS_Abort'.
1319 unwrapNewTypeStepper :: NormaliseStepper
1320 unwrapNewTypeStepper rec_nts tc tys
1321 | Just (ty', co) <- instNewTyCon_maybe tc tys
1322 = case checkRecTc rec_nts tc of
1323 Just rec_nts' -> NS_Step rec_nts' ty' co
1324 Nothing -> NS_Abort
1325
1326 | otherwise
1327 = NS_Done
1328
1329 -- | A general function for normalising the top-level of a type. It continues
1330 -- to use the provided 'NormaliseStepper' until that function fails, and then
1331 -- this function returns. The roles of the coercions produced by the
1332 -- 'NormaliseStepper' must all be the same, which is the role returned from
1333 -- the call to 'topNormaliseTypeX_maybe'.
1334 topNormaliseTypeX_maybe :: NormaliseStepper -> Type -> Maybe (Coercion, Type)
1335 topNormaliseTypeX_maybe stepper
1336 = go initRecTc Nothing
1337 where
1338 go rec_nts mb_co1 ty
1339 | Just (tc, tys) <- splitTyConApp_maybe ty
1340 = case stepper rec_nts tc tys of
1341 NS_Step rec_nts' ty' co2
1342 -> go rec_nts' (mb_co1 `trans` co2) ty'
1343
1344 NS_Done -> all_done
1345 NS_Abort -> Nothing
1346
1347 | otherwise
1348 = all_done
1349 where
1350 all_done | Just co <- mb_co1 = Just (co, ty)
1351 | otherwise = Nothing
1352
1353 Nothing `trans` co2 = Just co2
1354 (Just co1) `trans` co2 = Just (co1 `mkTransCo` co2)
1355
1356 topNormaliseNewType_maybe :: Type -> Maybe (Coercion, Type)
1357 -- ^ Sometimes we want to look through a @newtype@ and get its associated coercion.
1358 -- This function strips off @newtype@ layers enough to reveal something that isn't
1359 -- a @newtype@, or responds False to ok_tc. Specifically, here's the invariant:
1360 --
1361 -- > topNormaliseNewType_maybe ty = Just (co, ty')
1362 --
1363 -- then (a) @co : ty0 ~ ty'@.
1364 -- (b) ty' is not a newtype.
1365 --
1366 -- The function returns @Nothing@ for non-@newtypes@,
1367 -- or unsaturated applications
1368 --
1369 -- This function does *not* look through type families, because it has no access to
1370 -- the type family environment. If you do have that at hand, consider to use
1371 -- topNormaliseType_maybe, which should be a drop-in replacement for
1372 -- topNormaliseNewType_maybe
1373 --
1374 topNormaliseNewType_maybe ty
1375 = topNormaliseTypeX_maybe unwrapNewTypeStepper ty
1376
1377 {-
1378 ************************************************************************
1379 * *
1380 Equality of coercions
1381 * *
1382 ************************************************************************
1383 -}
1384
1385 -- | Determines syntactic equality of coercions
1386 coreEqCoercion :: Coercion -> Coercion -> Bool
1387 coreEqCoercion co1 co2 = coreEqCoercion2 rn_env co1 co2
1388 where rn_env = mkRnEnv2 (mkInScopeSet (tyCoVarsOfCo co1 `unionVarSet` tyCoVarsOfCo co2))
1389
1390 coreEqCoercion2 :: RnEnv2 -> Coercion -> Coercion -> Bool
1391 coreEqCoercion2 env (Refl eq1 ty1) (Refl eq2 ty2) = eq1 == eq2 && eqTypeX env ty1 ty2
1392 coreEqCoercion2 env (TyConAppCo eq1 tc1 cos1) (TyConAppCo eq2 tc2 cos2)
1393 = eq1 == eq2 && tc1 == tc2 && all2 (coreEqCoercion2 env) cos1 cos2
1394
1395 coreEqCoercion2 env (AppCo co11 co12) (AppCo co21 co22)
1396 = coreEqCoercion2 env co11 co21 && coreEqCoercion2 env co12 co22
1397
1398 coreEqCoercion2 env (ForAllCo v1 co1) (ForAllCo v2 co2)
1399 = coreEqCoercion2 (rnBndr2 env v1 v2) co1 co2
1400
1401 coreEqCoercion2 env (CoVarCo cv1) (CoVarCo cv2)
1402 = rnOccL env cv1 == rnOccR env cv2
1403
1404 coreEqCoercion2 env (AxiomInstCo con1 ind1 cos1) (AxiomInstCo con2 ind2 cos2)
1405 = con1 == con2
1406 && ind1 == ind2
1407 && all2 (coreEqCoercion2 env) cos1 cos2
1408
1409 -- the provenance string is just a note, so don't use in comparisons
1410 coreEqCoercion2 env (UnivCo _ r1 ty11 ty12) (UnivCo _ r2 ty21 ty22)
1411 = r1 == r2 && eqTypeX env ty11 ty21 && eqTypeX env ty12 ty22
1412
1413 coreEqCoercion2 env (SymCo co1) (SymCo co2)
1414 = coreEqCoercion2 env co1 co2
1415
1416 coreEqCoercion2 env (TransCo co11 co12) (TransCo co21 co22)
1417 = coreEqCoercion2 env co11 co21 && coreEqCoercion2 env co12 co22
1418
1419 coreEqCoercion2 env (NthCo d1 co1) (NthCo d2 co2)
1420 = d1 == d2 && coreEqCoercion2 env co1 co2
1421 coreEqCoercion2 env (LRCo d1 co1) (LRCo d2 co2)
1422 = d1 == d2 && coreEqCoercion2 env co1 co2
1423
1424 coreEqCoercion2 env (InstCo co1 ty1) (InstCo co2 ty2)
1425 = coreEqCoercion2 env co1 co2 && eqTypeX env ty1 ty2
1426
1427 coreEqCoercion2 env (SubCo co1) (SubCo co2)
1428 = coreEqCoercion2 env co1 co2
1429
1430 coreEqCoercion2 env (AxiomRuleCo a1 ts1 cs1) (AxiomRuleCo a2 ts2 cs2)
1431 = a1 == a2 && all2 (eqTypeX env) ts1 ts2 && all2 (coreEqCoercion2 env) cs1 cs2
1432
1433 coreEqCoercion2 _ _ _ = False
1434
1435 {-
1436 ************************************************************************
1437 * *
1438 Substitution of coercions
1439 * *
1440 ************************************************************************
1441 -}
1442
1443 -- | A substitution of 'Coercion's for 'CoVar's (OR 'TyVar's, when
1444 -- doing a \"lifting\" substitution)
1445 type CvSubstEnv = VarEnv Coercion
1446
1447 emptyCvSubstEnv :: CvSubstEnv
1448 emptyCvSubstEnv = emptyVarEnv
1449
1450 data CvSubst
1451 = CvSubst InScopeSet -- The in-scope type variables
1452 TvSubstEnv -- Substitution of types
1453 CvSubstEnv -- Substitution of coercions
1454
1455 instance Outputable CvSubst where
1456 ppr (CvSubst ins tenv cenv)
1457 = brackets $ sep[ ptext (sLit "CvSubst"),
1458 nest 2 (ptext (sLit "In scope:") <+> ppr ins),
1459 nest 2 (ptext (sLit "Type env:") <+> ppr tenv),
1460 nest 2 (ptext (sLit "Coercion env:") <+> ppr cenv) ]
1461
1462 emptyCvSubst :: CvSubst
1463 emptyCvSubst = CvSubst emptyInScopeSet emptyVarEnv emptyVarEnv
1464
1465 isEmptyCvSubst :: CvSubst -> Bool
1466 isEmptyCvSubst (CvSubst _ tenv cenv) = isEmptyVarEnv tenv && isEmptyVarEnv cenv
1467
1468 getCvInScope :: CvSubst -> InScopeSet
1469 getCvInScope (CvSubst in_scope _ _) = in_scope
1470
1471 zapCvSubstEnv :: CvSubst -> CvSubst
1472 zapCvSubstEnv (CvSubst in_scope _ _) = CvSubst in_scope emptyVarEnv emptyVarEnv
1473
1474 cvTvSubst :: CvSubst -> TvSubst
1475 cvTvSubst (CvSubst in_scope tvs _) = TvSubst in_scope tvs
1476
1477 tvCvSubst :: TvSubst -> CvSubst
1478 tvCvSubst (TvSubst in_scope tenv) = CvSubst in_scope tenv emptyCvSubstEnv
1479
1480 extendTvSubst :: CvSubst -> TyVar -> Type -> CvSubst
1481 extendTvSubst (CvSubst in_scope tenv cenv) tv ty
1482 = CvSubst in_scope (extendVarEnv tenv tv ty) cenv
1483
1484 extendTvSubstAndInScope :: CvSubst -> TyVar -> Type -> CvSubst
1485 extendTvSubstAndInScope (CvSubst in_scope tenv cenv) tv ty
1486 = CvSubst (in_scope `extendInScopeSetSet` tyVarsOfType ty)
1487 (extendVarEnv tenv tv ty)
1488 cenv
1489
1490 extendCvSubstAndInScope :: CvSubst -> CoVar -> Coercion -> CvSubst
1491 -- Also extends the in-scope set
1492 extendCvSubstAndInScope (CvSubst in_scope tenv cenv) cv co
1493 = CvSubst (in_scope `extendInScopeSetSet` tyCoVarsOfCo co)
1494 tenv
1495 (extendVarEnv cenv cv co)
1496
1497 substCoVarBndr :: CvSubst -> CoVar -> (CvSubst, CoVar)
1498 substCoVarBndr subst@(CvSubst in_scope tenv cenv) old_var
1499 = ASSERT( isCoVar old_var )
1500 (CvSubst (in_scope `extendInScopeSet` new_var) tenv new_cenv, new_var)
1501 where
1502 -- When we substitute (co :: t1 ~ t2) we may get the identity (co :: t ~ t)
1503 -- In that case, mkCoVarCo will return a ReflCoercion, and
1504 -- we want to substitute that (not new_var) for old_var
1505 new_co = mkCoVarCo new_var
1506 no_change = new_var == old_var && not (isReflCo new_co)
1507
1508 new_cenv | no_change = delVarEnv cenv old_var
1509 | otherwise = extendVarEnv cenv old_var new_co
1510
1511 new_var = uniqAway in_scope subst_old_var
1512 subst_old_var = mkCoVar (varName old_var) (substTy subst (varType old_var))
1513 -- It's important to do the substitution for coercions,
1514 -- because they can have free type variables
1515
1516 substTyVarBndr :: CvSubst -> TyVar -> (CvSubst, TyVar)
1517 substTyVarBndr (CvSubst in_scope tenv cenv) old_var
1518 = case Type.substTyVarBndr (TvSubst in_scope tenv) old_var of
1519 (TvSubst in_scope' tenv', new_var) -> (CvSubst in_scope' tenv' cenv, new_var)
1520
1521 mkCvSubst :: InScopeSet -> [(Var,Coercion)] -> CvSubst
1522 mkCvSubst in_scope prs = CvSubst in_scope Type.emptyTvSubstEnv (mkVarEnv prs)
1523
1524 zipOpenCvSubst :: [Var] -> [Coercion] -> CvSubst
1525 zipOpenCvSubst vs cos
1526 | debugIsOn && (length vs /= length cos)
1527 = pprTrace "zipOpenCvSubst" (ppr vs $$ ppr cos) emptyCvSubst
1528 | otherwise
1529 = CvSubst (mkInScopeSet (tyCoVarsOfCos cos)) emptyTvSubstEnv (zipVarEnv vs cos)
1530
1531 substCoWithTy :: InScopeSet -> TyVar -> Type -> Coercion -> Coercion
1532 substCoWithTy in_scope tv ty = substCoWithTys in_scope [tv] [ty]
1533
1534 substCoWithTys :: InScopeSet -> [TyVar] -> [Type] -> Coercion -> Coercion
1535 substCoWithTys in_scope tvs tys co
1536 | debugIsOn && (length tvs /= length tys)
1537 = pprTrace "substCoWithTys" (ppr tvs $$ ppr tys) co
1538 | otherwise
1539 = ASSERT( length tvs == length tys )
1540 substCo (CvSubst in_scope (zipVarEnv tvs tys) emptyVarEnv) co
1541
1542 -- | Substitute within a 'Coercion'
1543 substCo :: CvSubst -> Coercion -> Coercion
1544 substCo subst co | isEmptyCvSubst subst = co
1545 | otherwise = subst_co subst co
1546
1547 -- | Substitute within several 'Coercion's
1548 substCos :: CvSubst -> [Coercion] -> [Coercion]
1549 substCos subst cos | isEmptyCvSubst subst = cos
1550 | otherwise = map (substCo subst) cos
1551
1552 substTy :: CvSubst -> Type -> Type
1553 substTy subst = Type.substTy (cvTvSubst subst)
1554
1555 subst_co :: CvSubst -> Coercion -> Coercion
1556 subst_co subst co
1557 = go co
1558 where
1559 go_ty :: Type -> Type
1560 go_ty = Coercion.substTy subst
1561
1562 go :: Coercion -> Coercion
1563 go (Refl eq ty) = Refl eq $! go_ty ty
1564 go (TyConAppCo eq tc cos) = let args = map go cos
1565 in args `seqList` TyConAppCo eq tc args
1566 go (AppCo co1 co2) = mkAppCo (go co1) $! go co2
1567 go (ForAllCo tv co) = case substTyVarBndr subst tv of
1568 (subst', tv') ->
1569 ForAllCo tv' $! subst_co subst' co
1570 go (CoVarCo cv) = substCoVar subst cv
1571 go (AxiomInstCo con ind cos) = AxiomInstCo con ind $! map go cos
1572 go (UnivCo s r ty1 ty2) = (UnivCo s r $! go_ty ty1) $! go_ty ty2
1573 go (SymCo co) = mkSymCo (go co)
1574 go (TransCo co1 co2) = mkTransCo (go co1) (go co2)
1575 go (NthCo d co) = mkNthCo d (go co)
1576 go (LRCo lr co) = mkLRCo lr (go co)
1577 go (InstCo co ty) = mkInstCo (go co) $! go_ty ty
1578 go (SubCo co) = mkSubCo (go co)
1579 go (AxiomRuleCo co ts cs) = let ts1 = map go_ty ts
1580 cs1 = map go cs
1581 in ts1 `seqList` cs1 `seqList`
1582 AxiomRuleCo co ts1 cs1
1583
1584
1585
1586 substCoVar :: CvSubst -> CoVar -> Coercion
1587 substCoVar (CvSubst in_scope _ cenv) cv
1588 | Just co <- lookupVarEnv cenv cv = co
1589 | Just cv1 <- lookupInScope in_scope cv = ASSERT( isCoVar cv1 ) CoVarCo cv1
1590 | otherwise = WARN( True, ptext (sLit "substCoVar not in scope") <+> ppr cv $$ ppr in_scope)
1591 ASSERT( isCoVar cv ) CoVarCo cv
1592
1593 substCoVars :: CvSubst -> [CoVar] -> [Coercion]
1594 substCoVars subst cvs = map (substCoVar subst) cvs
1595
1596 lookupTyVar :: CvSubst -> TyVar -> Maybe Type
1597 lookupTyVar (CvSubst _ tenv _) tv = lookupVarEnv tenv tv
1598
1599 lookupCoVar :: CvSubst -> Var -> Maybe Coercion
1600 lookupCoVar (CvSubst _ _ cenv) v = lookupVarEnv cenv v
1601
1602 {-
1603 ************************************************************************
1604 * *
1605 "Lifting" substitution
1606 [(TyVar,Coercion)] -> Type -> Coercion
1607 * *
1608 ************************************************************************
1609
1610 Note [Lifting coercions over types: liftCoSubst]
1611 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1612 The KPUSH rule deals with this situation
1613 data T a = MkK (a -> Maybe a)
1614 g :: T t1 ~ K t2
1615 x :: t1 -> Maybe t1
1616
1617 case (K @t1 x) |> g of
1618 K (y:t2 -> Maybe t2) -> rhs
1619
1620 We want to push the coercion inside the constructor application.
1621 So we do this
1622
1623 g' :: t1~t2 = Nth 0 g
1624
1625 case K @t2 (x |> g' -> Maybe g') of
1626 K (y:t2 -> Maybe t2) -> rhs
1627
1628 The crucial operation is that we
1629 * take the type of K's argument: a -> Maybe a
1630 * and substitute g' for a
1631 thus giving *coercion*. This is what liftCoSubst does.
1632
1633 Note [Substituting kinds in liftCoSubst]
1634 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1635 We need to take care with kind polymorphism. Suppose
1636 K :: forall k (a:k). (forall b:k. a -> b) -> T k a
1637
1638 Now given (K @kk1 @ty1 v) |> g) where
1639 g :: T kk1 ty1 ~ T kk2 ty2
1640 we want to compute
1641 (forall b:k a->b) [ Nth 0 g/k, Nth 1 g/a ]
1642 Notice that we MUST substitute for 'k'; this happens in
1643 liftCoSubstTyVarBndr. But what should we substitute?
1644 We need to take b's kind 'k' and return a Kind, not a Coercion!
1645
1646 Happily we can do this because we know that all kind coercions
1647 ((Nth 0 g) in this case) are Refl. So we need a special purpose
1648 subst_kind: LiftCoSubst -> Kind -> Kind
1649 that expects a Refl coercion (or something equivalent to Refl)
1650 when it looks up a kind variable.
1651 -}
1652
1653 -- ----------------------------------------------------
1654 -- See Note [Lifting coercions over types: liftCoSubst]
1655 -- ----------------------------------------------------
1656
1657 data LiftCoSubst = LCS InScopeSet LiftCoEnv
1658
1659 type LiftCoEnv = VarEnv Coercion
1660 -- Maps *type variables* to *coercions*
1661 -- That's the whole point of this function!
1662
1663 liftCoSubstWith :: Role -> [TyVar] -> [Coercion] -> Type -> Coercion
1664 liftCoSubstWith r tvs cos ty
1665 = liftCoSubst r (zipEqual "liftCoSubstWith" tvs cos) ty
1666
1667 liftCoSubst :: Role -> [(TyVar,Coercion)] -> Type -> Coercion
1668 liftCoSubst r prs ty
1669 | null prs = Refl r ty
1670 | otherwise = ty_co_subst (LCS (mkInScopeSet (tyCoVarsOfCos (map snd prs)))
1671 (mkVarEnv prs)) r ty
1672
1673 -- | The \"lifting\" operation which substitutes coercions for type
1674 -- variables in a type to produce a coercion.
1675 --
1676 -- For the inverse operation, see 'liftCoMatch'
1677
1678 -- The Role parameter is the _desired_ role
1679 ty_co_subst :: LiftCoSubst -> Role -> Type -> Coercion
1680 ty_co_subst subst role ty
1681 = go role ty
1682 where
1683 go Phantom ty = lift_phantom ty
1684 go role (TyVarTy tv) = liftCoSubstTyVar subst role tv
1685 `orElse` Refl role (TyVarTy tv)
1686 -- A type variable from a non-cloned forall
1687 -- won't be in the substitution
1688 go role (AppTy ty1 ty2) = mkAppCo (go role ty1) (go Nominal ty2)
1689 go role (TyConApp tc tys) = mkTyConAppCo role tc
1690 (zipWith go (tyConRolesX role tc) tys)
1691 -- IA0_NOTE: Do we need to do anything
1692 -- about kind instantiations? I don't think
1693 -- so. see Note [Kind coercions]
1694 go role (FunTy ty1 ty2) = mkFunCo role (go role ty1) (go role ty2)
1695 go role (ForAllTy v ty) = mkForAllCo v' $! (ty_co_subst subst' role ty)
1696 where
1697 (subst', v') = liftCoSubstTyVarBndr subst v
1698 go role ty@(LitTy {}) = ASSERT( role == Nominal )
1699 mkReflCo role ty
1700
1701 lift_phantom ty = mkUnivCo (fsLit "lift_phantom")
1702 Phantom (liftCoSubstLeft subst ty)
1703 (liftCoSubstRight subst ty)
1704
1705 {-
1706 Note [liftCoSubstTyVar]
1707 ~~~~~~~~~~~~~~~~~~~~~~~
1708 This function can fail (i.e., return Nothing) for two separate reasons:
1709 1) The variable is not in the substutition
1710 2) The coercion found is of too low a role
1711
1712 liftCoSubstTyVar is called from two places: in liftCoSubst (naturally), and
1713 also in matchAxiom in OptCoercion. From liftCoSubst, the so-called lifting
1714 lemma guarantees that the roles work out. If we fail for reason 2) in this
1715 case, we really should panic -- something is deeply wrong. But, in matchAxiom,
1716 failing for reason 2) is fine. matchAxiom is trying to find a set of coercions
1717 that match, but it may fail, and this is healthy behavior. Bottom line: if
1718 you find that liftCoSubst is doing weird things (like leaving out-of-scope
1719 variables lying around), disable coercion optimization (bypassing matchAxiom)
1720 and use downgradeRole instead of downgradeRole_maybe. The panic will then happen,
1721 and you may learn something useful.
1722 -}
1723
1724 liftCoSubstTyVar :: LiftCoSubst -> Role -> TyVar -> Maybe Coercion
1725 liftCoSubstTyVar (LCS _ cenv) r tv
1726 = do { co <- lookupVarEnv cenv tv
1727 ; let co_role = coercionRole co -- could theoretically take this as
1728 -- a parameter, but painful
1729 ; downgradeRole_maybe r co_role co } -- see Note [liftCoSubstTyVar]
1730
1731 liftCoSubstTyVarBndr :: LiftCoSubst -> TyVar -> (LiftCoSubst, TyVar)
1732 liftCoSubstTyVarBndr subst@(LCS in_scope cenv) old_var
1733 = (LCS (in_scope `extendInScopeSet` new_var) new_cenv, new_var)
1734 where
1735 new_cenv | no_change = delVarEnv cenv old_var
1736 | otherwise = extendVarEnv cenv old_var (Refl Nominal (TyVarTy new_var))
1737
1738 no_change = no_kind_change && (new_var == old_var)
1739
1740 new_var1 = uniqAway in_scope old_var
1741
1742 old_ki = tyVarKind old_var
1743 no_kind_change = isEmptyVarSet (tyVarsOfType old_ki)
1744 new_var | no_kind_change = new_var1
1745 | otherwise = setTyVarKind new_var1 (subst_kind subst old_ki)
1746
1747 -- map every variable to the type on the *left* of its mapped coercion
1748 liftCoSubstLeft :: LiftCoSubst -> Type -> Type
1749 liftCoSubstLeft (LCS in_scope cenv) ty
1750 = Type.substTy (mkTvSubst in_scope (mapVarEnv (pFst . coercionKind) cenv)) ty
1751
1752 -- same, but to the type on the right
1753 liftCoSubstRight :: LiftCoSubst -> Type -> Type
1754 liftCoSubstRight (LCS in_scope cenv) ty
1755 = Type.substTy (mkTvSubst in_scope (mapVarEnv (pSnd . coercionKind) cenv)) ty
1756
1757 subst_kind :: LiftCoSubst -> Kind -> Kind
1758 -- See Note [Substituting kinds in liftCoSubst]
1759 subst_kind subst@(LCS _ cenv) kind
1760 = go kind
1761 where
1762 go (LitTy n) = n `seq` LitTy n
1763 go (TyVarTy kv) = subst_kv kv
1764 go (TyConApp tc tys) = let args = map go tys
1765 in args `seqList` TyConApp tc args
1766
1767 go (FunTy arg res) = (FunTy $! (go arg)) $! (go res)
1768 go (AppTy fun arg) = mkAppTy (go fun) $! (go arg)
1769 go (ForAllTy tv ty) = case liftCoSubstTyVarBndr subst tv of
1770 (subst', tv') ->
1771 ForAllTy tv' $! (subst_kind subst' ty)
1772
1773 subst_kv kv
1774 | Just co <- lookupVarEnv cenv kv
1775 , let co_kind = coercionKind co
1776 = ASSERT2( pFst co_kind `eqKind` pSnd co_kind, ppr kv $$ ppr co )
1777 pFst co_kind
1778 | otherwise
1779 = TyVarTy kv
1780
1781 -- | 'liftCoMatch' is sort of inverse to 'liftCoSubst'. In particular, if
1782 -- @liftCoMatch vars ty co == Just s@, then @tyCoSubst s ty == co@.
1783 -- That is, it matches a type against a coercion of the same
1784 -- "shape", and returns a lifting substitution which could have been
1785 -- used to produce the given coercion from the given type.
1786 liftCoMatch :: TyVarSet -> Type -> Coercion -> Maybe LiftCoSubst
1787 liftCoMatch tmpls ty co
1788 = case ty_co_match menv emptyVarEnv ty co of
1789 Just cenv -> Just (LCS in_scope cenv)
1790 Nothing -> Nothing
1791 where
1792 menv = ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope }
1793 in_scope = mkInScopeSet (tmpls `unionVarSet` tyCoVarsOfCo co)
1794 -- Like tcMatchTy, assume all the interesting variables
1795 -- in ty are in tmpls
1796
1797 -- | 'ty_co_match' does all the actual work for 'liftCoMatch'.
1798 ty_co_match :: MatchEnv -> LiftCoEnv -> Type -> Coercion -> Maybe LiftCoEnv
1799 ty_co_match menv subst ty co
1800 | Just ty' <- coreView ty = ty_co_match menv subst ty' co
1801
1802 -- Match a type variable against a non-refl coercion
1803 ty_co_match menv cenv (TyVarTy tv1) co
1804 | Just co1' <- lookupVarEnv cenv tv1' -- tv1' is already bound to co1
1805 = if coreEqCoercion2 (nukeRnEnvL rn_env) co1' co
1806 then Just cenv
1807 else Nothing -- no match since tv1 matches two different coercions
1808
1809 | tv1' `elemVarSet` me_tmpls menv -- tv1' is a template var
1810 = if any (inRnEnvR rn_env) (varSetElems (tyCoVarsOfCo co))
1811 then Nothing -- occurs check failed
1812 else return (extendVarEnv cenv tv1' co)
1813 -- BAY: I don't think we need to do any kind matching here yet
1814 -- (compare 'match'), but we probably will when moving to SHE.
1815
1816 | otherwise -- tv1 is not a template ty var, so the only thing it
1817 -- can match is a reflexivity coercion for itself.
1818 -- But that case is dealt with already
1819 = Nothing
1820
1821 where
1822 rn_env = me_env menv
1823 tv1' = rnOccL rn_env tv1
1824
1825 ty_co_match menv subst (AppTy ty1 ty2) co
1826 | Just (co1, co2) <- splitAppCo_maybe co -- c.f. Unify.match on AppTy
1827 = do { subst' <- ty_co_match menv subst ty1 co1
1828 ; ty_co_match menv subst' ty2 co2 }
1829
1830 ty_co_match menv subst (TyConApp tc1 tys) (TyConAppCo _ tc2 cos)
1831 | tc1 == tc2 = ty_co_matches menv subst tys cos
1832
1833 ty_co_match menv subst (FunTy ty1 ty2) (TyConAppCo _ tc cos)
1834 | tc == funTyCon = ty_co_matches menv subst [ty1,ty2] cos
1835
1836 ty_co_match menv subst (ForAllTy tv1 ty) (ForAllCo tv2 co)
1837 = ty_co_match menv' subst ty co
1838 where
1839 menv' = menv { me_env = rnBndr2 (me_env menv) tv1 tv2 }
1840
1841 ty_co_match menv subst ty co
1842 | Just co' <- pushRefl co = ty_co_match menv subst ty co'
1843 | otherwise = Nothing
1844
1845 ty_co_matches :: MatchEnv -> LiftCoEnv -> [Type] -> [Coercion] -> Maybe LiftCoEnv
1846 ty_co_matches menv = matchList (ty_co_match menv)
1847
1848 pushRefl :: Coercion -> Maybe Coercion
1849 pushRefl (Refl Nominal (AppTy ty1 ty2))
1850 = Just (AppCo (Refl Nominal ty1) (Refl Nominal ty2))
1851 pushRefl (Refl r (FunTy ty1 ty2))
1852 = Just (TyConAppCo r funTyCon [Refl r ty1, Refl r ty2])
1853 pushRefl (Refl r (TyConApp tc tys))
1854 = Just (TyConAppCo r tc (zipWith mkReflCo (tyConRolesX r tc) tys))
1855 pushRefl (Refl r (ForAllTy tv ty)) = Just (ForAllCo tv (Refl r ty))
1856 pushRefl _ = Nothing
1857
1858 {-
1859 ************************************************************************
1860 * *
1861 Sequencing on coercions
1862 * *
1863 ************************************************************************
1864 -}
1865
1866 seqCo :: Coercion -> ()
1867 seqCo (Refl eq ty) = eq `seq` seqType ty
1868 seqCo (TyConAppCo eq tc cos) = eq `seq` tc `seq` seqCos cos
1869 seqCo (AppCo co1 co2) = seqCo co1 `seq` seqCo co2
1870 seqCo (ForAllCo tv co) = seqType (tyVarKind tv) `seq` seqCo co
1871 seqCo (CoVarCo cv) = cv `seq` ()
1872 seqCo (AxiomInstCo con ind cos) = con `seq` ind `seq` seqCos cos
1873 seqCo (UnivCo s r ty1 ty2) = s `seq` r `seq` seqType ty1 `seq` seqType ty2
1874 seqCo (SymCo co) = seqCo co
1875 seqCo (TransCo co1 co2) = seqCo co1 `seq` seqCo co2
1876 seqCo (NthCo n co) = n `seq` seqCo co
1877 seqCo (LRCo lr co) = lr `seq` seqCo co
1878 seqCo (InstCo co ty) = seqCo co `seq` seqType ty
1879 seqCo (SubCo co) = seqCo co
1880 seqCo (AxiomRuleCo _ ts cs) = seqTypes ts `seq` seqCos cs
1881
1882 seqCos :: [Coercion] -> ()
1883 seqCos [] = ()
1884 seqCos (co:cos) = seqCo co `seq` seqCos cos
1885
1886 {-
1887 ************************************************************************
1888 * *
1889 The kind of a type, and of a coercion
1890 * *
1891 ************************************************************************
1892
1893 Note [Computing a coercion kind and role]
1894 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1895 To compute a coercion's kind is straightforward: see coercionKind.
1896 But to compute a coercion's role, in the case for NthCo we need
1897 its kind as well. So if we have two separate functions (one for kinds
1898 and one for roles) we can get exponentially bad behaviour, since each
1899 NthCo node makes a separate call to coercionKind, which traverses the
1900 sub-tree again. This was part of the problem in Trac #9233.
1901
1902 Solution: compute both together; hence coercionKindRole. We keep a
1903 separate coercionKind function because it's a bit more efficient if
1904 the kind is all you want.
1905 -}
1906
1907 coercionType :: Coercion -> Type
1908 coercionType co = case coercionKindRole co of
1909 (Pair ty1 ty2, r) -> mkCoercionType r ty1 ty2
1910
1911 ------------------
1912 -- | If it is the case that
1913 --
1914 -- > c :: (t1 ~ t2)
1915 --
1916 -- i.e. the kind of @c@ relates @t1@ and @t2@, then @coercionKind c = Pair t1 t2@.
1917
1918 coercionKind :: Coercion -> Pair Type
1919 coercionKind co = go co
1920 where
1921 go (Refl _ ty) = Pair ty ty
1922 go (TyConAppCo _ tc cos) = mkTyConApp tc <$> (sequenceA $ map go cos)
1923 go (AppCo co1 co2) = mkAppTy <$> go co1 <*> go co2
1924 go (ForAllCo tv co) = mkForAllTy tv <$> go co
1925 go (CoVarCo cv) = toPair $ coVarKind cv
1926 go (AxiomInstCo ax ind cos)
1927 | CoAxBranch { cab_tvs = tvs, cab_lhs = lhs, cab_rhs = rhs } <- coAxiomNthBranch ax ind
1928 , Pair tys1 tys2 <- sequenceA (map go cos)
1929 = ASSERT( cos `equalLength` tvs ) -- Invariant of AxiomInstCo: cos should
1930 -- exactly saturate the axiom branch
1931 Pair (substTyWith tvs tys1 (mkTyConApp (coAxiomTyCon ax) lhs))
1932 (substTyWith tvs tys2 rhs)
1933 go (UnivCo _ _ ty1 ty2) = Pair ty1 ty2
1934 go (SymCo co) = swap $ go co
1935 go (TransCo co1 co2) = Pair (pFst $ go co1) (pSnd $ go co2)
1936 go (NthCo d co) = tyConAppArgN d <$> go co
1937 go (LRCo lr co) = (pickLR lr . splitAppTy) <$> go co
1938 go (InstCo aco ty) = go_app aco [ty]
1939 go (SubCo co) = go co
1940 go (AxiomRuleCo ax tys cos) =
1941 case coaxrProves ax tys (map go cos) of
1942 Just res -> res
1943 Nothing -> panic "coercionKind: Malformed coercion"
1944
1945 go_app :: Coercion -> [Type] -> Pair Type
1946 -- Collect up all the arguments and apply all at once
1947 -- See Note [Nested InstCos]
1948 go_app (InstCo co ty) tys = go_app co (ty:tys)
1949 go_app co tys = (`applyTys` tys) <$> go co
1950
1951 -- | Apply 'coercionKind' to multiple 'Coercion's
1952 coercionKinds :: [Coercion] -> Pair [Type]
1953 coercionKinds tys = sequenceA $ map coercionKind tys
1954
1955 -- | Get a coercion's kind and role.
1956 -- Why both at once? See Note [Computing a coercion kind and role]
1957 coercionKindRole :: Coercion -> (Pair Type, Role)
1958 coercionKindRole = go
1959 where
1960 go (Refl r ty) = (Pair ty ty, r)
1961 go (TyConAppCo r tc cos)
1962 = (mkTyConApp tc <$> (sequenceA $ map coercionKind cos), r)
1963 go (AppCo co1 co2)
1964 = let (tys1, r1) = go co1 in
1965 (mkAppTy <$> tys1 <*> coercionKind co2, r1)
1966 go (ForAllCo tv co)
1967 = let (tys, r) = go co in
1968 (mkForAllTy tv <$> tys, r)
1969 go (CoVarCo cv) = (toPair $ coVarKind cv, coVarRole cv)
1970 go co@(AxiomInstCo ax _ _) = (coercionKind co, coAxiomRole ax)
1971 go (UnivCo _ r ty1 ty2) = (Pair ty1 ty2, r)
1972 go (SymCo co) = first swap $ go co
1973 go (TransCo co1 co2)
1974 = let (tys1, r) = go co1 in
1975 (Pair (pFst tys1) (pSnd $ coercionKind co2), r)
1976 go (NthCo d co)
1977 = let (Pair t1 t2, r) = go co
1978 (tc1, args1) = splitTyConApp t1
1979 (_tc2, args2) = splitTyConApp t2
1980 in
1981 ASSERT( tc1 == _tc2 )
1982 ((`getNth` d) <$> Pair args1 args2, nthRole r tc1 d)
1983 go co@(LRCo {}) = (coercionKind co, Nominal)
1984 go (InstCo co ty) = go_app co [ty]
1985 go (SubCo co) = (coercionKind co, Representational)
1986 go co@(AxiomRuleCo ax _ _) = (coercionKind co, coaxrRole ax)
1987
1988 go_app :: Coercion -> [Type] -> (Pair Type, Role)
1989 -- Collect up all the arguments and apply all at once
1990 -- See Note [Nested InstCos]
1991 go_app (InstCo co ty) tys = go_app co (ty:tys)
1992 go_app co tys
1993 = let (pair, r) = go co in
1994 ((`applyTys` tys) <$> pair, r)
1995
1996 -- | Retrieve the role from a coercion.
1997 coercionRole :: Coercion -> Role
1998 coercionRole = snd . coercionKindRole
1999 -- There's not a better way to do this, because NthCo needs the *kind*
2000 -- and role of its argument. Luckily, laziness should generally avoid
2001 -- the need for computing kinds in other cases.
2002
2003 {-
2004 Note [Nested InstCos]
2005 ~~~~~~~~~~~~~~~~~~~~~
2006 In Trac #5631 we found that 70% of the entire compilation time was
2007 being spent in coercionKind! The reason was that we had
2008 (g @ ty1 @ ty2 .. @ ty100) -- The "@s" are InstCos
2009 where
2010 g :: forall a1 a2 .. a100. phi
2011 If we deal with the InstCos one at a time, we'll do this:
2012 1. Find the kind of (g @ ty1 .. @ ty99) : forall a100. phi'
2013 2. Substitute phi'[ ty100/a100 ], a single tyvar->type subst
2014 But this is a *quadratic* algorithm, and the blew up Trac #5631.
2015 So it's very important to do the substitution simultaneously.
2016
2017 cf Type.applyTys (which in fact we call here)
2018 -}
2019
2020 applyCo :: Type -> Coercion -> Type
2021 -- Gives the type of (e co) where e :: (a~b) => ty
2022 applyCo ty co | Just ty' <- coreView ty = applyCo ty' co
2023 applyCo (FunTy _ ty) _ = ty
2024 applyCo _ _ = panic "applyCo"
2025
2026 {-
2027 Note [Kind coercions]
2028 ~~~~~~~~~~~~~~~~~~~~~
2029 Kind coercions are only of the form: Refl kind. They are only used to
2030 instantiate kind polymorphic type constructors in TyConAppCo. Remember
2031 that kind instantiation only happens with TyConApp, not AppTy.
2032 -}