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