Coercion.hs 78.6 KB
Newer Older
1
-- (c) The University of Glasgow 2006
2

3 4
{-# LANGUAGE CPP, DeriveDataTypeable #-}

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

dreixel's avatar
dreixel committed
15
        -- ** Functions over coercions
16
        coVarKind, coVarRole,
17
        coercionType, coercionKind, coercionKinds, isReflCo,
18
        isReflCo_maybe, coercionRole, coercionKindRole,
batterseapower's avatar
batterseapower committed
19
        mkCoercionType,
20

21
        -- ** Constructing coercions
22
        mkReflCo, mkCoVarCo,
23
        mkAxInstCo, mkUnbranchedAxInstCo, mkAxInstLHS, mkAxInstRHS,
24
        mkUnbranchedAxInstRHS,
25
        mkPiCo, mkPiCos, mkCoCast,
26
        mkSymCo, mkTransCo, mkNthCo, mkNthCoRole, mkLRCo,
27
        mkInstCo, mkAppCo, mkAppCoFlexible, mkTyConAppCo, mkFunCo,
28
        mkForAllCo, mkUnsafeCo, mkUnivCo, mkSubCo, mkPhantomCo,
29
        mkNewTypeCo, downgradeRole,
30
        mkAxiomRuleCo,
TomSchrijvers's avatar
TomSchrijvers committed
31

32
        -- ** Decomposition
33
        instNewTyCon_maybe,
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
34 35 36 37

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

39
        decomposeCo, getCoVar_maybe,
40 41
        splitAppCo_maybe,
        splitForAllCo_maybe,
42
        nthRole, tyConRolesX,
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
43
        setNominalRole_maybe,
44

45 46
        -- ** Coercion variables
        mkCoVar, isCoVar, isCoVarType, coVarName, setCoVarName, setCoVarUnique,
47 48 49

        -- ** Free variables
        tyCoVarsOfCo, tyCoVarsOfCos, coVarsOfCo, coercionSize,
50

51
        -- ** Substitution
52
        CvSubstEnv, emptyCvSubstEnv,
53 54
        CvSubst(..), emptyCvSubst, Coercion.lookupTyVar, lookupCoVar,
        isEmptyCvSubst, zapCvSubstEnv, getCvInScope,
55
        substCo, substCos, substCoVar, substCoVars,
56
        substCoWithTy, substCoWithTys,
57
        cvTvSubst, tvCvSubst, mkCvSubst, zipOpenCvSubst,
58 59
        substTy, extendTvSubst,
        extendCvSubstAndInScope, extendTvSubstAndInScope,
60
        substTyVarBndr, substCoVarBndr,
61

62 63
        -- ** Lifting
        liftCoMatch, liftCoSubstTyVar, liftCoSubstWith,
64

batterseapower's avatar
batterseapower committed
65
        -- ** Comparison
66
        coreEqCoercion, coreEqCoercion2,
67

68 69
        -- ** Forcing evaluation of coercions
        seqCo,
70

71
        -- * Pretty-printing
72 73
        pprCo, pprParendCo,
        pprCoAxiom, pprCoAxBranch, pprCoAxBranchHdr,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
74 75 76

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

78
        -- * Other
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
79
        applyCo,
80
       ) where
81 82 83

#include "HsVersions.h"

84
import Unify    ( MatchEnv(..), matchList )
85
import TypeRep
86 87
import qualified Type
import Type hiding( substTy, substTyVarBndr, extendTvSubst )
88
import TyCon
89
import CoAxiom
90
import Var
91
import VarEnv
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
92
import VarSet
93
import Binary
94
import Maybes   ( orElse )
95 96
import Name     ( Name, NamedThing(..), nameUnique, nameModule, getSrcSpan )
import OccName  ( parenSymOcc )
97 98
import Util
import BasicTypes
99
import Outputable
100 101
import Unique
import Pair
Simon Peyton Jones's avatar
Simon Peyton Jones committed
102
import SrcLoc
103
import PrelNames        ( funTyConKey, eqPrimTyConKey, eqReprPrimTyConKey )
104
#if __GLASGOW_HASKELL__ < 709
105
import Control.Applicative hiding ( empty )
106
import Data.Traversable (traverse, sequenceA)
107
#endif
108
import FastString
109
import ListSetOps
110 111

import qualified Data.Data as Data hiding ( TyCon )
112
import Control.Arrow ( first )
113

114 115 116
{-
************************************************************************
*                                                                      *
117
            Coercions
118 119 120
*                                                                      *
************************************************************************
-}
121

122 123
-- | A 'Coercion' is concrete evidence of the equality/convertibility
-- of two types.
124

125
-- If you edit this type, you may need to update the GHC formalism
126
-- See Note [GHC Formalism] in coreSyn/CoreLint.hs
127
data Coercion
128 129 130 131 132 133 134
  -- Each constructor has a "role signature", indicating the way roles are
  -- propagated through coercions. P, N, and R stand for coercions of the
  -- given role. e stands for a coercion of a specific unknown role (think
  -- "role polymorphism"). "e" stands for an explicit role parameter
  -- indicating role e. _ stands for a parameter that is not a Role or
  -- Coercion.

135
  -- These ones mirror the shape of types
136 137
  = -- Refl :: "e" -> _ -> e
    Refl Role Type  -- See Note [Refl invariant]
138 139 140 141 142 143 144 145 146 147
          -- Invariant: applications of (Refl T) to a bunch of identity coercions
          --            always show up as Refl.
          -- For example  (Refl T) (Refl a) (Refl b) shows up as (Refl (T a b)).

          -- Applications of (Refl T) to some coercions, at least one of
          -- which is NOT the identity, show up as TyConAppCo.
          -- (They may not be fully saturated however.)
          -- ConAppCo coercions (like all coercions other than Refl)
          -- are NEVER the identity.

148 149
          -- Use (Refl Representational _), not (SubCo (Refl Nominal _))

150
  -- These ones simply lift the correspondingly-named
151
  -- Type constructors into Coercions
152

153 154
  -- TyConAppCo :: "e" -> _ -> ?? -> e
  -- See Note [TyConAppCo roles]
155
  | TyConAppCo Role TyCon [Coercion]    -- lift TyConApp
156 157 158
               -- The TyCon is never a synonym;
               -- we expand synonyms eagerly
               -- But it can be a type function
159 160

  | AppCo Coercion Coercion        -- lift AppTy
161
          -- AppCo :: e -> N -> e
162 163 164

  -- See Note [Forall coercions]
  | ForAllCo TyVar Coercion       -- forall a. g
165
         -- :: _ -> e -> e
166 167

  -- These are special
168 169 170 171
  | CoVarCo CoVar      -- :: _ -> (N or R)
                       -- result role depends on the tycon of the variable's type

    -- AxiomInstCo :: e -> _ -> [N] -> e
172
  | AxiomInstCo (CoAxiom Branched) BranchIndex [Coercion]
173
     -- See also [CoAxiom index]
174
     -- The coercion arguments always *precisely* saturate
175
     -- arity of (that branch of) the CoAxiom.  If there are
176
     -- any left over, we use AppCo.  See
177 178
     -- See [Coercion axioms applied to coercions]

179
         -- see Note [UnivCo]
180 181
  | UnivCo FastString Role Type Type -- :: "e" -> _ -> _ -> e
                               -- the FastString is just a note for provenance
182 183
  | SymCo Coercion             -- :: e -> e
  | TransCo Coercion Coercion  -- :: e -> e -> e
184

185 186 187 188
    -- The number of types and coercions should match exactly the expectations
    -- of the CoAxiomRule (i.e., the rule is fully saturated).
  | AxiomRuleCo CoAxiomRule [Type] [Coercion]

189
  -- These are destructors
190

Jan Stolarek's avatar
Jan Stolarek committed
191 192
  | NthCo  Int         Coercion  -- Zero-indexed; decomposes (T t0 ... tn)
                                 -- and (F t0 ... tn), assuming F is injective.
193
    -- :: _ -> e -> ?? (inverse of TyConAppCo, see Note [TyConAppCo roles])
194 195
    -- See Note [NthCo and newtypes]

196
  | LRCo   LeftOrRight Coercion     -- Decomposes (t_left t_right)
197
    -- :: _ -> N -> N
198
  | InstCo Coercion Type
199 200 201 202
    -- :: e -> _ -> e

  | SubCo Coercion                  -- Turns a ~N into a ~R
    -- :: N -> R
203
  deriving (Data.Data, Data.Typeable)
204

205
-- If you edit this type, you may need to update the GHC formalism
206
-- See Note [GHC Formalism] in coreSyn/CoreLint.hs
207
data LeftOrRight = CLeft | CRight
208 209
                 deriving( Eq, Data.Data, Data.Typeable )

210 211 212 213 214 215 216 217 218
instance Binary LeftOrRight where
   put_ bh CLeft  = putByte bh 0
   put_ bh CRight = putByte bh 1

   get bh = do { h <- getByte bh
               ; case h of
                   0 -> return CLeft
                   _ -> return CRight }

219 220 221
pickLR :: LeftOrRight -> (a,a) -> a
pickLR CLeft  (l,_) = l
pickLR CRight (_,r) = r
222

223
{-
224 225
Note [Refl invariant]
~~~~~~~~~~~~~~~~~~~~~
226 227
Coercions have the following invariant
     Refl is always lifted as far as possible.
228 229 230 231 232 233 234 235 236 237 238 239 240 241 242

You might think that a consequencs is:
     Every identity coercions has Refl at the root

But that's not quite true because of coercion variables.  Consider
     g         where g :: Int~Int
     Left h    where h :: Maybe Int ~ Maybe Int
etc.  So the consequence is only true of coercions that
have no coercion variables.

Note [Coercion axioms applied to coercions]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The reason coercion axioms can be applied to coercions and not just
types is to allow for better optimization.  There are some cases where
we need to be able to "push transitivity inside" an axiom in order to
243
expose further opportunities for optimization.
244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278

For example, suppose we have

  C a : t[a] ~ F a
  g   : b ~ c

and we want to optimize

  sym (C b) ; t[g] ; C c

which has the kind

  F b ~ F c

(stopping through t[b] and t[c] along the way).

We'd like to optimize this to just F g -- but how?  The key is
that we need to allow axioms to be instantiated by *coercions*,
not just by types.  Then we can (in certain cases) push
transitivity inside the axiom instantiations, and then react
opposite-polarity instantiations of the same axiom.  In this
case, e.g., we match t[g] against the LHS of (C c)'s kind, to
obtain the substitution  a |-> g  (note this operation is sort
of the dual of lifting!) and hence end up with

  C g : t[b] ~ F c

which indeed has the same kind as  t[g] ; C c.

Now we have

  sym (C b) ; C g

which can be optimized to F g.

279 280 281 282 283 284 285 286 287 288 289 290
Note [CoAxiom index]
~~~~~~~~~~~~~~~~~~~~
A CoAxiom has 1 or more branches. Each branch has contains a list
of the free type variables in that branch, the LHS type patterns,
and the RHS type for that branch. When we apply an axiom to a list
of coercions, we must choose which branch of the axiom we wish to
use, as the different branches may have different numbers of free
type variables. (The number of type patterns is always the same
among branches, but that doesn't quite concern us here.)

The Int in the AxiomInstCo constructor is the 0-indexed number
of the chosen branch.
291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308

Note [Forall coercions]
~~~~~~~~~~~~~~~~~~~~~~~
Constructing coercions between forall-types can be a bit tricky.
Currently, the situation is as follows:

  ForAllCo TyVar Coercion

represents a coercion between polymorphic types, with the rule

           v : k       g : t1 ~ t2
  ----------------------------------------------
  ForAllCo v g : (all v:k . t1) ~ (all v:k . t2)

Note that it's only necessary to coerce between polymorphic types
where the type variables have identical kinds, because equality on
kinds is trivial.

309 310 311 312 313 314 315 316 317
Note [Predicate coercions]
~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we have
   g :: a~b
How can we coerce between types
   ([c]~a) => [a] -> c
and
   ([c]~b) => [b] -> c
where the equality predicate *itself* differs?
318

319 320
Answer: we simply treat (~) as an ordinary type constructor, so these
types really look like
321

322 323
   ((~) [c] a) -> [a] -> c
   ((~) [c] b) -> [b] -> c
324

325
So the coercion between the two is obviously
326

327
   ((~) [c] g) -> [g] -> c
328

329 330
Another way to see this to say that we simply collapse predicates to
their representation type (see Type.coreView and Type.predTypeRep).
331

332
This collapse is done by mkPredCo; there is no PredCo constructor
333
in Coercion.  This is important because we need Nth to work on
334 335 336
predicates too:
    Nth 1 ((~) [c] g) = g
See Simplify.simplCoercionF, which generates such selections.
337

dreixel's avatar
dreixel committed
338 339 340 341 342 343 344 345 346 347 348 349 350
Note [Kind coercions]
~~~~~~~~~~~~~~~~~~~~~
Suppose T :: * -> *, and g :: A ~ B
Then the coercion
   TyConAppCo T [g]      T g : T A ~ T B

Now suppose S :: forall k. k -> *, and g :: A ~ B
Then the coercion
   TyConAppCo S [Refl *, g]   T <*> g : T * A ~ T * B

Notice that the arguments to TyConAppCo are coercions, but the first
represents a *kind* coercion. Now, we don't allow any non-trivial kind
coercions, so it's an invariant that any such kind coercions are Refl.
351
Lint checks this.
dreixel's avatar
dreixel committed
352 353 354

However it's inconvenient to insist that these kind coercions are always
*structurally* (Refl k), because the key function exprIsConApp_maybe
355
pushes coercions into constructor arguments, so
dreixel's avatar
dreixel committed
356 357 358 359 360
       C k ty e |> g
may turn into
       C (Nth 0 g) ....
Now (Nth 0 g) will optimise to Refl, but perhaps not instantly.

361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475
Note [Roles]
~~~~~~~~~~~~
Roles are a solution to the GeneralizedNewtypeDeriving problem, articulated
in Trac #1496. The full story is in docs/core-spec/core-spec.pdf. Also, see
http://ghc.haskell.org/trac/ghc/wiki/RolesImplementation

Here is one way to phrase the problem:

Given:
newtype Age = MkAge Int
type family F x
type instance F Age = Bool
type instance F Int = Char

This compiles down to:
axAge :: Age ~ Int
axF1 :: F Age ~ Bool
axF2 :: F Int ~ Char

Then, we can make:
(sym (axF1) ; F axAge ; axF2) :: Bool ~ Char

Yikes!

The solution is _roles_, as articulated in "Generative Type Abstraction and
Type-level Computation" (POPL 2010), available at
http://www.seas.upenn.edu/~sweirich/papers/popl163af-weirich.pdf

The specification for roles has evolved somewhat since that paper. For the
current full details, see the documentation in docs/core-spec. Here are some
highlights.

We label every equality with a notion of type equivalence, of which there are
three options: Nominal, Representational, and Phantom. A ground type is
nominally equivalent only with itself. A newtype (which is considered a ground
type in Haskell) is representationally equivalent to its representation.
Anything is "phantomly" equivalent to anything else. We use "N", "R", and "P"
to denote the equivalences.

The axioms above would be:
axAge :: Age ~R Int
axF1 :: F Age ~N Bool
axF2 :: F Age ~N Char

Then, because transitivity applies only to coercions proving the same notion
of equivalence, the above construction is impossible.

However, there is still an escape hatch: we know that any two types that are
nominally equivalent are representationally equivalent as well. This is what
the form SubCo proves -- it "demotes" a nominal equivalence into a
representational equivalence. So, it would seem the following is possible:

sub (sym axF1) ; F axAge ; sub axF2 :: Bool ~R Char   -- WRONG

What saves us here is that the arguments to a type function F, lifted into a
coercion, *must* prove nominal equivalence. So, (F axAge) is ill-formed, and
we are safe.

Roles are attached to parameters to TyCons. When lifting a TyCon into a
coercion (through TyConAppCo), we need to ensure that the arguments to the
TyCon respect their roles. For example:

data T a b = MkT a (F b)

If we know that a1 ~R a2, then we know (T a1 b) ~R (T a2 b). But, if we know
that b1 ~R b2, we know nothing about (T a b1) and (T a b2)! This is because
the type function F branches on b's *name*, not representation. So, we say
that 'a' has role Representational and 'b' has role Nominal. The third role,
Phantom, is for parameters not used in the type's definition. Given the
following definition

data Q a = MkQ Int

the Phantom role allows us to say that (Q Bool) ~R (Q Char), because we
can construct the coercion Bool ~P Char (using UnivCo).

See the paper cited above for more examples and information.

Note [UnivCo]
~~~~~~~~~~~~~
The UnivCo ("universal coercion") serves two rather separate functions:
 - the implementation for unsafeCoerce#
 - placeholder for phantom parameters in a TyConAppCo

At Representational, it asserts that two (possibly unrelated)
types have the same representation and can be casted to one another.
This form is necessary for unsafeCoerce#.

For optimisation purposes, it is convenient to allow UnivCo to appear
at Nominal role. If we have

data Foo a = MkFoo (F a)   -- F is a type family

and we want an unsafe coercion from Foo Int to Foo Bool, then it would
be nice to have (TyConAppCo Foo (UnivCo Nominal Int Bool)). So, we allow
Nominal UnivCo's.

At Phantom role, it is used as an argument to TyConAppCo in the place
of a phantom parameter (a type parameter unused in the type definition).

For example:

data Q a = MkQ Int

We want a coercion for (Q Bool) ~R (Q Char).

(TyConAppCo Representational Q [UnivCo Phantom Bool Char]) does the trick.

Note [TyConAppCo roles]
~~~~~~~~~~~~~~~~~~~~~~~
The TyConAppCo constructor has a role parameter, indicating the role at
which the coercion proves equality. The choice of this parameter affects
the required roles of the arguments of the TyConAppCo. To help explain
it, assume the following definition:

Simon Peyton Jones's avatar
Simon Peyton Jones committed
476 477
  type instance F Int = Bool   -- Axiom axF : F Int ~N Bool
  newtype Age = MkAge Int      -- Axiom axAge : Age ~R Int
478
  data Foo a = MkFoo a         -- Role on Foo's parameter is Representational
479

Simon Peyton Jones's avatar
Simon Peyton Jones committed
480 481 482
TyConAppCo Nominal Foo axF : Foo (F Int) ~N Foo Bool
  For (TyConAppCo Nominal) all arguments must have role Nominal. Why?
  So that Foo Age ~N Foo Int does *not* hold.
483

Simon Peyton Jones's avatar
Simon Peyton Jones committed
484 485 486 487 488 489
TyConAppCo Representational Foo (SubCo axF) : Foo (F Int) ~R Foo Bool
TyConAppCo Representational Foo axAge       : Foo Age     ~R Foo Int
  For (TyConAppCo Representational), all arguments must have the roles
  corresponding to the result of tyConRoles on the TyCon. This is the
  whole point of having roles on the TyCon to begin with. So, we can
  have Foo Age ~R Foo Int, if Foo's parameter has role R.
490

Simon Peyton Jones's avatar
Simon Peyton Jones committed
491 492 493
  If a Representational TyConAppCo is over-saturated (which is otherwise fine),
  the spill-over arguments must all be at Nominal. This corresponds to the
  behavior for AppCo.
494

Simon Peyton Jones's avatar
Simon Peyton Jones committed
495 496 497
TyConAppCo Phantom Foo (UnivCo Phantom Int Bool) : Foo Int ~P Foo Bool
  All arguments must have role Phantom. This one isn't strictly
  necessary for soundness, but this choice removes ambiguity.
498

Simon Peyton Jones's avatar
Simon Peyton Jones committed
499 500
The rules here dictate the roles of the parameters to mkTyConAppCo
(should be checked by Lint).
501

502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529
Note [NthCo and newtypes]
~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we have

  newtype N a = MkN Int
  type role N representational

This yields axiom

  NTCo:N :: forall a. N a ~R Int

We can then build

  co :: forall a b. N a ~R N b
  co = NTCo:N a ; sym (NTCo:N b)

for any `a` and `b`. Because of the role annotation on N, if we use
NthCo, we'll get out a representational coercion. That is:

  NthCo 0 co :: forall a b. a ~R b

Yikes! Clearly, this is terrible. The solution is simple: forbid
NthCo to be used on newtypes if the internal coercion is representational.

This is not just some corner case discovered by a segfault somewhere;
it was discovered in the proof of soundness of roles and described
in the "Safe Coercions" paper (ICFP '14).

530 531
************************************************************************
*                                                                      *
532
\subsection{Coercion variables}
533 534 535
*                                                                      *
************************************************************************
-}
536 537 538 539 540 541 542 543 544 545 546 547 548 549

coVarName :: CoVar -> Name
coVarName = varName

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

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

isCoVar :: Var -> Bool
isCoVar v = isCoVarType (varType v)

isCoVarType :: Type -> Bool
550
isCoVarType ty      -- Tests for t1 ~# t2, the unboxed equality
551
  = case splitTyConApp_maybe ty of
552 553
      Just (tc,tys) -> (tc `hasKey` eqPrimTyConKey || tc `hasKey` eqReprPrimTyConKey)
                       && tys `lengthAtLeast` 2
554
      Nothing       -> False
555 556 557

tyCoVarsOfCo :: Coercion -> VarSet
-- Extracts type and coercion variables from a coercion
558 559 560 561 562
tyCoVarsOfCo (Refl _ ty)           = tyVarsOfType ty
tyCoVarsOfCo (TyConAppCo _ _ cos)  = tyCoVarsOfCos cos
tyCoVarsOfCo (AppCo co1 co2)       = tyCoVarsOfCo co1 `unionVarSet` tyCoVarsOfCo co2
tyCoVarsOfCo (ForAllCo tv co)      = tyCoVarsOfCo co `delVarSet` tv
tyCoVarsOfCo (CoVarCo v)           = unitVarSet v
563
tyCoVarsOfCo (AxiomInstCo _ _ cos) = tyCoVarsOfCos cos
564
tyCoVarsOfCo (UnivCo _ _ ty1 ty2)  = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2
565 566 567 568 569 570
tyCoVarsOfCo (SymCo co)            = tyCoVarsOfCo co
tyCoVarsOfCo (TransCo co1 co2)     = tyCoVarsOfCo co1 `unionVarSet` tyCoVarsOfCo co2
tyCoVarsOfCo (NthCo _ co)          = tyCoVarsOfCo co
tyCoVarsOfCo (LRCo _ co)           = tyCoVarsOfCo co
tyCoVarsOfCo (InstCo co ty)        = tyCoVarsOfCo co `unionVarSet` tyVarsOfType ty
tyCoVarsOfCo (SubCo co)            = tyCoVarsOfCo co
571
tyCoVarsOfCo (AxiomRuleCo _ ts cs) = tyVarsOfTypes ts `unionVarSet` tyCoVarsOfCos cs
572 573

tyCoVarsOfCos :: [Coercion] -> VarSet
574
tyCoVarsOfCos = mapUnionVarSet tyCoVarsOfCo
575 576 577

coVarsOfCo :: Coercion -> VarSet
-- Extract *coerction* variables only.  Tiresome to repeat the code, but easy.
578 579 580 581 582
coVarsOfCo (Refl _ _)            = emptyVarSet
coVarsOfCo (TyConAppCo _ _ cos)  = coVarsOfCos cos
coVarsOfCo (AppCo co1 co2)       = coVarsOfCo co1 `unionVarSet` coVarsOfCo co2
coVarsOfCo (ForAllCo _ co)       = coVarsOfCo co
coVarsOfCo (CoVarCo v)           = unitVarSet v
583
coVarsOfCo (AxiomInstCo _ _ cos) = coVarsOfCos cos
584
coVarsOfCo (UnivCo _ _ _ _)      = emptyVarSet
585 586 587 588 589 590
coVarsOfCo (SymCo co)            = coVarsOfCo co
coVarsOfCo (TransCo co1 co2)     = coVarsOfCo co1 `unionVarSet` coVarsOfCo co2
coVarsOfCo (NthCo _ co)          = coVarsOfCo co
coVarsOfCo (LRCo _ co)           = coVarsOfCo co
coVarsOfCo (InstCo co _)         = coVarsOfCo co
coVarsOfCo (SubCo co)            = coVarsOfCo co
591
coVarsOfCo (AxiomRuleCo _ _ cos) = coVarsOfCos cos
592 593

coVarsOfCos :: [Coercion] -> VarSet
594
coVarsOfCos = mapUnionVarSet coVarsOfCo
595 596

coercionSize :: Coercion -> Int
597 598 599 600 601
coercionSize (Refl _ ty)           = typeSize ty
coercionSize (TyConAppCo _ _ cos)  = 1 + sum (map coercionSize cos)
coercionSize (AppCo co1 co2)       = coercionSize co1 + coercionSize co2
coercionSize (ForAllCo _ co)       = 1 + coercionSize co
coercionSize (CoVarCo _)           = 1
602
coercionSize (AxiomInstCo _ _ cos) = 1 + sum (map coercionSize cos)
603
coercionSize (UnivCo _ _ ty1 ty2)  = typeSize ty1 + typeSize ty2
604 605 606 607 608 609
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 ty)        = 1 + coercionSize co + typeSize ty
coercionSize (SubCo co)            = 1 + coercionSize co
610 611
coercionSize (AxiomRuleCo _ tys cos) = 1 + sum (map typeSize tys)
                                         + sum (map coercionSize cos)
612

613 614 615
{-
************************************************************************
*                                                                      *
Simon Peyton Jones's avatar
Simon Peyton Jones committed
616
                            Tidying coercions
617 618 619
*                                                                      *
************************************************************************
-}
Simon Peyton Jones's avatar
Simon Peyton Jones committed
620 621 622 623 624

tidyCo :: TidyEnv -> Coercion -> Coercion
tidyCo env@(_, subst) co
  = go co
  where
625 626 627 628 629 630 631 632 633 634
    go (Refl r ty)            = Refl r (tidyType env ty)
    go (TyConAppCo r tc cos)  = let args = map go cos
                                in args `seqList` TyConAppCo r tc args
    go (AppCo co1 co2)        = (AppCo $! go co1) $! go co2
    go (ForAllCo tv co)       = ForAllCo tvp $! (tidyCo envp co)
                                where
                                  (envp, tvp) = tidyTyVarBndr env tv
    go (CoVarCo cv)           = case lookupVarEnv subst cv of
                                  Nothing  -> CoVarCo cv
                                  Just cv' -> CoVarCo cv'
Simon Peyton Jones's avatar
Simon Peyton Jones committed
635
    go (AxiomInstCo con ind cos) = let args = tidyCos env cos
636
                                   in args `seqList` AxiomInstCo con ind args
637
    go (UnivCo s r ty1 ty2)   = (UnivCo s r $! tidyType env ty1) $! tidyType env ty2
638 639 640 641 642 643
    go (SymCo co)             = SymCo $! go co
    go (TransCo co1 co2)      = (TransCo $! go co1) $! go co2
    go (NthCo d co)           = NthCo d $! go co
    go (LRCo lr co)           = LRCo lr $! go co
    go (InstCo co ty)         = (InstCo $! go co) $! tidyType env ty
    go (SubCo co)             = SubCo $! go co
Simon Peyton Jones's avatar
Simon Peyton Jones committed
644

645 646 647 648 649 650
    go (AxiomRuleCo ax tys cos) = let tys1 = map (tidyType env) tys
                                      cos1 = tidyCos env cos
                                  in tys1 `seqList` cos1 `seqList`
                                     AxiomRuleCo ax tys1 cos1


Simon Peyton Jones's avatar
Simon Peyton Jones committed
651 652 653
tidyCos :: TidyEnv -> [Coercion] -> [Coercion]
tidyCos env = map (tidyCo env)

654 655 656
{-
************************************************************************
*                                                                      *
657
                   Pretty-printing coercions
658 659
*                                                                      *
************************************************************************
660

661 662 663 664 665
@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.
666
-}
667

668 669 670 671 672 673 674
instance Outputable Coercion where
  ppr = pprCo

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

675
ppr_co :: TyPrec -> Coercion -> SDoc
676
ppr_co _ (Refl r ty) = angleBrackets (ppr ty) <> ppr_role r
677

678
ppr_co p co@(TyConAppCo _ tc [_,_])
679
  | tc `hasKey` funTyConKey = ppr_fun_co p co
680

681 682 683 684 685
ppr_co _ (TyConAppCo r tc cos)  = pprTcApp TyConPrec ppr_co tc cos <> ppr_role r
ppr_co p (AppCo co1 co2)        = maybeParen p TyConPrec $
                                  pprCo co1 <+> ppr_co TyConPrec co2
ppr_co p co@(ForAllCo {})       = ppr_forall_co p co
ppr_co _ (CoVarCo cv)           = parenSymOcc (getOccName cv) (ppr cv)
686
ppr_co p (AxiomInstCo con index cos)
687 688
  = pprPrefixApp p (ppr (getName con) <> brackets (ppr index))
                   (map (ppr_co TyConPrec) cos)
689

690 691 692 693 694
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])
695 696 697
ppr_co p (InstCo co ty) = maybeParen p TyConPrec $
                          pprParendCo co <> ptext (sLit "@") <> pprType ty

698
ppr_co p (UnivCo s r ty1 ty2) = pprPrefixApp p (ptext (sLit "UnivCo") <+> ftext s <+> ppr r)
699
                                           [pprParendType ty1, pprParendType ty2]
700
ppr_co p (SymCo co)         = pprPrefixApp p (ptext (sLit "Sym")) [pprParendCo co]
701 702
ppr_co p (NthCo n co)       = pprPrefixApp p (ptext (sLit "Nth:") <> int n) [pprParendCo co]
ppr_co p (LRCo sel co)      = pprPrefixApp p (ppr sel) [pprParendCo co]
703
ppr_co p (SubCo co)         = pprPrefixApp p (ptext (sLit "Sub")) [pprParendCo co]
704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721
ppr_co p (AxiomRuleCo co ts cs) = maybeParen p TopPrec $
                                  ppr_axiom_rule_co co ts cs

ppr_axiom_rule_co :: CoAxiomRule -> [Type] -> [Coercion] -> SDoc
ppr_axiom_rule_co co ts ps = ppr (coaxrName co) <> ppTs ts $$ nest 2 (ppPs ps)
  where
  ppTs []   = Outputable.empty
  ppTs [t]  = ptext (sLit "@") <> ppr_type TopPrec t
  ppTs ts   = ptext (sLit "@") <>
                parens (hsep $ punctuate comma $ map pprType ts)

  ppPs []   = Outputable.empty
  ppPs [p]  = pprParendCo p
  ppPs (p : ps) = ptext (sLit "(") <+> pprCo p $$
                  vcat [ ptext (sLit ",") <+> pprCo q | q <- ps ] $$
                  ptext (sLit ")")


722 723

ppr_role :: Role -> SDoc
724 725 726 727 728
ppr_role r = underscore <> pp_role
  where pp_role = case r of
                    Nominal          -> char 'N'
                    Representational -> char 'R'
                    Phantom          -> char 'P'
729

730 731 732 733
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

734 735 736
instance Outputable LeftOrRight where
  ppr CLeft    = ptext (sLit "Left")
  ppr CRight   = ptext (sLit "Right")
737

738
ppr_fun_co :: TyPrec -> Coercion -> SDoc
739 740
ppr_fun_co p co = pprArrowChain p (split co)
  where
741
    split :: Coercion -> [SDoc]
742
    split (TyConAppCo _ f [arg,res])
743 744 745 746
      | f `hasKey` funTyConKey
      = ppr_co FunPrec arg : split res
    split co = [ppr_co TopPrec co]

747
ppr_forall_co :: TyPrec -> Coercion -> SDoc
748 749
ppr_forall_co p ty
  = maybeParen p FunPrec $
750
    sep [pprForAll tvs, ppr_co TopPrec rho]
751 752 753 754 755
  where
    (tvs,  rho) = split1 [] ty
    split1 tvs (ForAllCo tv ty) = split1 (tv:tvs) ty
    split1 tvs ty               = (reverse tvs, ty)

756 757 758
pprCoAxiom :: CoAxiom br -> SDoc
pprCoAxiom ax@(CoAxiom { co_ax_tc = tc, co_ax_branches = branches })
  = hang (ptext (sLit "axiom") <+> ppr ax <+> dcolon)
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
759
       2 (vcat (map (pprCoAxBranch tc) $ fromBranches branches))
760 761

pprCoAxBranch :: TyCon -> CoAxBranch -> SDoc
762 763
pprCoAxBranch fam_tc (CoAxBranch { cab_tvs = tvs
                                 , cab_lhs = lhs
Simon Peyton Jones's avatar
Simon Peyton Jones committed
764
                                 , cab_rhs = rhs })
765
  = hang (pprUserForAll tvs)
766
       2 (hang (pprTypeApp fam_tc lhs) 2 (equals <+> (ppr rhs)))
Simon Peyton Jones's avatar
Simon Peyton Jones committed
767 768 769 770 771 772 773 774 775 776

pprCoAxBranchHdr :: CoAxiom br -> BranchIndex -> SDoc
pprCoAxBranchHdr ax@(CoAxiom { co_ax_tc = fam_tc, co_ax_name = name }) index
  | CoAxBranch { cab_lhs = tys, cab_loc = loc } <- coAxiomNthBranch ax index
  = hang (pprTypeApp fam_tc tys)
       2 (ptext (sLit "-- Defined") <+> ppr_loc loc)
  where
        ppr_loc loc
          | isGoodSrcSpan loc
          = ptext (sLit "at") <+> ppr (srcSpanStart loc)
777

Simon Peyton Jones's avatar
Simon Peyton Jones committed
778 779 780
          | otherwise
          = ptext (sLit "in") <+>
              quotes (ppr (nameModule name))
781

782 783 784
{-
************************************************************************
*                                                                      *
785
        Functions over Kinds
786 787 788
*                                                                      *
************************************************************************
-}
batterseapower's avatar
batterseapower committed
789

790
-- | This breaks a 'Coercion' with type @T A B C ~ T D E F@ into
791
-- a list of 'Coercion's of kinds @A ~ D@, @B ~ E@ and @E ~ F@. Hence:
batterseapower's avatar
batterseapower committed
792
--
793
-- > decomposeCo 3 c = [nth 0 c, nth 1 c, nth 2 c]
794
decomposeCo :: Arity -> Coercion -> [Coercion]
795
decomposeCo arity co
796 797
  = [mkNthCo n co | n <- [0..(arity-1)] ]
           -- Remember, Nth is zero-indexed
798 799 800

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

804
-- first result has role equal to input; second result is Nominal
805 806 807
splitAppCo_maybe :: Coercion -> Maybe (Coercion, Coercion)
-- ^ Attempt to take a coercion application apart.
splitAppCo_maybe (AppCo co1 co2) = Just (co1, co2)
808
splitAppCo_maybe (TyConAppCo r tc cos)
809
  | mightBeUnsaturatedTyCon tc || cos `lengthExceeds` tyConArity tc
810
  , Just (cos', co') <- snocView cos
811
  , Just co'' <- setNominalRole_maybe co'
812
  = Just (mkTyConAppCo r tc cos', co'') -- Never create unsaturated type family apps!
813 814
       -- Use mkTyConAppCo to preserve the invariant
       --  that identity coercions are always represented by Refl
815 816
splitAppCo_maybe (Refl r ty)
  | Just (ty1, ty2) <- splitAppTy_maybe ty
817
  = Just (Refl r ty1, Refl Nominal ty2)
818 819 820 821 822
splitAppCo_maybe _ = Nothing

splitForAllCo_maybe :: Coercion -> Maybe (TyVar, Coercion)
splitForAllCo_maybe (ForAllCo tv co) = Just (tv, co)
splitForAllCo_maybe _                = Nothing
823 824 825 826

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

827
coVarKind :: CoVar -> (Type,Type)
828 829
coVarKind cv
 | Just (tc, [_kind,ty1,ty2]) <- splitTyConApp_maybe (varType cv)
830
 = ASSERT(tc `hasKey` eqPrimTyConKey || tc `hasKey` eqReprPrimTyConKey)
831 832 833
   (ty1,ty2)
 | otherwise = panic "coVarKind, non coercion variable"

834 835 836 837 838 839 840 841 842 843 844 845 846 847
coVarRole :: CoVar -> Role
coVarRole cv
  | tc `hasKey` eqPrimTyConKey
  = Nominal
  | tc `hasKey` eqReprPrimTyConKey
  = Representational
  | otherwise
  = pprPanic "coVarRole: unknown tycon" (ppr cv)

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

848
-- | Makes a coercion type from two types: the types whose equality
849
-- is proven by the relevant 'Coercion'
850 851 852 853
mkCoercionType :: Role -> Type -> Type -> Type
mkCoercionType Nominal          = mkPrimEqPred
mkCoercionType Representational = mkReprPrimEqPred
mkCoercionType Phantom          = panic "mkCoercionType"
854

855
isReflCo :: Coercion -> Bool
856 857
isReflCo (Refl {})         = True
isReflCo _                 = False
858 859

isReflCo_maybe :: Coercion -> Maybe Type
860 861
isReflCo_maybe (Refl _ ty)       = Just ty
isReflCo_maybe _                 = Nothing
862

863 864 865
{-
************************************************************************
*                                                                      *
866
            Building coercions
867 868
*                                                                      *
************************************************************************
869

870 871 872 873 874 875 876 877 878
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.

879
downgradeRole_maybe: This function takes both the input role and the output role
880 881 882 883 884 885 886 887
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
888
of the input. But, that function is recursive, and the caller of downgradeRole_maybe
889 890
often knows the input role. So, this is more efficient.

891
downgradeRole: This is just like downgradeRole_maybe, but it panics if the conversion
892 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914
isn't a downgrade.

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.

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.)

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.

915
One might ask: shouldn't downgradeRole_maybe just use setNominalRole_maybe as appropriate?
916 917
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.
918
-}
919

920
mkCoVarCo :: CoVar -> Coercion
921
-- cv :: s ~# t
922
mkCoVarCo cv
923
  | ty1 `eqType` ty2 = Refl (coVarRole cv) ty1
924 925 926
  | otherwise        = CoVarCo cv
  where
    (ty1, ty2) = ASSERT( isCoVar cv ) coVarKind cv
927

928
mkReflCo :: Role -> Type -> Coercion
929
mkReflCo = Refl
930

931
mkAxInstCo :: Role -> CoAxiom br -> BranchIndex -> [Type] -> Coercion
932
-- mkAxInstCo can legitimately be called over-staturated;
933
-- i.e. with more type arguments than the coercion requires
934
mkAxInstCo role ax index tys
935
  | arity == n_tys = downgradeRole role ax_role $ AxiomInstCo ax_br index rtys
936
  | otherwise      = ASSERT( arity < n_tys )
937
                     downgradeRole role ax_role $
938
                     foldl AppCo (AxiomInstCo ax_br index (take arity rtys))
939 940
                                 (drop arity rtys)
  where
941 942 943 944 945 946 947
    n_tys     = length tys
    ax_br     = toBranchedAxiom ax
    branch    = coAxiomNthBranch ax_br index
    arity     = length $ coAxBranchTyVars branch
    arg_roles = coAxBranchRoles branch
    rtys      = zipWith mkReflCo (arg_roles ++ repeat Nominal) tys
    ax_role   = coAxiomRole ax
948 949

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

954
mkAxInstLHS, mkAxInstRHS :: CoAxiom br -> BranchIndex -> [Type] -> Type
955 956
-- Instantiate the axiom with specified types,
-- returning the instantiated RHS
957
-- A companion to mkAxInstCo:
958
--    mkAxInstRhs ax index tys = snd (coercionKind (mkAxInstCo ax index tys))
959 960 961
mkAxInstLHS ax index tys
  | CoAxBranch { cab_tvs = tvs, cab_lhs = lhs } <- coAxiomNthBranch ax index
  , (tys1, tys2) <- splitAtList tvs tys
962
  = ASSERT( tvs `equalLength` tys1 )
963 964 965 966 967
    mkTyConApp (coAxiomTyCon ax) (substTysWith tvs tys1 lhs ++ tys2)

mkAxInstRHS ax index tys
  | CoAxBranch { cab_tvs = tvs, cab_rhs = rhs } <- coAxiomNthBranch ax index
  , (tys1, tys2) <- splitAtList tvs tys
968
  = ASSERT( tvs `equalLength` tys1 )
969
    mkAppTys (substTyWith tvs tys1 rhs) tys2
970 971 972

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

974
-- | Apply a 'Coercion' to another 'Coercion'.
975 976
-- 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.
977
mkAppCo :: Coercion -> Coercion -> Coercion
978 979 980
mkAppCo co1 co2 = mkAppCoFlexible co1 Nominal co2
-- Note, mkAppCo is careful to maintain invariants regarding
-- where Refl constructors appear; see the comments in the definition
981
-- of Coercion and the Note [Refl invariant] in types/TypeRep.hs.
982 983 984 985 986 987

-- | Apply a 'Coercion' to another 'Coercion'.
-- The second 'Coercion's role is given, making this more flexible than
-- 'mkAppCo'.
mkAppCoFlexible :: Coercion