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