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