Coercion.lhs 69.6 KB
Newer Older
1
%
2 3
% (c) The University of Glasgow 2006
%
4 5

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

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

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

33
        -- ** Decomposition
34 35
        instNewTyCon_maybe,
        topNormaliseNewType_maybe,
36

37
        decomposeCo, getCoVar_maybe,
38 39
        splitAppCo_maybe,
        splitForAllCo_maybe,
40
        nthRole, tyConRolesX,
41
        nextRole,
42

43 44
        -- ** Coercion variables
        mkCoVar, isCoVar, isCoVarType, coVarName, setCoVarName, setCoVarUnique,
45 46 47

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

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

60 61
        -- ** Lifting
        liftCoMatch, liftCoSubstTyVar, liftCoSubstWith,
62

batterseapower's avatar
batterseapower committed
63
        -- ** Comparison
64
        coreEqCoercion, coreEqCoercion2,
65

66 67
        -- ** Forcing evaluation of coercions
        seqCo,
68

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

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

76
        -- * Other
batterseapower's avatar
batterseapower committed
77
        applyCo
78
       ) where
79 80 81

#include "HsVersions.h"

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

import qualified Data.Data as Data hiding ( TyCon )
107 108 109
\end{code}

%************************************************************************
110
%*                                                                      *
111
            Coercions
112
%*                                                                      *
113
%************************************************************************
114

115
\begin{code}
116 117
-- | A 'Coercion' is concrete evidence of the equality/convertibility
-- of two types.
118

119 120
-- If you edit this type, you may need to update the GHC formalism
-- See Note [GHC Formalism] in coreSyn/CoreLint.lhs
121
data Coercion
122 123 124 125 126 127 128
  -- 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.

129
  -- These ones mirror the shape of types
130 131
  = -- Refl :: "e" -> _ -> e
    Refl Role Type  -- See Note [Refl invariant]
132 133 134 135 136 137 138 139 140 141
          -- 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.

142 143
          -- Use (Refl Representational _), not (SubCo (Refl Nominal _))

144
  -- These ones simply lift the correspondingly-named
145
  -- Type constructors into Coercions
146

147 148
  -- TyConAppCo :: "e" -> _ -> ?? -> e
  -- See Note [TyConAppCo roles]
149
  | TyConAppCo Role TyCon [Coercion]    -- lift TyConApp
150 151 152
               -- The TyCon is never a synonym;
               -- we expand synonyms eagerly
               -- But it can be a type function
153 154

  | AppCo Coercion Coercion        -- lift AppTy
155
          -- AppCo :: e -> N -> e
156 157 158

  -- See Note [Forall coercions]
  | ForAllCo TyVar Coercion       -- forall a. g
159
         -- :: _ -> e -> e
160 161

  -- These are special
162 163 164 165
  | CoVarCo CoVar      -- :: _ -> (N or R)
                       -- result role depends on the tycon of the variable's type

    -- AxiomInstCo :: e -> _ -> [N] -> e
166
  | AxiomInstCo (CoAxiom Branched) BranchIndex [Coercion]
167
     -- See also [CoAxiom index]
168
     -- The coercion arguments always *precisely* saturate
169
     -- arity of (that branch of) the CoAxiom.  If there are
170
     -- any left over, we use AppCo.  See
171 172
     -- See [Coercion axioms applied to coercions]

173 174 175 176
         -- see Note [UnivCo]
  | UnivCo Role Type Type      -- :: "e" -> _ -> _ -> e
  | SymCo Coercion             -- :: e -> e
  | TransCo Coercion Coercion  -- :: e -> e -> e
177

178 179 180 181
    -- 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]

182
  -- These are destructors
183

184
  | NthCo  Int         Coercion     -- Zero-indexed; decomposes (T t0 ... tn)
185
    -- :: _ -> e -> ?? (inverse of TyConAppCo, see Note [TyConAppCo roles])
186
  | LRCo   LeftOrRight Coercion     -- Decomposes (t_left t_right)
187
    -- :: _ -> N -> N
188
  | InstCo Coercion Type
189 190 191 192
    -- :: e -> _ -> e

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

195 196
-- If you edit this type, you may need to update the GHC formalism
-- See Note [GHC Formalism] in coreSyn/CoreLint.lhs
197
data LeftOrRight = CLeft | CRight
198 199
                 deriving( Eq, Data.Data, Data.Typeable )

200 201 202 203 204 205 206 207 208
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 }

209 210 211
pickLR :: LeftOrRight -> (a,a) -> a
pickLR CLeft  (l,_) = l
pickLR CRight (_,r) = r
212 213
\end{code}

214 215
Note [Refl invariant]
~~~~~~~~~~~~~~~~~~~~~
216 217
Coercions have the following invariant
     Refl is always lifted as far as possible.
218 219 220 221 222 223 224 225 226 227 228 229 230 231 232

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
233
expose further opportunities for optimization.
234 235 236 237 238 239 240 241 242 243 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

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.

269 270 271 272 273 274 275 276 277 278 279 280
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.
281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298

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.

299 300 301 302 303 304 305 306 307
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?
308

309 310
Answer: we simply treat (~) as an ordinary type constructor, so these
types really look like
311

312 313
   ((~) [c] a) -> [a] -> c
   ((~) [c] b) -> [b] -> c
314

315
So the coercion between the two is obviously
316

317
   ((~) [c] g) -> [g] -> c
318

319 320
Another way to see this to say that we simply collapse predicates to
their representation type (see Type.coreView and Type.predTypeRep).
321

322
This collapse is done by mkPredCo; there is no PredCo constructor
323
in Coercion.  This is important because we need Nth to work on
324 325 326
predicates too:
    Nth 1 ((~) [c] g) = g
See Simplify.simplCoercionF, which generates such selections.
327

dreixel's avatar
dreixel committed
328 329 330 331 332 333 334 335 336 337 338 339 340
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.
341
Lint checks this.
dreixel's avatar
dreixel committed
342 343 344

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

351 352 353 354 355 356 357 358 359 360 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 476 477 478 479 480 481 482 483 484 485 486
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:

newtype Age = MkAge Int

Nominal: All arguments must have role Nominal. Why? So that Foo Age ~N Foo Int
does *not* hold.

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.

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.

Phantom: All arguments must have role Phantom. This one isn't strictly
necessary for soundness, but this choice removes ambiguity.



The rules here also dictate what the parameters to mkTyConAppCo.

487
%************************************************************************
488
%*                                                                      *
489
\subsection{Coercion variables}
490
%*                                                                      *
491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506
%************************************************************************

\begin{code}
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
507
isCoVarType ty      -- Tests for t1 ~# t2, the unboxed equality
508
  = case splitTyConApp_maybe ty of
509 510
      Just (tc,tys) -> (tc `hasKey` eqPrimTyConKey || tc `hasKey` eqReprPrimTyConKey)
                       && tys `lengthAtLeast` 2
511
      Nothing       -> False
512 513 514 515 516 517
\end{code}


\begin{code}
tyCoVarsOfCo :: Coercion -> VarSet
-- Extracts type and coercion variables from a coercion
518 519 520 521 522
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
523
tyCoVarsOfCo (AxiomInstCo _ _ cos) = tyCoVarsOfCos cos
524 525 526 527 528 529 530
tyCoVarsOfCo (UnivCo _ ty1 ty2)    = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2
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
531
tyCoVarsOfCo (AxiomRuleCo _ ts cs) = tyVarsOfTypes ts `unionVarSet` tyCoVarsOfCos cs
532 533 534 535 536 537

tyCoVarsOfCos :: [Coercion] -> VarSet
tyCoVarsOfCos cos = foldr (unionVarSet . tyCoVarsOfCo) emptyVarSet cos

coVarsOfCo :: Coercion -> VarSet
-- Extract *coerction* variables only.  Tiresome to repeat the code, but easy.
538 539 540 541 542
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
543
coVarsOfCo (AxiomInstCo _ _ cos) = coVarsOfCos cos
544 545 546 547 548 549 550
coVarsOfCo (UnivCo _ _ _)        = emptyVarSet
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
551
coVarsOfCo (AxiomRuleCo _ _ cos) = coVarsOfCos cos
552 553 554 555 556

coVarsOfCos :: [Coercion] -> VarSet
coVarsOfCos cos = foldr (unionVarSet . coVarsOfCo) emptyVarSet cos

coercionSize :: Coercion -> Int
557 558 559 560 561
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
562
coercionSize (AxiomInstCo _ _ cos) = 1 + sum (map coercionSize cos)
563 564 565 566 567 568 569
coercionSize (UnivCo _ ty1 ty2)  = typeSize ty1 + typeSize ty2
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
570 571
coercionSize (AxiomRuleCo _ tys cos) = 1 + sum (map typeSize tys)
                                         + sum (map coercionSize cos)
572 573
\end{code}

Simon Peyton Jones's avatar
Simon Peyton Jones committed
574
%************************************************************************
575
%*                                                                      *
Simon Peyton Jones's avatar
Simon Peyton Jones committed
576
                            Tidying coercions
577
%*                                                                      *
Simon Peyton Jones's avatar
Simon Peyton Jones committed
578 579 580 581 582 583 584
%************************************************************************

\begin{code}
tidyCo :: TidyEnv -> Coercion -> Coercion
tidyCo env@(_, subst) co
  = go co
  where
585 586 587 588 589 590 591 592 593 594
    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
595
    go (AxiomInstCo con ind cos) = let args = tidyCos env cos
596 597 598 599 600 601 602 603
                                   in args `seqList` AxiomInstCo con ind args
    go (UnivCo r ty1 ty2)     = (UnivCo r $! tidyType env ty1) $! tidyType env ty2
    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
604

605 606 607 608 609 610
    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
611 612 613 614
tidyCos :: TidyEnv -> [Coercion] -> [Coercion]
tidyCos env = map (tidyCo env)
\end{code}

615
%************************************************************************
616
%*                                                                      *
617 618
                   Pretty-printing coercions
%*                                                                      *
619 620
%************************************************************************

621 622 623 624 625
@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.
626 627

\begin{code}
628 629 630 631 632 633 634 635
instance Outputable Coercion where
  ppr = pprCo

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

ppr_co :: Prec -> Coercion -> SDoc
636
ppr_co _ (Refl r ty) = angleBrackets (ppr ty) <> ppr_role r
637

638
ppr_co p co@(TyConAppCo _ tc [_,_])
639
  | tc `hasKey` funTyConKey = ppr_fun_co p co
640

641 642 643 644 645
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)
646
ppr_co p (AxiomInstCo con index cos)
647 648
  = pprPrefixApp p (ppr (getName con) <> brackets (ppr index))
                   (map (ppr_co TyConPrec) cos)
649

650 651 652 653 654
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])
655 656 657
ppr_co p (InstCo co ty) = maybeParen p TyConPrec $
                          pprParendCo co <> ptext (sLit "@") <> pprType ty

658
ppr_co p (UnivCo r ty1 ty2) = pprPrefixApp p (ptext (sLit "UnivCo") <+> ppr r)
659
                                           [pprParendType ty1, pprParendType ty2]
660
ppr_co p (SymCo co)         = pprPrefixApp p (ptext (sLit "Sym")) [pprParendCo co]
661 662
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]
663
ppr_co p (SubCo co)         = pprPrefixApp p (ptext (sLit "Sub")) [pprParendCo co]
664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681
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 ")")


682 683

ppr_role :: Role -> SDoc
684 685 686 687 688
ppr_role r = underscore <> pp_role
  where pp_role = case r of
                    Nominal          -> char 'N'
                    Representational -> char 'R'
                    Phantom          -> char 'P'
689

690 691 692 693
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

694 695 696
instance Outputable LeftOrRight where
  ppr CLeft    = ptext (sLit "Left")
  ppr CRight   = ptext (sLit "Right")
697 698 699 700

ppr_fun_co :: Prec -> Coercion -> SDoc
ppr_fun_co p co = pprArrowChain p (split co)
  where
701
    split :: Coercion -> [SDoc]
702
    split (TyConAppCo _ f [arg,res])
703 704 705 706 707 708 709
      | f `hasKey` funTyConKey
      = ppr_co FunPrec arg : split res
    split co = [ppr_co TopPrec co]

ppr_forall_co :: Prec -> Coercion -> SDoc
ppr_forall_co p ty
  = maybeParen p FunPrec $
710
    sep [pprForAll tvs, ppr_co TopPrec rho]
711 712 713 714 715 716
  where
    (tvs,  rho) = split1 [] ty
    split1 tvs (ForAllCo tv ty) = split1 (tv:tvs) ty
    split1 tvs ty               = (reverse tvs, ty)
\end{code}

717
\begin{code}
718 719 720 721 722 723
pprCoAxiom :: CoAxiom br -> SDoc
pprCoAxiom ax@(CoAxiom { co_ax_tc = tc, co_ax_branches = branches })
  = hang (ptext (sLit "axiom") <+> ppr ax <+> dcolon)
       2 (vcat (map (pprCoAxBranch tc) $ fromBranchList branches))

pprCoAxBranch :: TyCon -> CoAxBranch -> SDoc
724 725
pprCoAxBranch fam_tc (CoAxBranch { cab_tvs = tvs
                                 , cab_lhs = lhs
Simon Peyton Jones's avatar
Simon Peyton Jones committed
726
                                 , cab_rhs = rhs })
727 728
  = hang (ifPprDebug (pprForAll tvs))
       2 (hang (pprTypeApp fam_tc lhs) 2 (equals <+> (ppr rhs)))
Simon Peyton Jones's avatar
Simon Peyton Jones committed
729 730 731 732 733 734 735 736 737 738

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

Simon Peyton Jones's avatar
Simon Peyton Jones committed
740 741 742
          | otherwise
          = ptext (sLit "in") <+>
              quotes (ppr (nameModule name))
743
\end{code}
744 745

%************************************************************************
746 747 748
%*                                                                      *
        Functions over Kinds
%*                                                                      *
749
%************************************************************************
batterseapower's avatar
batterseapower committed
750

751 752
\begin{code}
-- | This breaks a 'Coercion' with type @T A B C ~ T D E F@ into
753
-- a list of 'Coercion's of kinds @A ~ D@, @B ~ E@ and @E ~ F@. Hence:
batterseapower's avatar
batterseapower committed
754
--
755
-- > decomposeCo 3 c = [nth 0 c, nth 1 c, nth 2 c]
756
decomposeCo :: Arity -> Coercion -> [Coercion]
757
decomposeCo arity co
758 759
  = [mkNthCo n co | n <- [0..(arity-1)] ]
           -- Remember, Nth is zero-indexed
760 761 762

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

766
-- first result has role equal to input; second result is Nominal
767 768 769
splitAppCo_maybe :: Coercion -> Maybe (Coercion, Coercion)
-- ^ Attempt to take a coercion application apart.
splitAppCo_maybe (AppCo co1 co2) = Just (co1, co2)
770
splitAppCo_maybe (TyConAppCo r tc cos)
771
  | isDecomposableTyCon tc || cos `lengthExceeds` tyConArity tc
772
  , Just (cos', co') <- snocView cos
773 774
  , Just co'' <- unSubCo_maybe co'
  = Just (mkTyConAppCo r tc cos', co'') -- Never create unsaturated type family apps!
775 776
       -- Use mkTyConAppCo to preserve the invariant
       --  that identity coercions are always represented by Refl
777 778
splitAppCo_maybe (Refl r ty)
  | Just (ty1, ty2) <- splitAppTy_maybe ty
779
  = Just (Refl r ty1, Refl Nominal ty2)
780 781 782 783 784
splitAppCo_maybe _ = Nothing

splitForAllCo_maybe :: Coercion -> Maybe (TyVar, Coercion)
splitForAllCo_maybe (ForAllCo tv co) = Just (tv, co)
splitForAllCo_maybe _                = Nothing
785 786 787 788

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

789
coVarKind :: CoVar -> (Type,Type)
790 791
coVarKind cv
 | Just (tc, [_kind,ty1,ty2]) <- splitTyConApp_maybe (varType cv)
792
 = ASSERT(tc `hasKey` eqPrimTyConKey || tc `hasKey` eqReprPrimTyConKey)
793 794 795
   (ty1,ty2)
 | otherwise = panic "coVarKind, non coercion variable"

796 797 798 799 800 801 802 803 804 805 806 807 808 809
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)

810
-- | Makes a coercion type from two types: the types whose equality
811
-- is proven by the relevant 'Coercion'
812 813 814 815
mkCoercionType :: Role -> Type -> Type -> Type
mkCoercionType Nominal          = mkPrimEqPred
mkCoercionType Representational = mkReprPrimEqPred
mkCoercionType Phantom          = panic "mkCoercionType"
816

817
isReflCo :: Coercion -> Bool
818 819
isReflCo (Refl {})         = True
isReflCo _                 = False
820 821

isReflCo_maybe :: Coercion -> Maybe Type
822 823
isReflCo_maybe (Refl _ ty)       = Just ty
isReflCo_maybe _                 = Nothing
824
\end{code}
825

826
%************************************************************************
827
%*                                                                      *
828
            Building coercions
829
%*                                                                      *
830
%************************************************************************
831

832
\begin{code}
833
mkCoVarCo :: CoVar -> Coercion
834
-- cv :: s ~# t
835
mkCoVarCo cv
836
  | ty1 `eqType` ty2 = Refl (coVarRole cv) ty1
837 838 839
  | otherwise        = CoVarCo cv
  where
    (ty1, ty2) = ASSERT( isCoVar cv ) coVarKind cv
840

841
mkReflCo :: Role -> Type -> Coercion
842
mkReflCo = Refl
843

844
mkAxInstCo :: Role -> CoAxiom br -> BranchIndex -> [Type] -> Coercion
845
-- mkAxInstCo can legitimately be called over-staturated;
846
-- i.e. with more type arguments than the coercion requires
847 848
mkAxInstCo role ax index tys
  | arity == n_tys = maybeSubCo2 role ax_role $ AxiomInstCo ax_br index rtys
849
  | otherwise      = ASSERT( arity < n_tys )
850
                     maybeSubCo2 role ax_role $
851
                     foldl AppCo (AxiomInstCo ax_br index (take arity rtys))
852 853
                                 (drop arity rtys)
  where
854 855 856 857 858 859 860
    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
861 862

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

867
mkAxInstLHS, mkAxInstRHS :: CoAxiom br -> BranchIndex -> [Type] -> Type
868 869
-- Instantiate the axiom with specified types,
-- returning the instantiated RHS
870
-- A companion to mkAxInstCo:
871
--    mkAxInstRhs ax index tys = snd (coercionKind (mkAxInstCo ax index tys))
872 873 874
mkAxInstLHS ax index tys
  | CoAxBranch { cab_tvs = tvs, cab_lhs = lhs } <- coAxiomNthBranch ax index
  , (tys1, tys2) <- splitAtList tvs tys
875
  = ASSERT( tvs `equalLength` tys1 )
876 877 878 879 880
    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
881
  = ASSERT( tvs `equalLength` tys1 )
882
    mkAppTys (substTyWith tvs tys1 rhs) tys2
883 884 885

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

887
-- | Apply a 'Coercion' to another 'Coercion'.
888 889
-- 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.
890
mkAppCo :: Coercion -> Coercion -> Coercion
891 892 893 894 895 896 897 898 899 900
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
-- of Coercion and the Note [Refl invariant] in types/TypeRep.lhs.

-- | Apply a 'Coercion' to another 'Coercion'.
-- The second 'Coercion's role is given, making this more flexible than
-- 'mkAppCo'.
mkAppCoFlexible :: Coercion -> Role -> Coercion -> Coercion
mkAppCoFlexible (Refl r ty1) _ (Refl _ ty2)
901
  = Refl r (mkAppTy ty1 ty2)
902
mkAppCoFlexible (Refl r (TyConApp tc tys)) r2 co2
903 904
  = TyConAppCo r tc (zip_roles (tyConRolesX r tc) tys)
  where
905
    zip_roles (r1:_)  []        = [maybeSubCo2 r1 r2 co2]
906 907
    zip_roles (r1:rs) (ty1:tys) = mkReflCo r1 ty1 : zip_roles rs tys
    zip_roles _       _         = panic "zip_roles" -- but the roles are infinite...
908
mkAppCoFlexible (TyConAppCo r tc cos) r2 co
909
  = case r of
910 911
      Nominal          -> ASSERT( r2 == Nominal )
                          TyConAppCo Nominal tc (cos ++ [co])
912 913
      Representational -> TyConAppCo Representational tc (cos ++ [co'])
        where new_role = (tyConRolesX Representational tc) !! (length cos)
914
              co'      = maybeSubCo2 new_role r2 co
915 916
      Phantom          -> TyConAppCo Phantom tc (cos ++ [mkPhantomCo co])

917 918 919
mkAppCoFlexible co1 _r2 co2 = ASSERT( _r2 == Nominal )
                              AppCo co1 co2

batterseapower's avatar
batterseapower committed
920 921

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

926 927 928 929
-- | 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
930
               -- Expand type synonyms
931
  | Just (tv_co_prs, rhs_ty, leftover_cos) <- tcExpandTyCon_maybe tc cos
932
  = mkAppCos (liftCoSubst r tv_co_prs rhs_ty) leftover_cos
933

934
  | Just tys <- traverse isReflCo_maybe cos
935
  = Refl r (mkTyConApp tc tys)  -- See Note [Refl invariant]
936

937
  | otherwise = TyConAppCo r tc cos
938 939

-- | Make a function 'Coercion' between two other 'Coercion's
940 941
mkFunCo :: Role -> Coercion -> Coercion -> Coercion
mkFunCo r co1 co2 = mkTyConAppCo r funTyCon [co1, co2]
batterseapower's avatar
batterseapower committed
942 943

-- | Make a 'Coercion' which binds a variable within an inner 'Coercion'
944
mkForAllCo :: Var -> Coercion -> Coercion
945
-- note that a TyVar should be used here, not a CoVar (nor a TcTyVar)
946 947
mkForAllCo tv (Refl r ty)  = ASSERT( isTyVar tv ) Refl r (mkForAllTy tv ty)
mkForAllCo tv  co          = ASSERT( isTyVar tv ) ForAllCo tv co
batterseapower's avatar
batterseapower committed
948

949
-------------------------------
batterseapower's avatar
batterseapower committed
950

951 952 953 954 955 956 957
-- | 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.
958 959
mkSymCo co@(Refl {})             = co
mkSymCo    (UnivCo r ty1 ty2)    = UnivCo r ty2 ty1
960 961 962 963 964
mkSymCo    (SymCo co)            = co
mkSymCo co                       = SymCo co

-- | Create a new 'Coercion' by composing the two given 'Coercion's transitively.
mkTransCo :: Coercion -> Coercion -> Coercion
965 966 967 968 969 970 971 972 973 974 975 976
mkTransCo (Refl {}) co = co
mkTransCo co (Refl {}) = co
mkTransCo co1 co2      = TransCo co1 co2

-- 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
  = maybeSubCo2 role nth_role $ nth_co
  where
    nth_co = mkNthCo n co
    nth_role = coercionRole nth_co
977 978

mkNthCo :: Int -> Coercion -> Coercion
979
mkNthCo n (Refl r ty) = ASSERT( ok_tc_app ty n )
980 981 982
                        Refl r' (tyConAppArgN n ty)
  where tc = tyConAppTyCon ty
        r' = nthRole r tc n
983 984 985 986 987
mkNthCo n co        = ASSERT( ok_tc_app _ty1 n && ok_tc_app _ty2 n )
                      NthCo n co
                    where
                      Pair _ty1 _ty2 = coercionKind co

988

989
mkLRCo :: LeftOrRight -> Coercion -> Coercion
990 991
mkLRCo lr (Refl eq ty) = Refl eq (pickLR lr (splitAppTy ty))
mkLRCo lr co           = LRCo lr co
992

993 994 995 996
ok_tc_app :: Type -> Int -> Bool
ok_tc_app ty n = case splitTyConApp_maybe ty of
                   Just (_, tys) -> tys `lengthExceeds` n
                   Nothing       -> False
997

998
-- | Instantiates a 'Coercion' with a 'Type' argument.
999
mkInstCo :: Coercion -> Type -> Coercion
1000
mkInstCo co ty = InstCo co ty
1001 1002 1003 1004 1005 1006 1007

-- | Manufacture a coercion from thin air. Needless to say, this is
--   not usually safe, but it is used when we know we are dealing with
--   bottom, which is one case in which it is safe.  This is also used
--   to implement the @unsafeCoerce#@ primitive.  Optimise by pushing
--   down through type constructors.
mkUnsafeCo :: Type -> Type -> Coercion
1008 1009 1010 1011 1012 1013 1014
mkUnsafeCo = mkUnivCo Representational

mkUnivCo :: Role -> Type -> Type -> Coercion
mkUnivCo role ty1 ty2
  | ty1 `eqType` ty2 = Refl role ty1
  | otherwise        = UnivCo role ty1 ty2

1015 1016 1017
mkAxiomRuleCo :: CoAxiomRule -> [Type] -> [Coercion] -> Coercion
mkAxiomRuleCo = AxiomRuleCo

1018 1019 1020 1021 1022 1023
-- input coercion is Nominal
mkSubCo :: Coercion -> Coercion
mkSubCo (Refl Nominal ty) = Refl Representational ty
mkSubCo (TyConAppCo Nominal tc cos)
  = TyConAppCo Representational tc (applyRoles tc cos)
mkSubCo (UnivCo Nominal ty1 ty2) = UnivCo Representational ty1 ty2
Joachim Breitner's avatar
Joachim Breitner committed
1024
mkSubCo co = ASSERT2( coercionRole co == Nominal, ppr co <+> ppr (coercionRole co) )
1025 1026
             SubCo co

1027

1028 1029 1030 1031 1032 1033 1034 1035 </