Remove old coercion pretty-printer
[ghc.git] / compiler / types / Coercion.hs
1 {-
2 (c) The University of Glasgow 2006
3 -}
4
5 {-# LANGUAGE RankNTypes, CPP, MultiWayIf, FlexibleContexts #-}
6
7 -- | Module for (a) type kinds and (b) type coercions,
8 -- as used in System FC. See 'CoreSyn.Expr' for
9 -- more on System FC and how coercions fit into it.
10 --
11 module Coercion (
12 -- * Main data type
13 Coercion, CoercionN, CoercionR, CoercionP,
14 UnivCoProvenance, CoercionHole, LeftOrRight(..),
15 Var, CoVar, TyCoVar,
16 Role(..), ltRole,
17
18 -- ** Functions over coercions
19 coVarTypes, coVarKind, coVarKindsTypesRole, coVarRole,
20 coercionType, coercionKind, coercionKinds,
21 mkCoercionType,
22 coercionRole, coercionKindRole,
23
24 -- ** Constructing coercions
25 mkReflCo, mkRepReflCo, mkNomReflCo,
26 mkCoVarCo, mkCoVarCos,
27 mkAxInstCo, mkUnbranchedAxInstCo,
28 mkAxInstRHS, mkUnbranchedAxInstRHS,
29 mkAxInstLHS, mkUnbranchedAxInstLHS,
30 mkPiCo, mkPiCos, mkCoCast,
31 mkSymCo, mkTransCo, mkTransAppCo,
32 mkNthCo, mkNthCoRole, mkLRCo,
33 mkInstCo, mkAppCo, mkAppCos, mkTyConAppCo, mkFunCo, mkFunCos,
34 mkForAllCo, mkForAllCos, mkHomoForAllCos, mkHomoForAllCos_NoRefl,
35 mkPhantomCo, mkHomoPhantomCo, toPhantomCo,
36 mkUnsafeCo, mkHoleCo, mkUnivCo, mkSubCo,
37 mkAxiomInstCo, mkProofIrrelCo,
38 downgradeRole, maybeSubCo, mkAxiomRuleCo,
39 mkCoherenceCo, mkCoherenceRightCo, mkCoherenceLeftCo,
40 mkKindCo, castCoercionKind,
41
42 mkHeteroCoercionType,
43
44 -- ** Decomposition
45 instNewTyCon_maybe,
46
47 NormaliseStepper, NormaliseStepResult(..), composeSteppers,
48 mapStepResult, unwrapNewTypeStepper,
49 topNormaliseNewType_maybe, topNormaliseTypeX,
50
51 decomposeCo, decomposeFunCo, getCoVar_maybe,
52 splitTyConAppCo_maybe,
53 splitAppCo_maybe,
54 splitFunCo_maybe,
55 splitForAllCo_maybe,
56
57 nthRole, tyConRolesX, tyConRolesRepresentational, setNominalRole_maybe,
58
59 pickLR,
60
61 isReflCo, isReflCo_maybe, isReflexiveCo, isReflexiveCo_maybe,
62 isReflCoVar_maybe,
63
64 -- ** Coercion variables
65 mkCoVar, isCoVar, coVarName, setCoVarName, setCoVarUnique,
66 isCoVar_maybe,
67
68 -- ** Free variables
69 tyCoVarsOfCo, tyCoVarsOfCos, coVarsOfCo,
70 tyCoFVsOfCo, tyCoFVsOfCos, tyCoVarsOfCoDSet,
71 coercionSize,
72
73 -- ** Substitution
74 CvSubstEnv, emptyCvSubstEnv,
75 lookupCoVar,
76 substCo, substCos, substCoVar, substCoVars, substCoWith,
77 substCoVarBndr,
78 extendTvSubstAndInScope, getCvSubstEnv,
79
80 -- ** Lifting
81 liftCoSubst, liftCoSubstTyVar, liftCoSubstWith, liftCoSubstWithEx,
82 emptyLiftingContext, extendLiftingContext,
83 liftCoSubstVarBndrCallback, isMappedByLC,
84
85 mkSubstLiftingContext, zapLiftingContext,
86 substForAllCoBndrCallbackLC, lcTCvSubst, lcInScopeSet,
87
88 LiftCoEnv, LiftingContext(..), liftEnvSubstLeft, liftEnvSubstRight,
89 substRightCo, substLeftCo, swapLiftCoEnv, lcSubstLeft, lcSubstRight,
90
91 -- ** Comparison
92 eqCoercion, eqCoercionX,
93
94 -- ** Forcing evaluation of coercions
95 seqCo,
96
97 -- * Pretty-printing
98 pprCo, pprParendCo,
99 pprCoAxiom, pprCoAxBranch, pprCoAxBranchHdr,
100
101 -- * Tidying
102 tidyCo, tidyCos,
103
104 -- * Other
105 promoteCoercion
106 ) where
107
108 #include "HsVersions.h"
109
110 import TyCoRep
111 import Type
112 import TyCon
113 import CoAxiom
114 import Var
115 import VarEnv
116 import Name hiding ( varName )
117 import Util
118 import BasicTypes
119 import Outputable
120 import Unique
121 import Pair
122 import SrcLoc
123 import PrelNames
124 import TysPrim ( eqPhantPrimTyCon )
125 import ListSetOps
126 import Maybes
127 import UniqFM
128
129 import Control.Monad (foldM)
130 import Control.Arrow ( first )
131 import Data.Function ( on )
132
133 {-
134 %************************************************************************
135 %* *
136 -- The coercion arguments always *precisely* saturate
137 -- arity of (that branch of) the CoAxiom. If there are
138 -- any left over, we use AppCo. See
139 -- See [Coercion axioms applied to coercions] in TyCoRep
140
141 \subsection{Coercion variables}
142 %* *
143 %************************************************************************
144 -}
145
146 coVarName :: CoVar -> Name
147 coVarName = varName
148
149 setCoVarUnique :: CoVar -> Unique -> CoVar
150 setCoVarUnique = setVarUnique
151
152 setCoVarName :: CoVar -> Name -> CoVar
153 setCoVarName = setVarName
154
155 {-
156 %************************************************************************
157 %* *
158 Pretty-printing CoAxioms
159 %* *
160 %************************************************************************
161
162 Defined here to avoid module loops. CoAxiom is loaded very early on.
163
164 -}
165
166 pprCoAxiom :: CoAxiom br -> SDoc
167 pprCoAxiom ax@(CoAxiom { co_ax_branches = branches })
168 = hang (text "axiom" <+> ppr ax <+> dcolon)
169 2 (vcat (map (ppr_co_ax_branch (const pprType) ax) $ fromBranches branches))
170
171 pprCoAxBranch :: CoAxiom br -> CoAxBranch -> SDoc
172 pprCoAxBranch = ppr_co_ax_branch pprRhs
173 where
174 pprRhs fam_tc rhs
175 | Just (tycon, _) <- splitTyConApp_maybe rhs
176 , isDataFamilyTyCon fam_tc
177 = pprDataCons tycon
178
179 | otherwise
180 = ppr rhs
181
182 pprCoAxBranchHdr :: CoAxiom br -> BranchIndex -> SDoc
183 pprCoAxBranchHdr ax index = pprCoAxBranch ax (coAxiomNthBranch ax index)
184
185 ppr_co_ax_branch :: (TyCon -> Type -> SDoc) -> CoAxiom br -> CoAxBranch -> SDoc
186 ppr_co_ax_branch ppr_rhs
187 (CoAxiom { co_ax_tc = fam_tc, co_ax_name = name })
188 (CoAxBranch { cab_tvs = tvs
189 , cab_cvs = cvs
190 , cab_lhs = lhs
191 , cab_rhs = rhs
192 , cab_loc = loc })
193 = foldr1 (flip hangNotEmpty 2)
194 [ pprUserForAll (mkTyVarBinders Inferred (tvs ++ cvs))
195 , pprTypeApp fam_tc lhs <+> equals <+> ppr_rhs fam_tc rhs
196 , text "-- Defined" <+> pprLoc loc ]
197 where
198 pprLoc loc
199 | isGoodSrcSpan loc
200 = text "at" <+> ppr (srcSpanStart loc)
201
202 | otherwise
203 = text "in" <+>
204 quotes (ppr (nameModule name))
205
206 {-
207 %************************************************************************
208 %* *
209 Destructing coercions
210 %* *
211 %************************************************************************
212
213 Note [Function coercions]
214 ~~~~~~~~~~~~~~~~~~~~~~~~~
215 Remember that
216 (->) :: forall r1 r2. TYPE r1 -> TYPE r2 -> TYPE LiftedRep
217
218 Hence
219 FunCo r co1 co2 :: (s1->t1) ~r (s2->t2)
220 is short for
221 TyConAppCo (->) co_rep1 co_rep2 co1 co2
222 where co_rep1, co_rep2 are the coercions on the representations.
223 -}
224
225
226 -- | This breaks a 'Coercion' with type @T A B C ~ T D E F@ into
227 -- a list of 'Coercion's of kinds @A ~ D@, @B ~ E@ and @E ~ F@. Hence:
228 --
229 -- > decomposeCo 3 c = [nth 0 c, nth 1 c, nth 2 c]
230 decomposeCo :: Arity -> Coercion -> [Coercion]
231 decomposeCo arity co
232 = [mkNthCo n co | n <- [0..(arity-1)] ]
233 -- Remember, Nth is zero-indexed
234
235 decomposeFunCo :: Coercion -> (Coercion, Coercion)
236 -- Expects co :: (s1 -> t1) ~ (s2 -> t2)
237 -- Returns (co1 :: s1~s2, co2 :: t1~t2)
238 -- See Note [Function coercions] for the "2" and "3"
239 decomposeFunCo co = ASSERT2( all_ok, ppr co )
240 (mkNthCo 2 co, mkNthCo 3 co)
241 where
242 Pair s1t1 s2t2 = coercionKind co
243 all_ok = isFunTy s1t1 && isFunTy s2t2
244
245 -- | Attempts to obtain the type variable underlying a 'Coercion'
246 getCoVar_maybe :: Coercion -> Maybe CoVar
247 getCoVar_maybe (CoVarCo cv) = Just cv
248 getCoVar_maybe _ = Nothing
249
250 -- | Attempts to tease a coercion apart into a type constructor and the application
251 -- of a number of coercion arguments to that constructor
252 splitTyConAppCo_maybe :: Coercion -> Maybe (TyCon, [Coercion])
253 splitTyConAppCo_maybe (Refl r ty)
254 = do { (tc, tys) <- splitTyConApp_maybe ty
255 ; let args = zipWith mkReflCo (tyConRolesX r tc) tys
256 ; return (tc, args) }
257 splitTyConAppCo_maybe (TyConAppCo _ tc cos) = Just (tc, cos)
258 splitTyConAppCo_maybe (FunCo _ arg res) = Just (funTyCon, cos)
259 where cos = [mkRuntimeRepCo arg, mkRuntimeRepCo res, arg, res]
260 splitTyConAppCo_maybe _ = Nothing
261
262 -- first result has role equal to input; third result is Nominal
263 splitAppCo_maybe :: Coercion -> Maybe (Coercion, Coercion)
264 -- ^ Attempt to take a coercion application apart.
265 splitAppCo_maybe (AppCo co arg) = Just (co, arg)
266 splitAppCo_maybe (TyConAppCo r tc args)
267 | mightBeUnsaturatedTyCon tc || args `lengthExceeds` tyConArity tc
268 -- Never create unsaturated type family apps!
269 , Just (args', arg') <- snocView args
270 , Just arg'' <- setNominalRole_maybe arg'
271 = Just ( mkTyConAppCo r tc args', arg'' )
272 -- Use mkTyConAppCo to preserve the invariant
273 -- that identity coercions are always represented by Refl
274
275 splitAppCo_maybe (Refl r ty)
276 | Just (ty1, ty2) <- splitAppTy_maybe ty
277 = Just (mkReflCo r ty1, mkNomReflCo ty2)
278 splitAppCo_maybe _ = Nothing
279
280 splitFunCo_maybe :: Coercion -> Maybe (Coercion, Coercion)
281 splitFunCo_maybe (FunCo _ arg res) = Just (arg, res)
282 splitFunCo_maybe _ = Nothing
283
284 splitForAllCo_maybe :: Coercion -> Maybe (TyVar, Coercion, Coercion)
285 splitForAllCo_maybe (ForAllCo tv k_co co) = Just (tv, k_co, co)
286 splitForAllCo_maybe _ = Nothing
287
288 -------------------------------------------------------
289 -- and some coercion kind stuff
290
291 coVarTypes :: CoVar -> Pair Type
292 coVarTypes cv
293 | (_, _, ty1, ty2, _) <- coVarKindsTypesRole cv
294 = Pair ty1 ty2
295
296 coVarKindsTypesRole :: CoVar -> (Kind,Kind,Type,Type,Role)
297 coVarKindsTypesRole cv
298 | Just (tc, [k1,k2,ty1,ty2]) <- splitTyConApp_maybe (varType cv)
299 = let role
300 | tc `hasKey` eqPrimTyConKey = Nominal
301 | tc `hasKey` eqReprPrimTyConKey = Representational
302 | otherwise = panic "coVarKindsTypesRole"
303 in (k1,k2,ty1,ty2,role)
304 | otherwise = pprPanic "coVarKindsTypesRole, non coercion variable"
305 (ppr cv $$ ppr (varType cv))
306
307 coVarKind :: CoVar -> Type
308 coVarKind cv
309 = ASSERT( isCoVar cv )
310 varType cv
311
312 coVarRole :: CoVar -> Role
313 coVarRole cv
314 | tc `hasKey` eqPrimTyConKey
315 = Nominal
316 | tc `hasKey` eqReprPrimTyConKey
317 = Representational
318 | otherwise
319 = pprPanic "coVarRole: unknown tycon" (ppr cv <+> dcolon <+> ppr (varType cv))
320
321 where
322 tc = case tyConAppTyCon_maybe (varType cv) of
323 Just tc0 -> tc0
324 Nothing -> pprPanic "coVarRole: not tyconapp" (ppr cv)
325
326 -- | Makes a coercion type from two types: the types whose equality
327 -- is proven by the relevant 'Coercion'
328 mkCoercionType :: Role -> Type -> Type -> Type
329 mkCoercionType Nominal = mkPrimEqPred
330 mkCoercionType Representational = mkReprPrimEqPred
331 mkCoercionType Phantom = \ty1 ty2 ->
332 let ki1 = typeKind ty1
333 ki2 = typeKind ty2
334 in
335 TyConApp eqPhantPrimTyCon [ki1, ki2, ty1, ty2]
336
337 mkHeteroCoercionType :: Role -> Kind -> Kind -> Type -> Type -> Type
338 mkHeteroCoercionType Nominal = mkHeteroPrimEqPred
339 mkHeteroCoercionType Representational = mkHeteroReprPrimEqPred
340 mkHeteroCoercionType Phantom = panic "mkHeteroCoercionType"
341
342 -- | Given a coercion @co1 :: (a :: TYPE r1) ~ (b :: TYPE r2)@,
343 -- produce a coercion @rep_co :: r1 ~ r2@.
344 mkRuntimeRepCo :: HasDebugCallStack => Coercion -> Coercion
345 mkRuntimeRepCo co
346 = mkNthCo 0 kind_co
347 where
348 kind_co = mkKindCo co -- kind_co :: TYPE r1 ~ TYPE r2
349 -- (up to silliness with Constraint)
350
351 isReflCoVar_maybe :: CoVar -> Maybe Coercion
352 -- If cv :: t~t then isReflCoVar_maybe cv = Just (Refl t)
353 isReflCoVar_maybe cv
354 | Pair ty1 ty2 <- coVarTypes cv
355 , ty1 `eqType` ty2
356 = Just (Refl (coVarRole cv) ty1)
357 | otherwise
358 = Nothing
359
360 -- | Tests if this coercion is obviously reflexive. Guaranteed to work
361 -- very quickly. Sometimes a coercion can be reflexive, but not obviously
362 -- so. c.f. 'isReflexiveCo'
363 isReflCo :: Coercion -> Bool
364 isReflCo (Refl {}) = True
365 isReflCo _ = False
366
367 -- | Returns the type coerced if this coercion is reflexive. Guaranteed
368 -- to work very quickly. Sometimes a coercion can be reflexive, but not
369 -- obviously so. c.f. 'isReflexiveCo_maybe'
370 isReflCo_maybe :: Coercion -> Maybe (Type, Role)
371 isReflCo_maybe (Refl r ty) = Just (ty, r)
372 isReflCo_maybe _ = Nothing
373
374 -- | Slowly checks if the coercion is reflexive. Don't call this in a loop,
375 -- as it walks over the entire coercion.
376 isReflexiveCo :: Coercion -> Bool
377 isReflexiveCo = isJust . isReflexiveCo_maybe
378
379 -- | Extracts the coerced type from a reflexive coercion. This potentially
380 -- walks over the entire coercion, so avoid doing this in a loop.
381 isReflexiveCo_maybe :: Coercion -> Maybe (Type, Role)
382 isReflexiveCo_maybe (Refl r ty) = Just (ty, r)
383 isReflexiveCo_maybe co
384 | ty1 `eqType` ty2
385 = Just (ty1, r)
386 | otherwise
387 = Nothing
388 where (Pair ty1 ty2, r) = coercionKindRole co
389
390 {-
391 %************************************************************************
392 %* *
393 Building coercions
394 %* *
395 %************************************************************************
396
397 These "smart constructors" maintain the invariants listed in the definition
398 of Coercion, and they perform very basic optimizations.
399
400 Note [Role twiddling functions]
401 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
402
403 There are a plethora of functions for twiddling roles:
404
405 mkSubCo: Requires a nominal input coercion and always produces a
406 representational output. This is used when you (the programmer) are sure you
407 know exactly that role you have and what you want.
408
409 downgradeRole_maybe: This function takes both the input role and the output role
410 as parameters. (The *output* role comes first!) It can only *downgrade* a
411 role -- that is, change it from N to R or P, or from R to P. This one-way
412 behavior is why there is the "_maybe". If an upgrade is requested, this
413 function produces Nothing. This is used when you need to change the role of a
414 coercion, but you're not sure (as you're writing the code) of which roles are
415 involved.
416
417 This function could have been written using coercionRole to ascertain the role
418 of the input. But, that function is recursive, and the caller of downgradeRole_maybe
419 often knows the input role. So, this is more efficient.
420
421 downgradeRole: This is just like downgradeRole_maybe, but it panics if the
422 conversion isn't a downgrade.
423
424 setNominalRole_maybe: This is the only function that can *upgrade* a coercion.
425 The result (if it exists) is always Nominal. The input can be at any role. It
426 works on a "best effort" basis, as it should never be strictly necessary to
427 upgrade a coercion during compilation. It is currently only used within GHC in
428 splitAppCo_maybe. In order to be a proper inverse of mkAppCo, the second
429 coercion that splitAppCo_maybe returns must be nominal. But, it's conceivable
430 that splitAppCo_maybe is operating over a TyConAppCo that uses a
431 representational coercion. Hence the need for setNominalRole_maybe.
432 splitAppCo_maybe, in turn, is used only within coercion optimization -- thus,
433 it is not absolutely critical that setNominalRole_maybe be complete.
434
435 Note that setNominalRole_maybe will never upgrade a phantom UnivCo. Phantom
436 UnivCos are perfectly type-safe, whereas representational and nominal ones are
437 not. Indeed, `unsafeCoerce` is implemented via a representational UnivCo.
438 (Nominal ones are no worse than representational ones, so this function *will*
439 change a UnivCo Representational to a UnivCo Nominal.)
440
441 Conal Elliott also came across a need for this function while working with the
442 GHC API, as he was decomposing Core casts. The Core casts use representational
443 coercions, as they must, but his use case required nominal coercions (he was
444 building a GADT). So, that's why this function is exported from this module.
445
446 One might ask: shouldn't downgradeRole_maybe just use setNominalRole_maybe as
447 appropriate? I (Richard E.) have decided not to do this, because upgrading a
448 role is bizarre and a caller should have to ask for this behavior explicitly.
449
450 Note [mkTransAppCo]
451 ~~~~~~~~~~~~~~~~~~~
452 Suppose we have
453
454 co1 :: a ~R Maybe
455 co2 :: b ~R Int
456
457 and we want
458
459 co3 :: a b ~R Maybe Int
460
461 This seems sensible enough. But, we can't let (co3 = co1 co2), because
462 that's ill-roled! Note that mkAppCo requires a *nominal* second coercion.
463
464 The way around this is to use transitivity:
465
466 co3 = (co1 <b>_N) ; (Maybe co2) :: a b ~R Maybe Int
467
468 Or, it's possible everything is the other way around:
469
470 co1' :: Maybe ~R a
471 co2' :: Int ~R b
472
473 and we want
474
475 co3' :: Maybe Int ~R a b
476
477 then
478
479 co3' = (Maybe co2') ; (co1' <b>_N)
480
481 This is exactly what `mkTransAppCo` builds for us. Information for all
482 the arguments tends to be to hand at call sites, so it's quicker than
483 using, say, coercionKind.
484
485 -}
486
487 mkReflCo :: Role -> Type -> Coercion
488 mkReflCo r ty
489 = Refl r ty
490
491 -- | Make a representational reflexive coercion
492 mkRepReflCo :: Type -> Coercion
493 mkRepReflCo = mkReflCo Representational
494
495 -- | Make a nominal reflexive coercion
496 mkNomReflCo :: Type -> Coercion
497 mkNomReflCo = mkReflCo Nominal
498
499 -- | Apply a type constructor to a list of coercions. It is the
500 -- caller's responsibility to get the roles correct on argument coercions.
501 mkTyConAppCo :: HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
502 mkTyConAppCo r tc cos
503 | tc `hasKey` funTyConKey
504 , [_rep1, _rep2, co1, co2] <- cos -- See Note [Function coercions]
505 = -- (a :: TYPE ra) -> (b :: TYPE rb) ~ (c :: TYPE rc) -> (d :: TYPE rd)
506 -- rep1 :: ra ~ rc rep2 :: rb ~ rd
507 -- co1 :: a ~ c co2 :: b ~ d
508 mkFunCo r co1 co2
509
510 -- Expand type synonyms
511 | Just (tv_co_prs, rhs_ty, leftover_cos) <- expandSynTyCon_maybe tc cos
512 = mkAppCos (liftCoSubst r (mkLiftingContext tv_co_prs) rhs_ty) leftover_cos
513
514 | Just tys_roles <- traverse isReflCo_maybe cos
515 = Refl r (mkTyConApp tc (map fst tys_roles)) -- See Note [Refl invariant]
516
517 | otherwise = TyConAppCo r tc cos
518
519 -- | Build a function 'Coercion' from two other 'Coercion's. That is,
520 -- given @co1 :: a ~ b@ and @co2 :: x ~ y@ produce @co :: (a -> x) ~ (b -> y)@.
521 mkFunCo :: Role -> Coercion -> Coercion -> Coercion
522 mkFunCo r co1 co2
523 -- See Note [Refl invariant]
524 | Just (ty1, _) <- isReflCo_maybe co1
525 , Just (ty2, _) <- isReflCo_maybe co2
526 = Refl r (mkFunTy ty1 ty2)
527 | otherwise = FunCo r co1 co2
528
529 -- | Make nested function 'Coercion's
530 mkFunCos :: Role -> [Coercion] -> Coercion -> Coercion
531 mkFunCos r cos res_co = foldr (mkFunCo r) res_co cos
532
533 -- | Apply a 'Coercion' to another 'Coercion'.
534 -- The second coercion must be Nominal, unless the first is Phantom.
535 -- If the first is Phantom, then the second can be either Phantom or Nominal.
536 mkAppCo :: Coercion -- ^ :: t1 ~r t2
537 -> Coercion -- ^ :: s1 ~N s2, where s1 :: k1, s2 :: k2
538 -> Coercion -- ^ :: t1 s1 ~r t2 s2
539 mkAppCo (Refl r ty1) arg
540 | Just (ty2, _) <- isReflCo_maybe arg
541 = Refl r (mkAppTy ty1 ty2)
542
543 | Just (tc, tys) <- splitTyConApp_maybe ty1
544 -- Expand type synonyms; a TyConAppCo can't have a type synonym (Trac #9102)
545 = mkTyConAppCo r tc (zip_roles (tyConRolesX r tc) tys)
546 where
547 zip_roles (r1:_) [] = [downgradeRole r1 Nominal arg]
548 zip_roles (r1:rs) (ty1:tys) = mkReflCo r1 ty1 : zip_roles rs tys
549 zip_roles _ _ = panic "zip_roles" -- but the roles are infinite...
550
551 mkAppCo (TyConAppCo r tc args) arg
552 = case r of
553 Nominal -> mkTyConAppCo Nominal tc (args ++ [arg])
554 Representational -> mkTyConAppCo Representational tc (args ++ [arg'])
555 where new_role = (tyConRolesRepresentational tc) !! (length args)
556 arg' = downgradeRole new_role Nominal arg
557 Phantom -> mkTyConAppCo Phantom tc (args ++ [toPhantomCo arg])
558 mkAppCo co arg = AppCo co arg
559 -- Note, mkAppCo is careful to maintain invariants regarding
560 -- where Refl constructors appear; see the comments in the definition
561 -- of Coercion and the Note [Refl invariant] in TyCoRep.
562
563 -- | Applies multiple 'Coercion's to another 'Coercion', from left to right.
564 -- See also 'mkAppCo'.
565 mkAppCos :: Coercion
566 -> [Coercion]
567 -> Coercion
568 mkAppCos co1 cos = foldl mkAppCo co1 cos
569
570 -- | Like `mkAppCo`, but allows the second coercion to be other than
571 -- nominal. See Note [mkTransAppCo]. Role r3 cannot be more stringent
572 -- than either r1 or r2.
573 mkTransAppCo :: Role -- ^ r1
574 -> Coercion -- ^ co1 :: ty1a ~r1 ty1b
575 -> Type -- ^ ty1a
576 -> Type -- ^ ty1b
577 -> Role -- ^ r2
578 -> Coercion -- ^ co2 :: ty2a ~r2 ty2b
579 -> Type -- ^ ty2a
580 -> Type -- ^ ty2b
581 -> Role -- ^ r3
582 -> Coercion -- ^ :: ty1a ty2a ~r3 ty1b ty2b
583 mkTransAppCo r1 co1 ty1a ty1b r2 co2 ty2a ty2b r3
584 -- How incredibly fiddly! Is there a better way??
585 = case (r1, r2, r3) of
586 (_, _, Phantom)
587 -> mkPhantomCo kind_co (mkAppTy ty1a ty2a) (mkAppTy ty1b ty2b)
588 where -- ty1a :: k1a -> k2a
589 -- ty1b :: k1b -> k2b
590 -- ty2a :: k1a
591 -- ty2b :: k1b
592 -- ty1a ty2a :: k2a
593 -- ty1b ty2b :: k2b
594 kind_co1 = mkKindCo co1 -- :: k1a -> k2a ~N k1b -> k2b
595 kind_co = mkNthCo 1 kind_co1 -- :: k2a ~N k2b
596
597 (_, _, Nominal)
598 -> ASSERT( r1 == Nominal && r2 == Nominal )
599 mkAppCo co1 co2
600 (Nominal, Nominal, Representational)
601 -> mkSubCo (mkAppCo co1 co2)
602 (_, Nominal, Representational)
603 -> ASSERT( r1 == Representational )
604 mkAppCo co1 co2
605 (Nominal, Representational, Representational)
606 -> go (mkSubCo co1)
607 (_ , _, Representational)
608 -> ASSERT( r1 == Representational && r2 == Representational )
609 go co1
610 where
611 go co1_repr
612 | Just (tc1b, tys1b) <- splitTyConApp_maybe ty1b
613 , nextRole ty1b == r2
614 = (mkAppCo co1_repr (mkNomReflCo ty2a)) `mkTransCo`
615 (mkTyConAppCo Representational tc1b
616 (zipWith mkReflCo (tyConRolesRepresentational tc1b) tys1b
617 ++ [co2]))
618
619 | Just (tc1a, tys1a) <- splitTyConApp_maybe ty1a
620 , nextRole ty1a == r2
621 = (mkTyConAppCo Representational tc1a
622 (zipWith mkReflCo (tyConRolesRepresentational tc1a) tys1a
623 ++ [co2]))
624 `mkTransCo`
625 (mkAppCo co1_repr (mkNomReflCo ty2b))
626
627 | otherwise
628 = pprPanic "mkTransAppCo" (vcat [ ppr r1, ppr co1, ppr ty1a, ppr ty1b
629 , ppr r2, ppr co2, ppr ty2a, ppr ty2b
630 , ppr r3 ])
631
632 -- | Make a Coercion from a tyvar, a kind coercion, and a body coercion.
633 -- The kind of the tyvar should be the left-hand kind of the kind coercion.
634 mkForAllCo :: TyVar -> Coercion -> Coercion -> Coercion
635 mkForAllCo tv kind_co co
636 | Refl r ty <- co
637 , Refl {} <- kind_co
638 = Refl r (mkInvForAllTy tv ty)
639 | otherwise
640 = ForAllCo tv kind_co co
641
642 -- | Make nested ForAllCos
643 mkForAllCos :: [(TyVar, Coercion)] -> Coercion -> Coercion
644 mkForAllCos bndrs (Refl r ty)
645 = let (refls_rev'd, non_refls_rev'd) = span (isReflCo . snd) (reverse bndrs) in
646 foldl (flip $ uncurry ForAllCo)
647 (Refl r $ mkInvForAllTys (reverse (map fst refls_rev'd)) ty)
648 non_refls_rev'd
649 mkForAllCos bndrs co = foldr (uncurry ForAllCo) co bndrs
650
651 -- | Make a Coercion quantified over a type variable;
652 -- the variable has the same type in both sides of the coercion
653 mkHomoForAllCos :: [TyVar] -> Coercion -> Coercion
654 mkHomoForAllCos tvs (Refl r ty)
655 = Refl r (mkInvForAllTys tvs ty)
656 mkHomoForAllCos tvs ty = mkHomoForAllCos_NoRefl tvs ty
657
658 -- | Like 'mkHomoForAllCos', but doesn't check if the inner coercion
659 -- is reflexive.
660 mkHomoForAllCos_NoRefl :: [TyVar] -> Coercion -> Coercion
661 mkHomoForAllCos_NoRefl tvs orig_co = foldr go orig_co tvs
662 where
663 go tv co = ForAllCo tv (mkNomReflCo (tyVarKind tv)) co
664
665 mkCoVarCo :: CoVar -> Coercion
666 -- cv :: s ~# t
667 -- See Note [mkCoVarCo]
668 mkCoVarCo cv = CoVarCo cv
669
670 mkCoVarCos :: [CoVar] -> [Coercion]
671 mkCoVarCos = map mkCoVarCo
672
673 {- Note [mkCoVarCo]
674 ~~~~~~~~~~~~~~~~~~~
675 In the past, mkCoVarCo optimised (c :: t~t) to (Refl t). That is
676 valid (although see Note [Unbound RULE binders] in Rules), but
677 it's a relatively expensive test and perhaps better done in
678 optCoercion. Not a big deal either way.
679 -}
680
681 -- | Extract a covar, if possible. This check is dirty. Be ashamed
682 -- of yourself. (It's dirty because it cares about the structure of
683 -- a coercion, which is morally reprehensible.)
684 isCoVar_maybe :: Coercion -> Maybe CoVar
685 isCoVar_maybe (CoVarCo cv) = Just cv
686 isCoVar_maybe _ = Nothing
687
688 mkAxInstCo :: Role -> CoAxiom br -> BranchIndex -> [Type] -> [Coercion]
689 -> Coercion
690 -- mkAxInstCo can legitimately be called over-staturated;
691 -- i.e. with more type arguments than the coercion requires
692 mkAxInstCo role ax index tys cos
693 | arity == n_tys = downgradeRole role ax_role $
694 mkAxiomInstCo ax_br index (rtys `chkAppend` cos)
695 | otherwise = ASSERT( arity < n_tys )
696 downgradeRole role ax_role $
697 mkAppCos (mkAxiomInstCo ax_br index
698 (ax_args `chkAppend` cos))
699 leftover_args
700 where
701 n_tys = length tys
702 ax_br = toBranchedAxiom ax
703 branch = coAxiomNthBranch ax_br index
704 tvs = coAxBranchTyVars branch
705 arity = length tvs
706 arg_roles = coAxBranchRoles branch
707 rtys = zipWith mkReflCo (arg_roles ++ repeat Nominal) tys
708 (ax_args, leftover_args)
709 = splitAt arity rtys
710 ax_role = coAxiomRole ax
711
712 -- worker function; just checks to see if it should produce Refl
713 mkAxiomInstCo :: CoAxiom Branched -> BranchIndex -> [Coercion] -> Coercion
714 mkAxiomInstCo ax index args
715 = ASSERT( args `lengthIs` coAxiomArity ax index )
716 AxiomInstCo ax index args
717
718 -- to be used only with unbranched axioms
719 mkUnbranchedAxInstCo :: Role -> CoAxiom Unbranched
720 -> [Type] -> [Coercion] -> Coercion
721 mkUnbranchedAxInstCo role ax tys cos
722 = mkAxInstCo role ax 0 tys cos
723
724 mkAxInstRHS :: CoAxiom br -> BranchIndex -> [Type] -> [Coercion] -> Type
725 -- Instantiate the axiom with specified types,
726 -- returning the instantiated RHS
727 -- A companion to mkAxInstCo:
728 -- mkAxInstRhs ax index tys = snd (coercionKind (mkAxInstCo ax index tys))
729 mkAxInstRHS ax index tys cos
730 = ASSERT( tvs `equalLength` tys1 )
731 mkAppTys rhs' tys2
732 where
733 branch = coAxiomNthBranch ax index
734 tvs = coAxBranchTyVars branch
735 cvs = coAxBranchCoVars branch
736 (tys1, tys2) = splitAtList tvs tys
737 rhs' = substTyWith tvs tys1 $
738 substTyWithCoVars cvs cos $
739 coAxBranchRHS branch
740
741 mkUnbranchedAxInstRHS :: CoAxiom Unbranched -> [Type] -> [Coercion] -> Type
742 mkUnbranchedAxInstRHS ax = mkAxInstRHS ax 0
743
744 -- | Return the left-hand type of the axiom, when the axiom is instantiated
745 -- at the types given.
746 mkAxInstLHS :: CoAxiom br -> BranchIndex -> [Type] -> [Coercion] -> Type
747 mkAxInstLHS ax index tys cos
748 = ASSERT( tvs `equalLength` tys1 )
749 mkTyConApp fam_tc (lhs_tys `chkAppend` tys2)
750 where
751 branch = coAxiomNthBranch ax index
752 tvs = coAxBranchTyVars branch
753 cvs = coAxBranchCoVars branch
754 (tys1, tys2) = splitAtList tvs tys
755 lhs_tys = substTysWith tvs tys1 $
756 substTysWithCoVars cvs cos $
757 coAxBranchLHS branch
758 fam_tc = coAxiomTyCon ax
759
760 -- | Instantiate the left-hand side of an unbranched axiom
761 mkUnbranchedAxInstLHS :: CoAxiom Unbranched -> [Type] -> [Coercion] -> Type
762 mkUnbranchedAxInstLHS ax = mkAxInstLHS ax 0
763
764 -- | Manufacture an unsafe coercion from thin air.
765 -- Currently (May 14) this is used only to implement the
766 -- @unsafeCoerce#@ primitive. Optimise by pushing
767 -- down through type constructors.
768 mkUnsafeCo :: Role -> Type -> Type -> Coercion
769 mkUnsafeCo role ty1 ty2
770 = mkUnivCo UnsafeCoerceProv role ty1 ty2
771
772 -- | Make a coercion from a coercion hole
773 mkHoleCo :: CoercionHole -> Role
774 -> Type -> Type -> Coercion
775 mkHoleCo h r t1 t2 = mkUnivCo (HoleProv h) r t1 t2
776
777 -- | Make a universal coercion between two arbitrary types.
778 mkUnivCo :: UnivCoProvenance
779 -> Role -- ^ role of the built coercion, "r"
780 -> Type -- ^ t1 :: k1
781 -> Type -- ^ t2 :: k2
782 -> Coercion -- ^ :: t1 ~r t2
783 mkUnivCo prov role ty1 ty2
784 | ty1 `eqType` ty2 = Refl role ty1
785 | otherwise = UnivCo prov role ty1 ty2
786
787 -- | Create a symmetric version of the given 'Coercion' that asserts
788 -- equality between the same types but in the other "direction", so
789 -- a kind of @t1 ~ t2@ becomes the kind @t2 ~ t1@.
790 mkSymCo :: Coercion -> Coercion
791
792 -- Do a few simple optimizations, but don't bother pushing occurrences
793 -- of symmetry to the leaves; the optimizer will take care of that.
794 mkSymCo co@(Refl {}) = co
795 mkSymCo (SymCo co) = co
796 mkSymCo (SubCo (SymCo co)) = SubCo co
797 mkSymCo co = SymCo co
798
799 -- | Create a new 'Coercion' by composing the two given 'Coercion's transitively.
800 -- (co1 ; co2)
801 mkTransCo :: Coercion -> Coercion -> Coercion
802 mkTransCo co1 (Refl {}) = co1
803 mkTransCo (Refl {}) co2 = co2
804 mkTransCo co1 co2 = TransCo co1 co2
805
806 -- the Role is the desired one. It is the caller's responsibility to make
807 -- sure this request is reasonable
808 mkNthCoRole :: Role -> Int -> Coercion -> Coercion
809 mkNthCoRole role n co
810 = downgradeRole role nth_role $ nth_co
811 where
812 nth_co = mkNthCo n co
813 nth_role = coercionRole nth_co
814
815 mkNthCo :: Int -> Coercion -> Coercion
816 mkNthCo 0 (Refl _ ty)
817 | Just (tv, _) <- splitForAllTy_maybe ty
818 = Refl Nominal (tyVarKind tv)
819 mkNthCo n (Refl r ty)
820 = ASSERT2( ok_tc_app ty n, ppr n $$ ppr ty )
821 mkReflCo r' (tyConAppArgN n ty)
822 where tc = tyConAppTyCon ty
823 r' = nthRole r tc n
824
825 ok_tc_app :: Type -> Int -> Bool
826 ok_tc_app ty n
827 | Just (_, tys) <- splitTyConApp_maybe ty
828 = tys `lengthExceeds` n
829 | isForAllTy ty -- nth:0 pulls out a kind coercion from a hetero forall
830 = n == 0
831 | otherwise
832 = False
833
834 mkNthCo 0 (ForAllCo _ kind_co _) = kind_co
835 -- If co :: (forall a1:k1. t1) ~ (forall a2:k2. t2)
836 -- then (nth 0 co :: k1 ~ k2)
837
838 mkNthCo n co@(FunCo _ arg res)
839 -- See Note [Function coercions]
840 -- If FunCo _ arg_co res_co :: (s1:TYPE sk1 -> s2:TYPE sk2)
841 -- ~ (t1:TYPE tk1 -> t2:TYPE tk2)
842 -- Then we want to behave as if co was
843 -- TyConAppCo argk_co resk_co arg_co res_co
844 -- where
845 -- argk_co :: sk1 ~ tk1 = mkNthCo 0 (mkKindCo arg_co)
846 -- resk_co :: sk2 ~ tk2 = mkNthCo 0 (mkKindCo res_co)
847 -- i.e. mkRuntimeRepCo
848 = case n of
849 0 -> mkRuntimeRepCo arg
850 1 -> mkRuntimeRepCo res
851 2 -> arg
852 3 -> res
853 _ -> pprPanic "mkNthCo(FunCo)" (ppr n $$ ppr co)
854
855 mkNthCo n (TyConAppCo _ _ arg_cos) = arg_cos `getNth` n
856
857 mkNthCo n co = NthCo n co
858
859 mkLRCo :: LeftOrRight -> Coercion -> Coercion
860 mkLRCo lr (Refl eq ty) = Refl eq (pickLR lr (splitAppTy ty))
861 mkLRCo lr co = LRCo lr co
862
863 -- | Instantiates a 'Coercion'.
864 mkInstCo :: Coercion -> Coercion -> Coercion
865 mkInstCo (ForAllCo tv _kind_co body_co) (Refl _ arg)
866 = substCoWithUnchecked [tv] [arg] body_co
867 mkInstCo co arg = InstCo co arg
868
869 -- This could work harder to produce Refl coercions, but that would be
870 -- quite inefficient. Seems better not to try.
871 mkCoherenceCo :: Coercion -> Coercion -> Coercion
872 mkCoherenceCo co1 (Refl {}) = co1
873 mkCoherenceCo (CoherenceCo co1 co2) co3
874 = CoherenceCo co1 (co2 `mkTransCo` co3)
875 mkCoherenceCo co1 co2 = CoherenceCo co1 co2
876
877 -- | A CoherenceCo c1 c2 applies the coercion c2 to the left-hand type
878 -- in the kind of c1. This function uses sym to get the coercion on the
879 -- right-hand type of c1. Thus, if c1 :: s ~ t, then mkCoherenceRightCo c1 c2
880 -- has the kind (s ~ (t |> c2)) down through type constructors.
881 -- The second coercion must be representational.
882 mkCoherenceRightCo :: Coercion -> Coercion -> Coercion
883 mkCoherenceRightCo c1 c2 = mkSymCo (mkCoherenceCo (mkSymCo c1) c2)
884
885 -- | An explicitly directed synonym of mkCoherenceCo. The second
886 -- coercion must be representational.
887 mkCoherenceLeftCo :: Coercion -> Coercion -> Coercion
888 mkCoherenceLeftCo = mkCoherenceCo
889
890 infixl 5 `mkCoherenceCo`
891 infixl 5 `mkCoherenceRightCo`
892 infixl 5 `mkCoherenceLeftCo`
893
894 -- | Given @co :: (a :: k) ~ (b :: k')@ produce @co' :: k ~ k'@.
895 mkKindCo :: Coercion -> Coercion
896 mkKindCo (Refl _ ty) = Refl Nominal (typeKind ty)
897 mkKindCo (UnivCo (PhantomProv h) _ _ _) = h
898 mkKindCo (UnivCo (ProofIrrelProv h) _ _ _) = h
899 mkKindCo co
900 | Pair ty1 ty2 <- coercionKind co
901 -- generally, calling coercionKind during coercion creation is a bad idea,
902 -- as it can lead to exponential behavior. But, we don't have nested mkKindCos,
903 -- so it's OK here.
904 , let tk1 = typeKind ty1
905 tk2 = typeKind ty2
906 , tk1 `eqType` tk2
907 = Refl Nominal tk1
908 | otherwise
909 = KindCo co
910
911 -- input coercion is Nominal; see also Note [Role twiddling functions]
912 mkSubCo :: Coercion -> Coercion
913 mkSubCo (Refl Nominal ty) = Refl Representational ty
914 mkSubCo (TyConAppCo Nominal tc cos)
915 = TyConAppCo Representational tc (applyRoles tc cos)
916 mkSubCo (FunCo Nominal arg res)
917 = FunCo Representational
918 (downgradeRole Representational Nominal arg)
919 (downgradeRole Representational Nominal res)
920 mkSubCo co = ASSERT2( coercionRole co == Nominal, ppr co <+> ppr (coercionRole co) )
921 SubCo co
922
923 -- | Changes a role, but only a downgrade. See Note [Role twiddling functions]
924 downgradeRole_maybe :: Role -- ^ desired role
925 -> Role -- ^ current role
926 -> Coercion -> Maybe Coercion
927 -- In (downgradeRole_maybe dr cr co) it's a precondition that
928 -- cr = coercionRole co
929 downgradeRole_maybe Representational Nominal co = Just (mkSubCo co)
930 downgradeRole_maybe Nominal Representational _ = Nothing
931 downgradeRole_maybe Phantom Phantom co = Just co
932 downgradeRole_maybe Phantom _ co = Just (toPhantomCo co)
933 downgradeRole_maybe _ Phantom _ = Nothing
934 downgradeRole_maybe _ _ co = Just co
935
936 -- | Like 'downgradeRole_maybe', but panics if the change isn't a downgrade.
937 -- See Note [Role twiddling functions]
938 downgradeRole :: Role -- desired role
939 -> Role -- current role
940 -> Coercion -> Coercion
941 downgradeRole r1 r2 co
942 = case downgradeRole_maybe r1 r2 co of
943 Just co' -> co'
944 Nothing -> pprPanic "downgradeRole" (ppr co)
945
946 -- | If the EqRel is ReprEq, makes a SubCo; otherwise, does nothing.
947 -- Note that the input coercion should always be nominal.
948 maybeSubCo :: EqRel -> Coercion -> Coercion
949 maybeSubCo NomEq = id
950 maybeSubCo ReprEq = mkSubCo
951
952
953 mkAxiomRuleCo :: CoAxiomRule -> [Coercion] -> Coercion
954 mkAxiomRuleCo = AxiomRuleCo
955
956 -- | Make a "coercion between coercions".
957 mkProofIrrelCo :: Role -- ^ role of the created coercion, "r"
958 -> Coercion -- ^ :: phi1 ~N phi2
959 -> Coercion -- ^ g1 :: phi1
960 -> Coercion -- ^ g2 :: phi2
961 -> Coercion -- ^ :: g1 ~r g2
962
963 -- if the two coercion prove the same fact, I just don't care what
964 -- the individual coercions are.
965 mkProofIrrelCo r (Refl {}) g _ = Refl r (CoercionTy g)
966 mkProofIrrelCo r kco g1 g2 = mkUnivCo (ProofIrrelProv kco) r
967 (mkCoercionTy g1) (mkCoercionTy g2)
968
969 {-
970 %************************************************************************
971 %* *
972 Roles
973 %* *
974 %************************************************************************
975 -}
976
977 -- | Converts a coercion to be nominal, if possible.
978 -- See Note [Role twiddling functions]
979 setNominalRole_maybe :: Coercion -> Maybe Coercion
980 setNominalRole_maybe co
981 | Nominal <- coercionRole co = Just co
982 setNominalRole_maybe (SubCo co) = Just co
983 setNominalRole_maybe (Refl _ ty) = Just $ Refl Nominal ty
984 setNominalRole_maybe (TyConAppCo Representational tc cos)
985 = do { cos' <- mapM setNominalRole_maybe cos
986 ; return $ TyConAppCo Nominal tc cos' }
987 setNominalRole_maybe (FunCo Representational co1 co2)
988 = do { co1' <- setNominalRole_maybe co1
989 ; co2' <- setNominalRole_maybe co2
990 ; return $ FunCo Nominal co1' co2'
991 }
992 setNominalRole_maybe (SymCo co)
993 = SymCo <$> setNominalRole_maybe co
994 setNominalRole_maybe (TransCo co1 co2)
995 = TransCo <$> setNominalRole_maybe co1 <*> setNominalRole_maybe co2
996 setNominalRole_maybe (AppCo co1 co2)
997 = AppCo <$> setNominalRole_maybe co1 <*> pure co2
998 setNominalRole_maybe (ForAllCo tv kind_co co)
999 = ForAllCo tv kind_co <$> setNominalRole_maybe co
1000 setNominalRole_maybe (NthCo n co)
1001 = NthCo n <$> setNominalRole_maybe co
1002 setNominalRole_maybe (InstCo co arg)
1003 = InstCo <$> setNominalRole_maybe co <*> pure arg
1004 setNominalRole_maybe (CoherenceCo co1 co2)
1005 = CoherenceCo <$> setNominalRole_maybe co1 <*> pure co2
1006 setNominalRole_maybe (UnivCo prov _ co1 co2)
1007 | case prov of UnsafeCoerceProv -> True -- it's always unsafe
1008 PhantomProv _ -> False -- should always be phantom
1009 ProofIrrelProv _ -> True -- it's always safe
1010 PluginProv _ -> False -- who knows? This choice is conservative.
1011 HoleProv _ -> False -- no no no.
1012 = Just $ UnivCo prov Nominal co1 co2
1013 setNominalRole_maybe _ = Nothing
1014
1015 -- | Make a phantom coercion between two types. The coercion passed
1016 -- in must be a nominal coercion between the kinds of the
1017 -- types.
1018 mkPhantomCo :: Coercion -> Type -> Type -> Coercion
1019 mkPhantomCo h t1 t2
1020 = mkUnivCo (PhantomProv h) Phantom t1 t2
1021
1022 -- | Make a phantom coercion between two types of the same kind.
1023 mkHomoPhantomCo :: Type -> Type -> Coercion
1024 mkHomoPhantomCo t1 t2
1025 = ASSERT( k1 `eqType` typeKind t2 )
1026 mkPhantomCo (mkNomReflCo k1) t1 t2
1027 where
1028 k1 = typeKind t1
1029
1030 -- takes any coercion and turns it into a Phantom coercion
1031 toPhantomCo :: Coercion -> Coercion
1032 toPhantomCo co
1033 = mkPhantomCo (mkKindCo co) ty1 ty2
1034 where Pair ty1 ty2 = coercionKind co
1035
1036 -- Convert args to a TyConAppCo Nominal to the same TyConAppCo Representational
1037 applyRoles :: TyCon -> [Coercion] -> [Coercion]
1038 applyRoles tc cos
1039 = zipWith (\r -> downgradeRole r Nominal) (tyConRolesRepresentational tc) cos
1040
1041 -- the Role parameter is the Role of the TyConAppCo
1042 -- defined here because this is intimiately concerned with the implementation
1043 -- of TyConAppCo
1044 tyConRolesX :: Role -> TyCon -> [Role]
1045 tyConRolesX Representational tc = tyConRolesRepresentational tc
1046 tyConRolesX role _ = repeat role
1047
1048 tyConRolesRepresentational :: TyCon -> [Role]
1049 tyConRolesRepresentational tc = tyConRoles tc ++ repeat Nominal
1050
1051 nthRole :: Role -> TyCon -> Int -> Role
1052 nthRole Nominal _ _ = Nominal
1053 nthRole Phantom _ _ = Phantom
1054 nthRole Representational tc n
1055 = (tyConRolesRepresentational tc) `getNth` n
1056
1057 ltRole :: Role -> Role -> Bool
1058 -- Is one role "less" than another?
1059 -- Nominal < Representational < Phantom
1060 ltRole Phantom _ = False
1061 ltRole Representational Phantom = True
1062 ltRole Representational _ = False
1063 ltRole Nominal Nominal = False
1064 ltRole Nominal _ = True
1065
1066 -------------------------------
1067
1068 -- | like mkKindCo, but aggressively & recursively optimizes to avoid using
1069 -- a KindCo constructor. The output role is nominal.
1070 promoteCoercion :: Coercion -> Coercion
1071
1072 -- First cases handles anything that should yield refl.
1073 promoteCoercion co = case co of
1074
1075 _ | ki1 `eqType` ki2
1076 -> mkNomReflCo (typeKind ty1)
1077 -- no later branch should return refl
1078 -- The ASSERT( False )s throughout
1079 -- are these cases explicitly, but they should never fire.
1080
1081 Refl _ ty -> ASSERT( False )
1082 mkNomReflCo (typeKind ty)
1083
1084 TyConAppCo _ tc args
1085 | Just co' <- instCoercions (mkNomReflCo (tyConKind tc)) args
1086 -> co'
1087 | otherwise
1088 -> mkKindCo co
1089
1090 AppCo co1 arg
1091 | Just co' <- instCoercion (coercionKind (mkKindCo co1))
1092 (promoteCoercion co1) arg
1093 -> co'
1094 | otherwise
1095 -> mkKindCo co
1096
1097 ForAllCo _ _ g
1098 -> promoteCoercion g
1099
1100 FunCo _ _ _
1101 -> mkNomReflCo liftedTypeKind
1102
1103 CoVarCo {}
1104 -> mkKindCo co
1105
1106 AxiomInstCo {}
1107 -> mkKindCo co
1108
1109 UnivCo UnsafeCoerceProv _ t1 t2
1110 -> mkUnsafeCo Nominal (typeKind t1) (typeKind t2)
1111 UnivCo (PhantomProv kco) _ _ _
1112 -> kco
1113 UnivCo (ProofIrrelProv kco) _ _ _
1114 -> kco
1115 UnivCo (PluginProv _) _ _ _
1116 -> mkKindCo co
1117 UnivCo (HoleProv _) _ _ _
1118 -> mkKindCo co
1119
1120 SymCo g
1121 -> mkSymCo (promoteCoercion g)
1122
1123 TransCo co1 co2
1124 -> mkTransCo (promoteCoercion co1) (promoteCoercion co2)
1125
1126 NthCo n co1
1127 | Just (_, args) <- splitTyConAppCo_maybe co1
1128 , args `lengthExceeds` n
1129 -> promoteCoercion (args !! n)
1130
1131 | Just _ <- splitForAllCo_maybe co
1132 , n == 0
1133 -> ASSERT( False ) mkNomReflCo liftedTypeKind
1134
1135 | otherwise
1136 -> mkKindCo co
1137
1138 LRCo lr co1
1139 | Just (lco, rco) <- splitAppCo_maybe co1
1140 -> case lr of
1141 CLeft -> promoteCoercion lco
1142 CRight -> promoteCoercion rco
1143
1144 | otherwise
1145 -> mkKindCo co
1146
1147 InstCo g _
1148 -> promoteCoercion g
1149
1150 CoherenceCo g h
1151 -> mkSymCo h `mkTransCo` promoteCoercion g
1152
1153 KindCo _
1154 -> ASSERT( False )
1155 mkNomReflCo liftedTypeKind
1156
1157 SubCo g
1158 -> promoteCoercion g
1159
1160 AxiomRuleCo {}
1161 -> mkKindCo co
1162
1163 where
1164 Pair ty1 ty2 = coercionKind co
1165 ki1 = typeKind ty1
1166 ki2 = typeKind ty2
1167
1168 -- | say @g = promoteCoercion h@. Then, @instCoercion g w@ yields @Just g'@,
1169 -- where @g' = promoteCoercion (h w)@.
1170 -- fails if this is not possible, if @g@ coerces between a forall and an ->
1171 -- or if second parameter has a representational role and can't be used
1172 -- with an InstCo. The result role matches is representational.
1173 instCoercion :: Pair Type -- type of the first coercion
1174 -> Coercion -- ^ must be nominal
1175 -> Coercion
1176 -> Maybe Coercion
1177 instCoercion (Pair lty rty) g w
1178 | isForAllTy lty && isForAllTy rty
1179 , Just w' <- setNominalRole_maybe w
1180 = Just $ mkInstCo g w'
1181 | isFunTy lty && isFunTy rty
1182 = Just $ mkNthCo 3 g -- extract result type, which is the 4th argument to (->)
1183 | otherwise -- one forall, one funty...
1184 = Nothing
1185 where
1186
1187 instCoercions :: Coercion -> [Coercion] -> Maybe Coercion
1188 instCoercions g ws
1189 = let arg_ty_pairs = map coercionKind ws in
1190 snd <$> foldM go (coercionKind g, g) (zip arg_ty_pairs ws)
1191 where
1192 go :: (Pair Type, Coercion) -> (Pair Type, Coercion)
1193 -> Maybe (Pair Type, Coercion)
1194 go (g_tys, g) (w_tys, w)
1195 = do { g' <- instCoercion g_tys g w
1196 ; return (piResultTy <$> g_tys <*> w_tys, g') }
1197
1198 -- | Creates a new coercion with both of its types casted by different casts
1199 -- castCoercionKind g h1 h2, where g :: t1 ~ t2, has type (t1 |> h1) ~ (t2 |> h2)
1200 -- The second and third coercions must be nominal.
1201 castCoercionKind :: Coercion -> Coercion -> Coercion -> Coercion
1202 castCoercionKind g h1 h2
1203 = g `mkCoherenceLeftCo` h1 `mkCoherenceRightCo` h2
1204
1205 -- See note [Newtype coercions] in TyCon
1206
1207 mkPiCos :: Role -> [Var] -> Coercion -> Coercion
1208 mkPiCos r vs co = foldr (mkPiCo r) co vs
1209
1210 -- | Make a forall 'Coercion', where both types related by the coercion
1211 -- are quantified over the same type variable.
1212 mkPiCo :: Role -> Var -> Coercion -> Coercion
1213 mkPiCo r v co | isTyVar v = mkHomoForAllCos [v] co
1214 | otherwise = mkFunCo r (mkReflCo r (varType v)) co
1215
1216 -- The second coercion is sometimes lifted (~) and sometimes unlifted (~#).
1217 -- So, we have to make sure to supply the right parameter to decomposeCo.
1218 -- mkCoCast (c :: s1 ~# t1) (g :: (s1 ~# s2) ~# (t1 ~# t2)) :: s2 ~# t2
1219 -- Both coercions *must* have the same role.
1220 mkCoCast :: Coercion -> Coercion -> Coercion
1221 mkCoCast c g
1222 = mkSymCo g1 `mkTransCo` c `mkTransCo` g2
1223 where
1224 -- g :: (s1 ~# s2) ~# (t1 ~# t2)
1225 -- g1 :: s1 ~# t1
1226 -- g2 :: s2 ~# t2
1227 (_, args) = splitTyConApp (pFst $ coercionKind g)
1228 n_args = length args
1229 co_list = decomposeCo n_args g
1230 g1 = co_list `getNth` (n_args - 2)
1231 g2 = co_list `getNth` (n_args - 1)
1232
1233 {-
1234 %************************************************************************
1235 %* *
1236 Newtypes
1237 %* *
1238 %************************************************************************
1239 -}
1240
1241 -- | If @co :: T ts ~ rep_ty@ then:
1242 --
1243 -- > instNewTyCon_maybe T ts = Just (rep_ty, co)
1244 --
1245 -- Checks for a newtype, and for being saturated
1246 instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, Coercion)
1247 instNewTyCon_maybe tc tys
1248 | Just (tvs, ty, co_tc) <- unwrapNewTyConEtad_maybe tc -- Check for newtype
1249 , tvs `leLength` tys -- Check saturated enough
1250 = Just (applyTysX tvs ty tys, mkUnbranchedAxInstCo Representational co_tc tys [])
1251 | otherwise
1252 = Nothing
1253
1254 {-
1255 ************************************************************************
1256 * *
1257 Type normalisation
1258 * *
1259 ************************************************************************
1260 -}
1261
1262 -- | A function to check if we can reduce a type by one step. Used
1263 -- with 'topNormaliseTypeX'.
1264 type NormaliseStepper ev = RecTcChecker
1265 -> TyCon -- tc
1266 -> [Type] -- tys
1267 -> NormaliseStepResult ev
1268
1269 -- | The result of stepping in a normalisation function.
1270 -- See 'topNormaliseTypeX'.
1271 data NormaliseStepResult ev
1272 = NS_Done -- ^ Nothing more to do
1273 | NS_Abort -- ^ Utter failure. The outer function should fail too.
1274 | NS_Step RecTcChecker Type ev -- ^ We stepped, yielding new bits;
1275 -- ^ ev is evidence;
1276 -- Usually a co :: old type ~ new type
1277
1278 mapStepResult :: (ev1 -> ev2)
1279 -> NormaliseStepResult ev1 -> NormaliseStepResult ev2
1280 mapStepResult f (NS_Step rec_nts ty ev) = NS_Step rec_nts ty (f ev)
1281 mapStepResult _ NS_Done = NS_Done
1282 mapStepResult _ NS_Abort = NS_Abort
1283
1284 -- | Try one stepper and then try the next, if the first doesn't make
1285 -- progress.
1286 -- So if it returns NS_Done, it means that both steppers are satisfied
1287 composeSteppers :: NormaliseStepper ev -> NormaliseStepper ev
1288 -> NormaliseStepper ev
1289 composeSteppers step1 step2 rec_nts tc tys
1290 = case step1 rec_nts tc tys of
1291 success@(NS_Step {}) -> success
1292 NS_Done -> step2 rec_nts tc tys
1293 NS_Abort -> NS_Abort
1294
1295 -- | A 'NormaliseStepper' that unwraps newtypes, careful not to fall into
1296 -- a loop. If it would fall into a loop, it produces 'NS_Abort'.
1297 unwrapNewTypeStepper :: NormaliseStepper Coercion
1298 unwrapNewTypeStepper rec_nts tc tys
1299 | Just (ty', co) <- instNewTyCon_maybe tc tys
1300 = case checkRecTc rec_nts tc of
1301 Just rec_nts' -> NS_Step rec_nts' ty' co
1302 Nothing -> NS_Abort
1303
1304 | otherwise
1305 = NS_Done
1306
1307 -- | A general function for normalising the top-level of a type. It continues
1308 -- to use the provided 'NormaliseStepper' until that function fails, and then
1309 -- this function returns. The roles of the coercions produced by the
1310 -- 'NormaliseStepper' must all be the same, which is the role returned from
1311 -- the call to 'topNormaliseTypeX'.
1312 --
1313 -- Typically ev is Coercion.
1314 --
1315 -- If topNormaliseTypeX step plus ty = Just (ev, ty')
1316 -- then ty ~ev1~ t1 ~ev2~ t2 ... ~evn~ ty'
1317 -- and ev = ev1 `plus` ev2 `plus` ... `plus` evn
1318 -- If it returns Nothing then no newtype unwrapping could happen
1319 topNormaliseTypeX :: NormaliseStepper ev -> (ev -> ev -> ev)
1320 -> Type -> Maybe (ev, Type)
1321 topNormaliseTypeX stepper plus ty
1322 | Just (tc, tys) <- splitTyConApp_maybe ty
1323 , NS_Step rec_nts ty' ev <- stepper initRecTc tc tys
1324 = go rec_nts ev ty'
1325 | otherwise
1326 = Nothing
1327 where
1328 go rec_nts ev ty
1329 | Just (tc, tys) <- splitTyConApp_maybe ty
1330 = case stepper rec_nts tc tys of
1331 NS_Step rec_nts' ty' ev' -> go rec_nts' (ev `plus` ev') ty'
1332 NS_Done -> Just (ev, ty)
1333 NS_Abort -> Nothing
1334
1335 | otherwise
1336 = Just (ev, ty)
1337
1338 topNormaliseNewType_maybe :: Type -> Maybe (Coercion, Type)
1339 -- ^ Sometimes we want to look through a @newtype@ and get its associated coercion.
1340 -- This function strips off @newtype@ layers enough to reveal something that isn't
1341 -- a @newtype@. Specifically, here's the invariant:
1342 --
1343 -- > topNormaliseNewType_maybe rec_nts ty = Just (co, ty')
1344 --
1345 -- then (a) @co : ty0 ~ ty'@.
1346 -- (b) ty' is not a newtype.
1347 --
1348 -- The function returns @Nothing@ for non-@newtypes@,
1349 -- or unsaturated applications
1350 --
1351 -- This function does *not* look through type families, because it has no access to
1352 -- the type family environment. If you do have that at hand, consider to use
1353 -- topNormaliseType_maybe, which should be a drop-in replacement for
1354 -- topNormaliseNewType_maybe
1355 -- If topNormliseNewType_maybe ty = Just (co, ty'), then co : ty ~R ty'
1356 topNormaliseNewType_maybe ty
1357 = topNormaliseTypeX unwrapNewTypeStepper mkTransCo ty
1358
1359 {-
1360 %************************************************************************
1361 %* *
1362 Comparison of coercions
1363 %* *
1364 %************************************************************************
1365 -}
1366
1367 -- | Syntactic equality of coercions
1368 eqCoercion :: Coercion -> Coercion -> Bool
1369 eqCoercion = eqType `on` coercionType
1370
1371 -- | Compare two 'Coercion's, with respect to an RnEnv2
1372 eqCoercionX :: RnEnv2 -> Coercion -> Coercion -> Bool
1373 eqCoercionX env = eqTypeX env `on` coercionType
1374
1375 {-
1376 %************************************************************************
1377 %* *
1378 "Lifting" substitution
1379 [(TyCoVar,Coercion)] -> Type -> Coercion
1380 %* *
1381 %************************************************************************
1382
1383 Note [Lifting coercions over types: liftCoSubst]
1384 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1385 The KPUSH rule deals with this situation
1386 data T a = MkK (a -> Maybe a)
1387 g :: T t1 ~ K t2
1388 x :: t1 -> Maybe t1
1389
1390 case (K @t1 x) |> g of
1391 K (y:t2 -> Maybe t2) -> rhs
1392
1393 We want to push the coercion inside the constructor application.
1394 So we do this
1395
1396 g' :: t1~t2 = Nth 0 g
1397
1398 case K @t2 (x |> g' -> Maybe g') of
1399 K (y:t2 -> Maybe t2) -> rhs
1400
1401 The crucial operation is that we
1402 * take the type of K's argument: a -> Maybe a
1403 * and substitute g' for a
1404 thus giving *coercion*. This is what liftCoSubst does.
1405
1406 In the presence of kind coercions, this is a bit
1407 of a hairy operation. So, we refer you to the paper introducing kind coercions,
1408 available at www.cis.upenn.edu/~sweirich/papers/fckinds-extended.pdf
1409 -}
1410
1411 -- ----------------------------------------------------
1412 -- See Note [Lifting coercions over types: liftCoSubst]
1413 -- ----------------------------------------------------
1414
1415 data LiftingContext = LC TCvSubst LiftCoEnv
1416 -- in optCoercion, we need to lift when optimizing InstCo.
1417 -- See Note [Optimising InstCo] in OptCoercion
1418 -- We thus propagate the substitution from OptCoercion here.
1419
1420 instance Outputable LiftingContext where
1421 ppr (LC _ env) = hang (text "LiftingContext:") 2 (ppr env)
1422
1423 type LiftCoEnv = VarEnv Coercion
1424 -- Maps *type variables* to *coercions*.
1425 -- That's the whole point of this function!
1426
1427 -- like liftCoSubstWith, but allows for existentially-bound types as well
1428 liftCoSubstWithEx :: Role -- desired role for output coercion
1429 -> [TyVar] -- universally quantified tyvars
1430 -> [Coercion] -- coercions to substitute for those
1431 -> [TyVar] -- existentially quantified tyvars
1432 -> [Type] -- types to be bound to ex vars
1433 -> (Type -> Coercion, [Type]) -- (lifting function, converted ex args)
1434 liftCoSubstWithEx role univs omegas exs rhos
1435 = let theta = mkLiftingContext (zipEqual "liftCoSubstWithExU" univs omegas)
1436 psi = extendLiftingContextEx theta (zipEqual "liftCoSubstWithExX" exs rhos)
1437 in (ty_co_subst psi role, substTyVars (lcSubstRight psi) exs)
1438
1439 liftCoSubstWith :: Role -> [TyCoVar] -> [Coercion] -> Type -> Coercion
1440 -- NB: This really can be called with CoVars, when optimising axioms.
1441 liftCoSubstWith r tvs cos ty
1442 = liftCoSubst r (mkLiftingContext $ zipEqual "liftCoSubstWith" tvs cos) ty
1443
1444 -- | @liftCoSubst role lc ty@ produces a coercion (at role @role@)
1445 -- that coerces between @lc_left(ty)@ and @lc_right(ty)@, where
1446 -- @lc_left@ is a substitution mapping type variables to the left-hand
1447 -- types of the mapped coercions in @lc@, and similar for @lc_right@.
1448 liftCoSubst :: HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion
1449 liftCoSubst r lc@(LC subst env) ty
1450 | isEmptyVarEnv env = Refl r (substTy subst ty)
1451 | otherwise = ty_co_subst lc r ty
1452
1453 emptyLiftingContext :: InScopeSet -> LiftingContext
1454 emptyLiftingContext in_scope = LC (mkEmptyTCvSubst in_scope) emptyVarEnv
1455
1456 mkLiftingContext :: [(TyCoVar,Coercion)] -> LiftingContext
1457 mkLiftingContext pairs
1458 = LC (mkEmptyTCvSubst $ mkInScopeSet $ tyCoVarsOfCos (map snd pairs))
1459 (mkVarEnv pairs)
1460
1461 mkSubstLiftingContext :: TCvSubst -> LiftingContext
1462 mkSubstLiftingContext subst = LC subst emptyVarEnv
1463
1464 -- | Extend a lifting context with a new /type/ mapping.
1465 extendLiftingContext :: LiftingContext -- ^ original LC
1466 -> TyVar -- ^ new variable to map...
1467 -> Coercion -- ^ ...to this lifted version
1468 -> LiftingContext
1469 extendLiftingContext (LC subst env) tv arg
1470 = ASSERT( isTyVar tv )
1471 LC subst (extendVarEnv env tv arg)
1472
1473 -- | Extend a lifting context with existential-variable bindings.
1474 -- This follows the lifting context extension definition in the
1475 -- "FC with Explicit Kind Equality" paper.
1476 extendLiftingContextEx :: LiftingContext -- ^ original lifting context
1477 -> [(TyVar,Type)] -- ^ ex. var / value pairs
1478 -> LiftingContext
1479 -- Note that this is more involved than extendLiftingContext. That function
1480 -- takes a coercion to extend with, so it's assumed that the caller has taken
1481 -- into account any of the kind-changing stuff worried about here.
1482 extendLiftingContextEx lc [] = lc
1483 extendLiftingContextEx lc@(LC subst env) ((v,ty):rest)
1484 -- This function adds bindings for *Nominal* coercions. Why? Because it
1485 -- works with existentially bound variables, which are considered to have
1486 -- nominal roles.
1487 = let lc' = LC (subst `extendTCvInScopeSet` tyCoVarsOfType ty)
1488 (extendVarEnv env v (mkSymCo $ mkCoherenceCo
1489 (mkNomReflCo ty)
1490 (ty_co_subst lc Nominal (tyVarKind v))))
1491 in extendLiftingContextEx lc' rest
1492
1493 -- | Erase the environments in a lifting context
1494 zapLiftingContext :: LiftingContext -> LiftingContext
1495 zapLiftingContext (LC subst _) = LC (zapTCvSubst subst) emptyVarEnv
1496
1497 -- | Like 'substForAllCoBndr', but works on a lifting context
1498 substForAllCoBndrCallbackLC :: Bool
1499 -> (Coercion -> Coercion)
1500 -> LiftingContext -> TyVar -> Coercion
1501 -> (LiftingContext, TyVar, Coercion)
1502 substForAllCoBndrCallbackLC sym sco (LC subst lc_env) tv co
1503 = (LC subst' lc_env, tv', co')
1504 where
1505 (subst', tv', co') = substForAllCoBndrCallback sym sco subst tv co
1506
1507 -- | The \"lifting\" operation which substitutes coercions for type
1508 -- variables in a type to produce a coercion.
1509 --
1510 -- For the inverse operation, see 'liftCoMatch'
1511 ty_co_subst :: LiftingContext -> Role -> Type -> Coercion
1512 ty_co_subst lc role ty
1513 = go role ty
1514 where
1515 go :: Role -> Type -> Coercion
1516 go Phantom ty = lift_phantom ty
1517 go r (TyVarTy tv) = expectJust "ty_co_subst bad roles" $
1518 liftCoSubstTyVar lc r tv
1519 go r (AppTy ty1 ty2) = mkAppCo (go r ty1) (go Nominal ty2)
1520 go r (TyConApp tc tys) = mkTyConAppCo r tc (zipWith go (tyConRolesX r tc) tys)
1521 go r (FunTy ty1 ty2) = mkFunCo r (go r ty1) (go r ty2)
1522 go r (ForAllTy (TvBndr v _) ty)
1523 = let (lc', v', h) = liftCoSubstVarBndr lc v in
1524 mkForAllCo v' h $! ty_co_subst lc' r ty
1525 go r ty@(LitTy {}) = ASSERT( r == Nominal )
1526 mkReflCo r ty
1527 go r (CastTy ty co) = castCoercionKind (go r ty) (substLeftCo lc co)
1528 (substRightCo lc co)
1529 go r (CoercionTy co) = mkProofIrrelCo r kco (substLeftCo lc co)
1530 (substRightCo lc co)
1531 where kco = go Nominal (coercionType co)
1532
1533 lift_phantom ty = mkPhantomCo (go Nominal (typeKind ty))
1534 (substTy (lcSubstLeft lc) ty)
1535 (substTy (lcSubstRight lc) ty)
1536
1537 {-
1538 Note [liftCoSubstTyVar]
1539 ~~~~~~~~~~~~~~~~~~~~~~~~~
1540 This function can fail if a coercion in the environment is of too low a role.
1541
1542 liftCoSubstTyVar is called from two places: in liftCoSubst (naturally), and
1543 also in matchAxiom in OptCoercion. From liftCoSubst, the so-called lifting
1544 lemma guarantees that the roles work out. If we fail in this
1545 case, we really should panic -- something is deeply wrong. But, in matchAxiom,
1546 failing is fine. matchAxiom is trying to find a set of coercions
1547 that match, but it may fail, and this is healthy behavior.
1548 -}
1549
1550 -- See Note [liftCoSubstTyVar]
1551 liftCoSubstTyVar :: LiftingContext -> Role -> TyVar -> Maybe Coercion
1552 liftCoSubstTyVar (LC subst env) r v
1553 | Just co_arg <- lookupVarEnv env v
1554 = downgradeRole_maybe r (coercionRole co_arg) co_arg
1555
1556 | otherwise
1557 = Just $ Refl r (substTyVar subst v)
1558
1559 liftCoSubstVarBndr :: LiftingContext -> TyVar
1560 -> (LiftingContext, TyVar, Coercion)
1561 liftCoSubstVarBndr lc tv
1562 = let (lc', tv', h, _) = liftCoSubstVarBndrCallback callback lc tv in
1563 (lc', tv', h)
1564 where
1565 callback lc' ty' = (ty_co_subst lc' Nominal ty', ())
1566
1567 -- the callback must produce a nominal coercion
1568 liftCoSubstVarBndrCallback :: (LiftingContext -> Type -> (Coercion, a))
1569 -> LiftingContext -> TyVar
1570 -> (LiftingContext, TyVar, Coercion, a)
1571 liftCoSubstVarBndrCallback fun lc@(LC subst cenv) old_var
1572 = ( LC (subst `extendTCvInScope` new_var) new_cenv
1573 , new_var, eta, stuff )
1574 where
1575 old_kind = tyVarKind old_var
1576 (eta, stuff) = fun lc old_kind
1577 Pair k1 _ = coercionKind eta
1578 new_var = uniqAway (getTCvInScope subst) (setVarType old_var k1)
1579
1580 lifted = Refl Nominal (TyVarTy new_var)
1581 new_cenv = extendVarEnv cenv old_var lifted
1582
1583 -- | Is a var in the domain of a lifting context?
1584 isMappedByLC :: TyCoVar -> LiftingContext -> Bool
1585 isMappedByLC tv (LC _ env) = tv `elemVarEnv` env
1586
1587 -- If [a |-> g] is in the substitution and g :: t1 ~ t2, substitute a for t1
1588 -- If [a |-> (g1, g2)] is in the substitution, substitute a for g1
1589 substLeftCo :: LiftingContext -> Coercion -> Coercion
1590 substLeftCo lc co
1591 = substCo (lcSubstLeft lc) co
1592
1593 -- Ditto, but for t2 and g2
1594 substRightCo :: LiftingContext -> Coercion -> Coercion
1595 substRightCo lc co
1596 = substCo (lcSubstRight lc) co
1597
1598 -- | Apply "sym" to all coercions in a 'LiftCoEnv'
1599 swapLiftCoEnv :: LiftCoEnv -> LiftCoEnv
1600 swapLiftCoEnv = mapVarEnv mkSymCo
1601
1602 lcSubstLeft :: LiftingContext -> TCvSubst
1603 lcSubstLeft (LC subst lc_env) = liftEnvSubstLeft subst lc_env
1604
1605 lcSubstRight :: LiftingContext -> TCvSubst
1606 lcSubstRight (LC subst lc_env) = liftEnvSubstRight subst lc_env
1607
1608 liftEnvSubstLeft :: TCvSubst -> LiftCoEnv -> TCvSubst
1609 liftEnvSubstLeft = liftEnvSubst pFst
1610
1611 liftEnvSubstRight :: TCvSubst -> LiftCoEnv -> TCvSubst
1612 liftEnvSubstRight = liftEnvSubst pSnd
1613
1614 liftEnvSubst :: (forall a. Pair a -> a) -> TCvSubst -> LiftCoEnv -> TCvSubst
1615 liftEnvSubst selector subst lc_env
1616 = composeTCvSubst (TCvSubst emptyInScopeSet tenv cenv) subst
1617 where
1618 pairs = nonDetUFMToList lc_env
1619 -- It's OK to use nonDetUFMToList here because we
1620 -- immediately forget the ordering by creating
1621 -- a VarEnv
1622 (tpairs, cpairs) = partitionWith ty_or_co pairs
1623 tenv = mkVarEnv_Directly tpairs
1624 cenv = mkVarEnv_Directly cpairs
1625
1626 ty_or_co :: (Unique, Coercion) -> Either (Unique, Type) (Unique, Coercion)
1627 ty_or_co (u, co)
1628 | Just equality_co <- isCoercionTy_maybe equality_ty
1629 = Right (u, equality_co)
1630 | otherwise
1631 = Left (u, equality_ty)
1632 where
1633 equality_ty = selector (coercionKind co)
1634
1635 -- | Extract the underlying substitution from the LiftingContext
1636 lcTCvSubst :: LiftingContext -> TCvSubst
1637 lcTCvSubst (LC subst _) = subst
1638
1639 -- | Get the 'InScopeSet' from a 'LiftingContext'
1640 lcInScopeSet :: LiftingContext -> InScopeSet
1641 lcInScopeSet (LC subst _) = getTCvInScope subst
1642
1643 {-
1644 %************************************************************************
1645 %* *
1646 Sequencing on coercions
1647 %* *
1648 %************************************************************************
1649 -}
1650
1651 seqCo :: Coercion -> ()
1652 seqCo (Refl r ty) = r `seq` seqType ty
1653 seqCo (TyConAppCo r tc cos) = r `seq` tc `seq` seqCos cos
1654 seqCo (AppCo co1 co2) = seqCo co1 `seq` seqCo co2
1655 seqCo (ForAllCo tv k co) = seqType (tyVarKind tv) `seq` seqCo k
1656 `seq` seqCo co
1657 seqCo (FunCo r co1 co2) = r `seq` seqCo co1 `seq` seqCo co2
1658 seqCo (CoVarCo cv) = cv `seq` ()
1659 seqCo (AxiomInstCo con ind cos) = con `seq` ind `seq` seqCos cos
1660 seqCo (UnivCo p r t1 t2)
1661 = seqProv p `seq` r `seq` seqType t1 `seq` seqType t2
1662 seqCo (SymCo co) = seqCo co
1663 seqCo (TransCo co1 co2) = seqCo co1 `seq` seqCo co2
1664 seqCo (NthCo n co) = n `seq` seqCo co
1665 seqCo (LRCo lr co) = lr `seq` seqCo co
1666 seqCo (InstCo co arg) = seqCo co `seq` seqCo arg
1667 seqCo (CoherenceCo co1 co2) = seqCo co1 `seq` seqCo co2
1668 seqCo (KindCo co) = seqCo co
1669 seqCo (SubCo co) = seqCo co
1670 seqCo (AxiomRuleCo _ cs) = seqCos cs
1671
1672 seqProv :: UnivCoProvenance -> ()
1673 seqProv UnsafeCoerceProv = ()
1674 seqProv (PhantomProv co) = seqCo co
1675 seqProv (ProofIrrelProv co) = seqCo co
1676 seqProv (PluginProv _) = ()
1677 seqProv (HoleProv _) = ()
1678
1679 seqCos :: [Coercion] -> ()
1680 seqCos [] = ()
1681 seqCos (co:cos) = seqCo co `seq` seqCos cos
1682
1683 {-
1684 %************************************************************************
1685 %* *
1686 The kind of a type, and of a coercion
1687 %* *
1688 %************************************************************************
1689
1690 Note [Computing a coercion kind and role]
1691 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1692 To compute a coercion's kind is straightforward: see coercionKind.
1693 But to compute a coercion's role, in the case for NthCo we need
1694 its kind as well. So if we have two separate functions (one for kinds
1695 and one for roles) we can get exponentially bad behaviour, since each
1696 NthCo node makes a separate call to coercionKind, which traverses the
1697 sub-tree again. This was part of the problem in Trac #9233.
1698
1699 Solution: compute both together; hence coercionKindRole. We keep a
1700 separate coercionKind function because it's a bit more efficient if
1701 the kind is all you want.
1702 -}
1703
1704 coercionType :: Coercion -> Type
1705 coercionType co = case coercionKindRole co of
1706 (Pair ty1 ty2, r) -> mkCoercionType r ty1 ty2
1707
1708 ------------------
1709 -- | If it is the case that
1710 --
1711 -- > c :: (t1 ~ t2)
1712 --
1713 -- i.e. the kind of @c@ relates @t1@ and @t2@, then @coercionKind c = Pair t1 t2@.
1714
1715 coercionKind :: Coercion -> Pair Type
1716 coercionKind co = go co
1717 where
1718 go (Refl _ ty) = Pair ty ty
1719 go (TyConAppCo _ tc cos)= mkTyConApp tc <$> (sequenceA $ map go cos)
1720 go (AppCo co1 co2) = mkAppTy <$> go co1 <*> go co2
1721 go (ForAllCo tv1 k_co co)
1722 = let Pair _ k2 = go k_co
1723 tv2 = setTyVarKind tv1 k2
1724 Pair ty1 ty2 = go co
1725 subst = zipTvSubst [tv1] [TyVarTy tv2 `mk_cast_ty` mkSymCo k_co]
1726 ty2' = substTyAddInScope subst ty2 in
1727 -- We need free vars of ty2 in scope to satisfy the invariant
1728 -- from Note [The substitution invariant]
1729 -- This is doing repeated substitutions and probably doesn't
1730 -- need to, see #11735
1731 mkInvForAllTy <$> Pair tv1 tv2 <*> Pair ty1 ty2'
1732 go (FunCo _ co1 co2) = mkFunTy <$> go co1 <*> go co2
1733 go (CoVarCo cv) = coVarTypes cv
1734 go (AxiomInstCo ax ind cos)
1735 | CoAxBranch { cab_tvs = tvs, cab_cvs = cvs
1736 , cab_lhs = lhs, cab_rhs = rhs } <- coAxiomNthBranch ax ind
1737 , let Pair tycos1 tycos2 = sequenceA (map go cos)
1738 (tys1, cotys1) = splitAtList tvs tycos1
1739 (tys2, cotys2) = splitAtList tvs tycos2
1740 cos1 = map stripCoercionTy cotys1
1741 cos2 = map stripCoercionTy cotys2
1742 = ASSERT( cos `equalLength` (tvs ++ cvs) )
1743 -- Invariant of AxiomInstCo: cos should
1744 -- exactly saturate the axiom branch
1745 Pair (substTyWith tvs tys1 $
1746 substTyWithCoVars cvs cos1 $
1747 mkTyConApp (coAxiomTyCon ax) lhs)
1748 (substTyWith tvs tys2 $
1749 substTyWithCoVars cvs cos2 rhs)
1750 go (UnivCo _ _ ty1 ty2) = Pair ty1 ty2
1751 go (SymCo co) = swap $ go co
1752 go (TransCo co1 co2) = Pair (pFst $ go co1) (pSnd $ go co2)
1753 go g@(NthCo d co)
1754 | Just argss <- traverse tyConAppArgs_maybe tys
1755 = ASSERT( and $ (`lengthExceeds` d) <$> argss )
1756 (`getNth` d) <$> argss
1757
1758 | d == 0
1759 , Just splits <- traverse splitForAllTy_maybe tys
1760 = (tyVarKind . fst) <$> splits
1761
1762 | otherwise
1763 = pprPanic "coercionKind" (ppr g)
1764 where
1765 tys = go co
1766 go (LRCo lr co) = (pickLR lr . splitAppTy) <$> go co
1767 go (InstCo aco arg) = go_app aco [arg]
1768 go (CoherenceCo g h)
1769 = let Pair ty1 ty2 = go g in
1770 Pair (mkCastTy ty1 h) ty2
1771 go (KindCo co) = typeKind <$> go co
1772 go (SubCo co) = go co
1773 go (AxiomRuleCo ax cos) = expectJust "coercionKind" $
1774 coaxrProves ax (map go cos)
1775
1776 go_app :: Coercion -> [Coercion] -> Pair Type
1777 -- Collect up all the arguments and apply all at once
1778 -- See Note [Nested InstCos]
1779 go_app (InstCo co arg) args = go_app co (arg:args)
1780 go_app co args = piResultTys <$> go co <*> (sequenceA $ map go args)
1781
1782 -- The real mkCastTy is too slow, and we can easily have nested ForAllCos.
1783 mk_cast_ty :: Type -> Coercion -> Type
1784 mk_cast_ty ty (Refl {}) = ty
1785 mk_cast_ty ty co = CastTy ty co
1786
1787 -- | Apply 'coercionKind' to multiple 'Coercion's
1788 coercionKinds :: [Coercion] -> Pair [Type]
1789 coercionKinds tys = sequenceA $ map coercionKind tys
1790
1791 -- | Get a coercion's kind and role.
1792 -- Why both at once? See Note [Computing a coercion kind and role]
1793 coercionKindRole :: Coercion -> (Pair Type, Role)
1794 coercionKindRole = go
1795 where
1796 go (Refl r ty) = (Pair ty ty, r)
1797 go (TyConAppCo r tc cos)
1798 = (mkTyConApp tc <$> (sequenceA $ map coercionKind cos), r)
1799 go (AppCo co1 co2)
1800 = let (tys1, r1) = go co1 in
1801 (mkAppTy <$> tys1 <*> coercionKind co2, r1)
1802 go (ForAllCo tv1 k_co co)
1803 = let Pair _ k2 = coercionKind k_co
1804 tv2 = setTyVarKind tv1 k2
1805 (Pair ty1 ty2, r) = go co
1806 subst = zipTvSubst [tv1] [TyVarTy tv2 `mkCastTy` mkSymCo k_co]
1807 ty2' = substTyAddInScope subst ty2 in
1808 -- We need free vars of ty2 in scope to satisfy the invariant
1809 -- from Note [The substitution invariant]
1810 -- This is doing repeated substitutions and probably doesn't
1811 -- need to, see #11735
1812 (mkInvForAllTy <$> Pair tv1 tv2 <*> Pair ty1 ty2', r)
1813 go (FunCo r co1 co2)
1814 = (mkFunTy <$> coercionKind co1 <*> coercionKind co2, r)
1815 go (CoVarCo cv) = (coVarTypes cv, coVarRole cv)
1816 go co@(AxiomInstCo ax _ _) = (coercionKind co, coAxiomRole ax)
1817 go (UnivCo _ r ty1 ty2) = (Pair ty1 ty2, r)
1818 go (SymCo co) = first swap $ go co
1819 go (TransCo co1 co2)
1820 = let (tys1, r) = go co1 in
1821 (Pair (pFst tys1) (pSnd $ coercionKind co2), r)
1822 go (NthCo d co)
1823 | Just (tv1, _) <- splitForAllTy_maybe ty1
1824 = ASSERT( d == 0 )
1825 let (tv2, _) = splitForAllTy ty2 in
1826 (tyVarKind <$> Pair tv1 tv2, Nominal)
1827
1828 | otherwise
1829 = let (tc1, args1) = splitTyConApp ty1
1830 (_tc2, args2) = splitTyConApp ty2
1831 in
1832 ASSERT2( tc1 == _tc2, ppr d $$ ppr tc1 $$ ppr _tc2 )
1833 ((`getNth` d) <$> Pair args1 args2, nthRole r tc1 d)
1834
1835 where
1836 (Pair ty1 ty2, r) = go co
1837 go co@(LRCo {}) = (coercionKind co, Nominal)
1838 go (InstCo co arg) = go_app co [arg]
1839 go (CoherenceCo co1 co2)
1840 = let (Pair t1 t2, r) = go co1 in
1841 (Pair (t1 `mkCastTy` co2) t2, r)
1842 go co@(KindCo {}) = (coercionKind co, Nominal)
1843 go (SubCo co) = (coercionKind co, Representational)
1844 go co@(AxiomRuleCo ax _) = (coercionKind co, coaxrRole ax)
1845
1846 go_app :: Coercion -> [Coercion] -> (Pair Type, Role)
1847 -- Collect up all the arguments and apply all at once
1848 -- See Note [Nested InstCos]
1849 go_app (InstCo co arg) args = go_app co (arg:args)
1850 go_app co args
1851 = let (pair, r) = go co in
1852 (piResultTys <$> pair <*> (sequenceA $ map coercionKind args), r)
1853
1854 -- | Retrieve the role from a coercion.
1855 coercionRole :: Coercion -> Role
1856 coercionRole = snd . coercionKindRole
1857 -- There's not a better way to do this, because NthCo needs the *kind*
1858 -- and role of its argument. Luckily, laziness should generally avoid
1859 -- the need for computing kinds in other cases.
1860
1861 {-
1862 Note [Nested InstCos]
1863 ~~~~~~~~~~~~~~~~~~~~~
1864 In Trac #5631 we found that 70% of the entire compilation time was
1865 being spent in coercionKind! The reason was that we had
1866 (g @ ty1 @ ty2 .. @ ty100) -- The "@s" are InstCos
1867 where
1868 g :: forall a1 a2 .. a100. phi
1869 If we deal with the InstCos one at a time, we'll do this:
1870 1. Find the kind of (g @ ty1 .. @ ty99) : forall a100. phi'
1871 2. Substitute phi'[ ty100/a100 ], a single tyvar->type subst
1872 But this is a *quadratic* algorithm, and the blew up Trac #5631.
1873 So it's very important to do the substitution simultaneously;
1874 cf Type.piResultTys (which in fact we call here).
1875
1876 -}