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