Fix #14729 by making the normaliser homogeneous
[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 tyConRolesX :: Role -> TyCon -> [Role]
1321 tyConRolesX Representational tc = tyConRolesRepresentational tc
1322 tyConRolesX role _ = repeat role
1323
1324 tyConRolesRepresentational :: TyCon -> [Role]
1325 tyConRolesRepresentational tc = tyConRoles tc ++ repeat Nominal
1326
1327 nthRole :: Role -> TyCon -> Int -> Role
1328 nthRole Nominal _ _ = Nominal
1329 nthRole Phantom _ _ = Phantom
1330 nthRole Representational tc n
1331 = (tyConRolesRepresentational tc) `getNth` n
1332
1333 ltRole :: Role -> Role -> Bool
1334 -- Is one role "less" than another?
1335 -- Nominal < Representational < Phantom
1336 ltRole Phantom _ = False
1337 ltRole Representational Phantom = True
1338 ltRole Representational _ = False
1339 ltRole Nominal Nominal = False
1340 ltRole Nominal _ = True
1341
1342 -------------------------------
1343
1344 -- | like mkKindCo, but aggressively & recursively optimizes to avoid using
1345 -- a KindCo constructor. The output role is nominal.
1346 promoteCoercion :: Coercion -> CoercionN
1347
1348 -- First cases handles anything that should yield refl.
1349 promoteCoercion co = case co of
1350
1351 _ | ki1 `eqType` ki2
1352 -> mkNomReflCo (typeKind ty1)
1353 -- no later branch should return refl
1354 -- The ASSERT( False )s throughout
1355 -- are these cases explicitly, but they should never fire.
1356
1357 Refl _ -> ASSERT( False )
1358 mkNomReflCo ki1
1359
1360 GRefl _ _ MRefl -> ASSERT( False )
1361 mkNomReflCo ki1
1362
1363 GRefl _ _ (MCo co) -> co
1364
1365 TyConAppCo _ tc args
1366 | Just co' <- instCoercions (mkNomReflCo (tyConKind tc)) args
1367 -> co'
1368 | otherwise
1369 -> mkKindCo co
1370
1371 AppCo co1 arg
1372 | Just co' <- instCoercion (coercionKind (mkKindCo co1))
1373 (promoteCoercion co1) arg
1374 -> co'
1375 | otherwise
1376 -> mkKindCo co
1377
1378 ForAllCo tv _ g
1379 | isTyVar tv
1380 -> promoteCoercion g
1381
1382 ForAllCo _ _ _
1383 -> ASSERT( False )
1384 mkNomReflCo liftedTypeKind
1385 -- See Note [Weird typing rule for ForAllTy] in Type
1386
1387 FunCo _ _ _
1388 -> ASSERT( False )
1389 mkNomReflCo liftedTypeKind
1390
1391 CoVarCo {} -> mkKindCo co
1392 HoleCo {} -> mkKindCo co
1393 AxiomInstCo {} -> mkKindCo co
1394 AxiomRuleCo {} -> mkKindCo co
1395
1396 UnivCo UnsafeCoerceProv _ t1 t2 -> mkUnsafeCo Nominal (typeKind t1) (typeKind t2)
1397 UnivCo (PhantomProv kco) _ _ _ -> kco
1398 UnivCo (ProofIrrelProv kco) _ _ _ -> kco
1399 UnivCo (PluginProv _) _ _ _ -> mkKindCo co
1400
1401 SymCo g
1402 -> mkSymCo (promoteCoercion g)
1403
1404 TransCo co1 co2
1405 -> mkTransCo (promoteCoercion co1) (promoteCoercion co2)
1406
1407 NthCo _ n co1
1408 | Just (_, args) <- splitTyConAppCo_maybe co1
1409 , args `lengthExceeds` n
1410 -> promoteCoercion (args !! n)
1411
1412 | Just _ <- splitForAllCo_maybe co
1413 , n == 0
1414 -> ASSERT( False ) mkNomReflCo liftedTypeKind
1415
1416 | otherwise
1417 -> mkKindCo co
1418
1419 LRCo lr co1
1420 | Just (lco, rco) <- splitAppCo_maybe co1
1421 -> case lr of
1422 CLeft -> promoteCoercion lco
1423 CRight -> promoteCoercion rco
1424
1425 | otherwise
1426 -> mkKindCo co
1427
1428 InstCo g _
1429 | isForAllTy_ty ty1
1430 -> ASSERT( isForAllTy_ty ty2 )
1431 promoteCoercion g
1432 | otherwise
1433 -> ASSERT( False)
1434 mkNomReflCo liftedTypeKind
1435 -- See Note [Weird typing rule for ForAllTy] in Type
1436
1437 KindCo _
1438 -> ASSERT( False )
1439 mkNomReflCo liftedTypeKind
1440
1441 SubCo g
1442 -> promoteCoercion g
1443
1444 where
1445 Pair ty1 ty2 = coercionKind co
1446 ki1 = typeKind ty1
1447 ki2 = typeKind ty2
1448
1449 -- | say @g = promoteCoercion h@. Then, @instCoercion g w@ yields @Just g'@,
1450 -- where @g' = promoteCoercion (h w)@.
1451 -- fails if this is not possible, if @g@ coerces between a forall and an ->
1452 -- or if second parameter has a representational role and can't be used
1453 -- with an InstCo.
1454 instCoercion :: Pair Type -- g :: lty ~ rty
1455 -> CoercionN -- ^ must be nominal
1456 -> Coercion
1457 -> Maybe CoercionN
1458 instCoercion (Pair lty rty) g w
1459 | (isForAllTy_ty lty && isForAllTy_ty rty)
1460 || (isForAllTy_co lty && isForAllTy_co rty)
1461 , Just w' <- setNominalRole_maybe (coercionRole w) w
1462 -- g :: (forall t1. t2) ~ (forall t1. t3)
1463 -- w :: s1 ~ s2
1464 -- returns mkInstCo g w' :: t2 [t1 |-> s1 ] ~ t3 [t1 |-> s2]
1465 = Just $ mkInstCo g w'
1466 | isFunTy lty && isFunTy rty
1467 -- g :: (t1 -> t2) ~ (t3 -> t4)
1468 -- returns t2 ~ t4
1469 = Just $ mkNthCo Nominal 3 g -- extract result type, which is the 4th argument to (->)
1470 | otherwise -- one forall, one funty...
1471 = Nothing
1472
1473 -- | Repeated use of 'instCoercion'
1474 instCoercions :: CoercionN -> [Coercion] -> Maybe CoercionN
1475 instCoercions g ws
1476 = let arg_ty_pairs = map coercionKind ws in
1477 snd <$> foldM go (coercionKind g, g) (zip arg_ty_pairs ws)
1478 where
1479 go :: (Pair Type, Coercion) -> (Pair Type, Coercion)
1480 -> Maybe (Pair Type, Coercion)
1481 go (g_tys, g) (w_tys, w)
1482 = do { g' <- instCoercion g_tys g w
1483 ; return (piResultTy <$> g_tys <*> w_tys, g') }
1484
1485 -- | Creates a new coercion with both of its types casted by different casts
1486 -- @castCoercionKind g r t1 t2 h1 h2@, where @g :: t1 ~r t2@,
1487 -- has type @(t1 |> h1) ~r (t2 |> h2)@.
1488 -- @h1@ and @h2@ must be nominal.
1489 castCoercionKind :: Coercion -> Role -> Type -> Type
1490 -> CoercionN -> CoercionN -> Coercion
1491 castCoercionKind g r t1 t2 h1 h2
1492 = mkCoherenceRightCo r t2 h2 (mkCoherenceLeftCo r t1 h1 g)
1493
1494 -- | Creates a new coercion with both of its types casted by different casts
1495 -- @castCoercionKind g h1 h2@, where @g :: t1 ~r t2@,
1496 -- has type @(t1 |> h1) ~r (t2 |> h2)@.
1497 -- @h1@ and @h2@ must be nominal.
1498 -- It calls @coercionKindRole@, so it's quite inefficient (which 'I' stands for)
1499 -- Use @castCoercionKind@ instead if @t1@, @t2@, and @r@ are known beforehand.
1500 castCoercionKindI :: Coercion -> CoercionN -> CoercionN -> Coercion
1501 castCoercionKindI g h1 h2
1502 = mkCoherenceRightCo r t2 h2 (mkCoherenceLeftCo r t1 h1 g)
1503 where (Pair t1 t2, r) = coercionKindRole g
1504
1505 -- See note [Newtype coercions] in TyCon
1506
1507 mkPiCos :: Role -> [Var] -> Coercion -> Coercion
1508 mkPiCos r vs co = foldr (mkPiCo r) co vs
1509
1510 -- | Make a forall 'Coercion', where both types related by the coercion
1511 -- are quantified over the same variable.
1512 mkPiCo :: Role -> Var -> Coercion -> Coercion
1513 mkPiCo r v co | isTyVar v = mkHomoForAllCos [v] co
1514 | isCoVar v = ASSERT( not (v `elemVarSet` tyCoVarsOfCo co) )
1515 -- We didn't call mkForAllCo here because if v does not appear
1516 -- in co, the argement coercion will be nominal. But here we
1517 -- want it to be r. It is only called in 'mkPiCos', which is
1518 -- only used in SimplUtils, where we are sure for
1519 -- now (Aug 2018) v won't occur in co.
1520 mkFunCo r (mkReflCo r (varType v)) co
1521 | otherwise = mkFunCo r (mkReflCo r (varType v)) co
1522
1523 -- mkCoCast (c :: s1 ~?r t1) (g :: (s1 ~?r t1) ~#R (s2 ~?r t2)) :: s2 ~?r t2
1524 -- The first coercion might be lifted or unlifted; thus the ~? above
1525 -- Lifted and unlifted equalities take different numbers of arguments,
1526 -- so we have to make sure to supply the right parameter to decomposeCo.
1527 -- Also, note that the role of the first coercion is the same as the role of
1528 -- the equalities related by the second coercion. The second coercion is
1529 -- itself always representational.
1530 mkCoCast :: Coercion -> CoercionR -> Coercion
1531 mkCoCast c g
1532 | (g2:g1:_) <- reverse co_list
1533 = mkSymCo g1 `mkTransCo` c `mkTransCo` g2
1534
1535 | otherwise
1536 = pprPanic "mkCoCast" (ppr g $$ ppr (coercionKind g))
1537 where
1538 -- g :: (s1 ~# t1) ~# (s2 ~# t2)
1539 -- g1 :: s1 ~# s2
1540 -- g2 :: t1 ~# t2
1541 (tc, _) = splitTyConApp (pFst $ coercionKind g)
1542 co_list = decomposeCo (tyConArity tc) g (tyConRolesRepresentational tc)
1543
1544 {-
1545 %************************************************************************
1546 %* *
1547 Newtypes
1548 %* *
1549 %************************************************************************
1550 -}
1551
1552 -- | If @co :: T ts ~ rep_ty@ then:
1553 --
1554 -- > instNewTyCon_maybe T ts = Just (rep_ty, co)
1555 --
1556 -- Checks for a newtype, and for being saturated
1557 instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, Coercion)
1558 instNewTyCon_maybe tc tys
1559 | Just (tvs, ty, co_tc) <- unwrapNewTyConEtad_maybe tc -- Check for newtype
1560 , tvs `leLength` tys -- Check saturated enough
1561 = Just (applyTysX tvs ty tys, mkUnbranchedAxInstCo Representational co_tc tys [])
1562 | otherwise
1563 = Nothing
1564
1565 {-
1566 ************************************************************************
1567 * *
1568 Type normalisation
1569 * *
1570 ************************************************************************
1571 -}
1572
1573 -- | A function to check if we can reduce a type by one step. Used
1574 -- with 'topNormaliseTypeX'.
1575 type NormaliseStepper ev = RecTcChecker
1576 -> TyCon -- tc
1577 -> [Type] -- tys
1578 -> NormaliseStepResult ev
1579
1580 -- | The result of stepping in a normalisation function.
1581 -- See 'topNormaliseTypeX'.
1582 data NormaliseStepResult ev
1583 = NS_Done -- ^ Nothing more to do
1584 | NS_Abort -- ^ Utter failure. The outer function should fail too.
1585 | NS_Step RecTcChecker Type ev -- ^ We stepped, yielding new bits;
1586 -- ^ ev is evidence;
1587 -- Usually a co :: old type ~ new type
1588
1589 mapStepResult :: (ev1 -> ev2)
1590 -> NormaliseStepResult ev1 -> NormaliseStepResult ev2
1591 mapStepResult f (NS_Step rec_nts ty ev) = NS_Step rec_nts ty (f ev)
1592 mapStepResult _ NS_Done = NS_Done
1593 mapStepResult _ NS_Abort = NS_Abort
1594
1595 -- | Try one stepper and then try the next, if the first doesn't make
1596 -- progress.
1597 -- So if it returns NS_Done, it means that both steppers are satisfied
1598 composeSteppers :: NormaliseStepper ev -> NormaliseStepper ev
1599 -> NormaliseStepper ev
1600 composeSteppers step1 step2 rec_nts tc tys
1601 = case step1 rec_nts tc tys of
1602 success@(NS_Step {}) -> success
1603 NS_Done -> step2 rec_nts tc tys
1604 NS_Abort -> NS_Abort
1605
1606 -- | A 'NormaliseStepper' that unwraps newtypes, careful not to fall into
1607 -- a loop. If it would fall into a loop, it produces 'NS_Abort'.
1608 unwrapNewTypeStepper :: NormaliseStepper Coercion
1609 unwrapNewTypeStepper rec_nts tc tys
1610 | Just (ty', co) <- instNewTyCon_maybe tc tys
1611 = case checkRecTc rec_nts tc of
1612 Just rec_nts' -> NS_Step rec_nts' ty' co
1613 Nothing -> NS_Abort
1614
1615 | otherwise
1616 = NS_Done
1617
1618 -- | A general function for normalising the top-level of a type. It continues
1619 -- to use the provided 'NormaliseStepper' until that function fails, and then
1620 -- this function returns. The roles of the coercions produced by the
1621 -- 'NormaliseStepper' must all be the same, which is the role returned from
1622 -- the call to 'topNormaliseTypeX'.
1623 --
1624 -- Typically ev is Coercion.
1625 --
1626 -- If topNormaliseTypeX step plus ty = Just (ev, ty')
1627 -- then ty ~ev1~ t1 ~ev2~ t2 ... ~evn~ ty'
1628 -- and ev = ev1 `plus` ev2 `plus` ... `plus` evn
1629 -- If it returns Nothing then no newtype unwrapping could happen
1630 topNormaliseTypeX :: NormaliseStepper ev -> (ev -> ev -> ev)
1631 -> Type -> Maybe (ev, Type)
1632 topNormaliseTypeX stepper plus ty
1633 | Just (tc, tys) <- splitTyConApp_maybe ty
1634 , NS_Step rec_nts ty' ev <- stepper initRecTc tc tys
1635 = go rec_nts ev ty'
1636 | otherwise
1637 = Nothing
1638 where
1639 go rec_nts ev ty
1640 | Just (tc, tys) <- splitTyConApp_maybe ty
1641 = case stepper rec_nts tc tys of
1642 NS_Step rec_nts' ty' ev' -> go rec_nts' (ev `plus` ev') ty'
1643 NS_Done -> Just (ev, ty)
1644 NS_Abort -> Nothing
1645
1646 | otherwise
1647 = Just (ev, ty)
1648
1649 topNormaliseNewType_maybe :: Type -> Maybe (Coercion, Type)
1650 -- ^ Sometimes we want to look through a @newtype@ and get its associated coercion.
1651 -- This function strips off @newtype@ layers enough to reveal something that isn't
1652 -- a @newtype@. Specifically, here's the invariant:
1653 --
1654 -- > topNormaliseNewType_maybe rec_nts ty = Just (co, ty')
1655 --
1656 -- then (a) @co : ty0 ~ ty'@.
1657 -- (b) ty' is not a newtype.
1658 --
1659 -- The function returns @Nothing@ for non-@newtypes@,
1660 -- or unsaturated applications
1661 --
1662 -- This function does *not* look through type families, because it has no access to
1663 -- the type family environment. If you do have that at hand, consider to use
1664 -- topNormaliseType_maybe, which should be a drop-in replacement for
1665 -- topNormaliseNewType_maybe
1666 -- If topNormliseNewType_maybe ty = Just (co, ty'), then co : ty ~R ty'
1667 topNormaliseNewType_maybe ty
1668 = topNormaliseTypeX unwrapNewTypeStepper mkTransCo ty
1669
1670 {-
1671 %************************************************************************
1672 %* *
1673 Comparison of coercions
1674 %* *
1675 %************************************************************************
1676 -}
1677
1678 -- | Syntactic equality of coercions
1679 eqCoercion :: Coercion -> Coercion -> Bool
1680 eqCoercion = eqType `on` coercionType
1681
1682 -- | Compare two 'Coercion's, with respect to an RnEnv2
1683 eqCoercionX :: RnEnv2 -> Coercion -> Coercion -> Bool
1684 eqCoercionX env = eqTypeX env `on` coercionType
1685
1686 {-
1687 %************************************************************************
1688 %* *
1689 "Lifting" substitution
1690 [(TyCoVar,Coercion)] -> Type -> Coercion
1691 %* *
1692 %************************************************************************
1693
1694 Note [Lifting coercions over types: liftCoSubst]
1695 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1696 The KPUSH rule deals with this situation
1697 data T a = K (a -> Maybe a)
1698 g :: T t1 ~ T t2
1699 x :: t1 -> Maybe t1
1700
1701 case (K @t1 x) |> g of
1702 K (y:t2 -> Maybe t2) -> rhs
1703
1704 We want to push the coercion inside the constructor application.
1705 So we do this
1706
1707 g' :: t1~t2 = Nth 0 g
1708
1709 case K @t2 (x |> g' -> Maybe g') of
1710 K (y:t2 -> Maybe t2) -> rhs
1711
1712 The crucial operation is that we
1713 * take the type of K's argument: a -> Maybe a
1714 * and substitute g' for a
1715 thus giving *coercion*. This is what liftCoSubst does.
1716
1717 In the presence of kind coercions, this is a bit
1718 of a hairy operation. So, we refer you to the paper introducing kind coercions,
1719 available at www.cis.upenn.edu/~sweirich/papers/fckinds-extended.pdf
1720
1721 Note [extendLiftingContextEx]
1722 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1723 Consider we have datatype
1724 K :: \/k. \/a::k. P -> T k -- P be some type
1725 g :: T k1 ~ T k2
1726
1727 case (K @k1 @t1 x) |> g of
1728 K y -> rhs
1729
1730 We want to push the coercion inside the constructor application.
1731 We first get the coercion mapped by the universal type variable k:
1732 lc = k |-> Nth 0 g :: k1~k2
1733
1734 Here, the important point is that the kind of a is coerced, and P might be
1735 dependent on the existential type variable a.
1736 Thus we first get the coercion of a's kind
1737 g2 = liftCoSubst lc k :: k1 ~ k2
1738
1739 Then we store a new mapping into the lifting context
1740 lc2 = a |-> (t1 ~ t1 |> g2), lc
1741
1742 So later when we can correctly deal with the argument type P
1743 liftCoSubst lc2 P :: P [k|->k1][a|->t1] ~ P[k|->k2][a |-> (t1|>g2)]
1744
1745 This is exactly what extendLiftingContextEx does.
1746 * For each (tyvar:k, ty) pair, we product the mapping
1747 tyvar |-> (ty ~ ty |> (liftCoSubst lc k))
1748 * For each (covar:s1~s2, ty) pair, we produce the mapping
1749 covar |-> (co ~ co')
1750 co' = Sym (liftCoSubst lc s1) ;; covar ;; liftCoSubst lc s2 :: s1'~s2'
1751
1752 This follows the lifting context extension definition in the
1753 "FC with Explicit Kind Equality" paper.
1754 -}
1755
1756 -- ----------------------------------------------------
1757 -- See Note [Lifting coercions over types: liftCoSubst]
1758 -- ----------------------------------------------------
1759
1760 data LiftingContext = LC TCvSubst LiftCoEnv
1761 -- in optCoercion, we need to lift when optimizing InstCo.
1762 -- See Note [Optimising InstCo] in OptCoercion
1763 -- We thus propagate the substitution from OptCoercion here.
1764
1765 instance Outputable LiftingContext where
1766 ppr (LC _ env) = hang (text "LiftingContext:") 2 (ppr env)
1767
1768 type LiftCoEnv = VarEnv Coercion
1769 -- Maps *type variables* to *coercions*.
1770 -- That's the whole point of this function!
1771 -- Also maps coercion variables to ProofIrrelCos.
1772
1773 -- like liftCoSubstWith, but allows for existentially-bound types as well
1774 liftCoSubstWithEx :: Role -- desired role for output coercion
1775 -> [TyVar] -- universally quantified tyvars
1776 -> [Coercion] -- coercions to substitute for those
1777 -> [TyCoVar] -- existentially quantified tycovars
1778 -> [Type] -- types and coercions to be bound to ex vars
1779 -> (Type -> Coercion, [Type]) -- (lifting function, converted ex args)
1780 liftCoSubstWithEx role univs omegas exs rhos
1781 = let theta = mkLiftingContext (zipEqual "liftCoSubstWithExU" univs omegas)
1782 psi = extendLiftingContextEx theta (zipEqual "liftCoSubstWithExX" exs rhos)
1783 in (ty_co_subst psi role, substTys (lcSubstRight psi) (mkTyCoVarTys exs))
1784
1785 liftCoSubstWith :: Role -> [TyCoVar] -> [Coercion] -> Type -> Coercion
1786 liftCoSubstWith r tvs cos ty
1787 = liftCoSubst r (mkLiftingContext $ zipEqual "liftCoSubstWith" tvs cos) ty
1788
1789 -- | @liftCoSubst role lc ty@ produces a coercion (at role @role@)
1790 -- that coerces between @lc_left(ty)@ and @lc_right(ty)@, where
1791 -- @lc_left@ is a substitution mapping type variables to the left-hand
1792 -- types of the mapped coercions in @lc@, and similar for @lc_right@.
1793 liftCoSubst :: HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion
1794 liftCoSubst r lc@(LC subst env) ty
1795 | isEmptyVarEnv env = mkReflCo r (substTy subst ty)
1796 | otherwise = ty_co_subst lc r ty
1797
1798 emptyLiftingContext :: InScopeSet -> LiftingContext
1799 emptyLiftingContext in_scope = LC (mkEmptyTCvSubst in_scope) emptyVarEnv
1800
1801 mkLiftingContext :: [(TyCoVar,Coercion)] -> LiftingContext
1802 mkLiftingContext pairs
1803 = LC (mkEmptyTCvSubst $ mkInScopeSet $ tyCoVarsOfCos (map snd pairs))
1804 (mkVarEnv pairs)
1805
1806 mkSubstLiftingContext :: TCvSubst -> LiftingContext
1807 mkSubstLiftingContext subst = LC subst emptyVarEnv
1808
1809 -- | Extend a lifting context with a new mapping.
1810 extendLiftingContext :: LiftingContext -- ^ original LC
1811 -> TyCoVar -- ^ new variable to map...
1812 -> Coercion -- ^ ...to this lifted version
1813 -> LiftingContext
1814 -- mappings to reflexive coercions are just substitutions
1815 extendLiftingContext (LC subst env) tv arg
1816 | Just (ty, _) <- isReflCo_maybe arg
1817 = LC (extendTCvSubst subst tv ty) env
1818 | otherwise
1819 = LC subst (extendVarEnv env tv arg)
1820
1821 -- | Extend a lifting context with a new mapping, and extend the in-scope set
1822 extendLiftingContextAndInScope :: LiftingContext -- ^ Original LC
1823 -> TyCoVar -- ^ new variable to map...
1824 -> Coercion -- ^ to this coercion
1825 -> LiftingContext
1826 extendLiftingContextAndInScope (LC subst env) tv co
1827 = extendLiftingContext (LC (extendTCvInScopeSet subst (tyCoVarsOfCo co)) env) tv co
1828
1829 -- | Extend a lifting context with existential-variable bindings.
1830 -- See Note [extendLiftingContextEx]
1831 extendLiftingContextEx :: LiftingContext -- ^ original lifting context
1832 -> [(TyCoVar,Type)] -- ^ ex. var / value pairs
1833 -> LiftingContext
1834 -- Note that this is more involved than extendLiftingContext. That function
1835 -- takes a coercion to extend with, so it's assumed that the caller has taken
1836 -- into account any of the kind-changing stuff worried about here.
1837 extendLiftingContextEx lc [] = lc
1838 extendLiftingContextEx lc@(LC subst env) ((v,ty):rest)
1839 -- This function adds bindings for *Nominal* coercions. Why? Because it
1840 -- works with existentially bound variables, which are considered to have
1841 -- nominal roles.
1842 | isTyVar v
1843 = let lc' = LC (subst `extendTCvInScopeSet` tyCoVarsOfType ty)
1844 (extendVarEnv env v $
1845 mkGReflRightCo Nominal
1846 ty
1847 (ty_co_subst lc Nominal (tyVarKind v)))
1848 in extendLiftingContextEx lc' rest
1849 | CoercionTy co <- ty
1850 = -- co :: s1 ~r s2
1851 -- lift_s1 :: s1 ~r s1'
1852 -- lift_s2 :: s2 ~r s2'
1853 -- kco :: (s1 ~r s2) ~N (s1' ~r s2')
1854 ASSERT( isCoVar v )
1855 let (_, _, s1, s2, r) = coVarKindsTypesRole v
1856 lift_s1 = ty_co_subst lc r s1
1857 lift_s2 = ty_co_subst lc r s2
1858 kco = mkTyConAppCo Nominal (equalityTyCon r)
1859 [ mkKindCo lift_s1, mkKindCo lift_s2
1860 , lift_s1 , lift_s2 ]
1861 lc' = LC (subst `extendTCvInScopeSet` tyCoVarsOfCo co)
1862 (extendVarEnv env v
1863 (mkProofIrrelCo Nominal kco co $
1864 (mkSymCo lift_s1) `mkTransCo` co `mkTransCo` lift_s2))
1865 in extendLiftingContextEx lc' rest
1866 | otherwise
1867 = pprPanic "extendLiftingContextEx" (ppr v <+> text "|->" <+> ppr ty)
1868
1869
1870 -- | Erase the environments in a lifting context
1871 zapLiftingContext :: LiftingContext -> LiftingContext
1872 zapLiftingContext (LC subst _) = LC (zapTCvSubst subst) emptyVarEnv
1873
1874 -- | Like 'substForAllCoBndr', but works on a lifting context
1875 substForAllCoBndrUsingLC :: Bool
1876 -> (Coercion -> Coercion)
1877 -> LiftingContext -> TyCoVar -> Coercion
1878 -> (LiftingContext, TyCoVar, Coercion)
1879 substForAllCoBndrUsingLC sym sco (LC subst lc_env) tv co
1880 = (LC subst' lc_env, tv', co')
1881 where
1882 (subst', tv', co') = substForAllCoBndrUsing sym sco subst tv co
1883
1884 -- | The \"lifting\" operation which substitutes coercions for type
1885 -- variables in a type to produce a coercion.
1886 --
1887 -- For the inverse operation, see 'liftCoMatch'
1888 ty_co_subst :: LiftingContext -> Role -> Type -> Coercion
1889 ty_co_subst lc role ty
1890 = go role ty
1891 where
1892 go :: Role -> Type -> Coercion
1893 go r ty | Just ty' <- coreView ty
1894 = go r ty'
1895 go Phantom ty = lift_phantom ty
1896 go r (TyVarTy tv) = expectJust "ty_co_subst bad roles" $
1897 liftCoSubstTyVar lc r tv
1898 go r (AppTy ty1 ty2) = mkAppCo (go r ty1) (go Nominal ty2)
1899 go r (TyConApp tc tys) = mkTyConAppCo r tc (zipWith go (tyConRolesX r tc) tys)
1900 go r (FunTy ty1 ty2) = mkFunCo r (go r ty1) (go r ty2)
1901 go r t@(ForAllTy (Bndr v _) ty)
1902 = let (lc', v', h) = liftCoSubstVarBndr lc v
1903 body_co = ty_co_subst lc' r ty in
1904 if isTyVar v' || almostDevoidCoVarOfCo v' body_co
1905 -- Lifting a ForAllTy over a coercion variable could fail as ForAllCo
1906 -- imposes an extra restriction on where a covar can appear. See last
1907 -- wrinkle in Note [Unused coercion variable in ForAllCo].
1908 -- We specifically check for this and panic because we know that
1909 -- there's a hole in the type system here, and we'd rather panic than
1910 -- fall into it.
1911 then mkForAllCo v' h body_co
1912 else pprPanic "ty_co_subst: covar is not almost devoid" (ppr t)
1913 go r ty@(LitTy {}) = ASSERT( r == Nominal )
1914 mkNomReflCo ty
1915 go r (CastTy ty co) = castCoercionKindI (go r ty) (substLeftCo lc co)
1916 (substRightCo lc co)
1917 go r (CoercionTy co) = mkProofIrrelCo r kco (substLeftCo lc co)
1918 (substRightCo lc co)
1919 where kco = go Nominal (coercionType co)
1920
1921 lift_phantom ty = mkPhantomCo (go Nominal (typeKind ty))
1922 (substTy (lcSubstLeft lc) ty)
1923 (substTy (lcSubstRight lc) ty)
1924
1925 {-
1926 Note [liftCoSubstTyVar]
1927 ~~~~~~~~~~~~~~~~~~~~~~~~~
1928 This function can fail if a coercion in the environment is of too low a role.
1929
1930 liftCoSubstTyVar is called from two places: in liftCoSubst (naturally), and
1931 also in matchAxiom in OptCoercion. From liftCoSubst, the so-called lifting
1932 lemma guarantees that the roles work out. If we fail in this
1933 case, we really should panic -- something is deeply wrong. But, in matchAxiom,
1934 failing is fine. matchAxiom is trying to find a set of coercions
1935 that match, but it may fail, and this is healthy behavior.
1936 -}
1937
1938 -- See Note [liftCoSubstTyVar]
1939 liftCoSubstTyVar :: LiftingContext -> Role -> TyVar -> Maybe Coercion
1940 liftCoSubstTyVar (LC subst env) r v
1941 | Just co_arg <- lookupVarEnv env v
1942 = downgradeRole_maybe r (coercionRole co_arg) co_arg
1943
1944 | otherwise
1945 = Just $ mkReflCo r (substTyVar subst v)
1946
1947 {- Note [liftCoSubstVarBndr]
1948
1949 callback:
1950 We want 'liftCoSubstVarBndrUsing' to be general enough to be reused in
1951 FamInstEnv, therefore the input arg 'fun' returns a pair with polymophic type
1952 in snd.
1953 However in 'liftCoSubstVarBndr', we don't need the snd, so we use unit and
1954 ignore the fourth component of the return value.
1955
1956 liftCoSubstTyVarBndrUsing:
1957 Given
1958 forall tv:k. t
1959 We want to get
1960 forall (tv:k1) (kind_co :: k1 ~ k2) body_co
1961
1962 We lift the kind k to get the kind_co
1963 kind_co = ty_co_subst k :: k1 ~ k2
1964
1965 Now in the LiftingContext, we add the new mapping
1966 tv |-> (tv :: k1) ~ ((tv |> kind_co) :: k2)
1967
1968 liftCoSubstCoVarBndrUsing:
1969 Given
1970 forall cv:(s1 ~ s2). t
1971 We want to get
1972 forall (cv:s1'~s2') (kind_co :: (s1'~s2') ~ (t1 ~ t2)) body_co
1973
1974 We lift s1 and s2 respectively to get
1975 eta1 :: s1' ~ t1
1976 eta2 :: s2' ~ t2
1977 And
1978 kind_co = TyConAppCo Nominal (~#) eta1 eta2
1979
1980 Now in the liftingContext, we add the new mapping
1981 cv |-> (cv :: s1' ~ s2') ~ ((sym eta1;cv;eta2) :: t1 ~ t2)
1982 -}
1983
1984 -- See Note [liftCoSubstVarBndr]
1985 liftCoSubstVarBndr :: LiftingContext -> TyCoVar
1986 -> (LiftingContext, TyCoVar, Coercion)
1987 liftCoSubstVarBndr lc tv
1988 = let (lc', tv', h, _) = liftCoSubstVarBndrUsing callback lc tv in
1989 (lc', tv', h)
1990 where
1991 callback lc' ty' = (ty_co_subst lc' Nominal ty', ())
1992
1993 -- the callback must produce a nominal coercion
1994 liftCoSubstVarBndrUsing :: (LiftingContext -> Type -> (CoercionN, a))
1995 -> LiftingContext -> TyCoVar
1996 -> (LiftingContext, TyCoVar, CoercionN, a)
1997 liftCoSubstVarBndrUsing fun lc old_var
1998 | isTyVar old_var
1999 = liftCoSubstTyVarBndrUsing fun lc old_var
2000 | otherwise
2001 = liftCoSubstCoVarBndrUsing fun lc old_var
2002
2003 -- Works for tyvar binder
2004 liftCoSubstTyVarBndrUsing :: (LiftingContext -> Type -> (CoercionN, a))
2005 -> LiftingContext -> TyVar
2006 -> (LiftingContext, TyVar, CoercionN, a)
2007 liftCoSubstTyVarBndrUsing fun lc@(LC subst cenv) old_var
2008 = ASSERT( isTyVar old_var )
2009 ( LC (subst `extendTCvInScope` new_var) new_cenv
2010 , new_var, eta, stuff )
2011 where
2012 old_kind = tyVarKind old_var
2013 (eta, stuff) = fun lc old_kind
2014 Pair k1 _ = coercionKind eta
2015 new_var = uniqAway (getTCvInScope subst) (setVarType old_var k1)
2016
2017 lifted = mkGReflRightCo Nominal (TyVarTy new_var) eta
2018 -- :: new_var ~ new_var |> eta
2019 new_cenv = extendVarEnv cenv old_var lifted
2020
2021 -- Works for covar binder
2022 liftCoSubstCoVarBndrUsing :: (LiftingContext -> Type -> (CoercionN, a))
2023 -> LiftingContext -> CoVar
2024 -> (LiftingContext, CoVar, CoercionN, a)
2025 liftCoSubstCoVarBndrUsing fun lc@(LC subst cenv) old_var
2026 = ASSERT( isCoVar old_var )
2027 ( LC (subst `extendTCvInScope` new_var) new_cenv
2028 , new_var, kind_co, stuff )
2029 where
2030 old_kind = coVarKind old_var
2031 (eta, stuff) = fun lc old_kind
2032 Pair k1 _ = coercionKind eta
2033 new_var = uniqAway (getTCvInScope subst) (setVarType old_var k1)
2034
2035 -- old_var :: s1 ~r s2
2036 -- eta :: (s1' ~r s2') ~N (t1 ~r t2)
2037 -- eta1 :: s1' ~r t1
2038 -- eta2 :: s2' ~r t2
2039 -- co1 :: s1' ~r s2'
2040 -- co2 :: t1 ~r t2
2041 -- kind_co :: (s1' ~r s2') ~N (t1 ~r t2)
2042 -- lifted :: co1 ~N co2
2043
2044 role = coVarRole old_var
2045 eta' = downgradeRole role Nominal eta
2046 eta1 = mkNthCo role 2 eta'
2047 eta2 = mkNthCo role 3 eta'
2048
2049 co1 = mkCoVarCo new_var
2050 co2 = mkSymCo eta1 `mkTransCo` co1 `mkTransCo` eta2
2051 kind_co = mkTyConAppCo Nominal (equalityTyCon role)
2052 [ mkKindCo co1, mkKindCo co2
2053 , co1 , co2 ]
2054 lifted = mkProofIrrelCo Nominal kind_co co1 co2
2055
2056 new_cenv = extendVarEnv cenv old_var lifted
2057
2058 -- | Is a var in the domain of a lifting context?
2059 isMappedByLC :: TyCoVar -> LiftingContext -> Bool
2060 isMappedByLC tv (LC _ env) = tv `elemVarEnv` env
2061
2062 -- If [a |-> g] is in the substitution and g :: t1 ~ t2, substitute a for t1
2063 -- If [a |-> (g1, g2)] is in the substitution, substitute a for g1
2064 substLeftCo :: LiftingContext -> Coercion -> Coercion
2065 substLeftCo lc co
2066 = substCo (lcSubstLeft lc) co
2067
2068 -- Ditto, but for t2 and g2
2069 substRightCo :: LiftingContext -> Coercion -> Coercion
2070 substRightCo lc co
2071 = substCo (lcSubstRight lc) co
2072
2073 -- | Apply "sym" to all coercions in a 'LiftCoEnv'
2074 swapLiftCoEnv :: LiftCoEnv -> LiftCoEnv
2075 swapLiftCoEnv = mapVarEnv mkSymCo
2076
2077 lcSubstLeft :: LiftingContext -> TCvSubst
2078 lcSubstLeft (LC subst lc_env) = liftEnvSubstLeft subst lc_env
2079
2080 lcSubstRight :: LiftingContext -> TCvSubst
2081 lcSubstRight (LC subst lc_env) = liftEnvSubstRight subst lc_env
2082
2083 liftEnvSubstLeft :: TCvSubst -> LiftCoEnv -> TCvSubst
2084 liftEnvSubstLeft = liftEnvSubst pFst
2085
2086 liftEnvSubstRight :: TCvSubst -> LiftCoEnv -> TCvSubst
2087 liftEnvSubstRight = liftEnvSubst pSnd
2088
2089 liftEnvSubst :: (forall a. Pair a -> a) -> TCvSubst -> LiftCoEnv -> TCvSubst
2090 liftEnvSubst selector subst lc_env
2091 = composeTCvSubst (TCvSubst emptyInScopeSet tenv cenv) subst
2092 where
2093 pairs = nonDetUFMToList lc_env
2094 -- It's OK to use nonDetUFMToList here because we
2095 -- immediately forget the ordering by creating
2096 -- a VarEnv
2097 (tpairs, cpairs) = partitionWith ty_or_co pairs
2098 tenv = mkVarEnv_Directly tpairs
2099 cenv = mkVarEnv_Directly cpairs
2100
2101 ty_or_co :: (Unique, Coercion) -> Either (Unique, Type) (Unique, Coercion)
2102 ty_or_co (u, co)
2103 | Just equality_co <- isCoercionTy_maybe equality_ty
2104 = Right (u, equality_co)
2105 | otherwise
2106 = Left (u, equality_ty)
2107 where
2108 equality_ty = selector (coercionKind co)
2109
2110 -- | Extract the underlying substitution from the LiftingContext
2111 lcTCvSubst :: LiftingContext -> TCvSubst
2112 lcTCvSubst (LC subst _) = subst
2113
2114 -- | Get the 'InScopeSet' from a 'LiftingContext'
2115 lcInScopeSet :: LiftingContext -> InScopeSet
2116 lcInScopeSet (LC subst _) = getTCvInScope subst
2117
2118 {-
2119 %************************************************************************
2120 %* *
2121 Sequencing on coercions
2122 %* *
2123 %************************************************************************
2124 -}
2125
2126 seqMCo :: MCoercion -> ()
2127 seqMCo MRefl = ()
2128 seqMCo (MCo co) = seqCo co
2129
2130 seqCo :: Coercion -> ()
2131 seqCo (Refl ty) = seqType ty
2132 seqCo (GRefl r ty mco) = r `seq` seqType ty `seq` seqMCo mco
2133 seqCo (TyConAppCo r tc cos) = r `seq` tc `seq` seqCos cos
2134 seqCo (AppCo co1 co2) = seqCo co1 `seq` seqCo co2
2135 seqCo (ForAllCo tv k co) = seqType (varType tv) `seq` seqCo k
2136 `seq` seqCo co
2137 seqCo (FunCo r co1 co2) = r `seq` seqCo co1 `seq` seqCo co2
2138 seqCo (CoVarCo cv) = cv `seq` ()
2139 seqCo (HoleCo h) = coHoleCoVar h `seq` ()
2140 seqCo (AxiomInstCo con ind cos) = con `seq` ind `seq` seqCos cos
2141 seqCo (UnivCo p r t1 t2)
2142 = seqProv p `seq` r `seq` seqType t1 `seq` seqType t2
2143 seqCo (SymCo co) = seqCo co
2144 seqCo (TransCo co1 co2) = seqCo co1 `seq` seqCo co2
2145 seqCo (NthCo r n co) = r `seq` n `seq` seqCo co
2146 seqCo (LRCo lr co) = lr `seq` seqCo co
2147 seqCo (InstCo co arg) = seqCo co `seq` seqCo arg
2148 seqCo (KindCo co) = seqCo co
2149 seqCo (SubCo co) = seqCo co
2150 seqCo (AxiomRuleCo _ cs) = seqCos cs
2151
2152 seqProv :: UnivCoProvenance -> ()
2153 seqProv UnsafeCoerceProv = ()
2154 seqProv (PhantomProv co) = seqCo co
2155 seqProv (ProofIrrelProv co) = seqCo co
2156 seqProv (PluginProv _) = ()
2157
2158 seqCos :: [Coercion] -> ()
2159 seqCos [] = ()
2160 seqCos (co:cos) = seqCo co `seq` seqCos cos
2161
2162 {-
2163 %************************************************************************
2164 %* *
2165 The kind of a type, and of a coercion
2166 %* *
2167 %************************************************************************
2168 -}
2169
2170 coercionType :: Coercion -> Type
2171 coercionType co = case coercionKindRole co of
2172 (Pair ty1 ty2, r) -> mkCoercionType r ty1 ty2
2173
2174 ------------------
2175 -- | If it is the case that
2176 --
2177 -- > c :: (t1 ~ t2)
2178 --
2179 -- i.e. the kind of @c@ relates @t1@ and @t2@, then @coercionKind c = Pair t1 t2@.
2180
2181 coercionKind :: Coercion -> Pair Type
2182 coercionKind co =
2183 go co
2184 where
2185 go (Refl ty) = Pair ty ty
2186 go (GRefl _ ty MRefl) = Pair ty ty
2187 go (GRefl _ ty (MCo co1)) = Pair ty (mkCastTy ty co1)
2188 go (TyConAppCo _ tc cos)= mkTyConApp tc <$> (sequenceA $ map go cos)
2189 go (AppCo co1 co2) = mkAppTy <$> go co1 <*> go co2
2190 go co@(ForAllCo tv1 k_co co1) -- works for both tyvar and covar
2191 | isGReflCo k_co = mkTyCoInvForAllTy tv1 <$> go co1
2192 -- kind_co always has kind @Type@, thus @isGReflCo@
2193 | otherwise = go_forall empty_subst co
2194 where
2195 empty_subst = mkEmptyTCvSubst (mkInScopeSet $ tyCoVarsOfCo co)
2196 go (FunCo _ co1 co2) = mkFunTy <$> go co1 <*> go co2
2197 go (CoVarCo cv) = coVarTypes cv
2198 go (HoleCo h) = coVarTypes (coHoleCoVar h)
2199 go (AxiomInstCo ax ind cos)
2200 | CoAxBranch { cab_tvs = tvs, cab_cvs = cvs
2201 , cab_lhs = lhs, cab_rhs = rhs } <- coAxiomNthBranch ax ind
2202 , let Pair tycos1 tycos2 = sequenceA (map go cos)
2203 (tys1, cotys1) = splitAtList tvs tycos1
2204 (tys2, cotys2) = splitAtList tvs tycos2
2205 cos1 = map stripCoercionTy cotys1
2206 cos2 = map stripCoercionTy cotys2
2207 = ASSERT( cos `equalLength` (tvs ++ cvs) )
2208 -- Invariant of AxiomInstCo: cos should
2209 -- exactly saturate the axiom branch
2210 Pair (substTyWith tvs tys1 $
2211 substTyWithCoVars cvs cos1 $
2212 mkTyConApp (coAxiomTyCon ax) lhs)
2213 (substTyWith tvs tys2 $
2214 substTyWithCoVars cvs cos2 rhs)
2215 go (UnivCo _ _ ty1 ty2) = Pair ty1 ty2
2216 go (SymCo co) = swap $ go co
2217 go (TransCo co1 co2) = Pair (pFst $ go co1) (pSnd $ go co2)
2218 go g@(NthCo _ d co)
2219 | Just argss <- traverse tyConAppArgs_maybe tys
2220 = ASSERT( and $ (`lengthExceeds` d) <$> argss )
2221 (`getNth` d) <$> argss
2222
2223 | d == 0
2224 , Just splits <- traverse splitForAllTy_maybe tys
2225 = (tyVarKind . fst) <$> splits
2226
2227 | otherwise
2228 = pprPanic "coercionKind" (ppr g)
2229 where
2230 tys = go co
2231 go (LRCo lr co) = (pickLR lr . splitAppTy) <$> go co
2232 go (InstCo aco arg) = go_app aco [arg]
2233 go (KindCo co) = typeKind <$> go co
2234 go (SubCo co) = go co
2235 go (AxiomRuleCo ax cos) = expectJust "coercionKind" $
2236 coaxrProves ax (map go cos)
2237
2238 go_app :: Coercion -> [Coercion] -> Pair Type
2239 -- Collect up all the arguments and apply all at once
2240 -- See Note [Nested InstCos]
2241 go_app (InstCo co arg) args = go_app co (arg:args)
2242 go_app co args = piResultTys <$> go co <*> (sequenceA $ map go args)
2243
2244 go_forall subst (ForAllCo tv1 k_co co)
2245 -- See Note [Nested ForAllCos]
2246 | isTyVar tv1
2247 = mkInvForAllTy <$> Pair tv1 tv2 <*> go_forall subst' co
2248 where
2249 Pair _ k2 = go k_co
2250 tv2 = setTyVarKind tv1 (substTy subst k2)
2251 subst' | isGReflCo k_co = extendTCvInScope subst tv1
2252 -- kind_co always has kind @Type@, thus @isGReflCo@
2253 | otherwise = extendTvSubst (extendTCvInScope subst tv2) tv1 $
2254 TyVarTy tv2 `mkCastTy` mkSymCo k_co
2255 go_forall subst (ForAllCo cv1 k_co co)
2256 | isCoVar cv1
2257 = mkTyCoInvForAllTy <$> Pair cv1 cv2 <*> go_forall subst' co
2258 where
2259 Pair _ k2 = go k_co
2260 r = coVarRole cv1
2261 eta1 = mkNthCo r 2 (downgradeRole r Nominal k_co)
2262 eta2 = mkNthCo r 3 (downgradeRole r Nominal k_co)
2263
2264 -- k_co :: (t1 ~r t2) ~N (s1 ~r s2)
2265 -- k1 = t1 ~r t2
2266 -- k2 = s1 ~r s2
2267 -- cv1 :: t1 ~r t2
2268 -- cv2 :: s1 ~r s2
2269 -- eta1 :: t1 ~r s1
2270 -- eta2 :: t2 ~r s2
2271 -- n_subst = (eta1 ; cv2 ; sym eta2) :: t1 ~r t2
2272
2273 cv2 = setVarType cv1 (substTy subst k2)
2274 n_subst = eta1 `mkTransCo` (mkCoVarCo cv2) `mkTransCo` (mkSymCo eta2)
2275 subst' | isReflCo k_co = extendTCvInScope subst cv1
2276 | otherwise = extendCvSubst (extendTCvInScope subst cv2)
2277 cv1 n_subst
2278
2279 go_forall subst other_co
2280 -- when other_co is not a ForAllCo
2281 = substTy subst `pLiftSnd` go other_co
2282
2283 {-
2284
2285 Note [Nested ForAllCos]
2286 ~~~~~~~~~~~~~~~~~~~~~~~
2287
2288 Suppose we need `coercionKind (ForAllCo a1 (ForAllCo a2 ... (ForAllCo an
2289 co)...) )`. We do not want to perform `n` single-type-variable
2290 substitutions over the kind of `co`; rather we want to do one substitution
2291 which substitutes for all of `a1`, `a2` ... simultaneously. If we do one
2292 at a time we get the performance hole reported in Trac #11735.
2293
2294 Solution: gather up the type variables for nested `ForAllCos`, and
2295 substitute for them all at once. Remarkably, for Trac #11735 this single
2296 change reduces /total/ compile time by a factor of more than ten.
2297
2298 -}
2299
2300 -- | Apply 'coercionKind' to multiple 'Coercion's
2301 coercionKinds :: [Coercion] -> Pair [Type]
2302 coercionKinds tys = sequenceA $ map coercionKind tys
2303
2304 -- | Get a coercion's kind and role.
2305 coercionKindRole :: Coercion -> (Pair Type, Role)
2306 coercionKindRole co = (coercionKind co, coercionRole co)
2307
2308 -- | Retrieve the role from a coercion.
2309 coercionRole :: Coercion -> Role
2310 coercionRole = go
2311 where
2312 go (Refl _) = Nominal
2313 go (GRefl r _ _) = r
2314 go (TyConAppCo r _ _) = r
2315 go (AppCo co1 _) = go co1
2316 go (ForAllCo _ _ co) = go co
2317 go (FunCo r _ _) = r
2318 go (CoVarCo cv) = coVarRole cv
2319 go (HoleCo h) = coVarRole (coHoleCoVar h)
2320 go (AxiomInstCo ax _ _) = coAxiomRole ax
2321 go (UnivCo _ r _ _) = r
2322 go (SymCo co) = go co
2323 go (TransCo co1 _co2) = go co1
2324 go (NthCo r _d _co) = r
2325 go (LRCo {}) = Nominal
2326 go (InstCo co _) = go co
2327 go (KindCo {}) = Nominal
2328 go (SubCo _) = Representational
2329 go (AxiomRuleCo ax _) = coaxrRole ax
2330
2331 {-
2332 Note [Nested InstCos]
2333 ~~~~~~~~~~~~~~~~~~~~~
2334 In Trac #5631 we found that 70% of the entire compilation time was
2335 being spent in coercionKind! The reason was that we had
2336 (g @ ty1 @ ty2 .. @ ty100) -- The "@s" are InstCos
2337 where
2338 g :: forall a1 a2 .. a100. phi
2339 If we deal with the InstCos one at a time, we'll do this:
2340 1. Find the kind of (g @ ty1 .. @ ty99) : forall a100. phi'
2341 2. Substitute phi'[ ty100/a100 ], a single tyvar->type subst
2342 But this is a *quadratic* algorithm, and the blew up Trac #5631.
2343 So it's very important to do the substitution simultaneously;
2344 cf Type.piResultTys (which in fact we call here).
2345
2346 -}
2347
2348 -- | Assuming that two types are the same, ignoring coercions, find
2349 -- a nominal coercion between the types. This is useful when optimizing
2350 -- transitivity over coercion applications, where splitting two
2351 -- AppCos might yield different kinds. See Note [EtaAppCo] in OptCoercion.
2352 buildCoercion :: Type -> Type -> CoercionN
2353 buildCoercion orig_ty1 orig_ty2 = go orig_ty1 orig_ty2
2354 where
2355 go ty1 ty2 | Just ty1' <- coreView ty1 = go ty1' ty2
2356 | Just ty2' <- coreView ty2 = go ty1 ty2'
2357
2358 go (CastTy ty1 co) ty2
2359 = let co' = go ty1 ty2
2360 r = coercionRole co'
2361 in mkCoherenceLeftCo r ty1 co co'
2362
2363 go ty1 (CastTy ty2 co)
2364 = let co' = go ty1 ty2
2365 r = coercionRole co'
2366 in mkCoherenceRightCo r ty2 co co'
2367
2368 go ty1@(TyVarTy tv1) _tyvarty
2369 = ASSERT( case _tyvarty of
2370 { TyVarTy tv2 -> tv1 == tv2
2371 ; _ -> False } )
2372 mkNomReflCo ty1
2373
2374 go (FunTy arg1 res1) (FunTy arg2 res2)
2375 = mkFunCo Nominal (go arg1 arg2) (go res1 res2)
2376
2377 go (TyConApp tc1 args1) (TyConApp tc2 args2)
2378 = ASSERT( tc1 == tc2 )
2379 mkTyConAppCo Nominal tc1 (zipWith go args1 args2)
2380
2381 go (AppTy ty1a ty1b) ty2
2382 | Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2
2383 = mkAppCo (go ty1a ty2a) (go ty1b ty2b)
2384
2385 go ty1 (AppTy ty2a ty2b)
2386 | Just (ty1a, ty1b) <- repSplitAppTy_maybe ty1
2387 = mkAppCo (go ty1a ty2a) (go ty1b ty2b)
2388
2389 go (ForAllTy (Bndr tv1 _flag1) ty1) (ForAllTy (Bndr tv2 _flag2) ty2)
2390 | isTyVar tv1
2391 = ASSERT( isTyVar tv2 )
2392 mkForAllCo tv1 kind_co (go ty1 ty2')
2393 where kind_co = go (tyVarKind tv1) (tyVarKind tv2)
2394 in_scope = mkInScopeSet $ tyCoVarsOfType ty2 `unionVarSet` tyCoVarsOfCo kind_co
2395 ty2' = substTyWithInScope in_scope [tv2]
2396 [mkTyVarTy tv1 `mkCastTy` kind_co]
2397 ty2
2398
2399 go (ForAllTy (Bndr cv1 _flag1) ty1) (ForAllTy (Bndr cv2 _flag2) ty2)
2400 = ASSERT( isCoVar cv1 && isCoVar cv2 )
2401 mkForAllCo cv1 kind_co (go ty1 ty2')
2402 where s1 = varType cv1
2403 s2 = varType cv2
2404 kind_co = go s1 s2
2405
2406 -- s1 = t1 ~r t2
2407 -- s2 = t3 ~r t4
2408 -- kind_co :: (t1 ~r t2) ~N (t3 ~r t4)
2409 -- eta1 :: t1 ~r t3
2410 -- eta2 :: t2 ~r t4
2411
2412 r = coVarRole cv1
2413 kind_co' = downgradeRole r Nominal kind_co
2414 eta1 = mkNthCo r 2 kind_co'
2415 eta2 = mkNthCo r 3 kind_co'
2416
2417 subst = mkEmptyTCvSubst $ mkInScopeSet $
2418 tyCoVarsOfType ty2 `unionVarSet` tyCoVarsOfCo kind_co
2419 ty2' = substTy (extendCvSubst subst cv2 $ mkSymCo eta1 `mkTransCo`
2420 mkCoVarCo cv1 `mkTransCo`
2421 eta2)
2422 ty2
2423
2424 go ty1@(LitTy lit1) _lit2
2425 = ASSERT( case _lit2 of
2426 { LitTy lit2 -> lit1 == lit2
2427 ; _ -> False } )
2428 mkNomReflCo ty1
2429
2430 go (CoercionTy co1) (CoercionTy co2)
2431 = mkProofIrrelCo Nominal kind_co co1 co2
2432 where
2433 kind_co = go (coercionType co1) (coercionType co2)
2434
2435 go ty1 ty2
2436 = pprPanic "buildKindCoercion" (vcat [ ppr orig_ty1, ppr orig_ty2
2437 , ppr ty1, ppr ty2 ])
2438
2439 {-
2440 %************************************************************************
2441 %* *
2442 Simplifying types
2443 %* *
2444 %************************************************************************
2445
2446 The function below morally belongs in TcFlatten, but it is used also in
2447 FamInstEnv, and so lives here.
2448
2449 Note [simplifyArgsWorker]
2450 ~~~~~~~~~~~~~~~~~~~~~~~~~
2451 Invariant (F2) of Note [Flattening] says that flattening is homogeneous.
2452 This causes some trouble when flattening a function applied to a telescope
2453 of arguments, perhaps with dependency. For example, suppose
2454
2455 type family F :: forall (j :: Type) (k :: Type). Maybe j -> Either j k -> Bool -> [k]
2456
2457 and we wish to flatten the args of (with kind applications explicit)
2458
2459 F a b (Just a c) (Right a b d) False
2460
2461 where all variables are skolems and
2462
2463 a :: Type
2464 b :: Type
2465 c :: a
2466 d :: k
2467
2468 [G] aco :: a ~ fa
2469 [G] bco :: b ~ fb
2470 [G] cco :: c ~ fc
2471 [G] dco :: d ~ fd
2472
2473 The first step is to flatten all the arguments. This is done before calling
2474 simplifyArgsWorker. We start from
2475
2476 a
2477 b
2478 Just a c
2479 Right a b d
2480 False
2481
2482 and get
2483
2484 (fa, co1 :: fa ~ a)
2485 (fb, co2 :: fb ~ b)
2486 (Just fa (fc |> aco) |> co6, co3 :: (Just fa (fc |> aco) |> co6) ~ (Just a c))
2487 (Right fa fb (fd |> bco) |> co7, co4 :: (Right fa fb (fd |> bco) |> co7) ~ (Right a b d))
2488 (False, co5 :: False ~ False)
2489
2490 where
2491 co6 :: Maybe fa ~ Maybe a
2492 co7 :: Either fa fb ~ Either a b
2493
2494 We now process the flattened args in left-to-right order. The first two args
2495 need no further processing. But now consider the third argument. Let f3 = the flattened
2496 result, Just fa (fc |> aco) |> co6.
2497 This f3 flattened argument has kind (Maybe a), due to
2498 (F2). And yet, when we build the application (F fa fb ...), we need this
2499 argument to have kind (Maybe fa), not (Maybe a). We must cast this argument.
2500 The coercion to use is
2501 determined by the kind of F: we see in F's kind that the third argument has
2502 kind Maybe j. Critically, we also know that the argument corresponding to j
2503 (in our example, a) flattened with a coercion co1. We can thus know the
2504 coercion needed for the 3rd argument is (Maybe (sym co1)), thus building
2505 (f3 |> Maybe (sym co1))
2506
2507 More generally, we must use the Lifting Lemma, as implemented in
2508 Coercion.liftCoSubst. As we work left-to-right, any variable that is a
2509 dependent parameter (j and k, in our example) gets mapped in a lifting context
2510 to the coercion that is output from flattening the corresponding argument (co1
2511 and co2, in our example). Then, after flattening later arguments, we lift the
2512 kind of these arguments in the lifting context that we've be building up.
2513 This coercion is then used to keep the result of flattening well-kinded.
2514
2515 Working through our example, this is what happens:
2516
2517 1. Extend the (empty) LC with [j |-> co1]. No new casting must be done,
2518 because the binder associated with the first argument has a closed type (no
2519 variables).
2520
2521 2. Extend the LC with [k |-> co2]. No casting to do.
2522
2523 3. Lifting the kind (Maybe j) with our LC
2524 yields co8 :: Maybe fa ~ Maybe a. Use (f3 |> sym co8) as the argument to
2525 F.
2526
2527 4. Lifting the kind (Either j k) with our LC
2528 yields co9 :: Either fa fb ~ Either a b. Use (f4 |> sym co9) as the 4th
2529 argument to F, where f4 is the flattened form of argument 4, written above.
2530
2531 5. We lift Bool with our LC, getting <Bool>;
2532 casting has no effect.
2533
2534 We're now almost done, but the new application (F fa fb (f3 |> sym co8) (f4 > sym co9) False)
2535 has the wrong kind. Its kind is [fb], instead of the original [b].
2536 So we must use our LC one last time to lift the result kind [k],
2537 getting res_co :: [fb] ~ [b], and we cast our result.
2538
2539 Accordingly, the final result is
2540
2541 F fa fb (Just fa (fc |> aco) |> Maybe (sym aco) |> sym (Maybe (sym aco)))
2542 (Right fa fb (fd |> bco) |> Either (sym aco) (sym bco) |> sym (Either (sym aco) (sym bco)))
2543 False
2544 |> [sym bco]
2545
2546 The res_co (in this case, [sym bco])
2547 is returned as the third return value from simplifyArgsWorker.
2548
2549 Note [Last case in simplifyArgsWorker]
2550 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2551 In writing simplifyArgsWorker's `go`, we know here that args cannot be empty,
2552 because that case is first. We've run out of
2553 binders. But perhaps inner_ki is a tyvar that has been instantiated with a
2554 Π-type.
2555
2556 Here is an example.
2557
2558 a :: forall (k :: Type). k -> k
2559 type family Star
2560 Proxy :: forall j. j -> Type
2561 axStar :: Star ~ Type
2562 type family NoWay :: Bool
2563 axNoWay :: NoWay ~ False
2564 bo :: Type
2565 [G] bc :: bo ~ Bool (in inert set)
2566
2567 co :: (forall j. j -> Type) ~ (forall (j :: Star). (j |> axStar) -> Star)
2568 co = forall (j :: sym axStar). (<j> -> sym axStar)
2569
2570 We are flattening:
2571 a (forall (j :: Star). (j |> axStar) -> Star) -- 1
2572 (Proxy |> co) -- 2
2573 (bo |> sym axStar) -- 3
2574 (NoWay |> sym bc) -- 4
2575 :: Star
2576
2577 First, we flatten all the arguments (before simplifyArgsWorker), like so:
2578
2579 (forall j. j -> Type, co1 :: (forall j. j -> Type) ~
2580 (forall (j :: Star). (j |> axStar) -> Star)) -- 1
2581 (Proxy |> co, co2 :: (Proxy |> co) ~ (Proxy |> co)) -- 2
2582 (Bool |> sym axStar, co3 :: (Bool |> sym axStar) ~ (bo |> sym axStar)) -- 3
2583 (False |> sym bc, co4 :: (False |> sym bc) ~ (NoWay |> sym bc)) -- 4
2584
2585 Then we do the process described in Note [simplifyArgsWorker].
2586
2587 1. Lifting Type (the kind of the first arg) gives us a reflexive coercion, so we
2588 don't use it. But we do build a lifting context [k -> co1] (where co1 is a
2589 result of flattening an argument, written above).
2590
2591 2. Lifting k gives us co1, so the second argument becomes (Proxy |> co |> sym co1).
2592 This is not a dependent argument, so we don't extend the lifting context.
2593
2594 Now we need to deal with argument (3). After flattening, should we tack on a homogenizing
2595 coercion? The way we normally tell is to lift the kind of the binder.
2596 But here, the remainder of the kind of `a` that we're left with
2597 after processing two arguments is just `k`.
2598
2599 The way forward is look up k in the lifting context, getting co1. If we're at
2600 all well-typed, co1 will be a coercion between Π-types, with at least one binder.
2601 So, let's
2602 decompose co1 with decomposePiCos. This decomposition needs arguments to use
2603 to instantiate any kind parameters. Look at the type of co1. If we just
2604 decomposed it, we would end up with coercions whose types include j, which is
2605 out of scope here. Accordingly, decomposePiCos takes a list of types whose
2606 kinds are the *right-hand* types in the decomposed coercion. (See comments on
2607 decomposePiCos.) Because the flattened types have unflattened kinds (because
2608 flattening is homogeneous), passing the list of flattened types to decomposePiCos
2609 just won't do: later arguments' kinds won't be as expected. So we need to get
2610 the *unflattened* types to pass to decomposePiCos. We can do this easily enough
2611 by taking the kind of the argument coercions, passed in originally.
2612
2613 (Alternative 1: We could re-engineer decomposePiCos to deal with this situation.
2614 But that function is already gnarly, and taking the right-hand types is correct
2615 at its other call sites, which are much more common than this one.)
2616
2617 (Alternative 2: We could avoid calling decomposePiCos entirely, integrating its
2618 behavior into simplifyArgsWorker. This would work, I think, but then all of the
2619 complication of decomposePiCos would end up layered on top of all the complication
2620 here. Please, no.)
2621
2622 (Alternative 3: We could pass the unflattened arguments into simplifyArgsWorker
2623 so that we don't have to recreate them. But that would complicate the interface
2624 of this function to handle a very dark, dark corner case. Better to keep our
2625 demons to ourselves here instead of exposing them to callers. This decision is
2626 easily reversed if there is ever any performance trouble due to the call of
2627 coercionKind.)
2628
2629 So we now call
2630
2631 decomposePiCos co1
2632 (Pair (forall j. j -> Type) (forall (j :: Star). (j |> axStar) -> Star))
2633 [bo |> sym axStar, NoWay |> sym bc]
2634
2635 to get
2636
2637 co5 :: Star ~ Type
2638 co6 :: (j |> axStar) ~ (j |> co5), substituted to
2639 (bo |> sym axStar |> axStar) ~ (bo |> sym axStar |> co5)
2640 == bo ~ bo
2641 res_co :: Type ~ Star
2642
2643 We then use these casts on (the flattened) (3) and (4) to get
2644
2645 (Bool |> sym axStar |> co5 :: Type) -- (C3)
2646 (False |> sym bc |> co6 :: bo) -- (C4)
2647
2648 We can simplify to
2649
2650 Bool -- (C3)
2651 (False |> sym bc :: bo) -- (C4)
2652
2653 Of course, we still must do the processing in Note [simplifyArgsWorker] to finish
2654 the job. We thus want to recur. Our new function kind is the left-hand type of
2655 co1 (gotten, recall, by lifting the variable k that was the return kind of the
2656 original function). Why the left-hand type (as opposed to the right-hand type)?
2657 Because we have casted all the arguments according to decomposePiCos, which gets
2658 us from the right-hand type to the left-hand one. We thus recur with that new
2659 function kind, zapping our lifting context, because we have essentially applied
2660 it.
2661
2662 This recursive call returns ([Bool, False], [...], Refl). The Bool and False
2663 are the correct arguments we wish to return. But we must be careful about the
2664 result coercion: our new, flattened application will have kind Type, but we
2665 want to make sure that the result coercion casts this back to Star. (Why?
2666 Because we started with an application of kind Star, and flattening is homogeneous.)
2667
2668 So, we have to twiddle the result coercion appropriately.
2669
2670 Let's check whether this is well-typed. We know
2671
2672 a :: forall (k :: Type). k -> k
2673
2674 a (forall j. j -> Type) :: (forall j. j -> Type) -> forall j. j -> Type
2675
2676 a (forall j. j -> Type)
2677 Proxy
2678 :: forall j. j -> Type
2679
2680 a (forall j. j -> Type)
2681 Proxy
2682 Bool
2683 :: Bool -> Type
2684
2685 a (forall j. j -> Type)
2686 Proxy
2687 Bool
2688 False
2689 :: Type
2690
2691 a (forall j. j -> Type)
2692 Proxy
2693 Bool
2694 False
2695 |> res_co
2696 :: Star
2697
2698 as desired.
2699
2700 Whew.
2701
2702 -}
2703
2704
2705 -- This is shared between the flattener and the normaliser in FamInstEnv.
2706 -- See Note [simplifyArgsWorker]
2707 {-# INLINE simplifyArgsWorker #-}
2708 simplifyArgsWorker :: [TyCoBinder] -> Kind
2709 -- the binders & result kind (not a Π-type) of the function applied to the args
2710 -- list of binders can be shorter or longer than the list of args
2711 -> TyCoVarSet -- free vars of the args
2712 -> [Role] -- list of roles, r
2713 -> [(Type, Coercion)] -- flattened type arguments, arg
2714 -- each comes with the coercion used to flatten it,
2715 -- with co :: flattened_type ~ original_type
2716 -> ([Type], [Coercion], CoercionN)
2717 -- Returns (xis, cos, res_co), where each co :: xi ~ arg,
2718 -- and res_co :: kind (f xis) ~ kind (f tys), where f is the function applied to the args
2719 -- Precondition: if f :: forall bndrs. inner_ki (where bndrs and inner_ki are passed in),
2720 -- then (f orig_tys) is well kinded. Note that (f flattened_tys) might *not* be well-kinded.
2721 -- Massaging the flattened_tys in order to make (f flattened_tys) well-kinded is what this
2722 -- function is all about. That is, (f xis), where xis are the returned arguments, *is*
2723 -- well kinded.
2724 simplifyArgsWorker orig_ki_binders orig_inner_ki orig_fvs
2725 orig_roles orig_simplified_args
2726 = go [] [] orig_lc orig_ki_binders orig_inner_ki orig_roles orig_simplified_args
2727 where
2728 orig_lc = emptyLiftingContext $ mkInScopeSet $ orig_fvs
2729
2730 go :: [Type] -- Xis accumulator, in reverse order
2731 -> [Coercion] -- Coercions accumulator, in reverse order
2732 -- These are in 1-to-1 correspondence
2733 -> LiftingContext -- mapping from tyvars to flattening coercions
2734 -> [TyCoBinder] -- Unsubsted binders of function's kind
2735 -> Kind -- Unsubsted result kind of function (not a Pi-type)
2736 -> [Role] -- Roles at which to flatten these ...
2737 -> [(Type, Coercion)] -- flattened arguments, with their flattening coercions
2738 -> ([Type], [Coercion], CoercionN)
2739 go acc_xis acc_cos lc binders inner_ki _ []
2740 = (reverse acc_xis, reverse acc_cos, kind_co)
2741 where
2742 final_kind = mkTyCoPiTys binders inner_ki
2743 kind_co = liftCoSubst Nominal lc final_kind
2744
2745 go acc_xis acc_cos lc (binder:binders) inner_ki (role:roles) ((xi,co):args)
2746 = -- By Note [Flattening] in TcFlatten invariant (F2),
2747 -- tcTypeKind(xi) = tcTypeKind(ty). But, it's possible that xi will be
2748 -- used as an argument to a function whose kind is different, if
2749 -- earlier arguments have been flattened to new types. We thus
2750 -- need a coercion (kind_co :: old_kind ~ new_kind).
2751 --
2752 -- The bangs here have been observed to improve performance
2753 -- significantly in optimized builds.
2754 let kind_co = mkSymCo $
2755 liftCoSubst Nominal lc (tyCoBinderType binder)
2756 !casted_xi = xi `mkCastTy` kind_co
2757 casted_co = mkCoherenceLeftCo role xi kind_co co
2758
2759 -- now, extend the lifting context with the new binding
2760 !new_lc | Just tv <- tyCoBinderVar_maybe binder
2761 = extendLiftingContextAndInScope lc tv casted_co
2762 | otherwise
2763 = lc
2764 in
2765 go (casted_xi : acc_xis)
2766 (casted_co : acc_cos)
2767 new_lc
2768 binders
2769 inner_ki
2770 roles
2771 args
2772
2773
2774 -- See Note [Last case in simplifyArgsWorker]
2775 go acc_xis acc_cos lc [] inner_ki roles args
2776 | Just k <- getTyVar_maybe inner_ki
2777 , Just co1 <- liftCoSubstTyVar lc Nominal k
2778 = let co1_kind = coercionKind co1
2779 unflattened_tys = map (pSnd . coercionKind . snd) args
2780 (arg_cos, res_co) = decomposePiCos co1 co1_kind unflattened_tys
2781 casted_args = ASSERT2( equalLength args arg_cos
2782 , ppr args $$ ppr arg_cos )
2783 [ (casted_xi, casted_co)
2784 | ((xi, co), arg_co, role) <- zip3 args arg_cos roles
2785 , let casted_xi = xi `mkCastTy` arg_co
2786 casted_co = mkCoherenceLeftCo role xi arg_co co ]
2787 -- In general decomposePiCos can return fewer cos than tys,
2788 -- but not here; because we're well typed, there will be enough
2789 -- binders. Note that decomposePiCos does substitutions, so even
2790 -- if the original substitution results in something ending with
2791 -- ... -> k, that k will be substituted to perhaps reveal more
2792 -- binders.
2793 zapped_lc = zapLiftingContext lc
2794 Pair flattened_kind _ = co1_kind
2795 (bndrs, new_inner) = splitPiTys flattened_kind
2796
2797 (xis_out, cos_out, res_co_out)
2798 = go acc_xis acc_cos zapped_lc bndrs new_inner roles casted_args
2799 in
2800 (xis_out, cos_out, res_co_out `mkTransCo` res_co)
2801
2802 go _ _ _ _ _ _ _ = panic
2803 "simplifyArgsWorker wandered into deeper water than usual"
2804 -- This debug information is commented out because leaving it in
2805 -- causes a ~2% increase in allocations in T9872d.
2806 -- That's independent of the analagous case in flatten_args_fast
2807 -- in TcFlatten:
2808 -- each of these causes a 2% increase on its own, so commenting them
2809 -- both out gives a 4% decrease in T9872d.
2810 {-
2811
2812 (vcat [ppr orig_binders,
2813 ppr orig_inner_ki,
2814 ppr (take 10 orig_roles), -- often infinite!
2815 ppr orig_tys])
2816 -}