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