ff0c9c5e9ef87a47f944ccd933dda508f46b5cbb
[ghc.git] / compiler / types / Coercion.hs
1 {-
2 (c) The University of Glasgow 2006
3 -}
4
5 {-# LANGUAGE RankNTypes, CPP, MultiWayIf, FlexibleContexts #-}
6
7 -- | Module for (a) type kinds and (b) type coercions,
8 -- as used in System FC. See 'CoreSyn.Expr' for
9 -- more on System FC and how coercions fit into it.
10 --
11 module Coercion (
12 -- * Main data type
13 Coercion, CoercionN, CoercionR, CoercionP, MCoercion(..), MCoercionR,
14 UnivCoProvenance, CoercionHole(..), coHoleCoVar, setCoHoleCoVar,
15 LeftOrRight(..),
16 Var, CoVar, TyCoVar,
17 Role(..), ltRole,
18
19 -- ** Functions over coercions
20 coVarTypes, coVarKind, coVarKindsTypesRole, coVarRole,
21 coercionType, coercionKind, coercionKinds,
22 mkCoercionType,
23 coercionRole, coercionKindRole,
24
25 -- ** Constructing coercions
26 mkGReflCo, mkReflCo, mkRepReflCo, mkNomReflCo,
27 mkCoVarCo, mkCoVarCos,
28 mkAxInstCo, mkUnbranchedAxInstCo,
29 mkAxInstRHS, mkUnbranchedAxInstRHS,
30 mkAxInstLHS, mkUnbranchedAxInstLHS,
31 mkPiCo, mkPiCos, mkCoCast,
32 mkSymCo, mkTransCo,
33 mkNthCo, nthCoRole, mkLRCo,
34 mkInstCo, mkAppCo, mkAppCos, mkTyConAppCo, mkFunCo,
35 mkForAllCo, mkForAllCos, mkHomoForAllCos,
36 mkPhantomCo,
37 mkUnsafeCo, mkHoleCo, mkUnivCo, mkSubCo,
38 mkAxiomInstCo, mkProofIrrelCo,
39 downgradeRole, maybeSubCo, mkAxiomRuleCo,
40 mkGReflRightCo, mkGReflLeftCo, mkCoherenceLeftCo, mkCoherenceRightCo,
41 mkKindCo, castCoercionKind, castCoercionKindI,
42
43 mkHeteroCoercionType,
44
45 -- ** Decomposition
46 instNewTyCon_maybe,
47
48 NormaliseStepper, NormaliseStepResult(..), composeSteppers,
49 mapStepResult, unwrapNewTypeStepper,
50 topNormaliseNewType_maybe, topNormaliseTypeX,
51
52 decomposeCo, decomposeFunCo, decomposePiCos, getCoVar_maybe,
53 splitTyConAppCo_maybe,
54 splitAppCo_maybe,
55 splitFunCo_maybe,
56 splitForAllCo_maybe,
57 splitForAllCo_ty_maybe, splitForAllCo_co_maybe,
58
59 nthRole, tyConRolesX, tyConRolesRepresentational, setNominalRole_maybe,
60
61 pickLR,
62
63 isGReflCo, isReflCo, isReflCo_maybe, isGReflCo_maybe, isReflexiveCo, isReflexiveCo_maybe,
64 isReflCoVar_maybe,
65
66 -- ** Coercion variables
67 mkCoVar, isCoVar, coVarName, setCoVarName, setCoVarUnique,
68 isCoVar_maybe,
69
70 -- ** Free variables
71 tyCoVarsOfCo, tyCoVarsOfCos, coVarsOfCo,
72 tyCoFVsOfCo, tyCoFVsOfCos, tyCoVarsOfCoDSet,
73 coercionSize,
74
75 -- ** Substitution
76 CvSubstEnv, emptyCvSubstEnv,
77 lookupCoVar,
78 substCo, substCos, substCoVar, substCoVars, substCoWith,
79 substCoVarBndr,
80 extendTvSubstAndInScope, getCvSubstEnv,
81
82 -- ** Lifting
83 liftCoSubst, liftCoSubstTyVar, liftCoSubstWith, liftCoSubstWithEx,
84 emptyLiftingContext, extendLiftingContext, extendLiftingContextAndInScope,
85 liftCoSubstVarBndrUsing, isMappedByLC,
86
87 mkSubstLiftingContext, zapLiftingContext,
88 substForAllCoBndrUsingLC, lcTCvSubst, lcInScopeSet,
89
90 LiftCoEnv, LiftingContext(..), liftEnvSubstLeft, liftEnvSubstRight,
91 substRightCo, substLeftCo, swapLiftCoEnv, lcSubstLeft, lcSubstRight,
92
93 -- ** Comparison
94 eqCoercion, eqCoercionX,
95
96 -- ** Forcing evaluation of coercions
97 seqCo,
98
99 -- * Pretty-printing
100 pprCo, pprParendCo,
101 pprCoAxiom, pprCoAxBranch, pprCoAxBranchLHS,
102 pprCoAxBranchUser, tidyCoAxBndrsForUser,
103 etaExpandCoAxBranch,
104
105 -- * Tidying
106 tidyCo, tidyCos,
107
108 -- * Other
109 promoteCoercion, buildCoercion
110 ) where
111
112 #include "HsVersions.h"
113
114 import {-# SOURCE #-} ToIface (toIfaceTyCon, tidyToIfaceTcArgs)
115
116 import GhcPrelude
117
118 import IfaceType
119 import TyCoRep
120 import Type
121 import TyCon
122 import CoAxiom
123 import Var
124 import VarEnv
125 import VarSet
126 import Name hiding ( varName )
127 import Util
128 import BasicTypes
129 import Outputable
130 import Unique
131 import Pair
132 import SrcLoc
133 import PrelNames
134 import TysPrim ( eqPhantPrimTyCon )
135 import ListSetOps
136 import Maybes
137 import UniqFM
138
139 import Control.Monad (foldM, zipWithM)
140 import Data.Function ( on )
141 import Data.Char( isDigit )
142
143 {-
144 %************************************************************************
145 %* *
146 -- The coercion arguments always *precisely* saturate
147 -- arity of (that branch of) the CoAxiom. If there are
148 -- any left over, we use AppCo. See
149 -- See [Coercion axioms applied to coercions] in TyCoRep
150
151 \subsection{Coercion variables}
152 %* *
153 %************************************************************************
154 -}
155
156 coVarName :: CoVar -> Name
157 coVarName = varName
158
159 setCoVarUnique :: CoVar -> Unique -> CoVar
160 setCoVarUnique = setVarUnique
161
162 setCoVarName :: CoVar -> Name -> CoVar
163 setCoVarName = setVarName
164
165 {-
166 %************************************************************************
167 %* *
168 Pretty-printing CoAxioms
169 %* *
170 %************************************************************************
171
172 Defined here to avoid module loops. CoAxiom is loaded very early on.
173
174 -}
175
176 etaExpandCoAxBranch :: CoAxBranch -> ([TyVar], [Type], Type)
177 -- Return the (tvs,lhs,rhs) after eta-expanding,
178 -- to the way in which the axiom was originally written
179 -- See Note [Eta reduction for data families] in CoAxiom
180 etaExpandCoAxBranch (CoAxBranch { cab_tvs = tvs
181 , cab_eta_tvs = eta_tvs
182 , cab_lhs = lhs
183 , cab_rhs = rhs })
184 -- ToDo: what about eta_cvs?
185 = (tvs ++ eta_tvs, lhs ++ eta_tys, mkAppTys rhs eta_tys)
186 where
187 eta_tys = mkTyVarTys eta_tvs
188
189 pprCoAxiom :: CoAxiom br -> SDoc
190 -- Used in debug-printing only
191 pprCoAxiom ax@(CoAxiom { co_ax_tc = tc, co_ax_branches = branches })
192 = hang (text "axiom" <+> ppr ax <+> dcolon)
193 2 (vcat (map (pprCoAxBranchUser tc) (fromBranches branches)))
194
195 pprCoAxBranchUser :: TyCon -> CoAxBranch -> SDoc
196 -- Used when printing injectivity errors (FamInst.makeInjectivityErrors)
197 -- and inaccessible branches (TcValidity.inaccessibleCoAxBranch)
198 -- This happens in error messages: don't print the RHS of a data
199 -- family axiom, which is meaningless to a user
200 pprCoAxBranchUser tc br
201 | isDataFamilyTyCon tc = pprCoAxBranchLHS tc br
202 | otherwise = pprCoAxBranch tc br
203
204 pprCoAxBranchLHS :: TyCon -> CoAxBranch -> SDoc
205 -- Print the family-instance equation when reporting
206 -- a conflict between equations (FamInst.conflictInstErr)
207 -- For type families the RHS is important; for data families not so.
208 -- Indeed for data families the RHS is a mysterious internal
209 -- type constructor, so we suppress it (Trac #14179)
210 -- See FamInstEnv Note [Family instance overlap conflicts]
211 pprCoAxBranchLHS = ppr_co_ax_branch pp_rhs
212 where
213 pp_rhs _ _ = empty
214
215 pprCoAxBranch :: TyCon -> CoAxBranch -> SDoc
216 pprCoAxBranch = ppr_co_ax_branch ppr_rhs
217 where
218 ppr_rhs env rhs = equals <+> pprPrecTypeX env topPrec rhs
219
220 ppr_co_ax_branch :: (TidyEnv -> Type -> SDoc)
221 -> TyCon -> CoAxBranch -> SDoc
222 ppr_co_ax_branch ppr_rhs fam_tc branch
223 = foldr1 (flip hangNotEmpty 2)
224 [ pprUserForAll (mkTyCoVarBinders Inferred bndrs')
225 -- See Note [Printing foralls in type family instances] in IfaceType
226 , pp_lhs <+> ppr_rhs tidy_env ee_rhs
227 , text "-- Defined" <+> pp_loc ]
228 where
229 loc = coAxBranchSpan branch
230 pp_loc | isGoodSrcSpan loc = text "at" <+> ppr (srcSpanStart loc)
231 | otherwise = text "in" <+> ppr loc
232
233 -- Eta-expand LHS and RHS types, because sometimes data family
234 -- instances are eta-reduced.
235 -- See Note [Eta reduction for data families] in FamInstEnv.
236 (ee_tvs, ee_lhs, ee_rhs) = etaExpandCoAxBranch branch
237
238 pp_lhs = pprIfaceTypeApp topPrec (toIfaceTyCon fam_tc)
239 (tidyToIfaceTcArgs tidy_env fam_tc ee_lhs)
240
241 (tidy_env, bndrs') = tidyCoAxBndrsForUser emptyTidyEnv ee_tvs
242
243 tidyCoAxBndrsForUser :: TidyEnv -> [Var] -> (TidyEnv, [Var])
244 -- Tidy wildcards "_1", "_2" to "_", and do not return them
245 -- in the list of binders to be printed
246 -- This is so that in error messages we see
247 -- forall a. F _ [a] _ = ...
248 -- rather than
249 -- forall a _1 _2. F _1 [a] _2 = ...
250 --
251 -- This is a rather disgusting function
252 tidyCoAxBndrsForUser init_env tcvs
253 = (tidy_env, reverse tidy_bndrs)
254 where
255 (tidy_env, tidy_bndrs) = foldl tidy_one (init_env, []) tcvs
256
257 tidy_one (env@(occ_env, subst), rev_bndrs') bndr
258 | is_wildcard bndr = (env_wild, rev_bndrs')
259 | otherwise = (env', bndr' : rev_bndrs')
260 where
261 (env', bndr') = tidyVarBndr env bndr
262 env_wild = (occ_env, extendVarEnv subst bndr wild_bndr)
263 wild_bndr = setVarName bndr $
264 tidyNameOcc (varName bndr) (mkTyVarOcc "_")
265 -- Tidy the binder to "_"
266
267 is_wildcard :: Var -> Bool
268 is_wildcard tv = case occNameString (getOccName tv) of
269 ('_' : rest) -> all isDigit rest
270 _ -> False
271
272 {-
273 %************************************************************************
274 %* *
275 Destructing coercions
276 %* *
277 %************************************************************************
278
279 Note [Function coercions]
280 ~~~~~~~~~~~~~~~~~~~~~~~~~
281 Remember that
282 (->) :: forall r1 r2. TYPE r1 -> TYPE r2 -> TYPE LiftedRep
283
284 Hence
285 FunCo r co1 co2 :: (s1->t1) ~r (s2->t2)
286 is short for
287 TyConAppCo (->) co_rep1 co_rep2 co1 co2
288 where co_rep1, co_rep2 are the coercions on the representations.
289 -}
290
291
292 -- | This breaks a 'Coercion' with type @T A B C ~ T D E F@ into
293 -- a list of 'Coercion's of kinds @A ~ D@, @B ~ E@ and @E ~ F@. Hence:
294 --
295 -- > decomposeCo 3 c [r1, r2, r3] = [nth r1 0 c, nth r2 1 c, nth r3 2 c]
296 decomposeCo :: Arity -> Coercion
297 -> [Role] -- the roles of the output coercions
298 -- this must have at least as many
299 -- entries as the Arity provided
300 -> [Coercion]
301 decomposeCo arity co rs
302 = [mkNthCo r n co | (n,r) <- [0..(arity-1)] `zip` rs ]
303 -- Remember, Nth is zero-indexed
304
305 decomposeFunCo :: HasDebugCallStack
306 => Role -- Role of the input coercion
307 -> Coercion -- Input coercion
308 -> (Coercion, Coercion)
309 -- Expects co :: (s1 -> t1) ~ (s2 -> t2)
310 -- Returns (co1 :: s1~s2, co2 :: t1~t2)
311 -- See Note [Function coercions] for the "2" and "3"
312 decomposeFunCo r co = ASSERT2( all_ok, ppr co )
313 (mkNthCo r 2 co, mkNthCo r 3 co)
314 where
315 Pair s1t1 s2t2 = coercionKind co
316 all_ok = isFunTy s1t1 && isFunTy s2t2
317
318 {- Note [Pushing a coercion into a pi-type]
319 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
320 Suppose we have this:
321 (f |> co) t1 .. tn
322 Then we want to push the coercion into the arguments, so as to make
323 progress. For example of why you might want to do so, see Note
324 [Respecting definitional equality] in TyCoRep.
325
326 This is done by decomposePiCos. Specifically, if
327 decomposePiCos co [t1,..,tn] = ([co1,...,cok], cor)
328 then
329 (f |> co) t1 .. tn = (f (t1 |> co1) ... (tk |> cok)) |> cor) t(k+1) ... tn
330
331 Notes:
332
333 * k can be smaller than n! That is decomposePiCos can return *fewer*
334 coercions than there are arguments (ie k < n), if the kind provided
335 doesn't have enough binders.
336
337 * If there is a type error, we might see
338 (f |> co) t1
339 where co :: (forall a. ty) ~ (ty1 -> ty2)
340 Here 'co' is insoluble, but we don't want to crash in decoposePiCos.
341 So decomposePiCos carefully tests both sides of the coercion to check
342 they are both foralls or both arrows. Not doing this caused Trac #15343.
343 -}
344
345 decomposePiCos :: HasDebugCallStack
346 => CoercionN -> Pair Type -- Coercion and its kind
347 -> [Type]
348 -> ([CoercionN], CoercionN)
349 -- See Note [Pushing a coercion into a pi-type]
350 decomposePiCos orig_co (Pair orig_k1 orig_k2) orig_args
351 = go [] (orig_subst,orig_k1) orig_co (orig_subst,orig_k2) orig_args
352 where
353 orig_subst = mkEmptyTCvSubst $ mkInScopeSet $
354 tyCoVarsOfTypes orig_args `unionVarSet` tyCoVarsOfCo orig_co
355
356 go :: [CoercionN] -- accumulator for argument coercions, reversed
357 -> (TCvSubst,Kind) -- Lhs kind of coercion
358 -> CoercionN -- coercion originally applied to the function
359 -> (TCvSubst,Kind) -- Rhs kind of coercion
360 -> [Type] -- Arguments to that function
361 -> ([CoercionN], Coercion)
362 -- Invariant: co :: subst1(k2) ~ subst2(k2)
363
364 go acc_arg_cos (subst1,k1) co (subst2,k2) (ty:tys)
365 | Just (a, t1) <- splitForAllTy_maybe k1
366 , Just (b, t2) <- splitForAllTy_maybe k2
367 -- know co :: (forall a:s1.t1) ~ (forall b:s2.t2)
368 -- function :: forall a:s1.t1 (the function is not passed to decomposePiCos)
369 -- a :: s1
370 -- b :: s2
371 -- ty :: s2
372 -- need arg_co :: s2 ~ s1
373 -- res_co :: t1[ty |> arg_co / a] ~ t2[ty / b]
374 = let arg_co = mkNthCo Nominal 0 (mkSymCo co)
375 res_co = mkInstCo co (mkGReflLeftCo Nominal ty arg_co)
376 subst1' = extendTCvSubst subst1 a (ty `CastTy` arg_co)
377 subst2' = extendTCvSubst subst2 b ty
378 in
379 go (arg_co : acc_arg_cos) (subst1', t1) res_co (subst2', t2) tys
380
381 | Just (_s1, t1) <- splitFunTy_maybe k1
382 , Just (_s2, t2) <- splitFunTy_maybe k2
383 -- know co :: (s1 -> t1) ~ (s2 -> t2)
384 -- function :: s1 -> t1
385 -- ty :: s2
386 -- need arg_co :: s2 ~ s1
387 -- res_co :: t1 ~ t2
388 = let (sym_arg_co, res_co) = decomposeFunCo Nominal co
389 arg_co = mkSymCo sym_arg_co
390 in
391 go (arg_co : acc_arg_cos) (subst1,t1) res_co (subst2,t2) tys
392
393 | not (isEmptyTCvSubst subst1) || not (isEmptyTCvSubst subst2)
394 = go acc_arg_cos (zapTCvSubst subst1, substTy subst1 k1)
395 co
396 (zapTCvSubst subst2, substTy subst1 k2)
397 (ty:tys)
398
399 -- tys might not be empty, if the left-hand type of the original coercion
400 -- didn't have enough binders
401 go acc_arg_cos _ki1 co _ki2 _tys = (reverse acc_arg_cos, co)
402
403 -- | Attempts to obtain the type variable underlying a 'Coercion'
404 getCoVar_maybe :: Coercion -> Maybe CoVar
405 getCoVar_maybe (CoVarCo cv) = Just cv
406 getCoVar_maybe _ = Nothing
407
408 -- | Attempts to tease a coercion apart into a type constructor and the application
409 -- of a number of coercion arguments to that constructor
410 splitTyConAppCo_maybe :: Coercion -> Maybe (TyCon, [Coercion])
411 splitTyConAppCo_maybe co
412 | Just (ty, r) <- isReflCo_maybe co
413 = do { (tc, tys) <- splitTyConApp_maybe ty
414 ; let args = zipWith mkReflCo (tyConRolesX r tc) tys
415 ; return (tc, args) }
416 splitTyConAppCo_maybe (TyConAppCo _ tc cos) = Just (tc, cos)
417 splitTyConAppCo_maybe (FunCo _ arg res) = Just (funTyCon, cos)
418 where cos = [mkRuntimeRepCo arg, mkRuntimeRepCo res, arg, res]
419 splitTyConAppCo_maybe _ = Nothing
420
421 -- first result has role equal to input; third result is Nominal
422 splitAppCo_maybe :: Coercion -> Maybe (Coercion, Coercion)
423 -- ^ Attempt to take a coercion application apart.
424 splitAppCo_maybe (AppCo co arg) = Just (co, arg)
425 splitAppCo_maybe (TyConAppCo r tc args)
426 | args `lengthExceeds` tyConArity tc
427 , Just (args', arg') <- snocView args
428 = Just ( mkTyConAppCo r tc args', arg' )
429
430 | mightBeUnsaturatedTyCon tc
431 -- Never create unsaturated type family apps!
432 , Just (args', arg') <- snocView args
433 , Just arg'' <- setNominalRole_maybe (nthRole r tc (length args')) arg'
434 = Just ( mkTyConAppCo r tc args', arg'' )
435 -- Use mkTyConAppCo to preserve the invariant
436 -- that identity coercions are always represented by Refl
437
438 splitAppCo_maybe co
439 | Just (ty, r) <- isReflCo_maybe co
440 , Just (ty1, ty2) <- splitAppTy_maybe ty
441 = Just (mkReflCo r ty1, mkNomReflCo ty2)
442 splitAppCo_maybe _ = Nothing
443
444 splitFunCo_maybe :: Coercion -> Maybe (Coercion, Coercion)
445 splitFunCo_maybe (FunCo _ arg res) = Just (arg, res)
446 splitFunCo_maybe _ = Nothing
447
448 splitForAllCo_maybe :: Coercion -> Maybe (TyCoVar, Coercion, Coercion)
449 splitForAllCo_maybe (ForAllCo tv k_co co) = Just (tv, k_co, co)
450 splitForAllCo_maybe _ = Nothing
451
452 -- | Like 'splitForAllCo_maybe', but only returns Just for tyvar binder
453 splitForAllCo_ty_maybe :: Coercion -> Maybe (TyVar, Coercion, Coercion)
454 splitForAllCo_ty_maybe (ForAllCo tv k_co co)
455 | isTyVar tv = Just (tv, k_co, co)
456 splitForAllCo_ty_maybe _ = Nothing
457
458 -- | Like 'splitForAllCo_maybe', but only returns Just for covar binder
459 splitForAllCo_co_maybe :: Coercion -> Maybe (CoVar, Coercion, Coercion)
460 splitForAllCo_co_maybe (ForAllCo cv k_co co)
461 | isCoVar cv = Just (cv, k_co, co)
462 splitForAllCo_co_maybe _ = Nothing
463
464 -------------------------------------------------------
465 -- and some coercion kind stuff
466
467 coVarTypes :: HasDebugCallStack => CoVar -> Pair Type
468 coVarTypes cv
469 | (_, _, ty1, ty2, _) <- coVarKindsTypesRole cv
470 = Pair ty1 ty2
471
472 coVarKindsTypesRole :: HasDebugCallStack => CoVar -> (Kind,Kind,Type,Type,Role)
473 coVarKindsTypesRole cv
474 | Just (tc, [k1,k2,ty1,ty2]) <- splitTyConApp_maybe (varType cv)
475 = let role
476 | tc `hasKey` eqPrimTyConKey = Nominal
477 | tc `hasKey` eqReprPrimTyConKey = Representational
478 | otherwise = panic "coVarKindsTypesRole"
479 in (k1,k2,ty1,ty2,role)
480 | otherwise = pprPanic "coVarKindsTypesRole, non coercion variable"
481 (ppr cv $$ ppr (varType cv))
482
483 coVarKind :: CoVar -> Type
484 coVarKind cv
485 = ASSERT( isCoVar cv )
486 varType cv
487
488 coVarRole :: CoVar -> Role
489 coVarRole cv
490 | tc `hasKey` eqPrimTyConKey
491 = Nominal
492 | tc `hasKey` eqReprPrimTyConKey
493 = Representational
494 | otherwise
495 = pprPanic "coVarRole: unknown tycon" (ppr cv <+> dcolon <+> ppr (varType cv))
496
497 where
498 tc = case tyConAppTyCon_maybe (varType cv) of
499 Just tc0 -> tc0
500 Nothing -> pprPanic "coVarRole: not tyconapp" (ppr cv)
501
502 -- | Makes a coercion type from two types: the types whose equality
503 -- is proven by the relevant 'Coercion'
504 mkCoercionType :: Role -> Type -> Type -> Type
505 mkCoercionType Nominal = mkPrimEqPred
506 mkCoercionType Representational = mkReprPrimEqPred
507 mkCoercionType Phantom = \ty1 ty2 ->
508 let ki1 = typeKind ty1
509 ki2 = typeKind ty2
510 in
511 TyConApp eqPhantPrimTyCon [ki1, ki2, ty1, ty2]
512
513 mkHeteroCoercionType :: Role -> Kind -> Kind -> Type -> Type -> Type
514 mkHeteroCoercionType Nominal = mkHeteroPrimEqPred
515 mkHeteroCoercionType Representational = mkHeteroReprPrimEqPred
516 mkHeteroCoercionType Phantom = panic "mkHeteroCoercionType"
517
518 -- | Given a coercion @co1 :: (a :: TYPE r1) ~ (b :: TYPE r2)@,
519 -- produce a coercion @rep_co :: r1 ~ r2@.
520 mkRuntimeRepCo :: HasDebugCallStack => Coercion -> Coercion
521 mkRuntimeRepCo co
522 = mkNthCo Nominal 0 kind_co
523 where
524 kind_co = mkKindCo co -- kind_co :: TYPE r1 ~ TYPE r2
525 -- (up to silliness with Constraint)
526
527 isReflCoVar_maybe :: Var -> Maybe Coercion
528 -- If cv :: t~t then isReflCoVar_maybe cv = Just (Refl t)
529 -- Works on all kinds of Vars, not just CoVars
530 isReflCoVar_maybe cv
531 | isCoVar cv
532 , Pair ty1 ty2 <- coVarTypes cv
533 , ty1 `eqType` ty2
534 = Just (mkReflCo (coVarRole cv) ty1)
535 | otherwise
536 = Nothing
537
538 -- | Tests if this coercion is obviously a generalized reflexive coercion.
539 -- Guaranteed to work very quickly.
540 isGReflCo :: Coercion -> Bool
541 isGReflCo (GRefl{}) = True
542 isGReflCo (Refl{}) = True -- Refl ty == GRefl N ty MRefl
543 isGReflCo _ = False
544
545 -- | Tests if this MCoercion is obviously generalized reflexive
546 -- Guaranteed to work very quickly.
547 isGReflMCo :: MCoercion -> Bool
548 isGReflMCo MRefl = True
549 isGReflMCo (MCo co) | isGReflCo co = True
550 isGReflMCo _ = False
551
552 -- | Tests if this coercion is obviously reflexive. Guaranteed to work
553 -- very quickly. Sometimes a coercion can be reflexive, but not obviously
554 -- so. c.f. 'isReflexiveCo'
555 isReflCo :: Coercion -> Bool
556 isReflCo (Refl{}) = True
557 isReflCo (GRefl _ _ mco) | isGReflMCo mco = True
558 isReflCo _ = False
559
560 -- | Returns the type coerced if this coercion is a generalized reflexive
561 -- coercion. Guaranteed to work very quickly.
562 isGReflCo_maybe :: Coercion -> Maybe (Type, Role)
563 isGReflCo_maybe (GRefl r ty _) = Just (ty, r)
564 isGReflCo_maybe (Refl ty) = Just (ty, Nominal)
565 isGReflCo_maybe _ = Nothing
566
567 -- | Returns the type coerced if this coercion is reflexive. Guaranteed
568 -- to work very quickly. Sometimes a coercion can be reflexive, but not
569 -- obviously so. c.f. 'isReflexiveCo_maybe'
570 isReflCo_maybe :: Coercion -> Maybe (Type, Role)
571 isReflCo_maybe (Refl ty) = Just (ty, Nominal)
572 isReflCo_maybe (GRefl r ty mco) | isGReflMCo mco = Just (ty, r)
573 isReflCo_maybe _ = Nothing
574
575 -- | Slowly checks if the coercion is reflexive. Don't call this in a loop,
576 -- as it walks over the entire coercion.
577 isReflexiveCo :: Coercion -> Bool
578 isReflexiveCo = isJust . isReflexiveCo_maybe
579
580 -- | Extracts the coerced type from a reflexive coercion. This potentially
581 -- walks over the entire coercion, so avoid doing this in a loop.
582 isReflexiveCo_maybe :: Coercion -> Maybe (Type, Role)
583 isReflexiveCo_maybe (Refl ty) = Just (ty, Nominal)
584 isReflexiveCo_maybe (GRefl r ty mco) | isGReflMCo mco = Just (ty, r)
585 isReflexiveCo_maybe co
586 | ty1 `eqType` ty2
587 = Just (ty1, r)
588 | otherwise
589 = Nothing
590 where (Pair ty1 ty2, r) = coercionKindRole co
591
592 {-
593 %************************************************************************
594 %* *
595 Building coercions
596 %* *
597 %************************************************************************
598
599 These "smart constructors" maintain the invariants listed in the definition
600 of Coercion, and they perform very basic optimizations.
601
602 Note [Role twiddling functions]
603 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
604
605 There are a plethora of functions for twiddling roles:
606
607 mkSubCo: Requires a nominal input coercion and always produces a
608 representational output. This is used when you (the programmer) are sure you
609 know exactly that role you have and what you want.
610
611 downgradeRole_maybe: This function takes both the input role and the output role
612 as parameters. (The *output* role comes first!) It can only *downgrade* a
613 role -- that is, change it from N to R or P, or from R to P. This one-way
614 behavior is why there is the "_maybe". If an upgrade is requested, this
615 function produces Nothing. This is used when you need to change the role of a
616 coercion, but you're not sure (as you're writing the code) of which roles are
617 involved.
618
619 This function could have been written using coercionRole to ascertain the role
620 of the input. But, that function is recursive, and the caller of downgradeRole_maybe
621 often knows the input role. So, this is more efficient.
622
623 downgradeRole: This is just like downgradeRole_maybe, but it panics if the
624 conversion isn't a downgrade.
625
626 setNominalRole_maybe: This is the only function that can *upgrade* a coercion.
627 The result (if it exists) is always Nominal. The input can be at any role. It
628 works on a "best effort" basis, as it should never be strictly necessary to
629 upgrade a coercion during compilation. It is currently only used within GHC in
630 splitAppCo_maybe. In order to be a proper inverse of mkAppCo, the second
631 coercion that splitAppCo_maybe returns must be nominal. But, it's conceivable
632 that splitAppCo_maybe is operating over a TyConAppCo that uses a
633 representational coercion. Hence the need for setNominalRole_maybe.
634 splitAppCo_maybe, in turn, is used only within coercion optimization -- thus,
635 it is not absolutely critical that setNominalRole_maybe be complete.
636
637 Note that setNominalRole_maybe will never upgrade a phantom UnivCo. Phantom
638 UnivCos are perfectly type-safe, whereas representational and nominal ones are
639 not. Indeed, `unsafeCoerce` is implemented via a representational UnivCo.
640 (Nominal ones are no worse than representational ones, so this function *will*
641 change a UnivCo Representational to a UnivCo Nominal.)
642
643 Conal Elliott also came across a need for this function while working with the
644 GHC API, as he was decomposing Core casts. The Core casts use representational
645 coercions, as they must, but his use case required nominal coercions (he was
646 building a GADT). So, that's why this function is exported from this module.
647
648 One might ask: shouldn't downgradeRole_maybe just use setNominalRole_maybe as
649 appropriate? I (Richard E.) have decided not to do this, because upgrading a
650 role is bizarre and a caller should have to ask for this behavior explicitly.
651
652 -}
653
654 -- | Make a generalized reflexive coercion
655 mkGReflCo :: Role -> Type -> MCoercionN -> Coercion
656 mkGReflCo r ty mco
657 | isGReflMCo mco = if r == Nominal then Refl ty
658 else GRefl r ty MRefl
659 | otherwise = GRefl r ty mco
660
661 -- | Make a reflexive coercion
662 mkReflCo :: Role -> Type -> Coercion
663 mkReflCo Nominal ty = Refl ty
664 mkReflCo r ty = GRefl r ty MRefl
665
666 -- | Make a representational reflexive coercion
667 mkRepReflCo :: Type -> Coercion
668 mkRepReflCo ty = GRefl Representational ty MRefl
669
670 -- | Make a nominal reflexive coercion
671 mkNomReflCo :: Type -> Coercion
672 mkNomReflCo = Refl
673
674 -- | Apply a type constructor to a list of coercions. It is the
675 -- caller's responsibility to get the roles correct on argument coercions.
676 mkTyConAppCo :: HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
677 mkTyConAppCo r tc cos
678 | tc `hasKey` funTyConKey
679 , [_rep1, _rep2, co1, co2] <- cos -- See Note [Function coercions]
680 = -- (a :: TYPE ra) -> (b :: TYPE rb) ~ (c :: TYPE rc) -> (d :: TYPE rd)
681 -- rep1 :: ra ~ rc rep2 :: rb ~ rd
682 -- co1 :: a ~ c co2 :: b ~ d
683 mkFunCo r co1 co2
684
685 -- Expand type synonyms
686 | Just (tv_co_prs, rhs_ty, leftover_cos) <- expandSynTyCon_maybe tc cos
687 = mkAppCos (liftCoSubst r (mkLiftingContext tv_co_prs) rhs_ty) leftover_cos
688
689 | Just tys_roles <- traverse isReflCo_maybe cos
690 = mkReflCo r (mkTyConApp tc (map fst tys_roles))
691 -- See Note [Refl invariant]
692
693 | otherwise = TyConAppCo r tc cos
694
695 -- | Build a function 'Coercion' from two other 'Coercion's. That is,
696 -- given @co1 :: a ~ b@ and @co2 :: x ~ y@ produce @co :: (a -> x) ~ (b -> y)@.
697 mkFunCo :: Role -> Coercion -> Coercion -> Coercion
698 mkFunCo r co1 co2
699 -- See Note [Refl invariant]
700 | Just (ty1, _) <- isReflCo_maybe co1
701 , Just (ty2, _) <- isReflCo_maybe co2
702 = mkReflCo r (mkFunTy ty1 ty2)
703 | otherwise = FunCo r co1 co2
704
705 -- | Apply a 'Coercion' to another 'Coercion'.
706 -- The second coercion must be Nominal, unless the first is Phantom.
707 -- If the first is Phantom, then the second can be either Phantom or Nominal.
708 mkAppCo :: Coercion -- ^ :: t1 ~r t2
709 -> Coercion -- ^ :: s1 ~N s2, where s1 :: k1, s2 :: k2
710 -> Coercion -- ^ :: t1 s1 ~r t2 s2
711 mkAppCo co arg
712 | Just (ty1, r) <- isReflCo_maybe co
713 , Just (ty2, _) <- isReflCo_maybe arg
714 = mkReflCo r (mkAppTy ty1 ty2)
715
716 | Just (ty1, r) <- isReflCo_maybe co
717 , Just (tc, tys) <- splitTyConApp_maybe ty1
718 -- Expand type synonyms; a TyConAppCo can't have a type synonym (Trac #9102)
719 = mkTyConAppCo r tc (zip_roles (tyConRolesX r tc) tys)
720 where
721 zip_roles (r1:_) [] = [downgradeRole r1 Nominal arg]
722 zip_roles (r1:rs) (ty1:tys) = mkReflCo r1 ty1 : zip_roles rs tys
723 zip_roles _ _ = panic "zip_roles" -- but the roles are infinite...
724
725 mkAppCo (TyConAppCo r tc args) arg
726 = case r of
727 Nominal -> mkTyConAppCo Nominal tc (args ++ [arg])
728 Representational -> mkTyConAppCo Representational tc (args ++ [arg'])
729 where new_role = (tyConRolesRepresentational tc) !! (length args)
730 arg' = downgradeRole new_role Nominal arg
731 Phantom -> mkTyConAppCo Phantom tc (args ++ [toPhantomCo arg])
732 mkAppCo co arg = AppCo co arg
733 -- Note, mkAppCo is careful to maintain invariants regarding
734 -- where Refl constructors appear; see the comments in the definition
735 -- of Coercion and the Note [Refl invariant] in TyCoRep.
736
737 -- | Applies multiple 'Coercion's to another 'Coercion', from left to right.
738 -- See also 'mkAppCo'.
739 mkAppCos :: Coercion
740 -> [Coercion]
741 -> Coercion
742 mkAppCos co1 cos = foldl' mkAppCo co1 cos
743
744 {- Note [Unused coercion variable in ForAllCo]
745
746 See Note [Unused coercion variable in ForAllTy] in TyCoRep for the motivation for
747 checking coercion variable in types.
748 To lift the design choice to (ForAllCo cv kind_co body_co), we have two options:
749
750 (1) In mkForAllCo, we check whether cv is a coercion variable
751 and whether it is not used in body_co. If so we construct a FunCo.
752 (2) We don't do this check in mkForAllCo.
753 In coercionKind, we use mkTyCoForAllTy to perform the check and construct
754 a FunTy when necessary.
755
756 We chose (2) for two reasons:
757
758 * for a coercion, all that matters is its kind, So ForAllCo or FunCo does not
759 make a difference.
760 * even if cv occurs in body_co, it is possible that cv does not occur in the kind
761 of body_co. Therefore the check in coercionKind is inevitable.
762
763 The last wrinkle is that there are restrictions around the use of the cv in the
764 coercion, as described in Section 5.8.5.2 of Richard's thesis. The idea is that
765 we cannot prove that the type system is consistent with unrestricted use of this
766 cv; the consistency proof uses an untyped rewrite relation that works over types
767 with all coercions and casts removed. So, we can allow the cv to appear only in
768 positions that are erased. As an approximation of this (and keeping close to the
769 published theory), we currently allow the cv only within the type in a Refl node
770 and under a GRefl node (including in the Coercion stored in a GRefl). It's
771 possible other places are OK, too, but this is a safe approximation.
772
773 Sadly, with heterogeneous equality, this restriction might be able to be violated;
774 Richard's thesis is unable to prove that it isn't. Specifically, the liftCoSubst
775 function might create an invalid coercion. Because a violation of the
776 restriction might lead to a program that "goes wrong", it is checked all the time,
777 even in a production compiler and without -dcore-list. We *have* proved that the
778 problem does not occur with homogeneous equality, so this check can be dropped
779 once ~# is made to be homogeneous.
780 -}
781
782
783 -- | Make a Coercion from a tycovar, a kind coercion, and a body coercion.
784 -- The kind of the tycovar should be the left-hand kind of the kind coercion.
785 -- See Note [Unused coercion variable in ForAllCo]
786 mkForAllCo :: TyCoVar -> CoercionN -> Coercion -> Coercion
787 mkForAllCo v kind_co co
788 | ASSERT( varType v `eqType` (pFst $ coercionKind kind_co)) True
789 , ASSERT( isTyVar v || almostDevoidCoVarOfCo v co) True
790 , Just (ty, r) <- isReflCo_maybe co
791 , isGReflCo kind_co
792 = mkReflCo r (mkTyCoInvForAllTy v ty)
793 | otherwise
794 = ForAllCo v kind_co co
795
796 -- | Like 'mkForAllCo', but the inner coercion shouldn't be an obvious
797 -- reflexive coercion. For example, it is guaranteed in 'mkForAllCos'.
798 -- The kind of the tycovar should be the left-hand kind of the kind coercion.
799 mkForAllCo_NoRefl :: TyCoVar -> CoercionN -> Coercion -> Coercion
800 mkForAllCo_NoRefl v kind_co co
801 | ASSERT( varType v `eqType` (pFst $ coercionKind kind_co)) True
802 , ASSERT( isTyVar v || almostDevoidCoVarOfCo v co) True
803 , ASSERT( not (isReflCo co)) True
804 , isCoVar v
805 , not (v `elemVarSet` tyCoVarsOfCo co)
806 = FunCo (coercionRole co) kind_co co
807 | otherwise
808 = ForAllCo v kind_co co
809
810 -- | Make nested ForAllCos
811 mkForAllCos :: [(TyCoVar, CoercionN)] -> Coercion -> Coercion
812 mkForAllCos bndrs co
813 | Just (ty, r ) <- isReflCo_maybe co
814 = let (refls_rev'd, non_refls_rev'd) = span (isReflCo . snd) (reverse bndrs) in
815 foldl' (flip $ uncurry mkForAllCo_NoRefl)
816 (mkReflCo r (mkTyCoInvForAllTys (reverse (map fst refls_rev'd)) ty))
817 non_refls_rev'd
818 | otherwise
819 = foldr (uncurry mkForAllCo_NoRefl) co bndrs
820
821 -- | Make a Coercion quantified over a type/coercion variable;
822 -- the variable has the same type in both sides of the coercion
823 mkHomoForAllCos :: [TyCoVar] -> Coercion -> Coercion
824 mkHomoForAllCos vs co
825 | Just (ty, r) <- isReflCo_maybe co
826 = mkReflCo r (mkTyCoInvForAllTys vs ty)
827 | otherwise
828 = mkHomoForAllCos_NoRefl vs co
829
830 -- | Like 'mkHomoForAllCos', but the inner coercion shouldn't be an obvious
831 -- reflexive coercion. For example, it is guaranteed in 'mkHomoForAllCos'.
832 mkHomoForAllCos_NoRefl :: [TyCoVar] -> Coercion -> Coercion
833 mkHomoForAllCos_NoRefl vs orig_co
834 = ASSERT( not (isReflCo orig_co))
835 foldr go orig_co vs
836 where
837 go v co = mkForAllCo_NoRefl v (mkNomReflCo (varType v)) co
838
839 mkCoVarCo :: CoVar -> Coercion
840 -- cv :: s ~# t
841 -- See Note [mkCoVarCo]
842 mkCoVarCo cv = CoVarCo cv
843
844 mkCoVarCos :: [CoVar] -> [Coercion]
845 mkCoVarCos = map mkCoVarCo
846
847 {- Note [mkCoVarCo]
848 ~~~~~~~~~~~~~~~~~~~
849 In the past, mkCoVarCo optimised (c :: t~t) to (Refl t). That is
850 valid (although see Note [Unbound RULE binders] in Rules), but
851 it's a relatively expensive test and perhaps better done in
852 optCoercion. Not a big deal either way.
853 -}
854
855 -- | Extract a covar, if possible. This check is dirty. Be ashamed
856 -- of yourself. (It's dirty because it cares about the structure of
857 -- a coercion, which is morally reprehensible.)
858 isCoVar_maybe :: Coercion -> Maybe CoVar
859 isCoVar_maybe (CoVarCo cv) = Just cv
860 isCoVar_maybe _ = Nothing
861
862 mkAxInstCo :: Role -> CoAxiom br -> BranchIndex -> [Type] -> [Coercion]
863 -> Coercion
864 -- mkAxInstCo can legitimately be called over-staturated;
865 -- i.e. with more type arguments than the coercion requires
866 mkAxInstCo role ax index tys cos
867 | arity == n_tys = downgradeRole role ax_role $
868 mkAxiomInstCo ax_br index (rtys `chkAppend` cos)
869 | otherwise = ASSERT( arity < n_tys )
870 downgradeRole role ax_role $
871 mkAppCos (mkAxiomInstCo ax_br index
872 (ax_args `chkAppend` cos))
873 leftover_args
874 where
875 n_tys = length tys
876 ax_br = toBranchedAxiom ax
877 branch = coAxiomNthBranch ax_br index
878 tvs = coAxBranchTyVars branch
879 arity = length tvs
880 arg_roles = coAxBranchRoles branch
881 rtys = zipWith mkReflCo (arg_roles ++ repeat Nominal) tys
882 (ax_args, leftover_args)
883 = splitAt arity rtys
884 ax_role = coAxiomRole ax
885
886 -- worker function
887 mkAxiomInstCo :: CoAxiom Branched -> BranchIndex -> [Coercion] -> Coercion
888 mkAxiomInstCo ax index args
889 = ASSERT( args `lengthIs` coAxiomArity ax index )
890 AxiomInstCo ax index args
891
892 -- to be used only with unbranched axioms
893 mkUnbranchedAxInstCo :: Role -> CoAxiom Unbranched
894 -> [Type] -> [Coercion] -> Coercion
895 mkUnbranchedAxInstCo role ax tys cos
896 = mkAxInstCo role ax 0 tys cos
897
898 mkAxInstRHS :: CoAxiom br -> BranchIndex -> [Type] -> [Coercion] -> Type
899 -- Instantiate the axiom with specified types,
900 -- returning the instantiated RHS
901 -- A companion to mkAxInstCo:
902 -- mkAxInstRhs ax index tys = snd (coercionKind (mkAxInstCo ax index tys))
903 mkAxInstRHS ax index tys cos
904 = ASSERT( tvs `equalLength` tys1 )
905 mkAppTys rhs' tys2
906 where
907 branch = coAxiomNthBranch ax index
908 tvs = coAxBranchTyVars branch
909 cvs = coAxBranchCoVars branch
910 (tys1, tys2) = splitAtList tvs tys
911 rhs' = substTyWith tvs tys1 $
912 substTyWithCoVars cvs cos $
913 coAxBranchRHS branch
914
915 mkUnbranchedAxInstRHS :: CoAxiom Unbranched -> [Type] -> [Coercion] -> Type
916 mkUnbranchedAxInstRHS ax = mkAxInstRHS ax 0
917
918 -- | Return the left-hand type of the axiom, when the axiom is instantiated
919 -- at the types given.
920 mkAxInstLHS :: CoAxiom br -> BranchIndex -> [Type] -> [Coercion] -> Type
921 mkAxInstLHS ax index tys cos
922 = ASSERT( tvs `equalLength` tys1 )
923 mkTyConApp fam_tc (lhs_tys `chkAppend` tys2)
924 where
925 branch = coAxiomNthBranch ax index
926 tvs = coAxBranchTyVars branch
927 cvs = coAxBranchCoVars branch
928 (tys1, tys2) = splitAtList tvs tys
929 lhs_tys = substTysWith tvs tys1 $
930 substTysWithCoVars cvs cos $
931 coAxBranchLHS branch
932 fam_tc = coAxiomTyCon ax
933
934 -- | Instantiate the left-hand side of an unbranched axiom
935 mkUnbranchedAxInstLHS :: CoAxiom Unbranched -> [Type] -> [Coercion] -> Type
936 mkUnbranchedAxInstLHS ax = mkAxInstLHS ax 0
937
938 -- | Manufacture an unsafe coercion from thin air.
939 -- Currently (May 14) this is used only to implement the
940 -- @unsafeCoerce#@ primitive. Optimise by pushing
941 -- down through type constructors.
942 mkUnsafeCo :: Role -> Type -> Type -> Coercion
943 mkUnsafeCo role ty1 ty2
944 = mkUnivCo UnsafeCoerceProv role ty1 ty2
945
946 -- | Make a coercion from a coercion hole
947 mkHoleCo :: CoercionHole -> Coercion
948 mkHoleCo h = HoleCo h
949
950 -- | Make a universal coercion between two arbitrary types.
951 mkUnivCo :: UnivCoProvenance
952 -> Role -- ^ role of the built coercion, "r"
953 -> Type -- ^ t1 :: k1
954 -> Type -- ^ t2 :: k2
955 -> Coercion -- ^ :: t1 ~r t2
956 mkUnivCo prov role ty1 ty2
957 | ty1 `eqType` ty2 = mkReflCo role ty1
958 | otherwise = UnivCo prov role ty1 ty2
959
960 -- | Create a symmetric version of the given 'Coercion' that asserts
961 -- equality between the same types but in the other "direction", so
962 -- a kind of @t1 ~ t2@ becomes the kind @t2 ~ t1@.
963 mkSymCo :: Coercion -> Coercion
964
965 -- Do a few simple optimizations, but don't bother pushing occurrences
966 -- of symmetry to the leaves; the optimizer will take care of that.
967 mkSymCo co | isReflCo co = co
968 mkSymCo (SymCo co) = co
969 mkSymCo (SubCo (SymCo co)) = SubCo co
970 mkSymCo co = SymCo co
971
972 -- | Create a new 'Coercion' by composing the two given 'Coercion's transitively.
973 -- (co1 ; co2)
974 mkTransCo :: Coercion -> Coercion -> Coercion
975 mkTransCo co1 co2 | isReflCo co1 = co2
976 | isReflCo co2 = co1
977 mkTransCo (GRefl r t1 (MCo co1)) (GRefl _ _ (MCo co2))
978 = GRefl r t1 (MCo $ mkTransCo co1 co2)
979 mkTransCo co1 co2 = TransCo co1 co2
980
981 mkNthCo :: HasDebugCallStack
982 => Role -- The role of the coercion you're creating
983 -> Int -- Zero-indexed
984 -> Coercion
985 -> Coercion
986 mkNthCo r n co
987 = ASSERT2( good_call, bad_call_msg )
988 go r n co
989 where
990 Pair ty1 ty2 = coercionKind co
991
992 go r 0 co
993 | Just (ty, _) <- isReflCo_maybe co
994 , Just (tv, _) <- splitForAllTy_maybe ty
995 = -- works for both tyvar and covar
996 ASSERT( r == Nominal )
997 mkNomReflCo (varType tv)
998
999 go r n co
1000 | Just (ty, r0) <- isReflCo_maybe co
1001 , let tc = tyConAppTyCon ty
1002 = ASSERT2( ok_tc_app ty n, ppr n $$ ppr ty )
1003 ASSERT( nthRole r0 tc n == r )
1004 mkReflCo r (tyConAppArgN n ty)
1005 where ok_tc_app :: Type -> Int -> Bool
1006 ok_tc_app ty n
1007 | Just (_, tys) <- splitTyConApp_maybe ty
1008 = tys `lengthExceeds` n
1009 | isForAllTy ty -- nth:0 pulls out a kind coercion from a hetero forall
1010 = n == 0
1011 | otherwise
1012 = False
1013
1014 go r 0 (ForAllCo _ kind_co _)
1015 = ASSERT( r == Nominal )
1016 kind_co
1017 -- If co :: (forall a1:k1. t1) ~ (forall a2:k2. t2)
1018 -- then (nth 0 co :: k1 ~N k2)
1019 -- If co :: (forall a1:t1 ~ t2. t1) ~ (forall a2:t3 ~ t4. t2)
1020 -- then (nth 0 co :: (t1 ~ t2) ~N (t3 ~ t4))
1021
1022 go r n co@(FunCo r0 arg res)
1023 -- See Note [Function coercions]
1024 -- If FunCo _ arg_co res_co :: (s1:TYPE sk1 -> s2:TYPE sk2)
1025 -- ~ (t1:TYPE tk1 -> t2:TYPE tk2)
1026 -- Then we want to behave as if co was
1027 -- TyConAppCo argk_co resk_co arg_co res_co
1028 -- where
1029 -- argk_co :: sk1 ~ tk1 = mkNthCo 0 (mkKindCo arg_co)
1030 -- resk_co :: sk2 ~ tk2 = mkNthCo 0 (mkKindCo res_co)
1031 -- i.e. mkRuntimeRepCo
1032 = case n of
1033 0 -> ASSERT( r == Nominal ) mkRuntimeRepCo arg
1034 1 -> ASSERT( r == Nominal ) mkRuntimeRepCo res
1035 2 -> ASSERT( r == r0 ) arg
1036 3 -> ASSERT( r == r0 ) res
1037 _ -> pprPanic "mkNthCo(FunCo)" (ppr n $$ ppr co)
1038
1039 go r n (TyConAppCo r0 tc arg_cos) = ASSERT2( r == nthRole r0 tc n
1040 , (vcat [ ppr tc
1041 , ppr arg_cos
1042 , ppr r0
1043 , ppr n
1044 , ppr r ]) )
1045 arg_cos `getNth` n
1046
1047 go r n co =
1048 NthCo r n co
1049
1050 -- Assertion checking
1051 bad_call_msg = vcat [ text "Coercion =" <+> ppr co
1052 , text "LHS ty =" <+> ppr ty1
1053 , text "RHS ty =" <+> ppr ty2
1054 , text "n =" <+> ppr n, text "r =" <+> ppr r
1055 , text "coercion role =" <+> ppr (coercionRole co) ]
1056 good_call
1057 -- If the Coercion passed in is between forall-types, then the Int must
1058 -- be 0 and the role must be Nominal.
1059 | Just (_tv1, _) <- splitForAllTy_maybe ty1
1060 , Just (_tv2, _) <- splitForAllTy_maybe ty2
1061 = n == 0 && r == Nominal
1062
1063 -- If the Coercion passed in is between T tys and T tys', then the Int
1064 -- must be less than the length of tys/tys' (which must be the same
1065 -- lengths).
1066 --
1067 -- If the role of the Coercion is nominal, then the role passed in must
1068 -- be nominal. If the role of the Coercion is representational, then the
1069 -- role passed in must be tyConRolesRepresentational T !! n. If the role
1070 -- of the Coercion is Phantom, then the role passed in must be Phantom.
1071 --
1072 -- See also Note [NthCo Cached Roles] if you're wondering why it's
1073 -- blaringly obvious that we should be *computing* this role instead of
1074 -- passing it in.
1075 | Just (tc1, tys1) <- splitTyConApp_maybe ty1
1076 , Just (tc2, tys2) <- splitTyConApp_maybe ty2
1077 , tc1 == tc2
1078 = let len1 = length tys1
1079 len2 = length tys2
1080 good_role = case coercionRole co of
1081 Nominal -> r == Nominal
1082 Representational -> r == (tyConRolesRepresentational tc1 !! n)
1083 Phantom -> r == Phantom
1084 in len1 == len2 && n < len1 && good_role
1085
1086 | otherwise
1087 = True
1088
1089
1090
1091 -- | If you're about to call @mkNthCo r n co@, then @r@ should be
1092 -- whatever @nthCoRole n co@ returns.
1093 nthCoRole :: Int -> Coercion -> Role
1094 nthCoRole n co
1095 | Just (tc, _) <- splitTyConApp_maybe lty
1096 = nthRole r tc n
1097
1098 | Just _ <- splitForAllTy_maybe lty
1099 = Nominal
1100
1101 | otherwise
1102 = pprPanic "nthCoRole" (ppr co)
1103
1104 where
1105 (Pair lty _, r) = coercionKindRole co
1106
1107 mkLRCo :: LeftOrRight -> Coercion -> Coercion
1108 mkLRCo lr co
1109 | Just (ty, eq) <- isReflCo_maybe co
1110 = mkReflCo eq (pickLR lr (splitAppTy ty))
1111 | otherwise
1112 = LRCo lr co
1113
1114 -- | Instantiates a 'Coercion'.
1115 mkInstCo :: Coercion -> Coercion -> Coercion
1116 mkInstCo (ForAllCo tcv _kind_co body_co) co
1117 | Just (arg, _) <- isReflCo_maybe co
1118 -- works for both tyvar and covar
1119 = substCoUnchecked (zipTCvSubst [tcv] [arg]) body_co
1120 mkInstCo co arg = InstCo co arg
1121
1122 -- | Given @ty :: k1@, @co :: k1 ~ k2@,
1123 -- produces @co' :: ty ~r (ty |> co)@
1124 mkGReflRightCo :: Role -> Type -> CoercionN -> Coercion
1125 mkGReflRightCo r ty co
1126 | isGReflCo co = mkReflCo r ty
1127 -- the kinds of @k1@ and @k2@ are the same, thus @isGReflCo@
1128 -- instead of @isReflCo@
1129 | otherwise = GRefl r ty (MCo co)
1130
1131 -- | Given @ty :: k1@, @co :: k1 ~ k2@,
1132 -- produces @co' :: (ty |> co) ~r ty@
1133 mkGReflLeftCo :: Role -> Type -> CoercionN -> Coercion
1134 mkGReflLeftCo r ty co
1135 | isGReflCo co = mkReflCo r ty
1136 -- the kinds of @k1@ and @k2@ are the same, thus @isGReflCo@
1137 -- instead of @isReflCo@
1138 | otherwise = mkSymCo $ GRefl r ty (MCo co)
1139
1140 -- | Given @ty :: k1@, @co :: k1 ~ k2@, @co2:: ty ~ ty'@,
1141 -- produces @co' :: (ty |> co) ~r ty'
1142 -- It is not only a utility function, but it saves allocation when co
1143 -- is a GRefl coercion.
1144 mkCoherenceLeftCo :: Role -> Type -> CoercionN -> Coercion -> Coercion
1145 mkCoherenceLeftCo r ty co co2
1146 | isGReflCo co = co2
1147 | otherwise = (mkSymCo $ GRefl r ty (MCo co)) `mkTransCo` co2
1148
1149 -- | Given @ty :: k1@, @co :: k1 ~ k2@, @co2:: ty' ~ ty@,
1150 -- produces @co' :: ty' ~r (ty |> co)
1151 -- It is not only a utility function, but it saves allocation when co
1152 -- is a GRefl coercion.
1153 mkCoherenceRightCo :: Role -> Type -> CoercionN -> Coercion -> Coercion
1154 mkCoherenceRightCo r ty co co2
1155 | isGReflCo co = co2
1156 | otherwise = co2 `mkTransCo` GRefl r ty (MCo co)
1157
1158 -- | Given @co :: (a :: k) ~ (b :: k')@ produce @co' :: k ~ k'@.
1159 mkKindCo :: Coercion -> Coercion
1160 mkKindCo co | Just (ty, _) <- isReflCo_maybe co = Refl (typeKind ty)
1161 mkKindCo (GRefl _ _ (MCo co)) = co
1162 mkKindCo (UnivCo (PhantomProv h) _ _ _) = h
1163 mkKindCo (UnivCo (ProofIrrelProv h) _ _ _) = h
1164 mkKindCo co
1165 | Pair ty1 ty2 <- coercionKind co
1166 -- generally, calling coercionKind during coercion creation is a bad idea,
1167 -- as it can lead to exponential behavior. But, we don't have nested mkKindCos,
1168 -- so it's OK here.
1169 , let tk1 = typeKind ty1
1170 tk2 = typeKind ty2
1171 , tk1 `eqType` tk2
1172 = Refl tk1
1173 | otherwise
1174 = KindCo co
1175
1176 mkSubCo :: Coercion -> Coercion
1177 -- Input coercion is Nominal, result is Representational
1178 -- see also Note [Role twiddling functions]
1179 mkSubCo (Refl ty) = GRefl Representational ty MRefl
1180 mkSubCo (GRefl Nominal ty co) = GRefl Representational ty co
1181 mkSubCo (TyConAppCo Nominal tc cos)
1182 = TyConAppCo Representational tc (applyRoles tc cos)
1183 mkSubCo (FunCo Nominal arg res)
1184 = FunCo Representational
1185 (downgradeRole Representational Nominal arg)
1186 (downgradeRole Representational Nominal res)
1187 mkSubCo co = ASSERT2( coercionRole co == Nominal, ppr co <+> ppr (coercionRole co) )
1188 SubCo co
1189
1190 -- | Changes a role, but only a downgrade. See Note [Role twiddling functions]
1191 downgradeRole_maybe :: Role -- ^ desired role
1192 -> Role -- ^ current role
1193 -> Coercion -> Maybe Coercion
1194 -- In (downgradeRole_maybe dr cr co) it's a precondition that
1195 -- cr = coercionRole co
1196
1197 downgradeRole_maybe Nominal Nominal co = Just co
1198 downgradeRole_maybe Nominal _ _ = Nothing
1199
1200 downgradeRole_maybe Representational Nominal co = Just (mkSubCo co)
1201 downgradeRole_maybe Representational Representational co = Just co
1202 downgradeRole_maybe Representational Phantom _ = Nothing
1203
1204 downgradeRole_maybe Phantom Phantom co = Just co
1205 downgradeRole_maybe Phantom _ co = Just (toPhantomCo co)
1206
1207 -- | Like 'downgradeRole_maybe', but panics if the change isn't a downgrade.
1208 -- See Note [Role twiddling functions]
1209 downgradeRole :: Role -- desired role
1210 -> Role -- current role
1211 -> Coercion -> Coercion
1212 downgradeRole r1 r2 co
1213 = case downgradeRole_maybe r1 r2 co of
1214 Just co' -> co'
1215 Nothing -> pprPanic "downgradeRole" (ppr co)
1216
1217 -- | If the EqRel is ReprEq, makes a SubCo; otherwise, does nothing.
1218 -- Note that the input coercion should always be nominal.
1219 maybeSubCo :: EqRel -> Coercion -> Coercion
1220 maybeSubCo NomEq = id
1221 maybeSubCo ReprEq = mkSubCo
1222
1223
1224 mkAxiomRuleCo :: CoAxiomRule -> [Coercion] -> Coercion
1225 mkAxiomRuleCo = AxiomRuleCo
1226
1227 -- | Make a "coercion between coercions".
1228 mkProofIrrelCo :: Role -- ^ role of the created coercion, "r"
1229 -> Coercion -- ^ :: phi1 ~N phi2
1230 -> Coercion -- ^ g1 :: phi1
1231 -> Coercion -- ^ g2 :: phi2
1232 -> Coercion -- ^ :: g1 ~r g2
1233
1234 -- if the two coercion prove the same fact, I just don't care what
1235 -- the individual coercions are.
1236 mkProofIrrelCo r co g _ | isGReflCo co = mkReflCo r (mkCoercionTy g)
1237 -- kco is a kind coercion, thus @isGReflCo@ rather than @isReflCo@
1238 mkProofIrrelCo r kco g1 g2 = mkUnivCo (ProofIrrelProv kco) r
1239 (mkCoercionTy g1) (mkCoercionTy g2)
1240
1241 {-
1242 %************************************************************************
1243 %* *
1244 Roles
1245 %* *
1246 %************************************************************************
1247 -}
1248
1249 -- | Converts a coercion to be nominal, if possible.
1250 -- See Note [Role twiddling functions]
1251 setNominalRole_maybe :: Role -- of input coercion
1252 -> Coercion -> Maybe Coercion
1253 setNominalRole_maybe r co
1254 | r == Nominal = Just co
1255 | otherwise = setNominalRole_maybe_helper co
1256 where
1257 setNominalRole_maybe_helper (SubCo co) = Just co
1258 setNominalRole_maybe_helper co@(Refl _) = Just co
1259 setNominalRole_maybe_helper (GRefl _ ty co) = Just $ GRefl Nominal ty co
1260 setNominalRole_maybe_helper (TyConAppCo Representational tc cos)
1261 = do { cos' <- zipWithM setNominalRole_maybe (tyConRolesX Representational tc) cos
1262 ; return $ TyConAppCo Nominal tc cos' }
1263 setNominalRole_maybe_helper (FunCo Representational co1 co2)
1264 = do { co1' <- setNominalRole_maybe Representational co1
1265 ; co2' <- setNominalRole_maybe Representational co2
1266 ; return $ FunCo Nominal co1' co2'
1267 }
1268 setNominalRole_maybe_helper (SymCo co)
1269 = SymCo <$> setNominalRole_maybe_helper co
1270 setNominalRole_maybe_helper (TransCo co1 co2)
1271 = TransCo <$> setNominalRole_maybe_helper co1 <*> setNominalRole_maybe_helper co2
1272 setNominalRole_maybe_helper (AppCo co1 co2)
1273 = AppCo <$> setNominalRole_maybe_helper co1 <*> pure co2
1274 setNominalRole_maybe_helper (ForAllCo tv kind_co co)
1275 = ForAllCo tv kind_co <$> setNominalRole_maybe_helper co
1276 setNominalRole_maybe_helper (NthCo _r n co)
1277 -- NB, this case recurses via setNominalRole_maybe, not
1278 -- setNominalRole_maybe_helper!
1279 = NthCo Nominal n <$> setNominalRole_maybe (coercionRole co) co
1280 setNominalRole_maybe_helper (InstCo co arg)
1281 = InstCo <$> setNominalRole_maybe_helper co <*> pure arg
1282 setNominalRole_maybe_helper (UnivCo prov _ co1 co2)
1283 | case prov of UnsafeCoerceProv -> True -- it's always unsafe
1284 PhantomProv _ -> False -- should always be phantom
1285 ProofIrrelProv _ -> True -- it's always safe
1286 PluginProv _ -> False -- who knows? This choice is conservative.
1287 = Just $ UnivCo prov Nominal co1 co2
1288 setNominalRole_maybe_helper _ = Nothing
1289
1290 -- | Make a phantom coercion between two types. The coercion passed
1291 -- in must be a nominal coercion between the kinds of the
1292 -- types.
1293 mkPhantomCo :: Coercion -> Type -> Type -> Coercion
1294 mkPhantomCo h t1 t2
1295 = mkUnivCo (PhantomProv h) Phantom t1 t2
1296
1297 -- takes any coercion and turns it into a Phantom coercion
1298 toPhantomCo :: Coercion -> Coercion
1299 toPhantomCo co
1300 = mkPhantomCo (mkKindCo co) ty1 ty2
1301 where Pair ty1 ty2 = coercionKind co
1302
1303 -- Convert args to a TyConAppCo Nominal to the same TyConAppCo Representational
1304 applyRoles :: TyCon -> [Coercion] -> [Coercion]
1305 applyRoles tc cos
1306 = zipWith (\r -> downgradeRole r Nominal) (tyConRolesRepresentational tc) cos
1307
1308 -- the Role parameter is the Role of the TyConAppCo
1309 -- defined here because this is intimately concerned with the implementation
1310 -- of TyConAppCo
1311 tyConRolesX :: Role -> TyCon -> [Role]
1312 tyConRolesX Representational tc = tyConRolesRepresentational tc
1313 tyConRolesX role _ = repeat role
1314
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) = mkFunTy <$> 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 Trac #11735.
2284
2285 Solution: gather up the type variables for nested `ForAllCos`, and
2286 substitute for them all at once. Remarkably, for Trac #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 Trac #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 Trac #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 -- | Assuming that two types are the same, ignoring coercions, find
2340 -- a nominal coercion between the types. This is useful when optimizing
2341 -- transitivity over coercion applications, where splitting two
2342 -- AppCos might yield different kinds. See Note [EtaAppCo] in OptCoercion.
2343 buildCoercion :: Type -> Type -> CoercionN
2344 buildCoercion orig_ty1 orig_ty2 = go orig_ty1 orig_ty2
2345 where
2346 go ty1 ty2 | Just ty1' <- coreView ty1 = go ty1' ty2
2347 | Just ty2' <- coreView ty2 = go ty1 ty2'
2348
2349 go (CastTy ty1 co) ty2
2350 = let co' = go ty1 ty2
2351 r = coercionRole co'
2352 in mkCoherenceLeftCo r ty1 co co'
2353
2354 go ty1 (CastTy ty2 co)
2355 = let co' = go ty1 ty2
2356 r = coercionRole co'
2357 in mkCoherenceRightCo r ty2 co co'
2358
2359 go ty1@(TyVarTy tv1) _tyvarty
2360 = ASSERT( case _tyvarty of
2361 { TyVarTy tv2 -> tv1 == tv2
2362 ; _ -> False } )
2363 mkNomReflCo ty1
2364
2365 go (FunTy arg1 res1) (FunTy arg2 res2)
2366 = mkFunCo Nominal (go arg1 arg2) (go res1 res2)
2367
2368 go (TyConApp tc1 args1) (TyConApp tc2 args2)
2369 = ASSERT( tc1 == tc2 )
2370 mkTyConAppCo Nominal tc1 (zipWith go args1 args2)
2371
2372 go (AppTy ty1a ty1b) ty2
2373 | Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2
2374 = mkAppCo (go ty1a ty2a) (go ty1b ty2b)
2375
2376 go ty1 (AppTy ty2a ty2b)
2377 | Just (ty1a, ty1b) <- repSplitAppTy_maybe ty1
2378 = mkAppCo (go ty1a ty2a) (go ty1b ty2b)
2379
2380 go (ForAllTy (Bndr tv1 _flag1) ty1) (ForAllTy (Bndr tv2 _flag2) ty2)
2381 | isTyVar tv1
2382 = ASSERT( isTyVar tv2 )
2383 mkForAllCo tv1 kind_co (go ty1 ty2')
2384 where kind_co = go (tyVarKind tv1) (tyVarKind tv2)
2385 in_scope = mkInScopeSet $ tyCoVarsOfType ty2 `unionVarSet` tyCoVarsOfCo kind_co
2386 ty2' = substTyWithInScope in_scope [tv2]
2387 [mkTyVarTy tv1 `mkCastTy` kind_co]
2388 ty2
2389
2390 go (ForAllTy (Bndr cv1 _flag1) ty1) (ForAllTy (Bndr cv2 _flag2) ty2)
2391 = ASSERT( isCoVar cv1 && isCoVar cv2 )
2392 mkForAllCo cv1 kind_co (go ty1 ty2')
2393 where s1 = varType cv1
2394 s2 = varType cv2
2395 kind_co = go s1 s2
2396
2397 -- s1 = t1 ~r t2
2398 -- s2 = t3 ~r t4
2399 -- kind_co :: (t1 ~r t2) ~N (t3 ~r t4)
2400 -- eta1 :: t1 ~r t3
2401 -- eta2 :: t2 ~r t4
2402
2403 r = coVarRole cv1
2404 kind_co' = downgradeRole r Nominal kind_co
2405 eta1 = mkNthCo r 2 kind_co'
2406 eta2 = mkNthCo r 3 kind_co'
2407
2408 subst = mkEmptyTCvSubst $ mkInScopeSet $
2409 tyCoVarsOfType ty2 `unionVarSet` tyCoVarsOfCo kind_co
2410 ty2' = substTy (extendCvSubst subst cv2 $ mkSymCo eta1 `mkTransCo`
2411 mkCoVarCo cv1 `mkTransCo`
2412 eta2)
2413 ty2
2414
2415 go ty1@(LitTy lit1) _lit2
2416 = ASSERT( case _lit2 of
2417 { LitTy lit2 -> lit1 == lit2
2418 ; _ -> False } )
2419 mkNomReflCo ty1
2420
2421 go (CoercionTy co1) (CoercionTy co2)
2422 = mkProofIrrelCo Nominal kind_co co1 co2
2423 where
2424 kind_co = go (coercionType co1) (coercionType co2)
2425
2426 go ty1 ty2
2427 = pprPanic "buildKindCoercion" (vcat [ ppr orig_ty1, ppr orig_ty2
2428 , ppr ty1, ppr ty2 ])