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