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