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