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