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