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