Coercion.hs 70.7 KB
Newer Older
1 2 3
{-
(c) The University of Glasgow 2006
-}
4

5
{-# LANGUAGE RankNTypes, CPP, DeriveDataTypeable, MultiWayIf #-}
6

7
-- | Module for (a) type kinds and (b) type coercions,
8
-- as used in System FC. See 'CoreSyn.Expr' for
batterseapower's avatar
batterseapower committed
9 10
-- more on System FC and how coercions fit into it.
--
11
module Coercion (
batterseapower's avatar
batterseapower committed
12
        -- * Main data type
13 14 15
        Coercion, CoercionN, CoercionR, CoercionP,
        UnivCoProvenance, CoercionHole, LeftOrRight(..),
        Var, CoVar, TyCoVar,
16
        Role(..), ltRole,
17

dreixel's avatar
dreixel committed
18
        -- ** Functions over coercions
19 20
        coVarTypes, coVarKind, coVarKindsTypesRole, coVarRole,
        coercionType, coercionKind, coercionKinds,
batterseapower's avatar
batterseapower committed
21
        mkCoercionType,
22
        coercionRole, coercionKindRole,
23

24
        -- ** Constructing coercions
25 26 27 28 29
        mkReflCo, mkRepReflCo, mkNomReflCo,
        mkCoVarCo, mkCoVarCos,
        mkAxInstCo, mkUnbranchedAxInstCo,
        mkAxInstRHS, mkUnbranchedAxInstRHS,
        mkAxInstLHS, mkUnbranchedAxInstLHS,
30
        mkPiCo, mkPiCos, mkCoCast,
31 32 33 34 35 36
        mkSymCo, mkTransCo, mkTransAppCo,
        mkNthCo, mkNthCoRole, mkLRCo,
        mkInstCo, mkAppCo, mkAppCos, mkTyConAppCo, mkFunCo, mkFunCos,
        mkForAllCo, mkForAllCos, mkHomoForAllCos, mkHomoForAllCos_NoRefl,
        mkPhantomCo, mkHomoPhantomCo, toPhantomCo,
        mkUnsafeCo, mkHoleCo, mkUnivCo, mkSubCo,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
37
        mkAxiomInstCo, mkProofIrrelCo,
38 39 40 41 42
        downgradeRole, maybeSubCo, mkAxiomRuleCo,
        mkCoherenceCo, mkCoherenceRightCo, mkCoherenceLeftCo,
        mkKindCo, castCoercionKind,

        mkHeteroCoercionType,
TomSchrijvers's avatar
TomSchrijvers committed
43

44
        -- ** Decomposition
45
        instNewTyCon_maybe,
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
46 47 48 49

        NormaliseStepper, NormaliseStepResult(..), composeSteppers,
        modifyStepResultCo, unwrapNewTypeStepper,
        topNormaliseNewType_maybe, topNormaliseTypeX_maybe,
50

51
        decomposeCo, getCoVar_maybe,
52
        splitTyConAppCo_maybe,
53 54
        splitAppCo_maybe,
        splitForAllCo_maybe,
55 56 57 58 59

        nthRole, tyConRolesX, setNominalRole_maybe,

        pickLR,

60
        isReflCo, isReflCo_maybe, isReflexiveCo, isReflexiveCo_maybe,
61

62
        -- ** Coercion variables
63 64
        mkCoVar, isCoVar, coVarName, setCoVarName, setCoVarUnique,
        isCoVar_maybe,
65 66

        -- ** Free variables
67 68 69
        tyCoVarsOfCo, tyCoVarsOfCos, coVarsOfCo,
        tyCoVarsOfCoAcc, tyCoVarsOfCosAcc, tyCoVarsOfCoDSet,
        coercionSize,
70

71
        -- ** Substitution
72
        CvSubstEnv, emptyCvSubstEnv,
73 74 75 76
        lookupCoVar,
        substCo, substCos, substCoVar, substCoVars, substCoWith,
        substCoVarBndr,
        extendTCvSubstAndInScope, getCvSubstEnv,
77

78
        -- ** Lifting
79 80 81 82 83 84 85 86 87
        liftCoSubst, liftCoSubstTyVar, liftCoSubstWith, liftCoSubstWithEx,
        emptyLiftingContext, extendLiftingContext,
        liftCoSubstVarBndrCallback, isMappedByLC,

        mkSubstLiftingContext, zapLiftingContext,
        substForAllCoBndrCallbackLC, lcTCvSubst, lcInScopeSet,

        LiftCoEnv, LiftingContext(..), liftEnvSubstLeft, liftEnvSubstRight,
        substRightCo, substLeftCo, swapLiftCoEnv, lcSubstLeft, lcSubstRight,
88

batterseapower's avatar
batterseapower committed
89
        -- ** Comparison
90
        eqCoercion, eqCoercionX,
91

92 93
        -- ** Forcing evaluation of coercions
        seqCo,
94

95
        -- * Pretty-printing
96
        pprCo, pprParendCo, pprCoBndr,
97
        pprCoAxiom, pprCoAxBranch, pprCoAxBranchHdr,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
98 99 100

        -- * Tidying
        tidyCo, tidyCos,
TomSchrijvers's avatar
TomSchrijvers committed
101

102
        -- * Other
103
        promoteCoercion
104
       ) where
105 106 107

#include "HsVersions.h"

108 109
import TyCoRep
import Type
110
import TyCon
111
import CoAxiom
112
import Var
113
import VarEnv
114
import Name hiding ( varName )
115 116
import Util
import BasicTypes
117
import Outputable
118 119
import Unique
import Pair
Simon Peyton Jones's avatar
Simon Peyton Jones committed
120
import SrcLoc
121 122 123 124 125 126
import PrelNames
import TysPrim          ( eqPhantPrimTyCon )
import ListSetOps
import Maybes

import Control.Monad (foldM)
127
import Control.Arrow ( first )
128
import Data.Function ( on )
129

130 131
-----------------------------------------------------------------
-- These synonyms are very useful as documentation
132

133 134 135 136 137 138 139
type CoercionN = Coercion   -- nominal coercion
type CoercionR = Coercion   -- representational coercion
type CoercionP = Coercion   -- phantom coercion

{-
%************************************************************************
%*                                                                      *
140
     -- The coercion arguments always *precisely* saturate
141
     -- arity of (that branch of) the CoAxiom.  If there are
142
     -- any left over, we use AppCo.  See
143 144
     -- See [Coercion axioms applied to coercions]

145
\subsection{Coercion variables}
146 147
%*                                                                      *
%************************************************************************
148
-}
149 150 151 152 153 154 155 156 157 158 159

coVarName :: CoVar -> Name
coVarName = varName

setCoVarUnique :: CoVar -> Unique -> CoVar
setCoVarUnique = setVarUnique

setCoVarName :: CoVar -> Name -> CoVar
setCoVarName   = setVarName

coercionSize :: Coercion -> Int
160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182
coercionSize (Refl _ ty)         = typeSize ty
coercionSize (TyConAppCo _ _ args) = 1 + sum (map coercionSize args)
coercionSize (AppCo co arg)      = coercionSize co + coercionSize arg
coercionSize (ForAllCo _ h co)   = 1 + coercionSize co + coercionSize h
coercionSize (CoVarCo _)         = 1
coercionSize (AxiomInstCo _ _ args) = 1 + sum (map coercionSize args)
coercionSize (UnivCo p _ t1 t2)  = 1 + provSize p + typeSize t1 + typeSize t2
coercionSize (SymCo co)          = 1 + coercionSize co
coercionSize (TransCo co1 co2)   = 1 + coercionSize co1 + coercionSize co2
coercionSize (NthCo _ co)        = 1 + coercionSize co
coercionSize (LRCo  _ co)        = 1 + coercionSize co
coercionSize (InstCo co arg)     = 1 + coercionSize co + coercionSize arg
coercionSize (CoherenceCo c1 c2) = 1 + coercionSize c1 + coercionSize c2
coercionSize (KindCo co)         = 1 + coercionSize co
coercionSize (SubCo co)          = 1 + coercionSize co
coercionSize (AxiomRuleCo _ cs)  = 1 + sum (map coercionSize cs)

provSize :: UnivCoProvenance -> Int
provSize UnsafeCoerceProv    = 1
provSize (PhantomProv co)    = 1 + coercionSize co
provSize (ProofIrrelProv co) = 1 + coercionSize co
provSize (PluginProv _)      = 1
provSize (HoleProv h)        = pprPanic "provSize hits a hole" (ppr h)
183

184
{-
185 186
%************************************************************************
%*                                                                      *
187
                   Pretty-printing coercions
188 189
%*                                                                      *
%************************************************************************
190

191 192 193 194 195
@pprCo@ is the standard @Coercion@ printer; the overloaded @ppr@
function is defined to use this.  @pprParendCo@ is the same, except it
puts parens around the type, except for the atomic cases.
@pprParendCo@ works just by setting the initial context precedence
very high.
196
-}
197

198
-- Outputable instances are in TyCoRep, to avoid orphans
199 200 201 202 203

pprCo, pprParendCo :: Coercion -> SDoc
pprCo       co = ppr_co TopPrec   co
pprParendCo co = ppr_co TyConPrec co

204
ppr_co :: TyPrec -> Coercion -> SDoc
205
ppr_co _ (Refl r ty) = angleBrackets (ppr ty) <> ppr_role r
206

207
ppr_co p co@(TyConAppCo _ tc [_,_])
208
  | tc `hasKey` funTyConKey = ppr_fun_co p co
209

210 211 212 213 214 215
ppr_co _ (TyConAppCo r tc cos) = pprTcAppCo TyConPrec ppr_co tc cos <> ppr_role r
ppr_co p (AppCo co arg)        = maybeParen p TyConPrec $
                                 pprCo co <+> ppr_co TyConPrec arg
ppr_co p co@(ForAllCo {})      = ppr_forall_co p co
ppr_co _ (CoVarCo cv)          = parenSymOcc (getOccName cv) (ppr cv)
ppr_co p (AxiomInstCo con index args)
216
  = pprPrefixApp p (ppr (getName con) <> brackets (ppr index))
217
                   (map (ppr_co TyConPrec) args)
218

219 220 221 222 223
ppr_co p co@(TransCo {}) = maybeParen p FunPrec $
                           case trans_co_list co [] of
                             [] -> panic "ppr_co"
                             (co:cos) -> sep ( ppr_co FunPrec co
                                             : [ char ';' <+> ppr_co FunPrec co | co <- cos])
224
ppr_co p (InstCo co arg) = maybeParen p TyConPrec $
225
                           pprParendCo co <> text "@" <> ppr_co TopPrec arg
226

227
ppr_co p (UnivCo UnsafeCoerceProv r ty1 ty2)
228
  = pprPrefixApp p (text "UnsafeCo" <+> ppr r)
229
                   [pprParendType ty1, pprParendType ty2]
230 231 232 233
ppr_co _ (UnivCo p r t1 t2)
  = char 'U'
    <> parens (ppr_prov <> comma <+> ppr t1 <> comma <+> ppr t2)
    <> ppr_role r
234
  where
235
    ppr_prov = case p of
236 237 238 239 240 241
      HoleProv h          -> text "hole:"   <> ppr h
      PhantomProv kind_co -> text "phant:"  <> ppr kind_co
      ProofIrrelProv co   -> text "irrel:"  <> ppr co
      PluginProv s        -> text "plugin:" <> text s
      UnsafeCoerceProv    -> text "unsafe"

242 243
ppr_co p (SymCo co)          = pprPrefixApp p (text "Sym") [pprParendCo co]
ppr_co p (NthCo n co)        = pprPrefixApp p (text "Nth:" <> int n) [pprParendCo co]
244 245
ppr_co p (LRCo sel co)       = pprPrefixApp p (ppr sel) [pprParendCo co]
ppr_co p (CoherenceCo c1 c2) = maybeParen p TyConPrec $
246
                               (ppr_co FunPrec c1) <+> (text "|>") <+>
247
                               (ppr_co FunPrec c2)
248 249
ppr_co p (KindCo co)         = pprPrefixApp p (text "kind") [pprParendCo co]
ppr_co p (SubCo co)         = pprPrefixApp p (text "Sub") [pprParendCo co]
250
ppr_co p (AxiomRuleCo co cs) = maybeParen p TopPrec $ ppr_axiom_rule_co co cs
251

252 253
ppr_axiom_rule_co :: CoAxiomRule -> [Coercion] -> SDoc
ppr_axiom_rule_co co ps = ppr (coaxrName co) <+> parens (interpp'SP ps)
254 255

ppr_role :: Role -> SDoc
256 257 258 259 260
ppr_role r = underscore <> pp_role
  where pp_role = case r of
                    Nominal          -> char 'N'
                    Representational -> char 'R'
                    Phantom          -> char 'P'
261

262 263 264 265
trans_co_list :: Coercion -> [Coercion] -> [Coercion]
trans_co_list (TransCo co1 co2) cos = trans_co_list co1 (trans_co_list co2 cos)
trans_co_list co                cos = co : cos

266
ppr_fun_co :: TyPrec -> Coercion -> SDoc
267 268
ppr_fun_co p co = pprArrowChain p (split co)
  where
269
    split :: Coercion -> [SDoc]
270
    split (TyConAppCo _ f [arg, res])
271 272 273 274
      | f `hasKey` funTyConKey
      = ppr_co FunPrec arg : split res
    split co = [ppr_co TopPrec co]

275
ppr_forall_co :: TyPrec -> Coercion -> SDoc
276
ppr_forall_co p (ForAllCo tv h co)
277
  = maybeParen p FunPrec $
278 279 280 281 282 283
    sep [pprCoBndr (tyVarName tv) h, ppr_co TopPrec co]
ppr_forall_co _ _ = panic "ppr_forall_co"

pprCoBndr :: Name -> Coercion -> SDoc
pprCoBndr name eta =
  forAllLit <+> parens (ppr name <+> dcolon <+> ppr eta) <> dot
284

285
pprCoAxiom :: CoAxiom br -> SDoc
286 287 288
pprCoAxiom ax@(CoAxiom { co_ax_branches = branches })
  = hang (text "axiom" <+> ppr ax <+> dcolon)
       2 (vcat (map (ppr_co_ax_branch (const ppr) ax) $ fromBranches branches))
289

290 291 292 293 294 295 296
pprCoAxBranch :: CoAxiom br -> CoAxBranch -> SDoc
pprCoAxBranch = ppr_co_ax_branch pprRhs
  where
    pprRhs fam_tc (TyConApp tycon _)
      | isDataFamilyTyCon fam_tc
      = pprDataCons tycon
    pprRhs _ rhs = ppr rhs
Simon Peyton Jones's avatar
Simon Peyton Jones committed
297 298

pprCoAxBranchHdr :: CoAxiom br -> BranchIndex -> SDoc
299 300 301 302 303 304
pprCoAxBranchHdr ax index = pprCoAxBranch ax (coAxiomNthBranch ax index)

ppr_co_ax_branch :: (TyCon -> Type -> SDoc) -> CoAxiom br -> CoAxBranch -> SDoc
ppr_co_ax_branch ppr_rhs
              (CoAxiom { co_ax_tc = fam_tc, co_ax_name = name })
              (CoAxBranch { cab_tvs = tvs
305
                          , cab_cvs = cvs
306 307 308 309
                          , cab_lhs = lhs
                          , cab_rhs = rhs
                          , cab_loc = loc })
  = foldr1 (flip hangNotEmpty 2)
310
        [ pprUserForAll (map (flip mkNamedBinder Invisible) (tvs ++ cvs))
311 312
        , pprTypeApp fam_tc lhs <+> equals <+> ppr_rhs fam_tc rhs
        , text "-- Defined" <+> pprLoc loc ]
Simon Peyton Jones's avatar
Simon Peyton Jones committed
313
  where
314
        pprLoc loc
Simon Peyton Jones's avatar
Simon Peyton Jones committed
315
          | isGoodSrcSpan loc
316
          = text "at" <+> ppr (srcSpanStart loc)
317

Simon Peyton Jones's avatar
Simon Peyton Jones committed
318
          | otherwise
319
          = text "in" <+>
Simon Peyton Jones's avatar
Simon Peyton Jones committed
320
              quotes (ppr (nameModule name))
321

322
{-
323 324 325 326 327
%************************************************************************
%*                                                                      *
        Destructing coercions
%*                                                                      *
%************************************************************************
328
-}
batterseapower's avatar
batterseapower committed
329

330
-- | This breaks a 'Coercion' with type @T A B C ~ T D E F@ into
331
-- a list of 'Coercion's of kinds @A ~ D@, @B ~ E@ and @E ~ F@. Hence:
batterseapower's avatar
batterseapower committed
332
--
333
-- > decomposeCo 3 c = [nth 0 c, nth 1 c, nth 2 c]
334
decomposeCo :: Arity -> Coercion -> [Coercion]
335
decomposeCo arity co
336 337
  = [mkNthCo n co | n <- [0..(arity-1)] ]
           -- Remember, Nth is zero-indexed
338 339 340

-- | Attempts to obtain the type variable underlying a 'Coercion'
getCoVar_maybe :: Coercion -> Maybe CoVar
341
getCoVar_maybe (CoVarCo cv) = Just cv
342 343
getCoVar_maybe _            = Nothing

344 345 346 347 348 349 350 351 352 353 354
-- | Attempts to tease a coercion apart into a type constructor and the application
-- of a number of coercion arguments to that constructor
splitTyConAppCo_maybe :: Coercion -> Maybe (TyCon, [Coercion])
splitTyConAppCo_maybe (Refl r ty)
  = do { (tc, tys) <- splitTyConApp_maybe ty
       ; let args = zipWith mkReflCo (tyConRolesX r tc) tys
       ; return (tc, args) }
splitTyConAppCo_maybe (TyConAppCo _ tc cos) = Just (tc, cos)
splitTyConAppCo_maybe _                     = Nothing

-- first result has role equal to input; third result is Nominal
355 356
splitAppCo_maybe :: Coercion -> Maybe (Coercion, Coercion)
-- ^ Attempt to take a coercion application apart.
357 358 359 360 361 362 363
splitAppCo_maybe (AppCo co arg) = Just (co, arg)
splitAppCo_maybe (TyConAppCo r tc args)
  | mightBeUnsaturatedTyCon tc || args `lengthExceeds` tyConArity tc
    -- Never create unsaturated type family apps!
  , Just (args', arg') <- snocView args
  , Just arg'' <- setNominalRole_maybe arg'
  = Just ( mkTyConAppCo r tc args', arg'' )
364 365
       -- Use mkTyConAppCo to preserve the invariant
       --  that identity coercions are always represented by Refl
366

367 368
splitAppCo_maybe (Refl r ty)
  | Just (ty1, ty2) <- splitAppTy_maybe ty
369
  = Just (mkReflCo r ty1, mkNomReflCo ty2)
370 371
splitAppCo_maybe _ = Nothing

372 373 374
splitForAllCo_maybe :: Coercion -> Maybe (TyVar, Coercion, Coercion)
splitForAllCo_maybe (ForAllCo tv k_co co) = Just (tv, k_co, co)
splitForAllCo_maybe _                     = Nothing
375 376 377 378

-------------------------------------------------------
-- and some coercion kind stuff

379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395
coVarTypes :: CoVar -> (Type,Type)
coVarTypes cv
  | (_, _, ty1, ty2, _) <- coVarKindsTypesRole cv
  = (ty1, ty2)

coVarKindsTypesRole :: CoVar -> (Kind,Kind,Type,Type,Role)
coVarKindsTypesRole cv
 | Just (tc, [k1,k2,ty1,ty2]) <- splitTyConApp_maybe (varType cv)
 = let role
         | tc `hasKey` eqPrimTyConKey     = Nominal
         | tc `hasKey` eqReprPrimTyConKey = Representational
         | otherwise                      = panic "coVarKindsTypesRole"
   in (k1,k2,ty1,ty2,role)
 | otherwise = pprPanic "coVarKindsTypesRole, non coercion variable"
                        (ppr cv $$ ppr (varType cv))

coVarKind :: CoVar -> Type
396
coVarKind cv
397 398
  = ASSERT( isCoVar cv )
    varType cv
399

400 401 402 403 404 405 406
coVarRole :: CoVar -> Role
coVarRole cv
  | tc `hasKey` eqPrimTyConKey
  = Nominal
  | tc `hasKey` eqReprPrimTyConKey
  = Representational
  | otherwise
407
  = pprPanic "coVarRole: unknown tycon" (ppr cv <+> dcolon <+> ppr (varType cv))
408 409 410 411 412 413

  where
    tc = case tyConAppTyCon_maybe (varType cv) of
           Just tc0 -> tc0
           Nothing  -> pprPanic "coVarRole: not tyconapp" (ppr cv)

414
-- | Makes a coercion type from two types: the types whose equality
415
-- is proven by the relevant 'Coercion'
416 417 418
mkCoercionType :: Role -> Type -> Type -> Type
mkCoercionType Nominal          = mkPrimEqPred
mkCoercionType Representational = mkReprPrimEqPred
419 420 421 422 423 424 425 426 427 428
mkCoercionType Phantom          = \ty1 ty2 ->
  let ki1 = typeKind ty1
      ki2 = typeKind ty2
  in
  TyConApp eqPhantPrimTyCon [ki1, ki2, ty1, ty2]

mkHeteroCoercionType :: Role -> Kind -> Kind -> Type -> Type -> Type
mkHeteroCoercionType Nominal          = mkHeteroPrimEqPred
mkHeteroCoercionType Representational = mkHeteroReprPrimEqPred
mkHeteroCoercionType Phantom          = panic "mkHeteroCoercionType"
429

430 431 432
-- | Tests if this coercion is obviously reflexive. Guaranteed to work
-- very quickly. Sometimes a coercion can be reflexive, but not obviously
-- so. c.f. 'isReflexiveCo'
433
isReflCo :: Coercion -> Bool
434 435
isReflCo (Refl {}) = True
isReflCo _         = False
436

437 438 439
-- | Returns the type coerced if this coercion is reflexive. Guaranteed
-- to work very quickly. Sometimes a coercion can be reflexive, but not
-- obviously so. c.f. 'isReflexiveCo_maybe'
440 441 442
isReflCo_maybe :: Coercion -> Maybe (Type, Role)
isReflCo_maybe (Refl r ty) = Just (ty, r)
isReflCo_maybe _           = Nothing
443

444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459
-- | Slowly checks if the coercion is reflexive. Don't call this in a loop,
-- as it walks over the entire coercion.
isReflexiveCo :: Coercion -> Bool
isReflexiveCo = isJust . isReflexiveCo_maybe

-- | Extracts the coerced type from a reflexive coercion. This potentially
-- walks over the entire coercion, so avoid doing this in a loop.
isReflexiveCo_maybe :: Coercion -> Maybe (Type, Role)
isReflexiveCo_maybe (Refl r ty) = Just (ty, r)
isReflexiveCo_maybe co
  | ty1 `eqType` ty2
  = Just (ty1, r)
  | otherwise
  = Nothing
  where (Pair ty1 ty2, r) = coercionKindRole co

460
{-
461 462
%************************************************************************
%*                                                                      *
463
            Building coercions
464 465 466 467 468
%*                                                                      *
%************************************************************************

These "smart constructors" maintain the invariants listed in the definition
of Coercion, and they perform very basic optimizations.
469

470 471 472 473 474 475 476 477 478
Note [Role twiddling functions]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

There are a plethora of functions for twiddling roles:

mkSubCo: Requires a nominal input coercion and always produces a
representational output. This is used when you (the programmer) are sure you
know exactly that role you have and what you want.

479
downgradeRole_maybe: This function takes both the input role and the output role
480 481 482 483 484 485 486 487
as parameters. (The *output* role comes first!) It can only *downgrade* a
role -- that is, change it from N to R or P, or from R to P. This one-way
behavior is why there is the "_maybe". If an upgrade is requested, this
function produces Nothing. This is used when you need to change the role of a
coercion, but you're not sure (as you're writing the code) of which roles are
involved.

This function could have been written using coercionRole to ascertain the role
488
of the input. But, that function is recursive, and the caller of downgradeRole_maybe
489 490
often knows the input role. So, this is more efficient.

491 492
downgradeRole: This is just like downgradeRole_maybe, but it panics if the
conversion isn't a downgrade.
493

494 495 496 497 498 499 500 501 502 503
setNominalRole_maybe: This is the only function that can *upgrade* a coercion.
The result (if it exists) is always Nominal. The input can be at any role. It
works on a "best effort" basis, as it should never be strictly necessary to
upgrade a coercion during compilation. It is currently only used within GHC in
splitAppCo_maybe. In order to be a proper inverse of mkAppCo, the second
coercion that splitAppCo_maybe returns must be nominal. But, it's conceivable
that splitAppCo_maybe is operating over a TyConAppCo that uses a
representational coercion. Hence the need for setNominalRole_maybe.
splitAppCo_maybe, in turn, is used only within coercion optimization -- thus,
it is not absolutely critical that setNominalRole_maybe be complete.
504 505 506 507 508 509 510

Note that setNominalRole_maybe will never upgrade a phantom UnivCo. Phantom
UnivCos are perfectly type-safe, whereas representational and nominal ones are
not. Indeed, `unsafeCoerce` is implemented via a representational UnivCo.
(Nominal ones are no worse than representational ones, so this function *will*
change a UnivCo Representational to a UnivCo Nominal.)

511 512 513 514
Conal Elliott also came across a need for this function while working with the
GHC API, as he was decomposing Core casts. The Core casts use representational
coercions, as they must, but his use case required nominal coercions (he was
building a GADT). So, that's why this function is exported from this module.
515

516 517 518
One might ask: shouldn't downgradeRole_maybe just use setNominalRole_maybe as
appropriate? I (Richard E.) have decided not to do this, because upgrading a
role is bizarre and a caller should have to ask for this behavior explicitly.
519

520 521 522
Note [mkTransAppCo]
~~~~~~~~~~~~~~~~~~~
Suppose we have
523

524 525
  co1 :: a ~R Maybe
  co2 :: b ~R Int
526

527
and we want
528

529
  co3 :: a b ~R Maybe Int
530

531 532
This seems sensible enough. But, we can't let (co3 = co1 co2), because
that's ill-roled! Note that mkAppCo requires a *nominal* second coercion.
533

534
The way around this is to use transitivity:
535

536
  co3 = (co1 <b>_N) ; (Maybe co2) :: a b ~R Maybe Int
537

538
Or, it's possible everything is the other way around:
539

540 541
  co1' :: Maybe ~R a
  co2' :: Int   ~R b
542

543
and we want
544

545
  co3' :: Maybe Int ~R a b
batterseapower's avatar
batterseapower committed
546

547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567
then

  co3' = (Maybe co2') ; (co1' <b>_N)

This is exactly what `mkTransAppCo` builds for us. Information for all
the arguments tends to be to hand at call sites, so it's quicker than
using, say, coercionKind.

-}

mkReflCo :: Role -> Type -> Coercion
mkReflCo r ty
  = Refl r ty

-- | Make a representational reflexive coercion
mkRepReflCo :: Type -> Coercion
mkRepReflCo = mkReflCo Representational

-- | Make a nominal reflexive coercion
mkNomReflCo :: Type -> Coercion
mkNomReflCo = mkReflCo Nominal
568

569 570 571 572
-- | Apply a type constructor to a list of coercions. It is the
-- caller's responsibility to get the roles correct on argument coercions.
mkTyConAppCo :: Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo r tc cos
573
               -- Expand type synonyms
574
  | Just (tv_co_prs, rhs_ty, leftover_cos) <- expandSynTyCon_maybe tc cos
575
  = mkAppCos (liftCoSubst r (mkLiftingContext tv_co_prs) rhs_ty) leftover_cos
576

577 578
  | Just tys_roles <- traverse isReflCo_maybe cos
  = Refl r (mkTyConApp tc (map fst tys_roles))    -- See Note [Refl invariant]
579

580
  | otherwise = TyConAppCo r tc cos
581 582

-- | Make a function 'Coercion' between two other 'Coercion's
583 584
mkFunCo :: Role -> Coercion -> Coercion -> Coercion
mkFunCo r co1 co2 = mkTyConAppCo r funTyCon [co1, co2]
batterseapower's avatar
batterseapower committed
585

586 587 588
-- | Make nested function 'Coercion's
mkFunCos :: Role -> [Coercion] -> Coercion -> Coercion
mkFunCos r cos res_co = foldr (mkFunCo r) res_co cos
batterseapower's avatar
batterseapower committed
589

590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837
-- | Apply a 'Coercion' to another 'Coercion'.
-- The second coercion must be Nominal, unless the first is Phantom.
-- If the first is Phantom, then the second can be either Phantom or Nominal.
mkAppCo :: Coercion     -- ^ :: t1 ~r t2
        -> Coercion     -- ^ :: s1 ~N s2, where s1 :: k1, s2 :: k2
        -> Coercion     -- ^ :: t1 s1 ~r t2 s2
mkAppCo (Refl r ty1) arg
  | Just (ty2, _) <- isReflCo_maybe arg
  = Refl r (mkAppTy ty1 ty2)

  | Just (tc, tys) <- splitTyConApp_maybe ty1
    -- Expand type synonyms; a TyConAppCo can't have a type synonym (Trac #9102)
  = TyConAppCo r tc (zip_roles (tyConRolesX r tc) tys)
  where
    zip_roles (r1:_)  []            = [downgradeRole r1 Nominal arg]
    zip_roles (r1:rs) (ty1:tys)     = mkReflCo r1 ty1 : zip_roles rs tys
    zip_roles _       _             = panic "zip_roles" -- but the roles are infinite...

mkAppCo (TyConAppCo r tc args) arg
  = case r of
      Nominal          -> TyConAppCo Nominal tc (args ++ [arg])
      Representational -> TyConAppCo Representational tc (args ++ [arg'])
        where new_role = (tyConRolesX Representational tc) !! (length args)
              arg'     = downgradeRole new_role Nominal arg
      Phantom          -> TyConAppCo Phantom tc (args ++ [toPhantomCo arg])
mkAppCo co arg = AppCo co  arg
-- Note, mkAppCo is careful to maintain invariants regarding
-- where Refl constructors appear; see the comments in the definition
-- of Coercion and the Note [Refl invariant] in TyCoRep.

-- | Applies multiple 'Coercion's to another 'Coercion', from left to right.
-- See also 'mkAppCo'.
mkAppCos :: Coercion
         -> [Coercion]
         -> Coercion
mkAppCos co1 cos = foldl mkAppCo co1 cos

-- | Like `mkAppCo`, but allows the second coercion to be other than
-- nominal. See Note [mkTransAppCo]. Role r3 cannot be more stringent
-- than either r1 or r2.
mkTransAppCo :: Role         -- ^ r1
             -> Coercion     -- ^ co1 :: ty1a ~r1 ty1b
             -> Type         -- ^ ty1a
             -> Type         -- ^ ty1b
             -> Role         -- ^ r2
             -> Coercion     -- ^ co2 :: ty2a ~r2 ty2b
             -> Type         -- ^ ty2a
             -> Type         -- ^ ty2b
             -> Role         -- ^ r3
             -> Coercion     -- ^ :: ty1a ty2a ~r3 ty1b ty2b
mkTransAppCo r1 co1 ty1a ty1b r2 co2 ty2a ty2b r3
-- How incredibly fiddly! Is there a better way??
  = case (r1, r2, r3) of
      (_,                _,                Phantom)
        -> mkPhantomCo kind_co (mkAppTy ty1a ty2a) (mkAppTy ty1b ty2b)
        where -- ty1a :: k1a -> k2a
              -- ty1b :: k1b -> k2b
              -- ty2a :: k1a
              -- ty2b :: k1b
              -- ty1a ty2a :: k2a
              -- ty1b ty2b :: k2b
              kind_co1 = mkKindCo co1        -- :: k1a -> k2a ~N k1b -> k2b
              kind_co  = mkNthCo 1 kind_co1  -- :: k2a ~N k2b

      (_,                _,                Nominal)
        -> ASSERT( r1 == Nominal && r2 == Nominal )
           mkAppCo co1 co2
      (Nominal,          Nominal,          Representational)
        -> mkSubCo (mkAppCo co1 co2)
      (_,                Nominal,          Representational)
        -> ASSERT( r1 == Representational )
           mkAppCo co1 co2
      (Nominal,          Representational, Representational)
        -> go (mkSubCo co1)
      (_               , _,                Representational)
        -> ASSERT( r1 == Representational && r2 == Representational )
           go co1
  where
    go co1_repr
      | Just (tc1b, tys1b) <- splitTyConApp_maybe ty1b
      , nextRole ty1b == r2
      = (mkAppCo co1_repr (mkNomReflCo ty2a)) `mkTransCo`
        (mkTyConAppCo Representational tc1b
           (zipWith mkReflCo (tyConRolesX Representational tc1b) tys1b
            ++ [co2]))

      | Just (tc1a, tys1a) <- splitTyConApp_maybe ty1a
      , nextRole ty1a == r2
      = (mkTyConAppCo Representational tc1a
           (zipWith mkReflCo (tyConRolesX Representational tc1a) tys1a
            ++ [co2]))
        `mkTransCo`
        (mkAppCo co1_repr (mkNomReflCo ty2b))

      | otherwise
      = pprPanic "mkTransAppCo" (vcat [ ppr r1, ppr co1, ppr ty1a, ppr ty1b
                                      , ppr r2, ppr co2, ppr ty2a, ppr ty2b
                                      , ppr r3 ])

-- | Make a Coercion from a tyvar, a kind coercion, and a body coercion.
-- The kind of the tyvar should be the left-hand kind of the kind coercion.
mkForAllCo :: TyVar -> Coercion -> Coercion -> Coercion
mkForAllCo tv kind_co co
  | Refl r ty <- co
  , Refl {} <- kind_co
  = Refl r (mkNamedForAllTy tv Invisible ty)
  | otherwise
  = ForAllCo tv kind_co co

-- | Make nested ForAllCos
mkForAllCos :: [(TyVar, Coercion)] -> Coercion -> Coercion
mkForAllCos bndrs (Refl r ty)
  = let (refls_rev'd, non_refls_rev'd) = span (isReflCo . snd) (reverse bndrs) in
    foldl (flip $ uncurry ForAllCo)
          (Refl r $ mkInvForAllTys (reverse (map fst refls_rev'd)) ty)
          non_refls_rev'd
mkForAllCos bndrs co = foldr (uncurry ForAllCo) co bndrs

-- | Make a Coercion quantified over a type variable;
-- the variable has the same type in both sides of the coercion
mkHomoForAllCos :: [TyVar] -> Coercion -> Coercion
mkHomoForAllCos tvs (Refl r ty)
  = Refl r (mkInvForAllTys tvs ty)
mkHomoForAllCos tvs ty = mkHomoForAllCos_NoRefl tvs ty

-- | Like 'mkHomoForAllCos', but doesn't check if the inner coercion
-- is reflexive.
mkHomoForAllCos_NoRefl :: [TyVar] -> Coercion -> Coercion
mkHomoForAllCos_NoRefl tvs orig_co = foldr go orig_co tvs
  where
    go tv co = ForAllCo tv (mkNomReflCo (tyVarKind tv)) co

mkCoVarCo :: CoVar -> Coercion
-- cv :: s ~# t
mkCoVarCo cv
  | ty1 `eqType` ty2 = Refl (coVarRole cv) ty1
  | otherwise        = CoVarCo cv
  where
    (ty1, ty2) = coVarTypes cv

mkCoVarCos :: [CoVar] -> [Coercion]
mkCoVarCos = map mkCoVarCo

-- | Extract a covar, if possible. This check is dirty. Be ashamed
-- of yourself. (It's dirty because it cares about the structure of
-- a coercion, which is morally reprehensible.)
isCoVar_maybe :: Coercion -> Maybe CoVar
isCoVar_maybe (CoVarCo cv) = Just cv
isCoVar_maybe _            = Nothing

mkAxInstCo :: Role -> CoAxiom br -> BranchIndex -> [Type] -> [Coercion]
           -> Coercion
-- mkAxInstCo can legitimately be called over-staturated;
-- i.e. with more type arguments than the coercion requires
mkAxInstCo role ax index tys cos
  | arity == n_tys = downgradeRole role ax_role $
                     mkAxiomInstCo ax_br index (rtys `chkAppend` cos)
  | otherwise      = ASSERT( arity < n_tys )
                     downgradeRole role ax_role $
                     mkAppCos (mkAxiomInstCo ax_br index
                                             (ax_args `chkAppend` cos))
                              leftover_args
  where
    n_tys         = length tys
    ax_br         = toBranchedAxiom ax
    branch        = coAxiomNthBranch ax_br index
    tvs           = coAxBranchTyVars branch
    arity         = length tvs
    arg_roles     = coAxBranchRoles branch
    rtys          = zipWith mkReflCo (arg_roles ++ repeat Nominal) tys
    (ax_args, leftover_args)
                  = splitAt arity rtys
    ax_role       = coAxiomRole ax

-- worker function; just checks to see if it should produce Refl
mkAxiomInstCo :: CoAxiom Branched -> BranchIndex -> [Coercion] -> Coercion
mkAxiomInstCo ax index args
  = ASSERT( coAxiomArity ax index == length args )
    AxiomInstCo ax index args

-- to be used only with unbranched axioms
mkUnbranchedAxInstCo :: Role -> CoAxiom Unbranched
                     -> [Type] -> [Coercion] -> Coercion
mkUnbranchedAxInstCo role ax tys cos
  = mkAxInstCo role ax 0 tys cos

mkAxInstRHS :: CoAxiom br -> BranchIndex -> [Type] -> [Coercion] -> Type
-- Instantiate the axiom with specified types,
-- returning the instantiated RHS
-- A companion to mkAxInstCo:
--    mkAxInstRhs ax index tys = snd (coercionKind (mkAxInstCo ax index tys))
mkAxInstRHS ax index tys cos
  = ASSERT( tvs `equalLength` tys1 )
    mkAppTys rhs' tys2
  where
    branch       = coAxiomNthBranch ax index
    tvs          = coAxBranchTyVars branch
    cvs          = coAxBranchCoVars branch
    (tys1, tys2) = splitAtList tvs tys
    rhs'         = substTyWith tvs tys1 $
                   substTyWithCoVars cvs cos $
                   coAxBranchRHS branch

mkUnbranchedAxInstRHS :: CoAxiom Unbranched -> [Type] -> [Coercion] -> Type
mkUnbranchedAxInstRHS ax = mkAxInstRHS ax 0

-- | Return the left-hand type of the axiom, when the axiom is instantiated
-- at the types given.
mkAxInstLHS :: CoAxiom br -> BranchIndex -> [Type] -> [Coercion] -> Type
mkAxInstLHS ax index tys cos
  = ASSERT( tvs `equalLength` tys1 )
    mkTyConApp fam_tc (lhs_tys `chkAppend` tys2)
  where
    branch       = coAxiomNthBranch ax index
    tvs          = coAxBranchTyVars branch
    cvs          = coAxBranchCoVars branch
    (tys1, tys2) = splitAtList tvs tys
    lhs_tys      = substTysWith tvs tys1 $
                   substTysWithCoVars cvs cos $
                   coAxBranchLHS branch
    fam_tc       = coAxiomTyCon ax

-- | Instantiate the left-hand side of an unbranched axiom
mkUnbranchedAxInstLHS :: CoAxiom Unbranched -> [Type] -> [Coercion] -> Type
mkUnbranchedAxInstLHS ax = mkAxInstLHS ax 0

-- | Manufacture an unsafe coercion from thin air.
--   Currently (May 14) this is used only to implement the
--   @unsafeCoerce#@ primitive.  Optimise by pushing
--   down through type constructors.
mkUnsafeCo :: Role -> Type -> Type -> Coercion
mkUnsafeCo role ty1 ty2
  = mkUnivCo UnsafeCoerceProv role ty1 ty2

-- | Make a coercion from a coercion hole
mkHoleCo :: CoercionHole -> Role
         -> Type -> Type -> Coercion
mkHoleCo h r t1 t2 = mkUnivCo (HoleProv h) r t1 t2

-- | Make a universal coercion between two arbitrary types.
mkUnivCo :: UnivCoProvenance
         -> Role       -- ^ role of the built coercion, "r"
         -> Type       -- ^ t1 :: k1
         -> Type       -- ^ t2 :: k2
         -> Coercion   -- ^ :: t1 ~r t2
mkUnivCo prov role ty1 ty2
  | ty1 `eqType` ty2 = Refl role ty1
  | otherwise        = UnivCo prov role ty1 ty2
batterseapower's avatar
batterseapower committed
838

839 840 841 842 843 844 845
-- | Create a symmetric version of the given 'Coercion' that asserts
--   equality between the same types but in the other "direction", so
--   a kind of @t1 ~ t2@ becomes the kind @t2 ~ t1@.
mkSymCo :: Coercion -> Coercion

-- Do a few simple optimizations, but don't bother pushing occurrences
-- of symmetry to the leaves; the optimizer will take care of that.
846 847 848 849
mkSymCo co@(Refl {})              = co
mkSymCo    (SymCo co)             = co
mkSymCo    (SubCo (SymCo co))     = SubCo co
mkSymCo co                        = SymCo co
850 851 852

-- | Create a new 'Coercion' by composing the two given 'Coercion's transitively.
mkTransCo :: Coercion -> Coercion -> Coercion
853 854 855
mkTransCo co1 (Refl {}) = co1
mkTransCo (Refl {}) co2 = co2
mkTransCo co1 co2       = TransCo co1 co2
856 857 858 859 860

-- the Role is the desired one. It is the caller's responsibility to make
-- sure this request is reasonable
mkNthCoRole :: Role -> Int -> Coercion -> Coercion
mkNthCoRole role n co
861
  = downgradeRole role nth_role $ nth_co
862 863 864
  where
    nth_co = mkNthCo n co
    nth_role = coercionRole nth_co
865 866

mkNthCo :: Int -> Coercion -> Coercion
867 868 869 870 871 872
mkNthCo 0 (Refl _ ty)
  | Just (tv, _) <- splitForAllTy_maybe ty
  = Refl Nominal (tyVarKind tv)
mkNthCo n (Refl r ty)
  = ASSERT( ok_tc_app ty n )
    mkReflCo r' (tyConAppArgN n ty)
873 874
  where tc = tyConAppTyCon ty
        r' = nthRole r tc n
875

876 877 878 879 880 881 882 883 884 885 886
        ok_tc_app :: Type -> Int -> Bool
        ok_tc_app ty n
          | Just (_, tys) <- splitTyConApp_maybe ty
          = tys `lengthExceeds` n
          | isForAllTy ty  -- nth:0 pulls out a kind coercion from a hetero forall
          = n == 0
          | otherwise
          = False

mkNthCo n (TyConAppCo _ _ cos) = cos `getNth` n
mkNthCo n co = NthCo n co
887

888
mkLRCo :: LeftOrRight -> Coercion -> Coercion
889 890
mkLRCo lr (Refl eq ty) = Refl eq (pickLR lr (splitAppTy ty))
mkLRCo lr co           = LRCo lr co
891

892 893 894
-- | Instantiates a 'Coercion'.
mkInstCo :: Coercion -> Coercion -> Coercion
mkInstCo (ForAllCo tv _kind_co body_co) (Refl _ arg)
895
  = substCoWithUnchecked [tv] [arg] body_co
896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932 933 934 935
mkInstCo co arg = InstCo co arg

-- This could work harder to produce Refl coercions, but that would be
-- quite inefficient. Seems better not to try.
mkCoherenceCo :: Coercion -> Coercion -> Coercion
mkCoherenceCo co1 (Refl {}) = co1
mkCoherenceCo (CoherenceCo co1 co2) co3
  = CoherenceCo co1 (co2 `mkTransCo` co3)
mkCoherenceCo co1 co2     = CoherenceCo co1 co2

-- | A CoherenceCo c1 c2 applies the coercion c2 to the left-hand type
-- in the kind of c1. This function uses sym to get the coercion on the
-- right-hand type of c1. Thus, if c1 :: s ~ t, then mkCoherenceRightCo c1 c2
-- has the kind (s ~ (t |> c2)) down through type constructors.
-- The second coercion must be representational.
mkCoherenceRightCo :: Coercion -> Coercion -> Coercion
mkCoherenceRightCo c1 c2 = mkSymCo (mkCoherenceCo (mkSymCo c1) c2)

-- | An explictly directed synonym of mkCoherenceCo. The second
-- coercion must be representational.
mkCoherenceLeftCo :: Coercion -> Coercion -> Coercion
mkCoherenceLeftCo = mkCoherenceCo

infixl 5 `mkCoherenceCo`
infixl 5 `mkCoherenceRightCo`
infixl 5 `mkCoherenceLeftCo`

mkKindCo :: Coercion -> Coercion
mkKindCo (Refl _ ty) = Refl Nominal (typeKind ty)
mkKindCo (UnivCo (PhantomProv h) _ _ _)    = h
mkKindCo (UnivCo (ProofIrrelProv h) _ _ _) = h
mkKindCo co
  | Pair ty1 ty2 <- coercionKind co
       -- generally, calling coercionKind during coercion creation is a bad idea,
       -- as it can lead to exponential behavior. But, we don't have nested mkKindCos,
       -- so it's OK here.
  , typeKind ty1 `eqType` typeKind ty2
  = Refl Nominal (typeKind ty1)
  | otherwise
  = KindCo co
936

937
-- input coercion is Nominal; see also Note [Role twiddling functions]
938 939 940 941
mkSubCo :: Coercion -> Coercion
mkSubCo (Refl Nominal ty) = Refl Representational ty
mkSubCo (TyConAppCo Nominal tc cos)
  = TyConAppCo Representational tc (applyRoles tc cos)
Joachim Breitner's avatar
Joachim Breitner committed
942
mkSubCo co = ASSERT2( coercionRole co == Nominal, ppr co <+> ppr (coercionRole co) )
943 944
             SubCo co

945 946 947 948
-- | Changes a role, but only a downgrade. See Note [Role twiddling functions]
downgradeRole_maybe :: Role   -- ^ desired role
                    -> Role   -- ^ current role
                    -> Coercion -> Maybe Coercion
Simon Peyton Jones's avatar
Simon Peyton Jones committed
949 950
-- In (downgradeRole_maybe dr cr co) it's a precondition that
--                                   cr = coercionRole co
951 952 953
downgradeRole_maybe Representational Nominal co = Just (mkSubCo co)
downgradeRole_maybe Nominal Representational _  = Nothing
downgradeRole_maybe Phantom Phantom          co = Just co
954
downgradeRole_maybe Phantom _                co = Just (toPhantomCo co)
955 956
downgradeRole_maybe _ Phantom                _  = Nothing
downgradeRole_maybe _ _                      co = Just co
957

958 959
-- | Like 'downgradeRole_maybe', but panics if the change isn't a downgrade.
-- See Note [Role twiddling functions]
960 961 962 963
downgradeRole :: Role  -- desired role
              -> Role  -- current role
              -> Coercion -> Coercion
downgradeRole r1 r2 co
964
  = case downgradeRole_maybe r1 r2 co of
965
      Just co' -> co'
966
      Nothing  -> pprPanic "downgradeRole" (ppr co)
967

968 969 970 971 972 973 974 975 976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000
-- | If the EqRel is ReprEq, makes a SubCo; otherwise, does nothing.
-- Note that the input coercion should always be nominal.
maybeSubCo :: EqRel -> Coercion -> Coercion
maybeSubCo NomEq  = id
maybeSubCo ReprEq = mkSubCo


mkAxiomRuleCo :: CoAxiomRule -> [Coercion] -> Coercion
mkAxiomRuleCo = AxiomRuleCo

-- | Make a "coercion between coercions".
mkProofIrrelCo :: Role       -- ^ role of the created coercion, "r"
               -> Coercion   -- ^ :: phi1 ~N phi2
               -> Coercion   -- ^ g1 :: phi1
               -> Coercion   -- ^ g2 :: phi2
               -> Coercion   -- ^ :: g1 ~r g2

-- if the two coercion prove the same fact, I just don't care what
-- the individual coercions are.
mkProofIrrelCo r (Refl {}) g  _  = Refl r (CoercionTy g)
mkProofIrrelCo r kco       g1 g2 = mkUnivCo (ProofIrrelProv kco) r
                                     (mkCoercionTy g1) (mkCoercionTy g2)

{-
%************************************************************************
%*                                                                      *
   Roles
%*                                                                      *
%************************************************************************
-}

-- | Converts a coercion to be nominal, if possible.
-- See Note [Role twiddling functions]
1001 1002
setNominalRole_maybe :: Coercion -> Maybe Coercion
setNominalRole_maybe co
1003
  | Nominal <- coercionRole co = Just co
1004 1005
setNominalRole_maybe (SubCo co)  = Just co
setNominalRole_maybe (Refl _ ty) = Just $ Refl Nominal ty
1006 1007
setNominalRole_maybe (TyConAppCo Representational tc cos)
  = do { cos' <- mapM setNominalRole_maybe cos
1008
       ; return $ TyConAppCo Nominal tc cos' }
1009 1010
setNominalRole_maybe (SymCo co)
  = SymCo <$> setNominalRole_maybe co
1011 1012 1013 1014
setNominalRole_maybe (TransCo co1 co2)
  = TransCo <$> setNominalRole_maybe co1 <*> setNominalRole_maybe co2
setNominalRole_maybe (AppCo co1 co2)
  = AppCo <$> setNominalRole_maybe co1 <*> pure co2
1015 1016
setNominalRole_maybe (ForAllCo tv kind_co co)
  = ForAllCo tv kind_co <$> setNominalRole_maybe co
1017 1018
setNominalRole_maybe (NthCo n co)
  = NthCo n <$> setNominalRole_maybe co
1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029
setNominalRole_maybe (InstCo co arg)
  = InstCo <$> setNominalRole_maybe co <*> pure arg
setNominalRole_maybe (CoherenceCo co1 co2)
  = CoherenceCo <$> setNominalRole_maybe co1 <*> pure co2
setNominalRole_maybe (UnivCo prov _ co1 co2)
  | case prov of UnsafeCoerceProv -> True   -- it's always unsafe
                 PhantomProv _    -> False  -- should always be phantom
                 ProofIrrelProv _ -> True   -- it's always safe
                 PluginProv _     -> False  -- who knows? This choice is conservative.
                 HoleProv _       -> False  -- no no no.
  = Just $ UnivCo prov Nominal co1 co2
1030
setNominalRole_maybe _ = Nothing
1031

1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046
-- | Make a phantom coercion between two types. The coercion passed
-- in must be a nominal coercion between the kinds of the
-- types.
mkPhantomCo :: Coercion -> Type -> Type -> Coercion
mkPhantomCo h t1 t2
  = mkUnivCo (PhantomProv h) Phantom t1 t2

-- | Make a phantom coercion between two types of the same kind.
mkHomoPhantomCo :: Type -> Type -> Coercion
mkHomoPhantomCo t1 t2
  = ASSERT( k1 `eqType` typeKind t2 )
    mkPhantomCo (mkNomReflCo k1) t1 t2
  where
    k1 = typeKind t1

1047
-- takes any coercion and turns it into a Phantom coercion
1048 1049 1050 1051
toPhantomCo :: Coercion -> Coercion
toPhantomCo co
  = mkPhantomCo (mkKindCo co) ty1 ty2
  where Pair ty1 ty2 = coercionKind co
1052 1053 1054 1055

-- Convert args to a TyConAppCo Nominal to the same TyConAppCo Representational
applyRoles :: TyCon -> [Coercion] -> [Coercion]
applyRoles tc cos
1056
  = zipWith (\r -> downgradeRole r Nominal) (tyConRolesX Representational tc) cos
1057 1058 1059 1060 1061 1062 1063 1064 1065 1066 1067 1068

-- the Role parameter is the Role of the TyConAppCo
-- defined here because this is intimiately concerned with the implementation
-- of TyConAppCo
tyConRolesX :: Role -> TyCon -> [Role]
tyConRolesX Representational tc = tyConRoles tc ++ repeat Nominal
tyConRolesX role             _  = repeat role

nthRole :: Role -> TyCon -> Int -> Role
nthRole Nominal _ _ = Nominal
nthRole Phantom _ _ = Phantom
nthRole Representational tc n
1069
  = (tyConRolesX Representational tc) `getNth` n
1070 1071

ltRole :: Role -> Role -> Bool
1072 1073
-- Is one role "less" than another?
--     Nominal < Representational < Phantom
1074 1075 1076 1077 1078
ltRole Phantom          _       = False
ltRole Representational Phantom = True
ltRole Representational _       = False
ltRole Nominal          Nominal = False
ltRole Nominal          _       = True
1079

1080 1081 1082 1083 1084 1085 1086 1087 1088 1089 1090 1091 1092 1093 1094 1095 1096 1097 1098 1099 1100 1101 1102 1103 1104 1105 1106 1107 1108 1109 1110 1111 1112 1113 1114 1115 1116 1117 1118 1119 1120 1121 1122 1123 1124 1125 1126 1127 1128 1129 1130 1131 1132 1133 1134 1135 1136 1137 1138 1139 1140 1141 1142 1143 1144 1145 1146 1147 1148 1149 1150 1151 1152 1153 1154 1155 1156 1157 1158 1159 1160 1161 1162 1163 1164 1165 1166 1167 1168 1169 1170 1171 1172 1173 1174 1175 1176 1177 1178 1179 1180 1181