Fix #15845 by defining etaExpandFamInstLHS and using it
[ghc.git] / compiler / types / Coercion.hs
1 {-
2 (c) The University of Glasgow 2006
3 -}
4
5 {-# LANGUAGE RankNTypes, CPP, MultiWayIf, FlexibleContexts #-}
6
7 -- | Module for (a) type kinds and (b) type coercions,
8 -- as used in System FC. See 'CoreSyn.Expr' for
9 -- more on System FC and how coercions fit into it.
10 --
11 module Coercion (
12 -- * Main data type
13 Coercion, CoercionN, CoercionR, CoercionP, MCoercion(..), MCoercionR,
14 UnivCoProvenance, CoercionHole(..), coHoleCoVar, setCoHoleCoVar,
15 LeftOrRight(..),
16 Var, CoVar, TyCoVar,
17 Role(..), ltRole,
18
19 -- ** Functions over coercions
20 coVarTypes, coVarKind, coVarKindsTypesRole, coVarRole,
21 coercionType, coercionKind, coercionKinds,
22 mkCoercionType,
23 coercionRole, coercionKindRole,
24
25 -- ** Constructing coercions
26 mkGReflCo, mkReflCo, mkRepReflCo, mkNomReflCo,
27 mkCoVarCo, mkCoVarCos,
28 mkAxInstCo, mkUnbranchedAxInstCo,
29 mkAxInstRHS, mkUnbranchedAxInstRHS,
30 mkAxInstLHS, mkUnbranchedAxInstLHS,
31 mkPiCo, mkPiCos, mkCoCast,
32 mkSymCo, mkTransCo,
33 mkNthCo, nthCoRole, mkLRCo,
34 mkInstCo, mkAppCo, mkAppCos, mkTyConAppCo, mkFunCo,
35 mkForAllCo, mkForAllCos, mkHomoForAllCos,
36 mkPhantomCo,
37 mkUnsafeCo, mkHoleCo, mkUnivCo, mkSubCo,
38 mkAxiomInstCo, mkProofIrrelCo,
39 downgradeRole, maybeSubCo, mkAxiomRuleCo,
40 mkGReflRightCo, mkGReflLeftCo, mkCoherenceLeftCo, mkCoherenceRightCo,
41 mkKindCo, castCoercionKind, castCoercionKindI,
42
43 mkHeteroCoercionType,
44
45 -- ** Decomposition
46 instNewTyCon_maybe,
47
48 NormaliseStepper, NormaliseStepResult(..), composeSteppers,
49 mapStepResult, unwrapNewTypeStepper,
50 topNormaliseNewType_maybe, topNormaliseTypeX,
51
52 decomposeCo, decomposeFunCo, decomposePiCos, getCoVar_maybe,
53 splitTyConAppCo_maybe,
54 splitAppCo_maybe,
55 splitFunCo_maybe,
56 splitForAllCo_maybe,
57 splitForAllCo_ty_maybe, splitForAllCo_co_maybe,
58
59 nthRole, tyConRolesX, tyConRolesRepresentational, setNominalRole_maybe,
60
61 pickLR,
62
63 isGReflCo, isReflCo, isReflCo_maybe, isGReflCo_maybe, isReflexiveCo, isReflexiveCo_maybe,
64 isReflCoVar_maybe,
65
66 -- ** Coercion variables
67 mkCoVar, isCoVar, coVarName, setCoVarName, setCoVarUnique,
68 isCoVar_maybe,
69
70 -- ** Free variables
71 tyCoVarsOfCo, tyCoVarsOfCos, coVarsOfCo,
72 tyCoFVsOfCo, tyCoFVsOfCos, tyCoVarsOfCoDSet,
73 coercionSize,
74
75 -- ** Substitution
76 CvSubstEnv, emptyCvSubstEnv,
77 lookupCoVar,
78 substCo, substCos, substCoVar, substCoVars, substCoWith,
79 substCoVarBndr,
80 extendTvSubstAndInScope, getCvSubstEnv,
81
82 -- ** Lifting
83 liftCoSubst, liftCoSubstTyVar, liftCoSubstWith, liftCoSubstWithEx,
84 emptyLiftingContext, extendLiftingContext, extendLiftingContextAndInScope,
85 liftCoSubstVarBndrUsing, isMappedByLC,
86
87 mkSubstLiftingContext, zapLiftingContext,
88 substForAllCoBndrUsingLC, lcTCvSubst, lcInScopeSet,
89
90 LiftCoEnv, LiftingContext(..), liftEnvSubstLeft, liftEnvSubstRight,
91 substRightCo, substLeftCo, swapLiftCoEnv, lcSubstLeft, lcSubstRight,
92
93 -- ** Comparison
94 eqCoercion, eqCoercionX,
95
96 -- ** Forcing evaluation of coercions
97 seqCo,
98
99 -- * Pretty-printing
100 pprCo, pprParendCo,
101 pprCoAxiom, pprCoAxBranch, pprCoAxBranchHdr,
102
103 -- * Tidying
104 tidyCo, tidyCos,
105
106 -- * Other
107 promoteCoercion, buildCoercion
108 ) where
109
110 #include "HsVersions.h"
111
112 import GhcPrelude
113
114 import TyCoRep
115 import Type
116 import TyCon
117 import CoAxiom
118 import Var
119 import VarEnv
120 import VarSet
121 import Name hiding ( varName )
122 import Util
123 import BasicTypes
124 import Outputable
125 import Unique
126 import Pair
127 import SrcLoc
128 import PrelNames
129 import TysPrim ( eqPhantPrimTyCon )
130 import ListSetOps
131 import Maybes
132 import UniqFM
133
134 import Control.Monad (foldM, zipWithM)
135 import Data.Function ( on )
136
137 {-
138 %************************************************************************
139 %* *
140 -- The coercion arguments always *precisely* saturate
141 -- arity of (that branch of) the CoAxiom. If there are
142 -- any left over, we use AppCo. See
143 -- See [Coercion axioms applied to coercions] in TyCoRep
144
145 \subsection{Coercion variables}
146 %* *
147 %************************************************************************
148 -}
149
150 coVarName :: CoVar -> Name
151 coVarName = varName
152
153 setCoVarUnique :: CoVar -> Unique -> CoVar
154 setCoVarUnique = setVarUnique
155
156 setCoVarName :: CoVar -> Name -> CoVar
157 setCoVarName = setVarName
158
159 {-
160 %************************************************************************
161 %* *
162 Pretty-printing CoAxioms
163 %* *
164 %************************************************************************
165
166 Defined here to avoid module loops. CoAxiom is loaded very early on.
167
168 -}
169
170 pprCoAxiom :: CoAxiom br -> SDoc
171 pprCoAxiom ax@(CoAxiom { co_ax_branches = branches })
172 = hang (text "axiom" <+> ppr ax <+> dcolon)
173 2 (vcat (map (ppr_co_ax_branch (\_ ty -> equals <+> pprType ty) ax) $
174 fromBranches branches))
175
176 pprCoAxBranch :: CoAxiom br -> CoAxBranch -> SDoc
177 pprCoAxBranch = ppr_co_ax_branch pprRhs
178 where
179 pprRhs fam_tc rhs
180 | isDataFamilyTyCon fam_tc
181 = empty -- Don't bother printing anything for the RHS of a data family
182 -- instance...
183
184 | otherwise
185 = equals <+> ppr rhs
186 -- ...but for a type family instance, do print out the RHS, since
187 -- it might be needed to disambiguate between duplicate instances
188 -- (#14179)
189
190 pprCoAxBranchHdr :: CoAxiom br -> BranchIndex -> SDoc
191 pprCoAxBranchHdr ax index = pprCoAxBranch ax (coAxiomNthBranch ax index)
192
193 ppr_co_ax_branch :: (TyCon -> Type -> SDoc) -> CoAxiom br -> CoAxBranch -> SDoc
194 ppr_co_ax_branch ppr_rhs
195 (CoAxiom { co_ax_tc = fam_tc, co_ax_name = name })
196 (CoAxBranch { cab_tvs = tvs
197 , cab_cvs = cvs
198 , cab_lhs = lhs
199 , cab_rhs = rhs
200 , cab_loc = loc })
201 = foldr1 (flip hangNotEmpty 2)
202 [ pprUserForAll (mkTyCoVarBinders Inferred (ee_tvs ++ cvs))
203 , pprTypeApp fam_tc ee_lhs <+> ppr_rhs fam_tc rhs
204 , text "-- Defined" <+> pprLoc loc ]
205 where
206 pprLoc loc
207 | isGoodSrcSpan loc
208 = text "at" <+> ppr (srcSpanStart loc)
209
210 | otherwise
211 = text "in" <+>
212 quotes (ppr (nameModule name))
213
214 -- Eta-expand LHS types, because sometimes data family instances
215 -- are eta-reduced.
216 -- See Note [Eta reduction for data families] in FamInstEnv.
217 (ee_tvs, ee_lhs) = etaExpandFamInstLHS tvs lhs rhs
218
219 {-
220 %************************************************************************
221 %* *
222 Destructing coercions
223 %* *
224 %************************************************************************
225
226 Note [Function coercions]
227 ~~~~~~~~~~~~~~~~~~~~~~~~~
228 Remember that
229 (->) :: forall r1 r2. TYPE r1 -> TYPE r2 -> TYPE LiftedRep
230
231 Hence
232 FunCo r co1 co2 :: (s1->t1) ~r (s2->t2)
233 is short for
234 TyConAppCo (->) co_rep1 co_rep2 co1 co2
235 where co_rep1, co_rep2 are the coercions on the representations.
236 -}
237
238
239 -- | This breaks a 'Coercion' with type @T A B C ~ T D E F@ into
240 -- a list of 'Coercion's of kinds @A ~ D@, @B ~ E@ and @E ~ F@. Hence:
241 --
242 -- > decomposeCo 3 c [r1, r2, r3] = [nth r1 0 c, nth r2 1 c, nth r3 2 c]
243 decomposeCo :: Arity -> Coercion
244 -> [Role] -- the roles of the output coercions
245 -- this must have at least as many
246 -- entries as the Arity provided
247 -> [Coercion]
248 decomposeCo arity co rs
249 = [mkNthCo r n co | (n,r) <- [0..(arity-1)] `zip` rs ]
250 -- Remember, Nth is zero-indexed
251
252 decomposeFunCo :: HasDebugCallStack
253 => Role -- Role of the input coercion
254 -> Coercion -- Input coercion
255 -> (Coercion, Coercion)
256 -- Expects co :: (s1 -> t1) ~ (s2 -> t2)
257 -- Returns (co1 :: s1~s2, co2 :: t1~t2)
258 -- See Note [Function coercions] for the "2" and "3"
259 decomposeFunCo r co = ASSERT2( all_ok, ppr co )
260 (mkNthCo r 2 co, mkNthCo r 3 co)
261 where
262 Pair s1t1 s2t2 = coercionKind co
263 all_ok = isFunTy s1t1 && isFunTy s2t2
264
265 {- Note [Pushing a coercion into a pi-type]
266 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
267 Suppose we have this:
268 (f |> co) t1 .. tn
269 Then we want to push the coercion into the arguments, so as to make
270 progress. For example of why you might want to do so, see Note
271 [Respecting definitional equality] in TyCoRep.
272
273 This is done by decomposePiCos. Specifically, if
274 decomposePiCos co [t1,..,tn] = ([co1,...,cok], cor)
275 then
276 (f |> co) t1 .. tn = (f (t1 |> co1) ... (tk |> cok)) |> cor) t(k+1) ... tn
277
278 Notes:
279
280 * k can be smaller than n! That is decomposePiCos can return *fewer*
281 coercions than there are arguments (ie k < n), if the kind provided
282 doesn't have enough binders.
283
284 * If there is a type error, we might see
285 (f |> co) t1
286 where co :: (forall a. ty) ~ (ty1 -> ty2)
287 Here 'co' is insoluble, but we don't want to crash in decoposePiCos.
288 So decomposePiCos carefully tests both sides of the coercion to check
289 they are both foralls or both arrows. Not doing this caused Trac #15343.
290 -}
291
292 decomposePiCos :: HasDebugCallStack
293 => CoercionN -> Pair Type -- Coercion and its kind
294 -> [Type]
295 -> ([CoercionN], CoercionN)
296 -- See Note [Pushing a coercion into a pi-type]
297 decomposePiCos orig_co (Pair orig_k1 orig_k2) orig_args
298 = go [] (orig_subst,orig_k1) orig_co (orig_subst,orig_k2) orig_args
299 where
300 orig_subst = mkEmptyTCvSubst $ mkInScopeSet $
301 tyCoVarsOfTypes orig_args `unionVarSet` tyCoVarsOfCo orig_co
302
303 go :: [CoercionN] -- accumulator for argument coercions, reversed
304 -> (TCvSubst,Kind) -- Lhs kind of coercion
305 -> CoercionN -- coercion originally applied to the function
306 -> (TCvSubst,Kind) -- Rhs kind of coercion
307 -> [Type] -- Arguments to that function
308 -> ([CoercionN], Coercion)
309 -- Invariant: co :: subst1(k2) ~ subst2(k2)
310
311 go acc_arg_cos (subst1,k1) co (subst2,k2) (ty:tys)
312 | Just (a, t1) <- splitForAllTy_maybe k1
313 , Just (b, t2) <- splitForAllTy_maybe k2
314 -- know co :: (forall a:s1.t1) ~ (forall b:s2.t2)
315 -- function :: forall a:s1.t1 (the function is not passed to decomposePiCos)
316 -- a :: s1
317 -- b :: s2
318 -- ty :: s2
319 -- need arg_co :: s2 ~ s1
320 -- res_co :: t1[ty |> arg_co / a] ~ t2[ty / b]
321 = let arg_co = mkNthCo Nominal 0 (mkSymCo co)
322 res_co = mkInstCo co (mkGReflLeftCo Nominal ty arg_co)
323 subst1' = extendTCvSubst subst1 a (ty `CastTy` arg_co)
324 subst2' = extendTCvSubst subst2 b ty
325 in
326 go (arg_co : acc_arg_cos) (subst1', t1) res_co (subst2', t2) tys
327
328 | Just (_s1, t1) <- splitFunTy_maybe k1
329 , Just (_s2, t2) <- splitFunTy_maybe k2
330 -- know co :: (s1 -> t1) ~ (s2 -> t2)
331 -- function :: s1 -> t1
332 -- ty :: s2
333 -- need arg_co :: s2 ~ s1
334 -- res_co :: t1 ~ t2
335 = let (sym_arg_co, res_co) = decomposeFunCo Nominal co
336 arg_co = mkSymCo sym_arg_co
337 in
338 go (arg_co : acc_arg_cos) (subst1,t1) res_co (subst2,t2) tys
339
340 | not (isEmptyTCvSubst subst1) || not (isEmptyTCvSubst subst2)
341 = go acc_arg_cos (zapTCvSubst subst1, substTy subst1 k1)
342 co
343 (zapTCvSubst subst2, substTy subst1 k2)
344 (ty:tys)
345
346 -- tys might not be empty, if the left-hand type of the original coercion
347 -- didn't have enough binders
348 go acc_arg_cos _ki1 co _ki2 _tys = (reverse acc_arg_cos, co)
349
350 -- | Attempts to obtain the type variable underlying a 'Coercion'
351 getCoVar_maybe :: Coercion -> Maybe CoVar
352 getCoVar_maybe (CoVarCo cv) = Just cv
353 getCoVar_maybe _ = Nothing
354
355 -- | Attempts to tease a coercion apart into a type constructor and the application
356 -- of a number of coercion arguments to that constructor
357 splitTyConAppCo_maybe :: Coercion -> Maybe (TyCon, [Coercion])
358 splitTyConAppCo_maybe co
359 | Just (ty, r) <- isReflCo_maybe co
360 = do { (tc, tys) <- splitTyConApp_maybe ty
361 ; let args = zipWith mkReflCo (tyConRolesX r tc) tys
362 ; return (tc, args) }
363 splitTyConAppCo_maybe (TyConAppCo _ tc cos) = Just (tc, cos)
364 splitTyConAppCo_maybe (FunCo _ arg res) = Just (funTyCon, cos)
365 where cos = [mkRuntimeRepCo arg, mkRuntimeRepCo res, arg, res]
366 splitTyConAppCo_maybe _ = Nothing
367
368 -- first result has role equal to input; third result is Nominal
369 splitAppCo_maybe :: Coercion -> Maybe (Coercion, Coercion)
370 -- ^ Attempt to take a coercion application apart.
371 splitAppCo_maybe (AppCo co arg) = Just (co, arg)
372 splitAppCo_maybe (TyConAppCo r tc args)
373 | args `lengthExceeds` tyConArity tc
374 , Just (args', arg') <- snocView args
375 = Just ( mkTyConAppCo r tc args', arg' )
376
377 | mightBeUnsaturatedTyCon tc
378 -- Never create unsaturated type family apps!
379 , Just (args', arg') <- snocView args
380 , Just arg'' <- setNominalRole_maybe (nthRole r tc (length args')) arg'
381 = Just ( mkTyConAppCo r tc args', arg'' )
382 -- Use mkTyConAppCo to preserve the invariant
383 -- that identity coercions are always represented by Refl
384
385 splitAppCo_maybe co
386 | Just (ty, r) <- isReflCo_maybe co
387 , Just (ty1, ty2) <- splitAppTy_maybe ty
388 = Just (mkReflCo r ty1, mkNomReflCo ty2)
389 splitAppCo_maybe _ = Nothing
390
391 splitFunCo_maybe :: Coercion -> Maybe (Coercion, Coercion)
392 splitFunCo_maybe (FunCo _ arg res) = Just (arg, res)
393 splitFunCo_maybe _ = Nothing
394
395 splitForAllCo_maybe :: Coercion -> Maybe (TyCoVar, Coercion, Coercion)
396 splitForAllCo_maybe (ForAllCo tv k_co co) = Just (tv, k_co, co)
397 splitForAllCo_maybe _ = Nothing
398
399 -- | Like 'splitForAllCo_maybe', but only returns Just for tyvar binder
400 splitForAllCo_ty_maybe :: Coercion -> Maybe (TyVar, Coercion, Coercion)
401 splitForAllCo_ty_maybe (ForAllCo tv k_co co)
402 | isTyVar tv = Just (tv, k_co, co)
403 splitForAllCo_ty_maybe _ = Nothing
404
405 -- | Like 'splitForAllCo_maybe', but only returns Just for covar binder
406 splitForAllCo_co_maybe :: Coercion -> Maybe (CoVar, Coercion, Coercion)
407 splitForAllCo_co_maybe (ForAllCo cv k_co co)
408 | isCoVar cv = Just (cv, k_co, co)
409 splitForAllCo_co_maybe _ = Nothing
410
411 -------------------------------------------------------
412 -- and some coercion kind stuff
413
414 coVarTypes :: HasDebugCallStack => CoVar -> Pair Type
415 coVarTypes cv
416 | (_, _, ty1, ty2, _) <- coVarKindsTypesRole cv
417 = Pair ty1 ty2
418
419 coVarKindsTypesRole :: HasDebugCallStack => CoVar -> (Kind,Kind,Type,Type,Role)
420 coVarKindsTypesRole cv
421 | Just (tc, [k1,k2,ty1,ty2]) <- splitTyConApp_maybe (varType cv)
422 = let role
423 | tc `hasKey` eqPrimTyConKey = Nominal
424 | tc `hasKey` eqReprPrimTyConKey = Representational
425 | otherwise = panic "coVarKindsTypesRole"
426 in (k1,k2,ty1,ty2,role)
427 | otherwise = pprPanic "coVarKindsTypesRole, non coercion variable"
428 (ppr cv $$ ppr (varType cv))
429
430 coVarKind :: CoVar -> Type
431 coVarKind cv
432 = ASSERT( isCoVar cv )
433 varType cv
434
435 coVarRole :: CoVar -> Role
436 coVarRole cv
437 | tc `hasKey` eqPrimTyConKey
438 = Nominal
439 | tc `hasKey` eqReprPrimTyConKey
440 = Representational
441 | otherwise
442 = pprPanic "coVarRole: unknown tycon" (ppr cv <+> dcolon <+> ppr (varType cv))
443
444 where
445 tc = case tyConAppTyCon_maybe (varType cv) of
446 Just tc0 -> tc0
447 Nothing -> pprPanic "coVarRole: not tyconapp" (ppr cv)
448
449 -- | Makes a coercion type from two types: the types whose equality
450 -- is proven by the relevant 'Coercion'
451 mkCoercionType :: Role -> Type -> Type -> Type
452 mkCoercionType Nominal = mkPrimEqPred
453 mkCoercionType Representational = mkReprPrimEqPred
454 mkCoercionType Phantom = \ty1 ty2 ->
455 let ki1 = typeKind ty1
456 ki2 = typeKind ty2
457 in
458 TyConApp eqPhantPrimTyCon [ki1, ki2, ty1, ty2]
459
460 mkHeteroCoercionType :: Role -> Kind -> Kind -> Type -> Type -> Type
461 mkHeteroCoercionType Nominal = mkHeteroPrimEqPred
462 mkHeteroCoercionType Representational = mkHeteroReprPrimEqPred
463 mkHeteroCoercionType Phantom = panic "mkHeteroCoercionType"
464
465 -- | Given a coercion @co1 :: (a :: TYPE r1) ~ (b :: TYPE r2)@,
466 -- produce a coercion @rep_co :: r1 ~ r2@.
467 mkRuntimeRepCo :: HasDebugCallStack => Coercion -> Coercion
468 mkRuntimeRepCo co
469 = mkNthCo Nominal 0 kind_co
470 where
471 kind_co = mkKindCo co -- kind_co :: TYPE r1 ~ TYPE r2
472 -- (up to silliness with Constraint)
473
474 isReflCoVar_maybe :: Var -> Maybe Coercion
475 -- If cv :: t~t then isReflCoVar_maybe cv = Just (Refl t)
476 -- Works on all kinds of Vars, not just CoVars
477 isReflCoVar_maybe cv
478 | isCoVar cv
479 , Pair ty1 ty2 <- coVarTypes cv
480 , ty1 `eqType` ty2
481 = Just (mkReflCo (coVarRole cv) ty1)
482 | otherwise
483 = Nothing
484
485 -- | Tests if this coercion is obviously a generalized reflexive coercion.
486 -- Guaranteed to work very quickly.
487 isGReflCo :: Coercion -> Bool
488 isGReflCo (GRefl{}) = True
489 isGReflCo (Refl{}) = True -- Refl ty == GRefl N ty MRefl
490 isGReflCo _ = False
491
492 -- | Tests if this MCoercion is obviously generalized reflexive
493 -- Guaranteed to work very quickly.
494 isGReflMCo :: MCoercion -> Bool
495 isGReflMCo MRefl = True
496 isGReflMCo (MCo co) | isGReflCo co = True
497 isGReflMCo _ = False
498
499 -- | Tests if this coercion is obviously reflexive. Guaranteed to work
500 -- very quickly. Sometimes a coercion can be reflexive, but not obviously
501 -- so. c.f. 'isReflexiveCo'
502 isReflCo :: Coercion -> Bool
503 isReflCo (Refl{}) = True
504 isReflCo (GRefl _ _ mco) | isGReflMCo mco = True
505 isReflCo _ = False
506
507 -- | Returns the type coerced if this coercion is a generalized reflexive
508 -- coercion. Guaranteed to work very quickly.
509 isGReflCo_maybe :: Coercion -> Maybe (Type, Role)
510 isGReflCo_maybe (GRefl r ty _) = Just (ty, r)
511 isGReflCo_maybe (Refl ty) = Just (ty, Nominal)
512 isGReflCo_maybe _ = Nothing
513
514 -- | Returns the type coerced if this coercion is reflexive. Guaranteed
515 -- to work very quickly. Sometimes a coercion can be reflexive, but not
516 -- obviously so. c.f. 'isReflexiveCo_maybe'
517 isReflCo_maybe :: Coercion -> Maybe (Type, Role)
518 isReflCo_maybe (Refl ty) = Just (ty, Nominal)
519 isReflCo_maybe (GRefl r ty mco) | isGReflMCo mco = Just (ty, r)
520 isReflCo_maybe _ = Nothing
521
522 -- | Slowly checks if the coercion is reflexive. Don't call this in a loop,
523 -- as it walks over the entire coercion.
524 isReflexiveCo :: Coercion -> Bool
525 isReflexiveCo = isJust . isReflexiveCo_maybe
526
527 -- | Extracts the coerced type from a reflexive coercion. This potentially
528 -- walks over the entire coercion, so avoid doing this in a loop.
529 isReflexiveCo_maybe :: Coercion -> Maybe (Type, Role)
530 isReflexiveCo_maybe (Refl ty) = Just (ty, Nominal)
531 isReflexiveCo_maybe (GRefl r ty mco) | isGReflMCo mco = Just (ty, r)
532 isReflexiveCo_maybe co
533 | ty1 `eqType` ty2
534 = Just (ty1, r)
535 | otherwise
536 = Nothing
537 where (Pair ty1 ty2, r) = coercionKindRole co
538
539 {-
540 %************************************************************************
541 %* *
542 Building coercions
543 %* *
544 %************************************************************************
545
546 These "smart constructors" maintain the invariants listed in the definition
547 of Coercion, and they perform very basic optimizations.
548
549 Note [Role twiddling functions]
550 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
551
552 There are a plethora of functions for twiddling roles:
553
554 mkSubCo: Requires a nominal input coercion and always produces a
555 representational output. This is used when you (the programmer) are sure you
556 know exactly that role you have and what you want.
557
558 downgradeRole_maybe: This function takes both the input role and the output role
559 as parameters. (The *output* role comes first!) It can only *downgrade* a
560 role -- that is, change it from N to R or P, or from R to P. This one-way
561 behavior is why there is the "_maybe". If an upgrade is requested, this
562 function produces Nothing. This is used when you need to change the role of a
563 coercion, but you're not sure (as you're writing the code) of which roles are
564 involved.
565
566 This function could have been written using coercionRole to ascertain the role
567 of the input. But, that function is recursive, and the caller of downgradeRole_maybe
568 often knows the input role. So, this is more efficient.
569
570 downgradeRole: This is just like downgradeRole_maybe, but it panics if the
571 conversion isn't a downgrade.
572
573 setNominalRole_maybe: This is the only function that can *upgrade* a coercion.
574 The result (if it exists) is always Nominal. The input can be at any role. It
575 works on a "best effort" basis, as it should never be strictly necessary to
576 upgrade a coercion during compilation. It is currently only used within GHC in
577 splitAppCo_maybe. In order to be a proper inverse of mkAppCo, the second
578 coercion that splitAppCo_maybe returns must be nominal. But, it's conceivable
579 that splitAppCo_maybe is operating over a TyConAppCo that uses a
580 representational coercion. Hence the need for setNominalRole_maybe.
581 splitAppCo_maybe, in turn, is used only within coercion optimization -- thus,
582 it is not absolutely critical that setNominalRole_maybe be complete.
583
584 Note that setNominalRole_maybe will never upgrade a phantom UnivCo. Phantom
585 UnivCos are perfectly type-safe, whereas representational and nominal ones are
586 not. Indeed, `unsafeCoerce` is implemented via a representational UnivCo.
587 (Nominal ones are no worse than representational ones, so this function *will*
588 change a UnivCo Representational to a UnivCo Nominal.)
589
590 Conal Elliott also came across a need for this function while working with the
591 GHC API, as he was decomposing Core casts. The Core casts use representational
592 coercions, as they must, but his use case required nominal coercions (he was
593 building a GADT). So, that's why this function is exported from this module.
594
595 One might ask: shouldn't downgradeRole_maybe just use setNominalRole_maybe as
596 appropriate? I (Richard E.) have decided not to do this, because upgrading a
597 role is bizarre and a caller should have to ask for this behavior explicitly.
598
599 -}
600
601 -- | Make a generalized reflexive coercion
602 mkGReflCo :: Role -> Type -> MCoercionN -> Coercion
603 mkGReflCo r ty mco
604 | isGReflMCo mco = if r == Nominal then Refl ty
605 else GRefl r ty MRefl
606 | otherwise = GRefl r ty mco
607
608 -- | Make a reflexive coercion
609 mkReflCo :: Role -> Type -> Coercion
610 mkReflCo Nominal ty = Refl ty
611 mkReflCo r ty = GRefl r ty MRefl
612
613 -- | Make a representational reflexive coercion
614 mkRepReflCo :: Type -> Coercion
615 mkRepReflCo ty = GRefl Representational ty MRefl
616
617 -- | Make a nominal reflexive coercion
618 mkNomReflCo :: Type -> Coercion
619 mkNomReflCo = Refl
620
621 -- | Apply a type constructor to a list of coercions. It is the
622 -- caller's responsibility to get the roles correct on argument coercions.
623 mkTyConAppCo :: HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
624 mkTyConAppCo r tc cos
625 | tc `hasKey` funTyConKey
626 , [_rep1, _rep2, co1, co2] <- cos -- See Note [Function coercions]
627 = -- (a :: TYPE ra) -> (b :: TYPE rb) ~ (c :: TYPE rc) -> (d :: TYPE rd)
628 -- rep1 :: ra ~ rc rep2 :: rb ~ rd
629 -- co1 :: a ~ c co2 :: b ~ d
630 mkFunCo r co1 co2
631
632 -- Expand type synonyms
633 | Just (tv_co_prs, rhs_ty, leftover_cos) <- expandSynTyCon_maybe tc cos
634 = mkAppCos (liftCoSubst r (mkLiftingContext tv_co_prs) rhs_ty) leftover_cos
635
636 | Just tys_roles <- traverse isReflCo_maybe cos
637 = mkReflCo r (mkTyConApp tc (map fst tys_roles))
638 -- See Note [Refl invariant]
639
640 | otherwise = TyConAppCo r tc cos
641
642 -- | Build a function 'Coercion' from two other 'Coercion's. That is,
643 -- given @co1 :: a ~ b@ and @co2 :: x ~ y@ produce @co :: (a -> x) ~ (b -> y)@.
644 mkFunCo :: Role -> Coercion -> Coercion -> Coercion
645 mkFunCo r co1 co2
646 -- See Note [Refl invariant]
647 | Just (ty1, _) <- isReflCo_maybe co1
648 , Just (ty2, _) <- isReflCo_maybe co2
649 = mkReflCo r (mkFunTy ty1 ty2)
650 | otherwise = FunCo r co1 co2
651
652 -- | Apply a 'Coercion' to another 'Coercion'.
653 -- The second coercion must be Nominal, unless the first is Phantom.
654 -- If the first is Phantom, then the second can be either Phantom or Nominal.
655 mkAppCo :: Coercion -- ^ :: t1 ~r t2
656 -> Coercion -- ^ :: s1 ~N s2, where s1 :: k1, s2 :: k2
657 -> Coercion -- ^ :: t1 s1 ~r t2 s2
658 mkAppCo co arg
659 | Just (ty1, r) <- isReflCo_maybe co
660 , Just (ty2, _) <- isReflCo_maybe arg
661 = mkReflCo r (mkAppTy ty1 ty2)
662
663 | Just (ty1, r) <- isReflCo_maybe co
664 , Just (tc, tys) <- splitTyConApp_maybe ty1
665 -- Expand type synonyms; a TyConAppCo can't have a type synonym (Trac #9102)
666 = mkTyConAppCo r tc (zip_roles (tyConRolesX r tc) tys)
667 where
668 zip_roles (r1:_) [] = [downgradeRole r1 Nominal arg]
669 zip_roles (r1:rs) (ty1:tys) = mkReflCo r1 ty1 : zip_roles rs tys
670 zip_roles _ _ = panic "zip_roles" -- but the roles are infinite...
671
672 mkAppCo (TyConAppCo r tc args) arg
673 = case r of
674 Nominal -> mkTyConAppCo Nominal tc (args ++ [arg])
675 Representational -> mkTyConAppCo Representational tc (args ++ [arg'])
676 where new_role = (tyConRolesRepresentational tc) !! (length args)
677 arg' = downgradeRole new_role Nominal arg
678 Phantom -> mkTyConAppCo Phantom tc (args ++ [toPhantomCo arg])
679 mkAppCo co arg = AppCo co arg
680 -- Note, mkAppCo is careful to maintain invariants regarding
681 -- where Refl constructors appear; see the comments in the definition
682 -- of Coercion and the Note [Refl invariant] in TyCoRep.
683
684 -- | Applies multiple 'Coercion's to another 'Coercion', from left to right.
685 -- See also 'mkAppCo'.
686 mkAppCos :: Coercion
687 -> [Coercion]
688 -> Coercion
689 mkAppCos co1 cos = foldl' mkAppCo co1 cos
690
691 {- Note [Unused coercion variable in ForAllCo]
692
693 See Note [Unused coercion variable in ForAllTy] in TyCoRep for the motivation for
694 checking coercion variable in types.
695 To lift the design choice to (ForAllCo cv kind_co body_co), we have two options:
696
697 (1) In mkForAllCo, we check whether cv is a coercion variable
698 and whether it is not used in body_co. If so we construct a FunCo.
699 (2) We don't do this check in mkForAllCo.
700 In coercionKind, we use mkTyCoForAllTy to perform the check and construct
701 a FunTy when necessary.
702
703 We chose (2) for two reasons:
704
705 * for a coercion, all that matters is its kind, So ForAllCo or FunCo does not
706 make a difference.
707 * even if cv occurs in body_co, it is possible that cv does not occur in the kind
708 of body_co. Therefore the check in coercionKind is inevitable.
709
710 The last wrinkle is that there are restrictions around the use of the cv in the
711 coercion, as described in Section 5.8.5.2 of Richard's thesis. The idea is that
712 we cannot prove that the type system is consistent with unrestricted use of this
713 cv; the consistency proof uses an untyped rewrite relation that works over types
714 with all coercions and casts removed. So, we can allow the cv to appear only in
715 positions that are erased. As an approximation of this (and keeping close to the
716 published theory), we currently allow the cv only within the type in a Refl node
717 and under a GRefl node (including in the Coercion stored in a GRefl). It's
718 possible other places are OK, too, but this is a safe approximation.
719
720 Sadly, with heterogeneous equality, this restriction might be able to be violated;
721 Richard's thesis is unable to prove that it isn't. Specifically, the liftCoSubst
722 function might create an invalid coercion. Because a violation of the
723 restriction might lead to a program that "goes wrong", it is checked all the time,
724 even in a production compiler and without -dcore-list. We *have* proved that the
725 problem does not occur with homogeneous equality, so this check can be dropped
726 once ~# is made to be homogeneous.
727 -}
728
729
730 -- | Make a Coercion from a tycovar, a kind coercion, and a body coercion.
731 -- The kind of the tycovar should be the left-hand kind of the kind coercion.
732 -- See Note [Unused coercion variable in ForAllCo]
733 mkForAllCo :: TyCoVar -> CoercionN -> Coercion -> Coercion
734 mkForAllCo v kind_co co
735 | ASSERT( varType v `eqType` (pFst $ coercionKind kind_co)) True
736 , ASSERT( isTyVar v || almostDevoidCoVarOfCo v co) True
737 , Just (ty, r) <- isReflCo_maybe co
738 , isGReflCo kind_co
739 = mkReflCo r (mkTyCoInvForAllTy v ty)
740 | otherwise
741 = ForAllCo v kind_co co
742
743 -- | Like 'mkForAllCo', but the inner coercion shouldn't be an obvious
744 -- reflexive coercion. For example, it is guaranteed in 'mkForAllCos'.
745 -- The kind of the tycovar should be the left-hand kind of the kind coercion.
746 mkForAllCo_NoRefl :: TyCoVar -> CoercionN -> Coercion -> Coercion
747 mkForAllCo_NoRefl v kind_co co
748 | ASSERT( varType v `eqType` (pFst $ coercionKind kind_co)) True
749 , ASSERT( isTyVar v || almostDevoidCoVarOfCo v co) True
750 , ASSERT( not (isReflCo co)) True
751 , isCoVar v
752 , not (v `elemVarSet` tyCoVarsOfCo co)
753 = FunCo (coercionRole co) kind_co co
754 | otherwise
755 = ForAllCo v kind_co co
756
757 -- | Make nested ForAllCos
758 mkForAllCos :: [(TyCoVar, CoercionN)] -> Coercion -> Coercion
759 mkForAllCos bndrs co
760 | Just (ty, r ) <- isReflCo_maybe co
761 = let (refls_rev'd, non_refls_rev'd) = span (isReflCo . snd) (reverse bndrs) in
762 foldl' (flip $ uncurry mkForAllCo_NoRefl)
763 (mkReflCo r (mkTyCoInvForAllTys (reverse (map fst refls_rev'd)) ty))
764 non_refls_rev'd
765 | otherwise
766 = foldr (uncurry mkForAllCo_NoRefl) co bndrs
767
768 -- | Make a Coercion quantified over a type/coercion variable;
769 -- the variable has the same type in both sides of the coercion
770 mkHomoForAllCos :: [TyCoVar] -> Coercion -> Coercion
771 mkHomoForAllCos vs co
772 | Just (ty, r) <- isReflCo_maybe co
773 = mkReflCo r (mkTyCoInvForAllTys vs ty)
774 | otherwise
775 = mkHomoForAllCos_NoRefl vs co
776
777 -- | Like 'mkHomoForAllCos', but the inner coercion shouldn't be an obvious
778 -- reflexive coercion. For example, it is guaranteed in 'mkHomoForAllCos'.
779 mkHomoForAllCos_NoRefl :: [TyCoVar] -> Coercion -> Coercion
780 mkHomoForAllCos_NoRefl vs orig_co
781 = ASSERT( not (isReflCo orig_co))
782 foldr go orig_co vs
783 where
784 go v co = mkForAllCo_NoRefl v (mkNomReflCo (varType v)) co
785
786 mkCoVarCo :: CoVar -> Coercion
787 -- cv :: s ~# t
788 -- See Note [mkCoVarCo]
789 mkCoVarCo cv = CoVarCo cv
790
791 mkCoVarCos :: [CoVar] -> [Coercion]
792 mkCoVarCos = map mkCoVarCo
793
794 {- Note [mkCoVarCo]
795 ~~~~~~~~~~~~~~~~~~~
796 In the past, mkCoVarCo optimised (c :: t~t) to (Refl t). That is
797 valid (although see Note [Unbound RULE binders] in Rules), but
798 it's a relatively expensive test and perhaps better done in
799 optCoercion. Not a big deal either way.
800 -}
801
802 -- | Extract a covar, if possible. This check is dirty. Be ashamed
803 -- of yourself. (It's dirty because it cares about the structure of
804 -- a coercion, which is morally reprehensible.)
805 isCoVar_maybe :: Coercion -> Maybe CoVar
806 isCoVar_maybe (CoVarCo cv) = Just cv
807 isCoVar_maybe _ = Nothing
808
809 mkAxInstCo :: Role -> CoAxiom br -> BranchIndex -> [Type] -> [Coercion]
810 -> Coercion
811 -- mkAxInstCo can legitimately be called over-staturated;
812 -- i.e. with more type arguments than the coercion requires
813 mkAxInstCo role ax index tys cos
814 | arity == n_tys = downgradeRole role ax_role $
815 mkAxiomInstCo ax_br index (rtys `chkAppend` cos)
816 | otherwise = ASSERT( arity < n_tys )
817 downgradeRole role ax_role $
818 mkAppCos (mkAxiomInstCo ax_br index
819 (ax_args `chkAppend` cos))
820 leftover_args
821 where
822 n_tys = length tys
823 ax_br = toBranchedAxiom ax
824 branch = coAxiomNthBranch ax_br index
825 tvs = coAxBranchTyVars branch
826 arity = length tvs
827 arg_roles = coAxBranchRoles branch
828 rtys = zipWith mkReflCo (arg_roles ++ repeat Nominal) tys
829 (ax_args, leftover_args)
830 = splitAt arity rtys
831 ax_role = coAxiomRole ax
832
833 -- worker function
834 mkAxiomInstCo :: CoAxiom Branched -> BranchIndex -> [Coercion] -> Coercion
835 mkAxiomInstCo ax index args
836 = ASSERT( args `lengthIs` coAxiomArity ax index )
837 AxiomInstCo ax index args
838
839 -- to be used only with unbranched axioms
840 mkUnbranchedAxInstCo :: Role -> CoAxiom Unbranched
841 -> [Type] -> [Coercion] -> Coercion
842 mkUnbranchedAxInstCo role ax tys cos
843 = mkAxInstCo role ax 0 tys cos
844
845 mkAxInstRHS :: CoAxiom br -> BranchIndex -> [Type] -> [Coercion] -> Type
846 -- Instantiate the axiom with specified types,
847 -- returning the instantiated RHS
848 -- A companion to mkAxInstCo:
849 -- mkAxInstRhs ax index tys = snd (coercionKind (mkAxInstCo ax index tys))
850 mkAxInstRHS ax index tys cos
851 = ASSERT( tvs `equalLength` tys1 )
852 mkAppTys rhs' tys2
853 where
854 branch = coAxiomNthBranch ax index
855 tvs = coAxBranchTyVars branch
856 cvs = coAxBranchCoVars branch
857 (tys1, tys2) = splitAtList tvs tys
858 rhs' = substTyWith tvs tys1 $
859 substTyWithCoVars cvs cos $
860 coAxBranchRHS branch
861
862 mkUnbranchedAxInstRHS :: CoAxiom Unbranched -> [Type] -> [Coercion] -> Type
863 mkUnbranchedAxInstRHS ax = mkAxInstRHS ax 0
864
865 -- | Return the left-hand type of the axiom, when the axiom is instantiated
866 -- at the types given.
867 mkAxInstLHS :: CoAxiom br -> BranchIndex -> [Type] -> [Coercion] -> Type
868 mkAxInstLHS ax index tys cos
869 = ASSERT( tvs `equalLength` tys1 )
870 mkTyConApp fam_tc (lhs_tys `chkAppend` tys2)
871 where
872 branch = coAxiomNthBranch ax index
873 tvs = coAxBranchTyVars branch
874 cvs = coAxBranchCoVars branch
875 (tys1, tys2) = splitAtList tvs tys
876 lhs_tys = substTysWith tvs tys1 $
877 substTysWithCoVars cvs cos $
878 coAxBranchLHS branch
879 fam_tc = coAxiomTyCon ax
880
881 -- | Instantiate the left-hand side of an unbranched axiom
882 mkUnbranchedAxInstLHS :: CoAxiom Unbranched -> [Type] -> [Coercion] -> Type
883 mkUnbranchedAxInstLHS ax = mkAxInstLHS ax 0
884
885 -- | Manufacture an unsafe coercion from thin air.
886 -- Currently (May 14) this is used only to implement the
887 -- @unsafeCoerce#@ primitive. Optimise by pushing
888 -- down through type constructors.
889 mkUnsafeCo :: Role -> Type -> Type -> Coercion
890 mkUnsafeCo role ty1 ty2
891 = mkUnivCo UnsafeCoerceProv role ty1 ty2
892
893 -- | Make a coercion from a coercion hole
894 mkHoleCo :: CoercionHole -> Coercion
895 mkHoleCo h = HoleCo h
896
897 -- | Make a universal coercion between two arbitrary types.
898 mkUnivCo :: UnivCoProvenance
899 -> Role -- ^ role of the built coercion, "r"
900 -> Type -- ^ t1 :: k1
901 -> Type -- ^ t2 :: k2
902 -> Coercion -- ^ :: t1 ~r t2
903 mkUnivCo prov role ty1 ty2
904 | ty1 `eqType` ty2 = mkReflCo role ty1
905 | otherwise = UnivCo prov role ty1 ty2
906
907 -- | Create a symmetric version of the given 'Coercion' that asserts
908 -- equality between the same types but in the other "direction", so
909 -- a kind of @t1 ~ t2@ becomes the kind @t2 ~ t1@.
910 mkSymCo :: Coercion -> Coercion
911
912 -- Do a few simple optimizations, but don't bother pushing occurrences
913 -- of symmetry to the leaves; the optimizer will take care of that.
914 mkSymCo co | isReflCo co = co
915 mkSymCo (SymCo co) = co
916 mkSymCo (SubCo (SymCo co)) = SubCo co
917 mkSymCo co = SymCo co
918
919 -- | Create a new 'Coercion' by composing the two given 'Coercion's transitively.
920 -- (co1 ; co2)
921 mkTransCo :: Coercion -> Coercion -> Coercion
922 mkTransCo co1 co2 | isReflCo co1 = co2
923 | isReflCo co2 = co1
924 mkTransCo (GRefl r t1 (MCo co1)) (GRefl _ _ (MCo co2))
925 = GRefl r t1 (MCo $ mkTransCo co1 co2)
926 mkTransCo co1 co2 = TransCo co1 co2
927
928 mkNthCo :: HasDebugCallStack
929 => Role -- the role of the coercion you're creating
930 -> Int
931 -> Coercion
932 -> Coercion
933 mkNthCo r n co
934 = ASSERT2( good_call, bad_call_msg )
935 go r n co
936 where
937 Pair ty1 ty2 = coercionKind co
938
939 go r 0 co
940 | Just (ty, _) <- isReflCo_maybe co
941 , Just (tv, _) <- splitForAllTy_maybe ty
942 = -- works for both tyvar and covar
943 ASSERT( r == Nominal )
944 mkNomReflCo (varType tv)
945
946 go r n co
947 | Just (ty, r0) <- isReflCo_maybe co
948 , let tc = tyConAppTyCon ty
949 = ASSERT2( ok_tc_app ty n, ppr n $$ ppr ty )
950 ASSERT( nthRole r0 tc n == r )
951 mkReflCo r (tyConAppArgN n ty)
952 where ok_tc_app :: Type -> Int -> Bool
953 ok_tc_app ty n
954 | Just (_, tys) <- splitTyConApp_maybe ty
955 = tys `lengthExceeds` n
956 | isForAllTy ty -- nth:0 pulls out a kind coercion from a hetero forall
957 = n == 0
958 | otherwise
959 = False
960
961 go r 0 (ForAllCo _ kind_co _)
962 = ASSERT( r == Nominal )
963 kind_co
964 -- If co :: (forall a1:k1. t1) ~ (forall a2:k2. t2)
965 -- then (nth 0 co :: k1 ~N k2)
966 -- If co :: (forall a1:t1 ~ t2. t1) ~ (forall a2:t3 ~ t4. t2)
967 -- then (nth 0 co :: (t1 ~ t2) ~N (t3 ~ t4))
968
969 go r n co@(FunCo r0 arg res)
970 -- See Note [Function coercions]
971 -- If FunCo _ arg_co res_co :: (s1:TYPE sk1 -> s2:TYPE sk2)
972 -- ~ (t1:TYPE tk1 -> t2:TYPE tk2)
973 -- Then we want to behave as if co was
974 -- TyConAppCo argk_co resk_co arg_co res_co
975 -- where
976 -- argk_co :: sk1 ~ tk1 = mkNthCo 0 (mkKindCo arg_co)
977 -- resk_co :: sk2 ~ tk2 = mkNthCo 0 (mkKindCo res_co)
978 -- i.e. mkRuntimeRepCo
979 = case n of
980 0 -> ASSERT( r == Nominal ) mkRuntimeRepCo arg
981 1 -> ASSERT( r == Nominal ) mkRuntimeRepCo res
982 2 -> ASSERT( r == r0 ) arg
983 3 -> ASSERT( r == r0 ) res
984 _ -> pprPanic "mkNthCo(FunCo)" (ppr n $$ ppr co)
985
986 go r n (TyConAppCo r0 tc arg_cos) = ASSERT2( r == nthRole r0 tc n
987 , (vcat [ ppr tc
988 , ppr arg_cos
989 , ppr r0
990 , ppr n
991 , ppr r ]) )
992 arg_cos `getNth` n
993
994 go r n co =
995 NthCo r n co
996
997 -- Assertion checking
998 bad_call_msg = vcat [ text "Coercion =" <+> ppr co
999 , text "LHS ty =" <+> ppr ty1
1000 , text "RHS ty =" <+> ppr ty2
1001 , text "n =" <+> ppr n, text "r =" <+> ppr r
1002 , text "coercion role =" <+> ppr (coercionRole co) ]
1003 good_call
1004 -- If the Coercion passed in is between forall-types, then the Int must
1005 -- be 0 and the role must be Nominal.
1006 | Just (_tv1, _) <- splitForAllTy_maybe ty1
1007 , Just (_tv2, _) <- splitForAllTy_maybe ty2
1008 = n == 0 && r == Nominal
1009
1010 -- If the Coercion passed in is between T tys and T tys', then the Int
1011 -- must be less than the length of tys/tys' (which must be the same
1012 -- lengths).
1013 --
1014 -- If the role of the Coercion is nominal, then the role passed in must
1015 -- be nominal. If the role of the Coercion is representational, then the
1016 -- role passed in must be tyConRolesRepresentational T !! n. If the role
1017 -- of the Coercion is Phantom, then the role passed in must be Phantom.
1018 --
1019 -- See also Note [NthCo Cached Roles] if you're wondering why it's
1020 -- blaringly obvious that we should be *computing* this role instead of
1021 -- passing it in.
1022 | Just (tc1, tys1) <- splitTyConApp_maybe ty1
1023 , Just (tc2, tys2) <- splitTyConApp_maybe ty2
1024 , tc1 == tc2
1025 = let len1 = length tys1
1026 len2 = length tys2
1027 good_role = case coercionRole co of
1028 Nominal -> r == Nominal
1029 Representational -> r == (tyConRolesRepresentational tc1 !! n)
1030 Phantom -> r == Phantom
1031 in len1 == len2 && n < len1 && good_role
1032
1033 | otherwise
1034 = True
1035
1036
1037
1038 -- | If you're about to call @mkNthCo r n co@, then @r@ should be
1039 -- whatever @nthCoRole n co@ returns.
1040 nthCoRole :: Int -> Coercion -> Role
1041 nthCoRole n co
1042 | Just (tc, _) <- splitTyConApp_maybe lty
1043 = nthRole r tc n
1044
1045 | Just _ <- splitForAllTy_maybe lty
1046 = Nominal
1047
1048 | otherwise
1049 = pprPanic "nthCoRole" (ppr co)
1050
1051 where
1052 (Pair lty _, r) = coercionKindRole co
1053
1054 mkLRCo :: LeftOrRight -> Coercion -> Coercion
1055 mkLRCo lr co
1056 | Just (ty, eq) <- isReflCo_maybe co
1057 = mkReflCo eq (pickLR lr (splitAppTy ty))
1058 | otherwise
1059 = LRCo lr co
1060
1061 -- | Instantiates a 'Coercion'.
1062 mkInstCo :: Coercion -> Coercion -> Coercion
1063 mkInstCo (ForAllCo tcv _kind_co body_co) co
1064 | Just (arg, _) <- isReflCo_maybe co
1065 -- works for both tyvar and covar
1066 = substCoUnchecked (zipTCvSubst [tcv] [arg]) body_co
1067 mkInstCo co arg = InstCo co arg
1068
1069 -- | Given @ty :: k1@, @co :: k1 ~ k2@,
1070 -- produces @co' :: ty ~r (ty |> co)@
1071 mkGReflRightCo :: Role -> Type -> CoercionN -> Coercion
1072 mkGReflRightCo r ty co
1073 | isGReflCo co = mkReflCo r ty
1074 -- the kinds of @k1@ and @k2@ are the same, thus @isGReflCo@
1075 -- instead of @isReflCo@
1076 | otherwise = GRefl r ty (MCo co)
1077
1078 -- | Given @ty :: k1@, @co :: k1 ~ k2@,
1079 -- produces @co' :: (ty |> co) ~r ty@
1080 mkGReflLeftCo :: Role -> Type -> CoercionN -> Coercion
1081 mkGReflLeftCo r ty co
1082 | isGReflCo co = mkReflCo r ty
1083 -- the kinds of @k1@ and @k2@ are the same, thus @isGReflCo@
1084 -- instead of @isReflCo@
1085 | otherwise = mkSymCo $ GRefl r ty (MCo co)
1086
1087 -- | Given @ty :: k1@, @co :: k1 ~ k2@, @co2:: ty ~ ty'@,
1088 -- produces @co' :: (ty |> co) ~r ty'
1089 -- It is not only a utility function, but it saves allocation when co
1090 -- is a GRefl coercion.
1091 mkCoherenceLeftCo :: Role -> Type -> CoercionN -> Coercion -> Coercion
1092 mkCoherenceLeftCo r ty co co2
1093 | isGReflCo co = co2
1094 | otherwise = (mkSymCo $ GRefl r ty (MCo co)) `mkTransCo` co2
1095
1096 -- | Given @ty :: k1@, @co :: k1 ~ k2@, @co2:: ty' ~ ty@,
1097 -- produces @co' :: ty' ~r (ty |> co)
1098 -- It is not only a utility function, but it saves allocation when co
1099 -- is a GRefl coercion.
1100 mkCoherenceRightCo :: Role -> Type -> CoercionN -> Coercion -> Coercion
1101 mkCoherenceRightCo r ty co co2
1102 | isGReflCo co = co2
1103 | otherwise = co2 `mkTransCo` GRefl r ty (MCo co)
1104
1105 -- | Given @co :: (a :: k) ~ (b :: k')@ produce @co' :: k ~ k'@.
1106 mkKindCo :: Coercion -> Coercion
1107 mkKindCo co | Just (ty, _) <- isReflCo_maybe co = Refl (typeKind ty)
1108 mkKindCo (GRefl _ _ (MCo co)) = co
1109 mkKindCo (UnivCo (PhantomProv h) _ _ _) = h
1110 mkKindCo (UnivCo (ProofIrrelProv h) _ _ _) = h
1111 mkKindCo co
1112 | Pair ty1 ty2 <- coercionKind co
1113 -- generally, calling coercionKind during coercion creation is a bad idea,
1114 -- as it can lead to exponential behavior. But, we don't have nested mkKindCos,
1115 -- so it's OK here.
1116 , let tk1 = typeKind ty1
1117 tk2 = typeKind ty2
1118 , tk1 `eqType` tk2
1119 = Refl tk1
1120 | otherwise
1121 = KindCo co
1122
1123 mkSubCo :: Coercion -> Coercion
1124 -- Input coercion is Nominal, result is Representational
1125 -- see also Note [Role twiddling functions]
1126 mkSubCo (Refl ty) = GRefl Representational ty MRefl
1127 mkSubCo (GRefl Nominal ty co) = GRefl Representational ty co
1128 mkSubCo (TyConAppCo Nominal tc cos)
1129 = TyConAppCo Representational tc (applyRoles tc cos)
1130 mkSubCo (FunCo Nominal arg res)
1131 = FunCo Representational
1132 (downgradeRole Representational Nominal arg)
1133 (downgradeRole Representational Nominal res)
1134 mkSubCo co = ASSERT2( coercionRole co == Nominal, ppr co <+> ppr (coercionRole co) )
1135 SubCo co
1136
1137 -- | Changes a role, but only a downgrade. See Note [Role twiddling functions]
1138 downgradeRole_maybe :: Role -- ^ desired role
1139 -> Role -- ^ current role
1140 -> Coercion -> Maybe Coercion
1141 -- In (downgradeRole_maybe dr cr co) it's a precondition that
1142 -- cr = coercionRole co
1143
1144 downgradeRole_maybe Nominal Nominal co = Just co
1145 downgradeRole_maybe Nominal _ _ = Nothing
1146
1147 downgradeRole_maybe Representational Nominal co = Just (mkSubCo co)
1148 downgradeRole_maybe Representational Representational co = Just co
1149 downgradeRole_maybe Representational Phantom _ = Nothing
1150
1151 downgradeRole_maybe Phantom Phantom co = Just co
1152 downgradeRole_maybe Phantom _ co = Just (toPhantomCo co)
1153
1154 -- | Like 'downgradeRole_maybe', but panics if the change isn't a downgrade.
1155 -- See Note [Role twiddling functions]
1156 downgradeRole :: Role -- desired role
1157 -> Role -- current role
1158 -> Coercion -> Coercion
1159 downgradeRole r1 r2 co
1160 = case downgradeRole_maybe r1 r2 co of
1161 Just co' -> co'
1162 Nothing -> pprPanic "downgradeRole" (ppr co)
1163
1164 -- | If the EqRel is ReprEq, makes a SubCo; otherwise, does nothing.
1165 -- Note that the input coercion should always be nominal.
1166 maybeSubCo :: EqRel -> Coercion -> Coercion
1167 maybeSubCo NomEq = id
1168 maybeSubCo ReprEq = mkSubCo
1169
1170
1171 mkAxiomRuleCo :: CoAxiomRule -> [Coercion] -> Coercion
1172 mkAxiomRuleCo = AxiomRuleCo
1173
1174 -- | Make a "coercion between coercions".
1175 mkProofIrrelCo :: Role -- ^ role of the created coercion, "r"
1176 -> Coercion -- ^ :: phi1 ~N phi2
1177 -> Coercion -- ^ g1 :: phi1
1178 -> Coercion -- ^ g2 :: phi2
1179 -> Coercion -- ^ :: g1 ~r g2
1180
1181 -- if the two coercion prove the same fact, I just don't care what
1182 -- the individual coercions are.
1183 mkProofIrrelCo r co g _ | isGReflCo co = mkReflCo r (mkCoercionTy g)
1184 -- kco is a kind coercion, thus @isGReflCo@ rather than @isReflCo@
1185 mkProofIrrelCo r kco g1 g2 = mkUnivCo (ProofIrrelProv kco) r
1186 (mkCoercionTy g1) (mkCoercionTy g2)
1187
1188 {-
1189 %************************************************************************
1190 %* *
1191 Roles
1192 %* *
1193 %************************************************************************
1194 -}
1195
1196 -- | Converts a coercion to be nominal, if possible.
1197 -- See Note [Role twiddling functions]
1198 setNominalRole_maybe :: Role -- of input coercion
1199 -> Coercion -> Maybe Coercion
1200 setNominalRole_maybe r co
1201 | r == Nominal = Just co
1202 | otherwise = setNominalRole_maybe_helper co
1203 where
1204 setNominalRole_maybe_helper (SubCo co) = Just co
1205 setNominalRole_maybe_helper co@(Refl _) = Just co
1206 setNominalRole_maybe_helper (GRefl _ ty co) = Just $ GRefl Nominal ty co
1207 setNominalRole_maybe_helper (TyConAppCo Representational tc cos)
1208 = do { cos' <- zipWithM setNominalRole_maybe (tyConRolesX Representational tc) cos
1209 ; return $ TyConAppCo Nominal tc cos' }
1210 setNominalRole_maybe_helper (FunCo Representational co1 co2)
1211 = do { co1' <- setNominalRole_maybe Representational co1
1212 ; co2' <- setNominalRole_maybe Representational co2
1213 ; return $ FunCo Nominal co1' co2'
1214 }
1215 setNominalRole_maybe_helper (SymCo co)
1216 = SymCo <$> setNominalRole_maybe_helper co
1217 setNominalRole_maybe_helper (TransCo co1 co2)
1218 = TransCo <$> setNominalRole_maybe_helper co1 <*> setNominalRole_maybe_helper co2
1219 setNominalRole_maybe_helper (AppCo co1 co2)
1220 = AppCo <$> setNominalRole_maybe_helper co1 <*> pure co2
1221 setNominalRole_maybe_helper (ForAllCo tv kind_co co)
1222 = ForAllCo tv kind_co <$> setNominalRole_maybe_helper co
1223 setNominalRole_maybe_helper (NthCo _r n co)
1224 -- NB, this case recurses via setNominalRole_maybe, not
1225 -- setNominalRole_maybe_helper!
1226 = NthCo Nominal n <$> setNominalRole_maybe (coercionRole co) co
1227 setNominalRole_maybe_helper (InstCo co arg)
1228 = InstCo <$> setNominalRole_maybe_helper co <*> pure arg
1229 setNominalRole_maybe_helper (UnivCo prov _ co1 co2)
1230 | case prov of UnsafeCoerceProv -> True -- it's always unsafe
1231 PhantomProv _ -> False -- should always be phantom
1232 ProofIrrelProv _ -> True -- it's always safe
1233 PluginProv _ -> False -- who knows? This choice is conservative.
1234 = Just $ UnivCo prov Nominal co1 co2
1235 setNominalRole_maybe_helper _ = Nothing
1236
1237 -- | Make a phantom coercion between two types. The coercion passed
1238 -- in must be a nominal coercion between the kinds of the
1239 -- types.
1240 mkPhantomCo :: Coercion -> Type -> Type -> Coercion
1241 mkPhantomCo h t1 t2
1242 = mkUnivCo (PhantomProv h) Phantom t1 t2
1243
1244 -- takes any coercion and turns it into a Phantom coercion
1245 toPhantomCo :: Coercion -> Coercion
1246 toPhantomCo co
1247 = mkPhantomCo (mkKindCo co) ty1 ty2
1248 where Pair ty1 ty2 = coercionKind co
1249
1250 -- Convert args to a TyConAppCo Nominal to the same TyConAppCo Representational
1251 applyRoles :: TyCon -> [Coercion] -> [Coercion]
1252 applyRoles tc cos
1253 = zipWith (\r -> downgradeRole r Nominal) (tyConRolesRepresentational tc) cos
1254
1255 -- the Role parameter is the Role of the TyConAppCo
1256 -- defined here because this is intimately concerned with the implementation
1257 -- of TyConAppCo
1258 tyConRolesX :: Role -> TyCon -> [Role]
1259 tyConRolesX Representational tc = tyConRolesRepresentational tc
1260 tyConRolesX role _ = repeat role
1261
1262 tyConRolesRepresentational :: TyCon -> [Role]
1263 tyConRolesRepresentational tc = tyConRoles tc ++ repeat Nominal
1264
1265 nthRole :: Role -> TyCon -> Int -> Role
1266 nthRole Nominal _ _ = Nominal
1267 nthRole Phantom _ _ = Phantom
1268 nthRole Representational tc n
1269 = (tyConRolesRepresentational tc) `getNth` n
1270
1271 ltRole :: Role -> Role -> Bool
1272 -- Is one role "less" than another?
1273 -- Nominal < Representational < Phantom
1274 ltRole Phantom _ = False
1275 ltRole Representational Phantom = True
1276 ltRole Representational _ = False
1277 ltRole Nominal Nominal = False
1278 ltRole Nominal _ = True
1279
1280 -------------------------------
1281
1282 -- | like mkKindCo, but aggressively & recursively optimizes to avoid using
1283 -- a KindCo constructor. The output role is nominal.
1284 promoteCoercion :: Coercion -> CoercionN
1285
1286 -- First cases handles anything that should yield refl.
1287 promoteCoercion co = case co of
1288
1289 _ | ki1 `eqType` ki2
1290 -> mkNomReflCo (typeKind ty1)
1291 -- no later branch should return refl
1292 -- The ASSERT( False )s throughout
1293 -- are these cases explicitly, but they should never fire.
1294
1295 Refl _ -> ASSERT( False )
1296 mkNomReflCo ki1
1297
1298 GRefl _ _ MRefl -> ASSERT( False )
1299 mkNomReflCo ki1
1300
1301 GRefl _ _ (MCo co) -> co
1302
1303 TyConAppCo _ tc args
1304 | Just co' <- instCoercions (mkNomReflCo (tyConKind tc)) args
1305 -> co'
1306 | otherwise
1307 -> mkKindCo co
1308
1309 AppCo co1 arg
1310 | Just co' <- instCoercion (coercionKind (mkKindCo co1))
1311 (promoteCoercion co1) arg
1312 -> co'
1313 | otherwise
1314 -> mkKindCo co
1315
1316 ForAllCo tv _ g
1317 | isTyVar tv
1318 -> promoteCoercion g
1319
1320 ForAllCo _ _ _
1321 -> ASSERT( False )
1322 mkNomReflCo liftedTypeKind
1323 -- See Note [Weird typing rule for ForAllTy] in Type
1324
1325 FunCo _ _ _
1326 -> ASSERT( False )
1327 mkNomReflCo liftedTypeKind
1328
1329 CoVarCo {} -> mkKindCo co
1330 HoleCo {} -> mkKindCo co
1331 AxiomInstCo {} -> mkKindCo co
1332 AxiomRuleCo {} -> mkKindCo co
1333
1334 UnivCo UnsafeCoerceProv _ t1 t2 -> mkUnsafeCo Nominal (typeKind t1) (typeKind t2)
1335 UnivCo (PhantomProv kco) _ _ _ -> kco
1336 UnivCo (ProofIrrelProv kco) _ _ _ -> kco
1337 UnivCo (PluginProv _) _ _ _ -> mkKindCo co
1338
1339 SymCo g
1340 -> mkSymCo (promoteCoercion g)
1341
1342 TransCo co1 co2
1343 -> mkTransCo (promoteCoercion co1) (promoteCoercion co2)
1344
1345 NthCo _ n co1
1346 | Just (_, args) <- splitTyConAppCo_maybe co1
1347 , args `lengthExceeds` n
1348 -> promoteCoercion (args !! n)
1349
1350 | Just _ <- splitForAllCo_maybe co
1351 , n == 0
1352 -> ASSERT( False ) mkNomReflCo liftedTypeKind
1353
1354 | otherwise
1355 -> mkKindCo co
1356
1357 LRCo lr co1
1358 | Just (lco, rco) <- splitAppCo_maybe co1
1359 -> case lr of
1360 CLeft -> promoteCoercion lco
1361 CRight -> promoteCoercion rco
1362
1363 | otherwise
1364 -> mkKindCo co
1365
1366 InstCo g _
1367 | isForAllTy_ty ty1
1368 -> ASSERT( isForAllTy_ty ty2 )
1369 promoteCoercion g
1370 | otherwise
1371 -> ASSERT( False)
1372 mkNomReflCo liftedTypeKind
1373 -- See Note [Weird typing rule for ForAllTy] in Type
1374
1375 KindCo _
1376 -> ASSERT( False )
1377 mkNomReflCo liftedTypeKind
1378
1379 SubCo g
1380 -> promoteCoercion g
1381
1382 where
1383 Pair ty1 ty2 = coercionKind co
1384 ki1 = typeKind ty1
1385 ki2 = typeKind ty2
1386
1387 -- | say @g = promoteCoercion h@. Then, @instCoercion g w@ yields @Just g'@,
1388 -- where @g' = promoteCoercion (h w)@.
1389 -- fails if this is not possible, if @g@ coerces between a forall and an ->
1390 -- or if second parameter has a representational role and can't be used
1391 -- with an InstCo.
1392 instCoercion :: Pair Type -- g :: lty ~ rty
1393 -> CoercionN -- ^ must be nominal
1394 -> Coercion
1395 -> Maybe CoercionN
1396 instCoercion (Pair lty rty) g w
1397 | (isForAllTy_ty lty && isForAllTy_ty rty)
1398 || (isForAllTy_co lty && isForAllTy_co rty)
1399 , Just w' <- setNominalRole_maybe (coercionRole w) w
1400 -- g :: (forall t1. t2) ~ (forall t1. t3)
1401 -- w :: s1 ~ s2
1402 -- returns mkInstCo g w' :: t2 [t1 |-> s1 ] ~ t3 [t1 |-> s2]
1403 = Just $ mkInstCo g w'
1404 | isFunTy lty && isFunTy rty
1405 -- g :: (t1 -> t2) ~ (t3 -> t4)
1406 -- returns t2 ~ t4
1407 = Just $ mkNthCo Nominal 3 g -- extract result type, which is the 4th argument to (->)
1408 | otherwise -- one forall, one funty...
1409 = Nothing
1410
1411 -- | Repeated use of 'instCoercion'
1412 instCoercions :: CoercionN -> [Coercion] -> Maybe CoercionN
1413 instCoercions g ws
1414 = let arg_ty_pairs = map coercionKind ws in
1415 snd <$> foldM go (coercionKind g, g) (zip arg_ty_pairs ws)
1416 where
1417 go :: (Pair Type, Coercion) -> (Pair Type, Coercion)
1418 -> Maybe (Pair Type, Coercion)
1419 go (g_tys, g) (w_tys, w)
1420 = do { g' <- instCoercion g_tys g w
1421 ; return (piResultTy <$> g_tys <*> w_tys, g') }
1422
1423 -- | Creates a new coercion with both of its types casted by different casts
1424 -- @castCoercionKind g r t1 t2 h1 h2@, where @g :: t1 ~r t2@,
1425 -- has type @(t1 |> h1) ~r (t2 |> h2)@.
1426 -- @h1@ and @h2@ must be nominal.
1427 castCoercionKind :: Coercion -> Role -> Type -> Type
1428 -> CoercionN -> CoercionN -> Coercion
1429 castCoercionKind g r t1 t2 h1 h2
1430 = mkCoherenceRightCo r t2 h2 (mkCoherenceLeftCo r t1 h1 g)
1431
1432 -- | Creates a new coercion with both of its types casted by different casts
1433 -- @castCoercionKind g h1 h2@, where @g :: t1 ~r t2@,
1434 -- has type @(t1 |> h1) ~r (t2 |> h2)@.
1435 -- @h1@ and @h2@ must be nominal.
1436 -- It calls @coercionKindRole@, so it's quite inefficient (which 'I' stands for)
1437 -- Use @castCoercionKind@ instead if @t1@, @t2@, and @r@ are known beforehand.
1438 castCoercionKindI :: Coercion -> CoercionN -> CoercionN -> Coercion
1439 castCoercionKindI g h1 h2
1440 = mkCoherenceRightCo r t2 h2 (mkCoherenceLeftCo r t1 h1 g)
1441 where (Pair t1 t2, r) = coercionKindRole g
1442
1443 -- See note [Newtype coercions] in TyCon
1444
1445 mkPiCos :: Role -> [Var] -> Coercion -> Coercion
1446 mkPiCos r vs co = foldr (mkPiCo r) co vs
1447
1448 -- | Make a forall 'Coercion', where both types related by the coercion
1449 -- are quantified over the same variable.
1450 mkPiCo :: Role -> Var -> Coercion -> Coercion
1451 mkPiCo r v co | isTyVar v = mkHomoForAllCos [v] co
1452 | isCoVar v = ASSERT( not (v `elemVarSet` tyCoVarsOfCo co) )
1453 -- We didn't call mkForAllCo here because if v does not appear
1454 -- in co, the argement coercion will be nominal. But here we
1455 -- want it to be r. It is only called in 'mkPiCos', which is
1456 -- only used in SimplUtils, where we are sure for
1457 -- now (Aug 2018) v won't occur in co.
1458 mkFunCo r (mkReflCo r (varType v)) co
1459 | otherwise = mkFunCo r (mkReflCo r (varType v)) co
1460
1461 -- mkCoCast (c :: s1 ~?r t1) (g :: (s1 ~?r t1) ~#R (s2 ~?r t2)) :: s2 ~?r t2
1462 -- The first coercion might be lifted or unlifted; thus the ~? above
1463 -- Lifted and unlifted equalities take different numbers of arguments,
1464 -- so we have to make sure to supply the right parameter to decomposeCo.
1465 -- Also, note that the role of the first coercion is the same as the role of
1466 -- the equalities related by the second coercion. The second coercion is
1467 -- itself always representational.
1468 mkCoCast :: Coercion -> CoercionR -> Coercion
1469 mkCoCast c g
1470 | (g2:g1:_) <- reverse co_list
1471 = mkSymCo g1 `mkTransCo` c `mkTransCo` g2
1472
1473 | otherwise
1474 = pprPanic "mkCoCast" (ppr g $$ ppr (coercionKind g))
1475 where
1476 -- g :: (s1 ~# t1) ~# (s2 ~# t2)
1477 -- g1 :: s1 ~# s2
1478 -- g2 :: t1 ~# t2
1479 (tc, _) = splitTyConApp (pFst $ coercionKind g)
1480 co_list = decomposeCo (tyConArity tc) g (tyConRolesRepresentational tc)
1481
1482 {-
1483 %************************************************************************
1484 %* *
1485 Newtypes
1486 %* *
1487 %************************************************************************
1488 -}
1489
1490 -- | If @co :: T ts ~ rep_ty@ then:
1491 --
1492 -- > instNewTyCon_maybe T ts = Just (rep_ty, co)
1493 --
1494 -- Checks for a newtype, and for being saturated
1495 instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, Coercion)
1496 instNewTyCon_maybe tc tys
1497 | Just (tvs, ty, co_tc) <- unwrapNewTyConEtad_maybe tc -- Check for newtype
1498 , tvs `leLength` tys -- Check saturated enough
1499 = Just (applyTysX tvs ty tys, mkUnbranchedAxInstCo Representational co_tc tys [])
1500 | otherwise
1501 = Nothing
1502
1503 {-
1504 ************************************************************************
1505 * *
1506 Type normalisation
1507 * *
1508 ************************************************************************
1509 -}
1510
1511 -- | A function to check if we can reduce a type by one step. Used
1512 -- with 'topNormaliseTypeX'.
1513 type NormaliseStepper ev = RecTcChecker
1514 -> TyCon -- tc
1515 -> [Type] -- tys
1516 -> NormaliseStepResult ev
1517
1518 -- | The result of stepping in a normalisation function.
1519 -- See 'topNormaliseTypeX'.
1520 data NormaliseStepResult ev
1521 = NS_Done -- ^ Nothing more to do
1522 | NS_Abort -- ^ Utter failure. The outer function should fail too.
1523 | NS_Step RecTcChecker Type ev -- ^ We stepped, yielding new bits;
1524 -- ^ ev is evidence;
1525 -- Usually a co :: old type ~ new type
1526
1527 mapStepResult :: (ev1 -> ev2)
1528 -> NormaliseStepResult ev1 -> NormaliseStepResult ev2
1529 mapStepResult f (NS_Step rec_nts ty ev) = NS_Step rec_nts ty (f ev)
1530 mapStepResult _ NS_Done = NS_Done
1531 mapStepResult _ NS_Abort = NS_Abort
1532
1533 -- | Try one stepper and then try the next, if the first doesn't make
1534 -- progress.
1535 -- So if it returns NS_Done, it means that both steppers are satisfied
1536 composeSteppers :: NormaliseStepper ev -> NormaliseStepper ev
1537 -> NormaliseStepper ev
1538 composeSteppers step1 step2 rec_nts tc tys
1539 = case step1 rec_nts tc tys of
1540 success@(NS_Step {}) -> success
1541 NS_Done -> step2 rec_nts tc tys
1542 NS_Abort -> NS_Abort
1543
1544 -- | A 'NormaliseStepper' that unwraps newtypes, careful not to fall into
1545 -- a loop. If it would fall into a loop, it produces 'NS_Abort'.
1546 unwrapNewTypeStepper :: NormaliseStepper Coercion
1547 unwrapNewTypeStepper rec_nts tc tys
1548 | Just (ty', co) <- instNewTyCon_maybe tc tys
1549 = case checkRecTc rec_nts tc of
1550 Just rec_nts' -> NS_Step rec_nts' ty' co
1551 Nothing -> NS_Abort
1552
1553 | otherwise
1554 = NS_Done
1555
1556 -- | A general function for normalising the top-level of a type. It continues
1557 -- to use the provided 'NormaliseStepper' until that function fails, and then
1558 -- this function returns. The roles of the coercions produced by the
1559 -- 'NormaliseStepper' must all be the same, which is the role returned from
1560 -- the call to 'topNormaliseTypeX'.
1561 --
1562 -- Typically ev is Coercion.
1563 --
1564 -- If topNormaliseTypeX step plus ty = Just (ev, ty')
1565 -- then ty ~ev1~ t1 ~ev2~ t2 ... ~evn~ ty'
1566 -- and ev = ev1 `plus` ev2 `plus` ... `plus` evn
1567 -- If it returns Nothing then no newtype unwrapping could happen
1568 topNormaliseTypeX :: NormaliseStepper ev -> (ev -> ev -> ev)
1569 -> Type -> Maybe (ev, Type)
1570 topNormaliseTypeX stepper plus ty
1571 | Just (tc, tys) <- splitTyConApp_maybe ty
1572 , NS_Step rec_nts ty' ev <- stepper initRecTc tc tys
1573 = go rec_nts ev ty'
1574 | otherwise
1575 = Nothing
1576 where
1577 go rec_nts ev ty
1578 | Just (tc, tys) <- splitTyConApp_maybe ty
1579 = case stepper rec_nts tc tys of
1580 NS_Step rec_nts' ty' ev' -> go rec_nts' (ev `plus` ev') ty'
1581 NS_Done -> Just (ev, ty)
1582 NS_Abort -> Nothing
1583
1584 | otherwise
1585 = Just (ev, ty)
1586
1587 topNormaliseNewType_maybe :: Type -> Maybe (Coercion, Type)
1588 -- ^ Sometimes we want to look through a @newtype@ and get its associated coercion.
1589 -- This function strips off @newtype@ layers enough to reveal something that isn't
1590 -- a @newtype@. Specifically, here's the invariant:
1591 --
1592 -- > topNormaliseNewType_maybe rec_nts ty = Just (co, ty')
1593 --
1594 -- then (a) @co : ty0 ~ ty'@.
1595 -- (b) ty' is not a newtype.
1596 --
1597 -- The function returns @Nothing@ for non-@newtypes@,
1598 -- or unsaturated applications
1599 --
1600 -- This function does *not* look through type families, because it has no access to
1601 -- the type family environment. If you do have that at hand, consider to use
1602 -- topNormaliseType_maybe, which should be a drop-in replacement for
1603 -- topNormaliseNewType_maybe
1604 -- If topNormliseNewType_maybe ty = Just (co, ty'), then co : ty ~R ty'
1605 topNormaliseNewType_maybe ty
1606 = topNormaliseTypeX unwrapNewTypeStepper mkTransCo ty
1607
1608 {-
1609 %************************************************************************
1610 %* *
1611 Comparison of coercions
1612 %* *
1613 %************************************************************************
1614 -}
1615
1616 -- | Syntactic equality of coercions
1617 eqCoercion :: Coercion -> Coercion -> Bool
1618 eqCoercion = eqType `on` coercionType
1619
1620 -- | Compare two 'Coercion's, with respect to an RnEnv2
1621 eqCoercionX :: RnEnv2 -> Coercion -> Coercion -> Bool
1622 eqCoercionX env = eqTypeX env `on` coercionType
1623
1624 {-
1625 %************************************************************************
1626 %* *
1627 "Lifting" substitution
1628 [(TyCoVar,Coercion)] -> Type -> Coercion
1629 %* *
1630 %************************************************************************
1631
1632 Note [Lifting coercions over types: liftCoSubst]
1633 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1634 The KPUSH rule deals with this situation
1635 data T a = K (a -> Maybe a)
1636 g :: T t1 ~ T t2
1637 x :: t1 -> Maybe t1
1638
1639 case (K @t1 x) |> g of
1640 K (y:t2 -> Maybe t2) -> rhs
1641
1642 We want to push the coercion inside the constructor application.
1643 So we do this
1644
1645 g' :: t1~t2 = Nth 0 g
1646
1647 case K @t2 (x |> g' -> Maybe g') of
1648 K (y:t2 -> Maybe t2) -> rhs
1649
1650 The crucial operation is that we
1651 * take the type of K's argument: a -> Maybe a
1652 * and substitute g' for a
1653 thus giving *coercion*. This is what liftCoSubst does.
1654
1655 In the presence of kind coercions, this is a bit
1656 of a hairy operation. So, we refer you to the paper introducing kind coercions,
1657 available at www.cis.upenn.edu/~sweirich/papers/fckinds-extended.pdf
1658
1659 Note [extendLiftingContextEx]
1660 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1661 Consider we have datatype
1662 K :: \/k. \/a::k. P -> T k -- P be some type
1663 g :: T k1 ~ T k2
1664
1665 case (K @k1 @t1 x) |> g of
1666 K y -> rhs
1667
1668 We want to push the coercion inside the constructor application.
1669 We first get the coercion mapped by the universal type variable k:
1670 lc = k |-> Nth 0 g :: k1~k2
1671
1672 Here, the important point is that the kind of a is coerced, and P might be
1673 dependent on the existential type variable a.
1674 Thus we first get the coercion of a's kind
1675 g2 = liftCoSubst lc k :: k1 ~ k2
1676
1677 Then we store a new mapping into the lifting context
1678 lc2 = a |-> (t1 ~ t1 |> g2), lc
1679
1680 So later when we can correctly deal with the argument type P
1681 liftCoSubst lc2 P :: P [k|->k1][a|->t1] ~ P[k|->k2][a |-> (t1|>g2)]
1682
1683 This is exactly what extendLiftingContextEx does.
1684 * For each (tyvar:k, ty) pair, we product the mapping
1685 tyvar |-> (ty ~ ty |> (liftCoSubst lc k))
1686 * For each (covar:s1~s2, ty) pair, we produce the mapping
1687 covar |-> (co ~ co')
1688 co' = Sym (liftCoSubst lc s1) ;; covar ;; liftCoSubst lc s2 :: s1'~s2'
1689
1690 This follows the lifting context extension definition in the
1691 "FC with Explicit Kind Equality" paper.
1692 -}
1693
1694 -- ----------------------------------------------------
1695 -- See Note [Lifting coercions over types: liftCoSubst]
1696 -- ----------------------------------------------------
1697
1698 data LiftingContext = LC TCvSubst LiftCoEnv
1699 -- in optCoercion, we need to lift when optimizing InstCo.
1700 -- See Note [Optimising InstCo] in OptCoercion
1701 -- We thus propagate the substitution from OptCoercion here.
1702
1703 instance Outputable LiftingContext where
1704 ppr (LC _ env) = hang (text "LiftingContext:") 2 (ppr env)
1705
1706 type LiftCoEnv = VarEnv Coercion
1707 -- Maps *type variables* to *coercions*.
1708 -- That's the whole point of this function!
1709 -- Also maps coercion variables to ProofIrrelCos.
1710
1711 -- like liftCoSubstWith, but allows for existentially-bound types as well
1712 liftCoSubstWithEx :: Role -- desired role for output coercion
1713 -> [TyVar] -- universally quantified tyvars
1714 -> [Coercion] -- coercions to substitute for those
1715 -> [TyCoVar] -- existentially quantified tycovars
1716 -> [Type] -- types and coercions to be bound to ex vars
1717 -> (Type -> Coercion, [Type]) -- (lifting function, converted ex args)
1718 liftCoSubstWithEx role univs omegas exs rhos
1719 = let theta = mkLiftingContext (zipEqual "liftCoSubstWithExU" univs omegas)
1720 psi = extendLiftingContextEx theta (zipEqual "liftCoSubstWithExX" exs rhos)
1721 in (ty_co_subst psi role, substTys (lcSubstRight psi) (mkTyCoVarTys exs))
1722
1723 liftCoSubstWith :: Role -> [TyCoVar] -> [Coercion] -> Type -> Coercion
1724 liftCoSubstWith r tvs cos ty
1725 = liftCoSubst r (mkLiftingContext $ zipEqual "liftCoSubstWith" tvs cos) ty
1726
1727 -- | @liftCoSubst role lc ty@ produces a coercion (at role @role@)
1728 -- that coerces between @lc_left(ty)@ and @lc_right(ty)@, where
1729 -- @lc_left@ is a substitution mapping type variables to the left-hand
1730 -- types of the mapped coercions in @lc@, and similar for @lc_right@.
1731 liftCoSubst :: HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion
1732 liftCoSubst r lc@(LC subst env) ty
1733 | isEmptyVarEnv env = mkReflCo r (substTy subst ty)
1734 | otherwise = ty_co_subst lc r ty
1735
1736 emptyLiftingContext :: InScopeSet -> LiftingContext
1737 emptyLiftingContext in_scope = LC (mkEmptyTCvSubst in_scope) emptyVarEnv
1738
1739 mkLiftingContext :: [(TyCoVar,Coercion)] -> LiftingContext
1740 mkLiftingContext pairs
1741 = LC (mkEmptyTCvSubst $ mkInScopeSet $ tyCoVarsOfCos (map snd pairs))
1742 (mkVarEnv pairs)
1743
1744 mkSubstLiftingContext :: TCvSubst -> LiftingContext
1745 mkSubstLiftingContext subst = LC subst emptyVarEnv
1746
1747 -- | Extend a lifting context with a new mapping.
1748 extendLiftingContext :: LiftingContext -- ^ original LC
1749 -> TyCoVar -- ^ new variable to map...
1750 -> Coercion -- ^ ...to this lifted version
1751 -> LiftingContext
1752 -- mappings to reflexive coercions are just substitutions
1753 extendLiftingContext (LC subst env) tv arg
1754 | Just (ty, _) <- isReflCo_maybe arg
1755 = LC (extendTCvSubst subst tv ty) env
1756 | otherwise
1757 = LC subst (extendVarEnv env tv arg)
1758
1759 -- | Extend a lifting context with a new mapping, and extend the in-scope set
1760 extendLiftingContextAndInScope :: LiftingContext -- ^ Original LC
1761 -> TyCoVar -- ^ new variable to map...
1762 -> Coercion -- ^ to this coercion
1763 -> LiftingContext
1764 extendLiftingContextAndInScope (LC subst env) tv co
1765 = extendLiftingContext (LC (extendTCvInScopeSet subst (tyCoVarsOfCo co)) env) tv co
1766
1767 -- | Extend a lifting context with existential-variable bindings.
1768 -- See Note [extendLiftingContextEx]
1769 extendLiftingContextEx :: LiftingContext -- ^ original lifting context
1770 -> [(TyCoVar,Type)] -- ^ ex. var / value pairs
1771 -> LiftingContext
1772 -- Note that this is more involved than extendLiftingContext. That function
1773 -- takes a coercion to extend with, so it's assumed that the caller has taken
1774 -- into account any of the kind-changing stuff worried about here.
1775 extendLiftingContextEx lc [] = lc
1776 extendLiftingContextEx lc@(LC subst env) ((v,ty):rest)
1777 -- This function adds bindings for *Nominal* coercions. Why? Because it
1778 -- works with existentially bound variables, which are considered to have
1779 -- nominal roles.
1780 | isTyVar v
1781 = let lc' = LC (subst `extendTCvInScopeSet` tyCoVarsOfType ty)
1782 (extendVarEnv env v $
1783 mkGReflRightCo Nominal
1784 ty
1785 (ty_co_subst lc Nominal (tyVarKind v)))
1786 in extendLiftingContextEx lc' rest
1787 | CoercionTy co <- ty
1788 = -- co :: s1 ~r s2
1789 -- lift_s1 :: s1 ~r s1'
1790 -- lift_s2 :: s2 ~r s2'
1791 -- kco :: (s1 ~r s2) ~N (s1' ~r s2')
1792 ASSERT( isCoVar v )
1793 let (_, _, s1, s2, r) = coVarKindsTypesRole v
1794 lift_s1 = ty_co_subst lc r s1
1795 lift_s2 = ty_co_subst lc r s2
1796 kco = mkTyConAppCo Nominal (equalityTyCon r)
1797 [ mkKindCo lift_s1, mkKindCo lift_s2
1798 , lift_s1 , lift_s2 ]
1799 lc' = LC (subst `extendTCvInScopeSet` tyCoVarsOfCo co)
1800 (extendVarEnv env v
1801 (mkProofIrrelCo Nominal kco co $
1802 (mkSymCo lift_s1) `mkTransCo` co `mkTransCo` lift_s2))
1803 in extendLiftingContextEx lc' rest
1804 | otherwise
1805 = pprPanic "extendLiftingContextEx" (ppr v <+> text "|->" <+> ppr ty)
1806
1807
1808 -- | Erase the environments in a lifting context
1809 zapLiftingContext :: LiftingContext -> LiftingContext
1810 zapLiftingContext (LC subst _) = LC (zapTCvSubst subst) emptyVarEnv
1811
1812 -- | Like 'substForAllCoBndr', but works on a lifting context
1813 substForAllCoBndrUsingLC :: Bool
1814 -> (Coercion -> Coercion)
1815 -> LiftingContext -> TyCoVar -> Coercion
1816 -> (LiftingContext, TyCoVar, Coercion)
1817 substForAllCoBndrUsingLC sym sco (LC subst lc_env) tv co
1818 = (LC subst' lc_env, tv', co')
1819 where
1820 (subst', tv', co') = substForAllCoBndrUsing sym sco subst tv co
1821
1822 -- | The \"lifting\" operation which substitutes coercions for type
1823 -- variables in a type to produce a coercion.
1824 --
1825 -- For the inverse operation, see 'liftCoMatch'
1826 ty_co_subst :: LiftingContext -> Role -> Type -> Coercion
1827 ty_co_subst lc role ty
1828 = go role ty
1829 where
1830 go :: Role -> Type -> Coercion
1831 go r ty | Just ty' <- coreView ty
1832 = go r ty'
1833 go Phantom ty = lift_phantom ty
1834 go r (TyVarTy tv) = expectJust "ty_co_subst bad roles" $
1835 liftCoSubstTyVar lc r tv
1836 go r (AppTy ty1 ty2) = mkAppCo (go r ty1) (go Nominal ty2)
1837 go r (TyConApp tc tys) = mkTyConAppCo r tc (zipWith go (tyConRolesX r tc) tys)
1838 go r (FunTy ty1 ty2) = mkFunCo r (go r ty1) (go r ty2)
1839 go r t@(ForAllTy (Bndr v _) ty)
1840 = let (lc', v', h) = liftCoSubstVarBndr lc v
1841 body_co = ty_co_subst lc' r ty in
1842 if isTyVar v' || almostDevoidCoVarOfCo v' body_co
1843 -- Lifting a ForAllTy over a coercion variable could fail as ForAllCo
1844 -- imposes an extra restriction on where a covar can appear. See last
1845 -- wrinkle in Note [Unused coercion variable in ForAllCo].
1846 -- We specifically check for this and panic because we know that
1847 -- there's a hole in the type system here, and we'd rather panic than
1848 -- fall into it.
1849 then mkForAllCo v' h body_co
1850 else pprPanic "ty_co_subst: covar is not almost devoid" (ppr t)
1851 go r ty@(LitTy {}) = ASSERT( r == Nominal )
1852 mkNomReflCo ty
1853 go r (CastTy ty co) = castCoercionKindI (go r ty) (substLeftCo lc co)
1854 (substRightCo lc co)
1855 go r (CoercionTy co) = mkProofIrrelCo r kco (substLeftCo lc co)
1856 (substRightCo lc co)
1857 where kco = go Nominal (coercionType co)
1858
1859 lift_phantom ty = mkPhantomCo (go Nominal (typeKind ty))
1860 (substTy (lcSubstLeft lc) ty)
1861 (substTy (lcSubstRight lc) ty)
1862
1863 {-
1864 Note [liftCoSubstTyVar]
1865 ~~~~~~~~~~~~~~~~~~~~~~~~~
1866 This function can fail if a coercion in the environment is of too low a role.
1867
1868 liftCoSubstTyVar is called from two places: in liftCoSubst (naturally), and
1869 also in matchAxiom in OptCoercion. From liftCoSubst, the so-called lifting
1870 lemma guarantees that the roles work out. If we fail in this
1871 case, we really should panic -- something is deeply wrong. But, in matchAxiom,
1872 failing is fine. matchAxiom is trying to find a set of coercions
1873 that match, but it may fail, and this is healthy behavior.
1874 -}
1875
1876 -- See Note [liftCoSubstTyVar]
1877 liftCoSubstTyVar :: LiftingContext -> Role -> TyVar -> Maybe Coercion
1878 liftCoSubstTyVar (LC subst env) r v
1879 | Just co_arg <- lookupVarEnv env v
1880 = downgradeRole_maybe r (coercionRole co_arg) co_arg
1881
1882 | otherwise
1883 = Just $ mkReflCo r (substTyVar subst v)
1884
1885 {- Note [liftCoSubstVarBndr]
1886
1887 callback:
1888 We want 'liftCoSubstVarBndrUsing' to be general enough to be reused in
1889 FamInstEnv, therefore the input arg 'fun' returns a pair with polymophic type
1890 in snd.
1891 However in 'liftCoSubstVarBndr', we don't need the snd, so we use unit and
1892 ignore the fourth component of the return value.
1893
1894 liftCoSubstTyVarBndrUsing:
1895 Given
1896 forall tv:k. t
1897 We want to get
1898 forall (tv:k1) (kind_co :: k1 ~ k2) body_co
1899
1900 We lift the kind k to get the kind_co
1901 kind_co = ty_co_subst k :: k1 ~ k2
1902
1903 Now in the LiftingContext, we add the new mapping
1904 tv |-> (tv :: k1) ~ ((tv |> kind_co) :: k2)
1905
1906 liftCoSubstCoVarBndrUsing:
1907 Given
1908 forall cv:(s1 ~ s2). t
1909 We want to get
1910 forall (cv:s1'~s2') (kind_co :: (s1'~s2') ~ (t1 ~ t2)) body_co
1911
1912 We lift s1 and s2 respectively to get
1913 eta1 :: s1' ~ t1
1914 eta2 :: s2' ~ t2
1915 And
1916 kind_co = TyConAppCo Nominal (~#) eta1 eta2
1917
1918 Now in the liftingContext, we add the new mapping
1919 cv |-> (cv :: s1' ~ s2') ~ ((sym eta1;cv;eta2) :: t1 ~ t2)
1920 -}
1921
1922 -- See Note [liftCoSubstVarBndr]
1923 liftCoSubstVarBndr :: LiftingContext -> TyCoVar
1924 -> (LiftingContext, TyCoVar, Coercion)
1925 liftCoSubstVarBndr lc tv
1926 = let (lc', tv', h, _) = liftCoSubstVarBndrUsing callback lc tv in
1927 (lc', tv', h)
1928 where
1929 callback lc' ty' = (ty_co_subst lc' Nominal ty', ())
1930
1931 -- the callback must produce a nominal coercion
1932 liftCoSubstVarBndrUsing :: (LiftingContext -> Type -> (CoercionN, a))
1933 -> LiftingContext -> TyCoVar
1934 -> (LiftingContext, TyCoVar, CoercionN, a)
1935 liftCoSubstVarBndrUsing fun lc old_var
1936 | isTyVar old_var
1937 = liftCoSubstTyVarBndrUsing fun lc old_var
1938 | otherwise
1939 = liftCoSubstCoVarBndrUsing fun lc old_var
1940
1941 -- Works for tyvar binder
1942 liftCoSubstTyVarBndrUsing :: (LiftingContext -> Type -> (CoercionN, a))
1943 -> LiftingContext -> TyVar
1944 -> (LiftingContext, TyVar, CoercionN, a)
1945 liftCoSubstTyVarBndrUsing fun lc@(LC subst cenv) old_var
1946 = ASSERT( isTyVar old_var )
1947 ( LC (subst `extendTCvInScope` new_var) new_cenv
1948 , new_var, eta, stuff )
1949 where
1950 old_kind = tyVarKind old_var
1951 (eta, stuff) = fun lc old_kind
1952 Pair k1 _ = coercionKind eta
1953 new_var = uniqAway (getTCvInScope subst) (setVarType old_var k1)
1954
1955 lifted = mkGReflRightCo Nominal (TyVarTy new_var) eta
1956 -- :: new_var ~ new_var |> eta
1957 new_cenv = extendVarEnv cenv old_var lifted
1958
1959 -- Works for covar binder
1960 liftCoSubstCoVarBndrUsing :: (LiftingContext -> Type -> (CoercionN, a))
1961 -> LiftingContext -> CoVar
1962 -> (LiftingContext, CoVar, CoercionN, a)
1963 liftCoSubstCoVarBndrUsing fun lc@(LC subst cenv) old_var
1964 = ASSERT( isCoVar old_var )
1965 ( LC (subst `extendTCvInScope` new_var) new_cenv
1966 , new_var, kind_co, stuff )
1967 where
1968 old_kind = coVarKind old_var
1969 (eta, stuff) = fun lc old_kind
1970 Pair k1 _ = coercionKind eta
1971 new_var = uniqAway (getTCvInScope subst) (setVarType old_var k1)
1972
1973 -- old_var :: s1 ~r s2
1974 -- eta :: (s1' ~r s2') ~N (t1 ~r t2)
1975 -- eta1 :: s1' ~r t1
1976 -- eta2 :: s2' ~r t2
1977 -- co1 :: s1' ~r s2'
1978 -- co2 :: t1 ~r t2
1979 -- kind_co :: (s1' ~r s2') ~N (t1 ~r t2)
1980 -- lifted :: co1 ~N co2
1981
1982 role = coVarRole old_var
1983 eta' = downgradeRole role Nominal eta
1984 eta1 = mkNthCo role 2 eta'
1985 eta2 = mkNthCo role 3 eta'
1986
1987 co1 = mkCoVarCo new_var
1988 co2 = mkSymCo eta1 `mkTransCo` co1 `mkTransCo` eta2
1989 kind_co = mkTyConAppCo Nominal (equalityTyCon role)
1990 [ mkKindCo co1, mkKindCo co2
1991 , co1 , co2 ]
1992 lifted = mkProofIrrelCo Nominal kind_co co1 co2
1993
1994 new_cenv = extendVarEnv cenv old_var lifted
1995
1996 -- | Is a var in the domain of a lifting context?
1997 isMappedByLC :: TyCoVar -> LiftingContext -> Bool
1998 isMappedByLC tv (LC _ env) = tv `elemVarEnv` env
1999
2000 -- If [a |-> g] is in the substitution and g :: t1 ~ t2, substitute a for t1
2001 -- If [a |-> (g1, g2)] is in the substitution, substitute a for g1
2002 substLeftCo :: LiftingContext -> Coercion -> Coercion
2003 substLeftCo lc co
2004 = substCo (lcSubstLeft lc) co
2005
2006 -- Ditto, but for t2 and g2
2007 substRightCo :: LiftingContext -> Coercion -> Coercion
2008 substRightCo lc co
2009 = substCo (lcSubstRight lc) co
2010
2011 -- | Apply "sym" to all coercions in a 'LiftCoEnv'
2012 swapLiftCoEnv :: LiftCoEnv -> LiftCoEnv
2013 swapLiftCoEnv = mapVarEnv mkSymCo
2014
2015 lcSubstLeft :: LiftingContext -> TCvSubst
2016 lcSubstLeft (LC subst lc_env) = liftEnvSubstLeft subst lc_env
2017
2018 lcSubstRight :: LiftingContext -> TCvSubst
2019 lcSubstRight (LC subst lc_env) = liftEnvSubstRight subst lc_env
2020
2021 liftEnvSubstLeft :: TCvSubst -> LiftCoEnv -> TCvSubst
2022 liftEnvSubstLeft = liftEnvSubst pFst
2023
2024 liftEnvSubstRight :: TCvSubst -> LiftCoEnv -> TCvSubst
2025 liftEnvSubstRight = liftEnvSubst pSnd
2026
2027 liftEnvSubst :: (forall a. Pair a -> a) -> TCvSubst -> LiftCoEnv -> TCvSubst
2028 liftEnvSubst selector subst lc_env
2029 = composeTCvSubst (TCvSubst emptyInScopeSet tenv cenv) subst
2030 where
2031 pairs = nonDetUFMToList lc_env
2032 -- It's OK to use nonDetUFMToList here because we
2033 -- immediately forget the ordering by creating
2034 -- a VarEnv
2035 (tpairs, cpairs) = partitionWith ty_or_co pairs
2036 tenv = mkVarEnv_Directly tpairs
2037 cenv = mkVarEnv_Directly cpairs
2038
2039 ty_or_co :: (Unique, Coercion) -> Either (Unique, Type) (Unique, Coercion)
2040 ty_or_co (u, co)
2041 | Just equality_co <- isCoercionTy_maybe equality_ty
2042 = Right (u, equality_co)
2043 | otherwise
2044 = Left (u, equality_ty)
2045 where
2046 equality_ty = selector (coercionKind co)
2047
2048 -- | Extract the underlying substitution from the LiftingContext
2049 lcTCvSubst :: LiftingContext -> TCvSubst
2050 lcTCvSubst (LC subst _) = subst
2051
2052 -- | Get the 'InScopeSet' from a 'LiftingContext'
2053 lcInScopeSet :: LiftingContext -> InScopeSet
2054 lcInScopeSet (LC subst _) = getTCvInScope subst
2055
2056 {-
2057 %************************************************************************
2058 %* *
2059 Sequencing on coercions
2060 %* *
2061 %************************************************************************
2062 -}
2063
2064 seqMCo :: MCoercion -> ()
2065 seqMCo MRefl = ()
2066 seqMCo (MCo co) = seqCo co
2067
2068 seqCo :: Coercion -> ()
2069 seqCo (Refl ty) = seqType ty
2070 seqCo (GRefl r ty mco) = r `seq` seqType ty `seq` seqMCo mco
2071 seqCo (TyConAppCo r tc cos) = r `seq` tc `seq` seqCos cos
2072 seqCo (AppCo co1 co2) = seqCo co1 `seq` seqCo co2
2073 seqCo (ForAllCo tv k co) = seqType (varType tv) `seq` seqCo k
2074 `seq` seqCo co
2075 seqCo (FunCo r co1 co2) = r `seq` seqCo co1 `seq` seqCo co2
2076 seqCo (CoVarCo cv) = cv `seq` ()
2077 seqCo (HoleCo h) = coHoleCoVar h `seq` ()
2078 seqCo (AxiomInstCo con ind cos) = con `seq` ind `seq` seqCos cos
2079 seqCo (UnivCo p r t1 t2)
2080 = seqProv p `seq` r `seq` seqType t1 `seq` seqType t2
2081 seqCo (SymCo co) = seqCo co
2082 seqCo (TransCo co1 co2) = seqCo co1 `seq` seqCo co2
2083 seqCo (NthCo r n co) = r `seq` n `seq` seqCo co
2084 seqCo (LRCo lr co) = lr `seq` seqCo co
2085 seqCo (InstCo co arg) = seqCo co `seq` seqCo arg
2086 seqCo (KindCo co) = seqCo co
2087 seqCo (SubCo co) = seqCo co
2088 seqCo (AxiomRuleCo _ cs) = seqCos cs
2089
2090 seqProv :: UnivCoProvenance -> ()
2091 seqProv UnsafeCoerceProv = ()
2092 seqProv (PhantomProv co) = seqCo co
2093 seqProv (ProofIrrelProv co) = seqCo co
2094 seqProv (PluginProv _) = ()
2095
2096 seqCos :: [Coercion] -> ()
2097 seqCos [] = ()
2098 seqCos (co:cos) = seqCo co `seq` seqCos cos
2099
2100 {-
2101 %************************************************************************
2102 %* *
2103 The kind of a type, and of a coercion
2104 %* *
2105 %************************************************************************
2106 -}
2107
2108 coercionType :: Coercion -> Type
2109 coercionType co = case coercionKindRole co of
2110 (Pair ty1 ty2, r) -> mkCoercionType r ty1 ty2
2111
2112 ------------------
2113 -- | If it is the case that
2114 --
2115 -- > c :: (t1 ~ t2)
2116 --
2117 -- i.e. the kind of @c@ relates @t1@ and @t2@, then @coercionKind c = Pair t1 t2@.
2118
2119 coercionKind :: Coercion -> Pair Type
2120 coercionKind co =
2121 go co
2122 where
2123 go (Refl ty) = Pair ty ty
2124 go (GRefl _ ty MRefl) = Pair ty ty
2125 go (GRefl _ ty (MCo co1)) = Pair ty (mkCastTy ty co1)
2126 go (TyConAppCo _ tc cos)= mkTyConApp tc <$> (sequenceA $ map go cos)
2127 go (AppCo co1 co2) = mkAppTy <$> go co1 <*> go co2
2128 go co@(ForAllCo tv1 k_co co1) -- works for both tyvar and covar
2129 | isGReflCo k_co = mkTyCoInvForAllTy tv1 <$> go co1
2130 -- kind_co always has kind @Type@, thus @isGReflCo@
2131 | otherwise = go_forall empty_subst co
2132 where
2133 empty_subst = mkEmptyTCvSubst (mkInScopeSet $ tyCoVarsOfCo co)
2134 go (FunCo _ co1 co2) = mkFunTy <$> go co1 <*> go co2
2135 go (CoVarCo cv) = coVarTypes cv
2136 go (HoleCo h) = coVarTypes (coHoleCoVar h)
2137 go (AxiomInstCo ax ind cos)
2138 | CoAxBranch { cab_tvs = tvs, cab_cvs = cvs
2139 , cab_lhs = lhs, cab_rhs = rhs } <- coAxiomNthBranch ax ind
2140 , let Pair tycos1 tycos2 = sequenceA (map go cos)
2141 (tys1, cotys1) = splitAtList tvs tycos1
2142 (tys2, cotys2) = splitAtList tvs tycos2
2143 cos1 = map stripCoercionTy cotys1
2144 cos2 = map stripCoercionTy cotys2
2145 = ASSERT( cos `equalLength` (tvs ++ cvs) )
2146 -- Invariant of AxiomInstCo: cos should
2147 -- exactly saturate the axiom branch
2148 Pair (substTyWith tvs tys1 $
2149 substTyWithCoVars cvs cos1 $
2150 mkTyConApp (coAxiomTyCon ax) lhs)
2151 (substTyWith tvs tys2 $
2152 substTyWithCoVars cvs cos2 rhs)
2153 go (UnivCo _ _ ty1 ty2) = Pair ty1 ty2
2154 go (SymCo co) = swap $ go co
2155 go (TransCo co1 co2) = Pair (pFst $ go co1) (pSnd $ go co2)
2156 go g@(NthCo _ d co)
2157 | Just argss <- traverse tyConAppArgs_maybe tys
2158 = ASSERT( and $ (`lengthExceeds` d) <$> argss )
2159 (`getNth` d) <$> argss
2160
2161 | d == 0
2162 , Just splits <- traverse splitForAllTy_maybe tys
2163 = (tyVarKind . fst) <$> splits
2164
2165 | otherwise
2166 = pprPanic "coercionKind" (ppr g)
2167 where
2168 tys = go co
2169 go (LRCo lr co) = (pickLR lr . splitAppTy) <$> go co
2170 go (InstCo aco arg) = go_app aco [arg]
2171 go (KindCo co) = typeKind <$> go co
2172 go (SubCo co) = go co
2173 go (AxiomRuleCo ax cos) = expectJust "coercionKind" $
2174 coaxrProves ax (map go cos)
2175
2176 go_app :: Coercion -> [Coercion] -> Pair Type
2177 -- Collect up all the arguments and apply all at once
2178 -- See Note [Nested InstCos]
2179 go_app (InstCo co arg) args = go_app co (arg:args)
2180 go_app co args = piResultTys <$> go co <*> (sequenceA $ map go args)
2181
2182 go_forall subst (ForAllCo tv1 k_co co)
2183 -- See Note [Nested ForAllCos]
2184 | isTyVar tv1
2185 = mkInvForAllTy <$> Pair tv1 tv2 <*> go_forall subst' co
2186 where
2187 Pair _ k2 = go k_co
2188 tv2 = setTyVarKind tv1 (substTy subst k2)
2189 subst' | isGReflCo k_co = extendTCvInScope subst tv1
2190 -- kind_co always has kind @Type@, thus @isGReflCo@
2191 | otherwise = extendTvSubst (extendTCvInScope subst tv2) tv1 $
2192 TyVarTy tv2 `mkCastTy` mkSymCo k_co
2193 go_forall subst (ForAllCo cv1 k_co co)
2194 | isCoVar cv1
2195 = mkTyCoInvForAllTy <$> Pair cv1 cv2 <*> go_forall subst' co
2196 where
2197 Pair _ k2 = go k_co
2198 r = coVarRole cv1
2199 eta1 = mkNthCo r 2 (downgradeRole r Nominal k_co)
2200 eta2 = mkNthCo r 3 (downgradeRole r Nominal k_co)
2201
2202 -- k_co :: (t1 ~r t2) ~N (s1 ~r s2)
2203 -- k1 = t1 ~r t2
2204 -- k2 = s1 ~r s2
2205 -- cv1 :: t1 ~r t2
2206 -- cv2 :: s1 ~r s2
2207 -- eta1 :: t1 ~r s1
2208 -- eta2 :: t2 ~r s2
2209 -- n_subst = (eta1 ; cv2 ; sym eta2) :: t1 ~r t2
2210
2211 cv2 = setVarType cv1 (substTy subst k2)
2212 n_subst = eta1 `mkTransCo` (mkCoVarCo cv2) `mkTransCo` (mkSymCo eta2)
2213 subst' | isReflCo k_co = extendTCvInScope subst cv1
2214 | otherwise = extendCvSubst (extendTCvInScope subst cv2)
2215 cv1 n_subst
2216
2217 go_forall subst other_co
2218 -- when other_co is not a ForAllCo
2219 = substTy subst `pLiftSnd` go other_co
2220
2221 {-
2222
2223 Note [Nested ForAllCos]
2224 ~~~~~~~~~~~~~~~~~~~~~~~
2225
2226 Suppose we need `coercionKind (ForAllCo a1 (ForAllCo a2 ... (ForAllCo an
2227 co)...) )`. We do not want to perform `n` single-type-variable
2228 substitutions over the kind of `co`; rather we want to do one substitution
2229 which substitutes for all of `a1`, `a2` ... simultaneously. If we do one
2230 at a time we get the performance hole reported in Trac #11735.
2231
2232 Solution: gather up the type variables for nested `ForAllCos`, and
2233 substitute for them all at once. Remarkably, for Trac #11735 this single
2234 change reduces /total/ compile time by a factor of more than ten.
2235
2236 -}
2237
2238 -- | Apply 'coercionKind' to multiple 'Coercion's
2239 coercionKinds :: [Coercion] -> Pair [Type]
2240 coercionKinds tys = sequenceA $ map coercionKind tys
2241
2242 -- | Get a coercion's kind and role.
2243 coercionKindRole :: Coercion -> (Pair Type, Role)
2244 coercionKindRole co = (coercionKind co, coercionRole co)
2245
2246 -- | Retrieve the role from a coercion.
2247 coercionRole :: Coercion -> Role
2248 coercionRole = go
2249 where
2250 go (Refl _) = Nominal
2251 go (GRefl r _ _) = r
2252 go (TyConAppCo r _ _) = r
2253 go (AppCo co1 _) = go co1
2254 go (ForAllCo _ _ co) = go co
2255 go (FunCo r _ _) = r
2256 go (CoVarCo cv) = coVarRole cv
2257 go (HoleCo h) = coVarRole (coHoleCoVar h)
2258 go (AxiomInstCo ax _ _) = coAxiomRole ax
2259 go (UnivCo _ r _ _) = r
2260 go (SymCo co) = go co
2261 go (TransCo co1 _co2) = go co1
2262 go (NthCo r _d _co) = r
2263 go (LRCo {}) = Nominal
2264 go (InstCo co _) = go co
2265 go (KindCo {}) = Nominal
2266 go (SubCo _) = Representational
2267 go (AxiomRuleCo ax _) = coaxrRole ax
2268
2269 {-
2270 Note [Nested InstCos]
2271 ~~~~~~~~~~~~~~~~~~~~~
2272 In Trac #5631 we found that 70% of the entire compilation time was
2273 being spent in coercionKind! The reason was that we had
2274 (g @ ty1 @ ty2 .. @ ty100) -- The "@s" are InstCos
2275 where
2276 g :: forall a1 a2 .. a100. phi
2277 If we deal with the InstCos one at a time, we'll do this:
2278 1. Find the kind of (g @ ty1 .. @ ty99) : forall a100. phi'
2279 2. Substitute phi'[ ty100/a100 ], a single tyvar->type subst
2280 But this is a *quadratic* algorithm, and the blew up Trac #5631.
2281 So it's very important to do the substitution simultaneously;
2282 cf Type.piResultTys (which in fact we call here).
2283
2284 -}
2285
2286 -- | Assuming that two types are the same, ignoring coercions, find
2287 -- a nominal coercion between the types. This is useful when optimizing
2288 -- transitivity over coercion applications, where splitting two
2289 -- AppCos might yield different kinds. See Note [EtaAppCo] in OptCoercion.
2290 buildCoercion :: Type -> Type -> CoercionN
2291 buildCoercion orig_ty1 orig_ty2 = go orig_ty1 orig_ty2
2292 where
2293 go ty1 ty2 | Just ty1' <- coreView ty1 = go ty1' ty2
2294 | Just ty2' <- coreView ty2 = go ty1 ty2'
2295
2296 go (CastTy ty1 co) ty2
2297 = let co' = go ty1 ty2
2298 r = coercionRole co'
2299 in mkCoherenceLeftCo r ty1 co co'
2300
2301 go ty1 (CastTy ty2 co)
2302 = let co' = go ty1 ty2
2303 r = coercionRole co'
2304 in mkCoherenceRightCo r ty2 co co'
2305
2306 go ty1@(TyVarTy tv1) _tyvarty
2307 = ASSERT( case _tyvarty of
2308 { TyVarTy tv2 -> tv1 == tv2
2309 ; _ -> False } )
2310 mkNomReflCo ty1
2311
2312 go (FunTy arg1 res1) (FunTy arg2 res2)
2313 = mkFunCo Nominal (go arg1 arg2) (go res1 res2)
2314
2315 go (TyConApp tc1 args1) (TyConApp tc2 args2)
2316 = ASSERT( tc1 == tc2 )
2317 mkTyConAppCo Nominal tc1 (zipWith go args1 args2)
2318
2319 go (AppTy ty1a ty1b) ty2
2320 | Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2
2321 = mkAppCo (go ty1a ty2a) (go ty1b ty2b)
2322
2323 go ty1 (AppTy ty2a ty2b)
2324 | Just (ty1a, ty1b) <- repSplitAppTy_maybe ty1
2325 = mkAppCo (go ty1a ty2a) (go ty1b ty2b)
2326
2327 go (ForAllTy (Bndr tv1 _flag1) ty1) (ForAllTy (Bndr tv2 _flag2) ty2)
2328 | isTyVar tv1
2329 = ASSERT( isTyVar tv2 )
2330 mkForAllCo tv1 kind_co (go ty1 ty2')
2331 where kind_co = go (tyVarKind tv1) (tyVarKind tv2)
2332 in_scope = mkInScopeSet $ tyCoVarsOfType ty2 `unionVarSet` tyCoVarsOfCo kind_co
2333 ty2' = substTyWithInScope in_scope [tv2]
2334 [mkTyVarTy tv1 `mkCastTy` kind_co]
2335 ty2
2336
2337 go (ForAllTy (Bndr cv1 _flag1) ty1) (ForAllTy (Bndr cv2 _flag2) ty2)
2338 = ASSERT( isCoVar cv1 && isCoVar cv2 )
2339 mkForAllCo cv1 kind_co (go ty1 ty2')
2340 where s1 = varType cv1
2341 s2 = varType cv2
2342 kind_co = go s1 s2
2343
2344 -- s1 = t1 ~r t2
2345 -- s2 = t3 ~r t4
2346 -- kind_co :: (t1 ~r t2) ~N (t3 ~r t4)
2347 -- eta1 :: t1 ~r t3
2348 -- eta2 :: t2 ~r t4
2349
2350 r = coVarRole cv1
2351 kind_co' = downgradeRole r Nominal kind_co
2352 eta1 = mkNthCo r 2 kind_co'
2353 eta2 = mkNthCo r 3 kind_co'
2354
2355 subst = mkEmptyTCvSubst $ mkInScopeSet $
2356 tyCoVarsOfType ty2 `unionVarSet` tyCoVarsOfCo kind_co
2357 ty2' = substTy (extendCvSubst subst cv2 $ mkSymCo eta1 `mkTransCo`
2358 mkCoVarCo cv1 `mkTransCo`
2359 eta2)
2360 ty2
2361
2362 go ty1@(LitTy lit1) _lit2
2363 = ASSERT( case _lit2 of
2364 { LitTy lit2 -> lit1 == lit2
2365 ; _ -> False } )
2366 mkNomReflCo ty1
2367
2368 go (CoercionTy co1) (CoercionTy co2)
2369 = mkProofIrrelCo Nominal kind_co co1 co2
2370 where
2371 kind_co = go (coercionType co1) (coercionType co2)
2372
2373 go ty1 ty2
2374 = pprPanic "buildKindCoercion" (vcat [ ppr orig_ty1, ppr orig_ty2
2375 , ppr ty1, ppr ty2 ])