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