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