TyCoRep.hs 125 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21
{-
(c) The University of Glasgow 2006
(c) The GRASP/AQUA Project, Glasgow University, 1998
\section[TyCoRep]{Type and Coercion - friends' interface}

Note [The Type-related module hierarchy]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  Class
  CoAxiom
  TyCon    imports Class, CoAxiom
  TyCoRep  imports Class, CoAxiom, TyCon
  TysPrim  imports TyCoRep ( including mkTyConTy )
  Kind     imports TysPrim ( mainly for primitive kinds )
  Type     imports Kind
  Coercion imports Type
-}

-- We expose the relevant stuff from this module via the Type module
{-# OPTIONS_HADDOCK hide #-}
{-# LANGUAGE CPP, DeriveDataTypeable, DeriveFunctor, DeriveFoldable,
             DeriveTraversable, MultiWayIf #-}
22
{-# LANGUAGE ImplicitParams #-}
23 24

module TyCoRep (
25 26 27
        TyThing(..), pprTyThingCategory, pprShortTyThing,

        -- * Types
28 29 30 31
        Type(..),
        TyLit(..),
        KindOrType, Kind,
        PredType, ThetaType,      -- Synonyms
32
        ArgFlag(..),
33

Ben Gamari's avatar
Ben Gamari committed
34
        -- * Coercions
35 36
        Coercion(..), LeftOrRight(..),
        UnivCoProvenance(..), CoercionHole(..),
37
        CoercionN, CoercionR, CoercionP, KindCoercion,
38

Ben Gamari's avatar
Ben Gamari committed
39
        -- * Functions over types
40
        mkTyConTy, mkTyVarTy, mkTyVarTys,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
41 42
        mkFunTy, mkFunTys, mkForAllTy, mkForAllTys,
        mkPiTy, mkPiTys,
43
        isLiftedTypeKind, isUnliftedTypeKind,
44 45
        isCoercionType, isRuntimeRepTy, isRuntimeRepVar,
        isRuntimeRepKindedTy, dropRuntimeRepArgs,
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
46
        sameVis,
47

Ben Gamari's avatar
Ben Gamari committed
48
        -- * Functions over binders
49
        TyBinder(..), TyVarBinder,
50
        binderVar, binderVars, binderKind, binderArgFlag,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
51
        delBinderVar,
52
        isInvisibleArgFlag, isVisibleArgFlag,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
53
        isInvisibleBinder, isVisibleBinder,
54

Ben Gamari's avatar
Ben Gamari committed
55
        -- * Functions over coercions
56 57
        pickLR,

Ben Gamari's avatar
Ben Gamari committed
58
        -- * Pretty-printing
59
        pprType, pprParendType, pprTypeApp, pprTvBndr, pprTvBndrs,
60
        pprSigmaType,
61 62 63 64 65
        pprTheta, pprForAll, pprForAllImplicit, pprUserForAll,
        pprThetaArrowTy, pprClassPred,
        pprKind, pprParendKind, pprTyLit,
        TyPrec(..), maybeParen, pprTcAppCo, pprTcAppTy,
        pprPrefixApp, pprArrowChain, ppr_type,
66
        pprDataCons, ppSuggestExplicitKinds,
67

Simon Peyton Jones's avatar
Simon Peyton Jones committed
68
        -- * Free variables
69
        tyCoVarsOfType, tyCoVarsOfTypeDSet, tyCoVarsOfTypes, tyCoVarsOfTypesDSet,
niteria's avatar
niteria committed
70 71
        tyCoFVsBndr, tyCoFVsOfType, tyCoVarsOfTypeList,
        tyCoFVsOfTypes, tyCoVarsOfTypesList,
72
        closeOverKindsDSet, closeOverKindsFV, closeOverKindsList,
73 74 75 76
        coVarsOfType, coVarsOfTypes,
        coVarsOfCo, coVarsOfCos,
        tyCoVarsOfCo, tyCoVarsOfCos,
        tyCoVarsOfCoDSet,
niteria's avatar
niteria committed
77
        tyCoFVsOfCo, tyCoFVsOfCos,
78 79 80
        tyCoVarsOfCoList, tyCoVarsOfProv,
        closeOverKinds,

Simon Peyton Jones's avatar
Simon Peyton Jones committed
81
        -- * Substitutions
82 83
        TCvSubst(..), TvSubstEnv, CvSubstEnv,
        emptyTvSubstEnv, emptyCvSubstEnv, composeTCvSubstEnv, composeTCvSubst,
84 85 86
        emptyTCvSubst, mkEmptyTCvSubst, isEmptyTCvSubst,
        mkTCvSubst, mkTvSubst,
        getTvSubstEnv,
87 88
        getCvSubstEnv, getTCvInScope, getTCvSubstRangeFVs,
        isInScope, notElemTCvSubst,
89 90
        setTvSubstEnv, setCvSubstEnv, zapTCvSubst,
        extendTCvInScope, extendTCvInScopeList, extendTCvInScopeSet,
91 92
        extendTCvSubst,
        extendCvSubst, extendCvSubstWithClone,
93
        extendTvSubst, extendTvSubstBinder, extendTvSubstWithClone,
94
        extendTvSubstList, extendTvSubstAndInScope,
95
        unionTCvSubst, zipTyEnv, zipCoEnv, mkTyCoInScopeSet,
niteria's avatar
niteria committed
96 97
        zipTvSubst, zipCvSubst,
        mkTvSubstPrs,
98 99 100

        substTyWith, substTyWithCoVars, substTysWith, substTysWithCoVars,
        substCoWith,
101 102
        substTy, substTyAddInScope,
        substTyUnchecked, substTysUnchecked, substThetaUnchecked,
103
        substTyWithUnchecked,
104
        substCoUnchecked, substCoWithUnchecked,
105
        substTyWithInScope,
106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123
        substTys, substTheta,
        lookupTyVar, substTyVarBndr,
        substCo, substCos, substCoVar, substCoVars, lookupCoVar,
        substCoVarBndr, cloneTyVarBndr, cloneTyVarBndrs,
        substTyVar, substTyVars,
        substForAllCoBndr,
        substTyVarBndrCallback, substForAllCoBndrCallback,
        substCoVarBndrCallback,

        -- * Tidying type related things up for printing
        tidyType,      tidyTypes,
        tidyOpenType,  tidyOpenTypes,
        tidyOpenKind,
        tidyTyCoVarBndr, tidyTyCoVarBndrs, tidyFreeTyCoVars,
        tidyOpenTyCoVar, tidyOpenTyCoVars,
        tidyTyVarOcc,
        tidyTopType,
        tidyKind,
124
        tidyCo, tidyCos,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
125
        tidyTyVarBinder, tidyTyVarBinders
126 127 128 129 130
    ) where

#include "HsVersions.h"

import {-# SOURCE #-} DataCon( dataConTyCon, dataConFullSig
Simon Peyton Jones's avatar
Simon Peyton Jones committed
131
                              , dataConUnivTyVarBinders, dataConExTyVarBinders
132
                              , DataCon, filterEqSpec )
133
import {-# SOURCE #-} Type( isPredTy, isCoercionTy, mkAppTy
134
                          , tyCoVarsOfTypesWellScoped
135 136
                          , partitionInvisibles, coreView, typeKind
                          , eqType )
137 138 139
   -- Transitively pulls in a LOT of stuff, better to break the loop

import {-# SOURCE #-} Coercion
140
import {-# SOURCE #-} ConLike ( ConLike(..), conLikeName )
141
import {-# SOURCE #-} TysWiredIn ( ptrRepLiftedTy )
142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163

-- friends:
import Var
import VarEnv
import VarSet
import Name hiding ( varName )
import BasicTypes
import TyCon
import Class
import CoAxiom
import FV

-- others
import PrelNames
import Binary
import Outputable
import DynFlags
import StaticFlags ( opt_PprStyle_Debug )
import FastString
import Pair
import UniqSupply
import Util
164
import UniqFM
165 166 167 168 169 170

-- libraries
import qualified Data.Data as Data hiding ( TyCon )
import Data.List
import Data.IORef ( IORef )   -- for CoercionHole

171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227
{-
%************************************************************************
%*                                                                      *
                        TyThing
%*                                                                      *
%************************************************************************

Despite the fact that DataCon has to be imported via a hi-boot route,
this module seems the right place for TyThing, because it's needed for
funTyCon and all the types in TysPrim.

It is also SOURCE-imported into Name.hs


Note [ATyCon for classes]
~~~~~~~~~~~~~~~~~~~~~~~~~
Both classes and type constructors are represented in the type environment
as ATyCon.  You can tell the difference, and get to the class, with
   isClassTyCon :: TyCon -> Bool
   tyConClass_maybe :: TyCon -> Maybe Class
The Class and its associated TyCon have the same Name.
-}

-- | A global typecheckable-thing, essentially anything that has a name.
-- Not to be confused with a 'TcTyThing', which is also a typecheckable
-- thing but in the *local* context.  See 'TcEnv' for how to retrieve
-- a 'TyThing' given a 'Name'.
data TyThing
  = AnId     Id
  | AConLike ConLike
  | ATyCon   TyCon       -- TyCons and classes; see Note [ATyCon for classes]
  | ACoAxiom (CoAxiom Branched)

instance Outputable TyThing where
  ppr = pprShortTyThing

instance NamedThing TyThing where       -- Can't put this with the type
  getName (AnId id)     = getName id    -- decl, because the DataCon instance
  getName (ATyCon tc)   = getName tc    -- isn't visible there
  getName (ACoAxiom cc) = getName cc
  getName (AConLike cl) = conLikeName cl

pprShortTyThing :: TyThing -> SDoc
-- c.f. PprTyThing.pprTyThing, which prints all the details
pprShortTyThing thing
  = pprTyThingCategory thing <+> quotes (ppr (getName thing))

pprTyThingCategory :: TyThing -> SDoc
pprTyThingCategory (ATyCon tc)
  | isClassTyCon tc = text "Class"
  | otherwise       = text "Type constructor"
pprTyThingCategory (ACoAxiom _) = text "Coercion axiom"
pprTyThingCategory (AnId   _)   = text "Identifier"
pprTyThingCategory (AConLike (RealDataCon _)) = text "Data constructor"
pprTyThingCategory (AConLike (PatSynCon _))  = text "Pattern synonym"


228 229 230 231 232
{- **********************************************************************
*                                                                       *
                        Type
*                                                                       *
********************************************************************** -}
233 234 235

-- | The key representation of types within the compiler

236 237 238 239 240
type KindOrType = Type -- See Note [Arguments to type constructors]

-- | The key type representing kinds in the compiler.
type Kind = Type

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 269 270 271 272 273
-- If you edit this type, you may need to update the GHC formalism
-- See Note [GHC Formalism] in coreSyn/CoreLint.hs
data Type
  -- See Note [Non-trivial definitional equality]
  = TyVarTy Var -- ^ Vanilla type or kind variable (*never* a coercion variable)

  | AppTy         -- See Note [AppTy rep]
        Type
        Type            -- ^ Type application to something other than a 'TyCon'. Parameters:
                        --
                        --  1) Function: must /not/ be a 'TyConApp',
                        --     must be another 'AppTy', or 'TyVarTy'
                        --
                        --  2) Argument type

  | TyConApp      -- See Note [AppTy rep]
        TyCon
        [KindOrType]    -- ^ Application of a 'TyCon', including newtypes /and/ synonyms.
                        -- Invariant: saturated applications of 'FunTyCon' must
                        -- use 'FunTy' and saturated synonyms must use their own
                        -- constructors. However, /unsaturated/ 'FunTyCon's
                        -- do appear as 'TyConApp's.
                        -- Parameters:
                        --
                        -- 1) Type constructor being applied to.
                        --
                        -- 2) Type arguments. Might not have enough type arguments
                        --    here to saturate the constructor.
                        --    Even type synonyms are not necessarily saturated;
                        --    for example unsaturated type synonyms
                        --    can appear as the right hand side of a type synonym.

  | ForAllTy
Simon Peyton Jones's avatar
Simon Peyton Jones committed
274
        {-# UNPACK #-} !TyVarBinder
275 276
        Type            -- ^ A Π type.

Simon Peyton Jones's avatar
Simon Peyton Jones committed
277 278
  | FunTy Type Type     -- ^ t1 -> t2   Very common, so an important special case

279 280 281 282
  | LitTy TyLit     -- ^ Type literals are similar to type constructors.

  | CastTy
        Type
283 284 285 286
        KindCoercion  -- ^ A kind cast. The coercion is always nominal.
                      -- INVARIANT: The cast is never refl.
                      -- INVARIANT: The cast is "pushed down" as far as it
                      -- can go. See Note [Pushing down casts]
287 288 289 290 291 292 293

  | CoercionTy
        Coercion    -- ^ Injection of a Coercion into a type
                    -- This should only ever be used in the RHS of an AppTy,
                    -- in the list of a TyConApp, when applying a promoted
                    -- GADT data constructor

294
  deriving Data.Data
295 296 297 298 299 300 301


-- NOTE:  Other parts of the code assume that type literals do not contain
-- types or type variables.
data TyLit
  = NumTyLit Integer
  | StrTyLit FastString
302
  deriving (Eq, Ord, Data.Data)
303

304 305
{- Note [The kind invariant]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323
The kinds
   #          UnliftedTypeKind
   OpenKind   super-kind of *, #

can never appear under an arrow or type constructor in a kind; they
can only be at the top level of a kind.  It follows that primitive TyCons,
which have a naughty pseudo-kind
   State# :: * -> #
must always be saturated, so that we can never get a type whose kind
has a UnliftedTypeKind or ArgTypeKind underneath an arrow.

Nor can we abstract over a type variable with any of these kinds.

    k :: = kk | # | ArgKind | (#) | OpenKind
    kk :: = * | kk -> kk | T kk1 ... kkn

So a type variable can only be abstracted kk.

324 325 326 327 328 329 330
Note [AppTy rep]
~~~~~~~~~~~~~~~~
Types of the form 'f a' must be of kind *, not #, so we are guaranteed
that they are represented by pointers.  The reason is that f must have
kind (kk -> kk) and kk cannot be unlifted; see Note [The kind invariant]
in TyCoRep.

331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370
Note [Arguments to type constructors]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Because of kind polymorphism, in addition to type application we now
have kind instantiation. We reuse the same notations to do so.

For example:

  Just (* -> *) Maybe
  Right * Nat Zero

are represented by:

  TyConApp (PromotedDataCon Just) [* -> *, Maybe]
  TyConApp (PromotedDataCon Right) [*, Nat, (PromotedDataCon Zero)]

Important note: Nat is used as a *kind* and not as a type. This can be
confusing, since type-level Nat and kind-level Nat are identical. We
use the kind of (PromotedDataCon Right) to know if its arguments are
kinds or types.

This kind instantiation only happens in TyConApp currently.

Note [Pushing down casts]
~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we have (a :: k1 -> *), (b :: k1), and (co :: * ~ q).
The type (a b |> co) is `eqType` to ((a |> co') b), where
co' = (->) <k1> co. Thus, to make this visible to functions
that inspect types, we always push down coercions, preferring
the second form. Note that this also applies to TyConApps!

Note [Non-trivial definitional equality]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Is Int |> <*> the same as Int? YES! In order to reduce headaches,
we decide that any reflexive casts in types are just ignored. More
generally, the `eqType` function, which defines Core's type equality
relation, ignores casts and coercion arguments, as long as the
two types have the same kind. This allows us to be a little sloppier
in keeping track of coercions, which is a good thing. It also means
that eqType does not depend on eqCoercion, which is also a good thing.

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
Why is this sensible? That is, why is something different than α-equivalence
appropriate for the implementation of eqType?

Anything smaller than ~ and homogeneous is an appropriate definition for
equality. The type safety of FC depends only on ~. Let's say η : τ ~ σ. Any
expression of type τ can be transmuted to one of type σ at any point by
casting. The same is true of types of type τ. So in some sense, τ and σ are
interchangeable.

But let's be more precise. If we examine the typing rules of FC (say, those in
http://www.cis.upenn.edu/~eir/papers/2015/equalities/equalities-extended.pdf)
there are several places where the same metavariable is used in two different
premises to a rule. (For example, see Ty_App.) There is an implicit equality
check here. What definition of equality should we use? By convention, we use
α-equivalence. Take any rule with one (or more) of these implicit equality
checks. Then there is an admissible rule that uses ~ instead of the implicit
check, adding in casts as appropriate.

The only problem here is that ~ is heterogeneous. To make the kinds work out
in the admissible rule that uses ~, it is necessary to homogenize the
coercions. That is, if we have η : (τ : κ1) ~ (σ : κ2), then we don't use η;
we use η |> kind η, which is homogeneous.

The effect of this all is that eqType, the implementation of the implicit
equality check, can use any homogeneous relation that is smaller than ~, as
those rules must also be admissible.

What would go wrong if we insisted on the casts matching? See the beginning of
Section 8 in the unpublished paper above. Theoretically, nothing at all goes
wrong. But in practical terms, getting the coercions right proved to be
nightmarish. And types would explode: during kind-checking, we often produce
reflexive kind coercions. When we try to cast by these, mkCastTy just discards
them. But if we used an eqType that distinguished between Int and Int |> <*>,
then we couldn't discard -- the output of kind-checking would be enormous,
and we would need enormous casts with lots of CoherenceCo's to straighten
them out.

Would anything go wrong if eqType respected type families? No, not at all. But
that makes eqType rather hard to implement.

Thus, the guideline for eqType is that it should be the largest
easy-to-implement relation that is still smaller than ~ and homogeneous. The
precise choice of relation is somewhat incidental, as long as the smart
constructors and destructors in Type respect whatever relation is chosen.

Another helpful principle with eqType is this:

 ** If (t1 eqType t2) then I can replace t1 by t2 anywhere. **

This principle also tells us that eqType must relate only types with the
same kinds.
422
-}
423

424 425
{- **********************************************************************
*                                                                       *
426
                  TyBinder and ArgFlag
427 428
*                                                                       *
********************************************************************** -}
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
429

430 431 432 433
-- | A 'TyBinder' represents an argument to a function. TyBinders can be dependent
-- ('Named') or nondependent ('Anon'). They may also be visible or not.
-- See Note [TyBinders]
data TyBinder
Simon Peyton Jones's avatar
Simon Peyton Jones committed
434
  = Named TyVarBinder
435
  | Anon Type   -- Visibility is determined by the type (Constraint vs. *)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
436 437 438 439 440 441 442 443 444
  deriving Data.Data

-- | Remove the binder's variable from the set, if the binder has
-- a variable.
delBinderVar :: VarSet -> TyVarBinder -> VarSet
delBinderVar vars (TvBndr tv _) = vars `delVarSet` tv

-- | Does this binder bind an invisible argument?
isInvisibleBinder :: TyBinder -> Bool
445
isInvisibleBinder (Named (TvBndr _ vis)) = isInvisibleArgFlag vis
Simon Peyton Jones's avatar
Simon Peyton Jones committed
446 447 448 449 450 451 452
isInvisibleBinder (Anon ty)              = isPredTy ty

-- | Does this binder bind a visible argument?
isVisibleBinder :: TyBinder -> Bool
isVisibleBinder = not . isInvisibleBinder


453 454
{- Note [TyBinders]
~~~~~~~~~~~~~~~~~~~
Simon Peyton Jones's avatar
Simon Peyton Jones committed
455 456
A ForAllTy contains a TyVarBinder.  But a type can be decomposed
to a telescope consisting of a [TyBinder]
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
457

458 459 460
A TyBinder represents the type of binders -- that is, the type of an
argument to a Pi-type. GHC Core currently supports two different
Pi-types:
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
461

462 463
 * A non-dependent function,
   written with ->, e.g. ty1 -> ty2
Simon Peyton Jones's avatar
Simon Peyton Jones committed
464
   represented as FunTy ty1 ty2
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
465

466 467
 * A dependent compile-time-only polytype,
   written with forall, e.g.  forall (a:*). ty
Simon Peyton Jones's avatar
Simon Peyton Jones committed
468
   represented as ForAllTy (TvBndr a v) ty
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
469

470 471 472 473
Both Pi-types classify terms/types that take an argument. In other
words, if `x` is either a function or a polytype, `x arg` makes sense
(for an appropriate `arg`). It is thus often convenient to group
Pi-types together.  This is ForAllTy.
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
474

475 476 477
The two constructors for TyBinder sort out the two different possibilities.
`Named` builds a polytype, while `Anon` builds an ordinary function.
(ForAllTy (Anon arg) res used to be called FunTy arg res.)
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
478

479
Note [TyBinders and ArgFlags]
480
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Simon Peyton Jones's avatar
Simon Peyton Jones committed
481
A ForAllTy contains a TyVarBinder.  Each TyVarBinder is equipped
482
with a ArgFlag, which says whether or not arguments for this
483 484 485 486 487 488 489 490
binder should be visible (explicit) in source Haskell.

-----------------------------------------------------------------------
                                            Occurrences look like this
 TyBinder          GHC displays type as     in Haskell souce code
-----------------------------------------------------------------------
In the type of a term
 Anon:             f :: type -> type         Arg required:     f x
491
 Named Inferred:   f :: forall {a}. type     Arg not allowed:  f
492
 Named Specified:  f :: forall a. type       Arg optional:     f  or  f @Int
493
 Named Required:         Illegal: See Note [No Required TyBinder in terms]
494 495 496

In the kind of a type
 Anon:             T :: kind -> kind         Required:            T *
497
 Named Inferred:   T :: forall {k}. kind     Arg not allowed:     T
498
 Named Specified:  T :: forall k. kind       Arg not allowed[1]:  T
499
 Named Required:   T :: forall k -> kind     Required:            T *
500 501 502 503 504 505 506 507 508 509
------------------------------------------------------------------------

[1] In types, in the Specified case, it would make sense to allow
    optional kind applications, thus (T @*), but we have not
    yet implemented that

---- Examples of where the different visiblities come from -----

In term declarations:

510 511 512
* Inferred.  Function defn, with no signature:  f1 x = x
  We infer f1 :: forall {a}. a -> a, with 'a' Inferred
  It's Inferred because it doesn't appear in any
513 514 515 516 517 518 519 520 521 522 523
  user-written signature for f1

* Specified.  Function defn, with signature (implicit forall):
     f2 :: a -> a; f2 x = x
  So f2 gets the type f2 :: forall a. a->a, with 'a' Specified
  even though 'a' is not bound in the source code by an explicit forall

* Specified.  Function defn, with signature (explicit forall):
     f3 :: forall a. a -> a; f3 x = x
  So f3 gets the type f3 :: forall a. a->a, with 'a' Specified

524
* Inferred/Specified.  Function signature with inferred kind polymorphism.
525
     f4 :: a b -> Int
526 527
  So 'f4' gets the type f4 :: forall {k} (a:k->*) (b:k). a b -> Int
  Here 'k' is Inferred (it's not mentioned in the type),
528 529 530 531 532 533 534 535
  but 'a' and 'b' are Specified.

* Specified.  Function signature with explicit kind polymorphism
     f5 :: a (b :: k) -> Int
  This time 'k' is Specified, because it is mentioned explicitly,
  so we get f5 :: forall (k:*) (a:k->*) (b:k). a b -> Int

* Similarly pattern synonyms:
536 537
  Inferred - from inferred types (e.g. no pattern type signature)
           - or from inferred kind polymorphism
538 539 540

In type declarations:

541
* Inferred (k)
542 543
     data T1 a b = MkT1 (a b)
  Here T1's kind is  T1 :: forall {k:*}. (k->*) -> k -> *
544
  The kind variable 'k' is Inferred, since it is not mentioned
545 546 547

  Note that 'a' and 'b' correspond to /Anon/ TyBinders in T1's kind,
  and Anon binders don't have a visibility flag. (Or you could think
548
  of Anon having an implicit Required flag.)
549 550 551 552

* Specified (k)
     data T2 (a::k->*) b = MkT (a b)
  Here T's kind is  T :: forall (k:*). (k->*) -> k -> *
Simon Peyton Jones's avatar
Simon Peyton Jones committed
553
  The kind variable 'k' is Specified, since it is mentioned in
554 555
  the signature.

556
* Required (k)
557 558
     data T k (a::k->*) b = MkT (a b)
  Here T's kind is  T :: forall k:* -> (k->*) -> k -> *
559
  The kind is Required, since it bound in a positional way in T's declaration
560 561
  Every use of T must be explicitly applied to a kind

562
* Inferred (k1), Specified (k)
563 564
     data T a b (c :: k) = MkT (a b) (Proxy c)
  Here T's kind is  T :: forall {k1:*} (k:*). (k1->*) -> k1 -> k -> *
Gabor Greif's avatar
Gabor Greif committed
565
  So 'k' is Specified, because it appears explicitly,
566
  but 'k1' is Inferred, because it does not
567 568 569 570 571 572 573 574 575 576

---- Printing -----

 We print forall types with enough syntax to tell you their visiblity
 flag.  But this is not source Haskell, and these types may not all
 be parsable.

 Specified: a list of Specified binders is written between `forall` and `.`:
               const :: forall a b. a -> b -> a

577
 Inferred:  with -fprint-explicit-foralls, Inferred binders are written
578 579 580 581
            in braces:
               f :: forall {k} (a:k). S k a -> Int
            Otherwise, they are printed like Specified binders.

582
 Required: binders are put between `forall` and `->`:
583 584 585 586 587
              T :: forall k -> *

---- Other points -----

* In classic Haskell, all named binders (that is, the type variables in
588
  a polymorphic function type f :: forall a. a -> a) have been Inferred.
589

590
* Inferred variables correspond to "generalized" variables from the
591 592
  Visible Type Applications paper (ESOP'16).

593
Note [No Required TyBinder in terms]
594
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
595
We don't allow Required foralls for term variables, including pattern
596 597 598
synonyms and data constructors.  Why?  Because then an application
would need a /compulsory/ type argument (possibly without an "@"?),
thus (f Int); and we don't have concrete syntax for that.
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
599

600
We could change this decision, but Required, Named TyBinders are rare
601
anyway.  (Most are Anons.)
602 603
-}

604 605 606 607 608 609 610 611

{- **********************************************************************
*                                                                       *
                        PredType
*                                                                       *
********************************************************************** -}


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
-- | A type of the form @p@ of kind @Constraint@ represents a value whose type is
-- the Haskell predicate @p@, where a predicate is what occurs before
-- the @=>@ in a Haskell type.
--
-- We use 'PredType' as documentation to mark those types that we guarantee to have
-- this kind.
--
-- It can be expanded into its representation, but:
--
-- * The type checker must treat it as opaque
--
-- * The rest of the compiler treats it as transparent
--
-- Consider these examples:
--
-- > f :: (Eq a) => a -> Int
-- > g :: (?x :: Int -> Int) => a -> Int
-- > h :: (r\l) => {r} => {l::Int | r}
--
-- Here the @Eq a@ and @?x :: Int -> Int@ and @r\l@ are all called \"predicates\"
type PredType = Type

-- | A collection of 'PredType's
type ThetaType = [PredType]

{-
(We don't support TREX records yet, but the setup is designed
to expand to allow them.)

A Haskell qualified type, such as that for f,g,h above, is
represented using
        * a FunTy for the double arrow
        * with a type of kind Constraint as the function argument

The predicate really does turn into a real extra argument to the
function.  If the argument has type (p :: Constraint) then the predicate p is
represented by evidence of type p.

650

651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671
%************************************************************************
%*                                                                      *
            Simple constructors
%*                                                                      *
%************************************************************************

These functions are here so that they can be used by TysPrim,
which in turn is imported by Type
-}

-- named with "Only" to prevent naive use of mkTyVarTy
mkTyVarTy  :: TyVar   -> Type
mkTyVarTy v = ASSERT2( isTyVar v, ppr v <+> dcolon <+> ppr (tyVarKind v) )
                  TyVarTy v

mkTyVarTys :: [TyVar] -> [Type]
mkTyVarTys = map mkTyVarTy -- a common use of mkTyVarTy

infixr 3 `mkFunTy`      -- Associates to the right
-- | Make an arrow type
mkFunTy :: Type -> Type -> Type
Simon Peyton Jones's avatar
Simon Peyton Jones committed
672
mkFunTy arg res = FunTy arg res
673 674 675 676 677

-- | Make nested arrow types
mkFunTys :: [Type] -> Type -> Type
mkFunTys tys ty = foldr mkFunTy ty tys

678
mkForAllTy :: TyVar -> ArgFlag -> Type -> Type
679
mkForAllTy tv vis ty = ForAllTy (TvBndr tv vis) ty
Simon Peyton Jones's avatar
Simon Peyton Jones committed
680

681
-- | Wraps foralls over the type using the provided 'TyVar's from left to right
Simon Peyton Jones's avatar
Simon Peyton Jones committed
682
mkForAllTys :: [TyVarBinder] -> Type -> Type
683 684
mkForAllTys tyvars ty = foldr ForAllTy ty tyvars

Simon Peyton Jones's avatar
Simon Peyton Jones committed
685 686 687 688 689 690 691
mkPiTy :: TyBinder -> Type -> Type
mkPiTy (Anon ty1) ty2 = FunTy ty1 ty2
mkPiTy (Named tvb) ty = ForAllTy tvb ty

mkPiTys :: [TyBinder] -> Type -> Type
mkPiTys tbs ty = foldr mkPiTy ty tbs

692 693 694
-- | Does this type classify a core (unlifted) Coercion?
-- At either role nominal or reprsentational
--    (t1 ~# t2) or (t1 ~R# t2)
695 696 697 698 699 700 701
isCoercionType :: Type -> Bool
isCoercionType (TyConApp tc tys)
  | (tc `hasKey` eqPrimTyConKey) || (tc `hasKey` eqReprPrimTyConKey)
  , length tys == 4
  = True
isCoercionType _ = False

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
702

703 704 705 706 707 708 709 710
-- | Create the plain type constructor type which has been applied to no type arguments at all.
mkTyConTy :: TyCon -> Type
mkTyConTy tycon = TyConApp tycon []

{-
Some basic functions, put here to break loops eg with the pretty printer
-}

711
-- | This version considers Constraint to be distinct from *.
712
isLiftedTypeKind :: Kind -> Bool
713
isLiftedTypeKind ki | Just ki' <- coreView ki = isLiftedTypeKind ki'
714 715 716
isLiftedTypeKind (TyConApp tc [TyConApp ptr_rep []])
  =  tc      `hasKey` tYPETyConKey
  && ptr_rep `hasKey` ptrRepLiftedDataConKey
717 718 719
isLiftedTypeKind _                = False

isUnliftedTypeKind :: Kind -> Bool
720
isUnliftedTypeKind ki | Just ki' <- coreView ki = isUnliftedTypeKind ki'
721 722 723 724 725 726 727
isUnliftedTypeKind (TyConApp tc [TyConApp ptr_rep []])
  | tc       `hasKey` tYPETyConKey
  , ptr_rep  `hasKey` ptrRepLiftedDataConKey
  = False
isUnliftedTypeKind (TyConApp tc [arg])
  = tc `hasKey` tYPETyConKey && isEmptyVarSet (tyCoVarsOfType arg)
      -- all other possibilities are unlifted
728 729
isUnliftedTypeKind _ = False

730 731 732 733 734
-- | Is this the type 'RuntimeRep'?
isRuntimeRepTy :: Type -> Bool
isRuntimeRepTy ty | Just ty' <- coreView ty = isRuntimeRepTy ty'
isRuntimeRepTy (TyConApp tc []) = tc `hasKey` runtimeRepTyConKey
isRuntimeRepTy _ = False
735

736 737 738
-- | Is this a type of kind RuntimeRep? (e.g. PtrRep)
isRuntimeRepKindedTy :: Type -> Bool
isRuntimeRepKindedTy = isRuntimeRepTy . typeKind
739

740 741 742
-- | Is a tyvar of type 'RuntimeRep'?
isRuntimeRepVar :: TyVar -> Bool
isRuntimeRepVar = isRuntimeRepTy . tyVarKind
743

744 745
-- | Drops prefix of RuntimeRep constructors in 'TyConApp's. Useful for e.g.
-- dropping 'PtrRep arguments of unboxed tuple TyCon applications:
746
--
747 748
--   dropRuntimeRepArgs [ 'PtrRepLifted, 'PtrRepUnlifted
--                      , String, Int# ] == [String, Int#]
749
--
750 751
dropRuntimeRepArgs :: [Type] -> [Type]
dropRuntimeRepArgs = dropWhile isRuntimeRepKindedTy
752

753 754 755 756 757 758 759 760 761 762 763 764 765 766 767
{-
%************************************************************************
%*                                                                      *
            Coercions
%*                                                                      *
%************************************************************************
-}

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

-- If you edit this type, you may need to update the GHC formalism
-- See Note [GHC Formalism] in coreSyn/CoreLint.hs
data Coercion
  -- Each constructor has a "role signature", indicating the way roles are
768 769 770 771 772 773
  -- 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.
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

  -- These ones mirror the shape of types
  = -- Refl :: "e" -> _ -> e
    Refl Role Type  -- See Note [Refl invariant]
          -- 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.

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

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

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

800
  | AppCo Coercion CoercionN             -- lift AppTy
801 802 803
          -- AppCo :: e -> N -> e

  -- See Note [Forall coercions]
804
  | ForAllCo TyVar KindCoercion Coercion
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
         -- ForAllCo :: _ -> N -> e -> e

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

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

  | UnivCo UnivCoProvenance Role Type Type
      -- :: _ -> "e" -> _ -> _ -> e

  | SymCo Coercion             -- :: e -> e
  | TransCo Coercion Coercion  -- :: e -> e -> e

    -- The number coercions should match exactly the expectations
    -- of the CoAxiomRule (i.e., the rule is fully saturated).
  | AxiomRuleCo CoAxiomRule [Coercion]

  | NthCo  Int         Coercion     -- Zero-indexed; decomposes (T t0 ... tn)
    -- :: _ -> e -> ?? (inverse of TyConAppCo, see Note [TyConAppCo roles])
    -- Using NthCo on a ForAllCo gives an N coercion always
    -- See Note [NthCo and newtypes]

834
  | LRCo   LeftOrRight CoercionN     -- Decomposes (t_left t_right)
835
    -- :: _ -> N -> N
836
  | InstCo Coercion CoercionN
837 838 839 840 841
    -- :: e -> N -> e
    -- See Note [InstCo roles]

  -- Coherence applies a coercion to the left-hand type of another coercion
  -- See Note [Coherence]
842
  | CoherenceCo Coercion KindCoercion
843 844 845 846 847 848 849
     -- :: e -> N -> e

  -- Extract a kind coercion from a (heterogeneous) type coercion
  -- NB: all kind coercions are Nominal
  | KindCo Coercion
     -- :: e -> N

850
  | SubCo CoercionN                  -- Turns a ~N into a ~R
851 852
    -- :: N -> R

853
  deriving Data.Data
854

855 856 857 858 859
type CoercionN = Coercion       -- always nominal
type CoercionR = Coercion       -- always representational
type CoercionP = Coercion       -- always phantom
type KindCoercion = CoercionN   -- always nominal

860 861 862
-- If you edit this type, you may need to update the GHC formalism
-- See Note [GHC Formalism] in coreSyn/CoreLint.hs
data LeftOrRight = CLeft | CRight
863
                 deriving( Eq, Data.Data )
864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 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 936 937 938 939 940 941 942 943 944 945 946 947 948 949 950 951 952 953 954 955 956 957 958 959 960 961 962 963 964 965 966 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 1001 1002 1003 1004 1005 1006 1007 1008 1009 1010 1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046 1047 1048 1049 1050 1051 1052 1053 1054 1055 1056 1057 1058 1059 1060 1061 1062 1063 1064 1065 1066 1067 1068 1069 1070 1071 1072 1073 1074 1075 1076 1077 1078 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 1182 1183 1184 1185 1186

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 }

pickLR :: LeftOrRight -> (a,a) -> a
pickLR CLeft  (l,_) = l
pickLR CRight (_,r) = r


{-
Note [Refl invariant]
~~~~~~~~~~~~~~~~~~~~~
Invariant 1:

Coercions have the following invariant
     Refl is always lifted as far as possible.

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
expose further opportunities for optimization.

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.

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.

Note [Forall coercions]
~~~~~~~~~~~~~~~~~~~~~~~
Constructing coercions between forall-types can be a bit tricky,
because the kinds of the bound tyvars can be different.

The typing rule is:


  kind_co : k1 ~ k2
  tv1:k1 |- co : t1 ~ t2
  -------------------------------------------------------------------
  ForAllCo tv1 kind_co co : all tv1:k1. t1  ~
                            all tv1:k2. (t2[tv1 |-> tv1 |> sym kind_co])

First, the TyVar stored in a ForAllCo is really an optimisation: this field
should be a Name, as its kind is redundant. Thinking of the field as a Name
is helpful in understanding what a ForAllCo means.

The idea is that kind_co gives the two kinds of the tyvar. See how, in the
conclusion, tv1 is assigned kind k1 on the left but kind k2 on the right.

Of course, a type variable can't have different kinds at the same time. So,
we arbitrarily prefer the first kind when using tv1 in the inner coercion
co, which shows that t1 equals t2.

The last wrinkle is that we need to fix the kinds in the conclusion. In
t2, tv1 is assumed to have kind k1, but it has kind k2 in the conclusion of
the rule. So we do a kind-fixing substitution, replacing (tv1:k1) with
(tv1:k2) |> sym kind_co. This substitution is slightly bizarre, because it
mentions the same name with different kinds, but it *is* well-kinded, noting
that `(tv1:k2) |> sym kind_co` has kind k1.

This all really would work storing just a Name in the ForAllCo. But we can't
add Names to, e.g., VarSets, and there generally is just an impedence mismatch
in a bunch of places. So we use tv1. When we need tv2, we can use
setTyVarKind.

Note [Coherence]
~~~~~~~~~~~~~~~~
The Coherence typing rule is thus:

  g1 : s ~ t    s : k1    g2 : k1 ~ k2
  ------------------------------------
  CoherenceCo g1 g2 : (s |> g2) ~ t

While this looks (and is) unsymmetric, a combination of other coercion
combinators can make the symmetric version.

For role information, see Note [Roles and kind coercions].

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?

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

   ((~) [c] a) -> [a] -> c
   ((~) [c] b) -> [b] -> c

So the coercion between the two is obviously

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

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

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

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 [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:

  type instance F Int = Bool   -- Axiom axF : F Int ~N Bool
  newtype Age = MkAge Int      -- Axiom axAge : Age ~R Int
  data Foo a = MkFoo a         -- Role on Foo's parameter is Representational

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.

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.

  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.

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.

The rules here dictate the roles of the parameters to mkTyConAppCo
(should be checked by Lint).

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

Note [InstCo roles]
~~~~~~~~~~~~~~~~~~~
Here is (essentially) the typing rule for InstCo:

g :: (forall a. t1) ~r (forall a. t2)
w :: s1 ~N s2
------------------------------- InstCo
InstCo g w :: (t1 [a |-> s1]) ~r (t2 [a |-> s2])

Note that the Coercion w *must* be nominal. This is necessary
because the variable a might be used in a "nominal position"
(that is, a place where role inference would require a nominal
role) in t1 or t2. If we allowed w to be representational, we
could get bogus equalities.

A more nuanced treatment might be able to relax this condition
somewhat, by checking if t1 and/or t2 use their bound variables
in nominal ways. If not, having w be representational is OK.

1187 1188 1189 1190 1191 1192 1193 1194 1195 1196 1197 1198 1199 1200 1201 1202 1203 1204 1205

%************************************************************************
%*                                                                      *
                UnivCoProvenance
%*                                                                      *
%************************************************************************

A UnivCo is a coercion whose proof does not directly express its role
and kind (indeed for some UnivCos, like UnsafeCoerceProv, there /is/
no proof).

The different kinds of UnivCo are described by UnivCoProvenance.  Really
each is entirely separate, but they all share the need to represent their
role and kind, which is done in the UnivCo constructor.

-}

-- | For simplicity, we have just one UnivCo that represents a coercion from
-- some type to some other type, with (in general) no restrictions on the
1206 1207 1208 1209 1210 1211
-- type. The UnivCoProvenance specifies more exactly what the coercion really
-- is and why a program should (or shouldn't!) trust the coercion.
-- It is reasonable to consider each constructor of 'UnivCoProvenance'
-- as a totally independent coercion form; their only commonality is
-- that they don't tell you what types they coercion between. (That info
-- is in the 'UnivCo' constructor of 'Coercion'.
1212 1213 1214
data UnivCoProvenance
  = UnsafeCoerceProv   -- ^ From @unsafeCoerce#@. These are unsound.

1215 1216
  | PhantomProv KindCoercion -- ^ See Note [Phantom coercions]. Only in Phantom
                             -- roled coercions
1217

1218 1219 1220
  | ProofIrrelProv KindCoercion  -- ^ From the fact that any two coercions are
                                 --   considered equivalent. See Note [ProofIrrelProv].
                                 -- Can be used in Nominal or Representational coercions
1221 1222 1223 1224 1225

  | PluginProv String  -- ^ From a plugin, which asserts that this coercion
                       --   is sound. The string is for the use of the plugin.

  | HoleProv CoercionHole  -- ^ See Note [Coercion holes]
1226
  deriving Data.Data
1227 1228 1229 1230 1231 1232 1233 1234 1235 1236 1237 1238 1239 1240 1241 1242 1243 1244 1245 1246 1247 1248 1249 1250 1251 1252 1253 1254 1255 1256

instance Outputable UnivCoProvenance where
  ppr UnsafeCoerceProv   = text "(unsafeCoerce#)"
  ppr (PhantomProv _)    = text "(phantom)"
  ppr (ProofIrrelProv _) = text "(proof irrel.)"
  ppr (PluginProv str)   = parens (text "plugin" <+> brackets (text str))
  ppr (HoleProv hole)    = parens (text "hole" <> ppr hole)

-- | A coercion to be filled in by the type-checker. See Note [Coercion holes]
data CoercionHole
  = CoercionHole { chUnique   :: Unique   -- ^ used only for debugging
                 , chCoercion :: IORef (Maybe Coercion)
                 }

instance Data.Data CoercionHole where
  -- don't traverse?
  toConstr _   = abstractConstr "CoercionHole"
  gunfold _ _  = error "gunfold"
  dataTypeOf _ = mkNoRepType "CoercionHole"

instance Outputable CoercionHole where
  ppr (CoercionHole u _) = braces (ppr u)


{- Note [Phantom coercions]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
     data T a = T1 | T2
Then we have
     T s ~R T t
1257 1258 1259 1260 1261
for any old s,t. The witness for this is (TyConAppCo T Rep co),
where (co :: s ~P t) is a phantom coercion built with PhantomProv.
The role of the UnivCo is always Phantom.  The Coercion stored is the
(nominal) kind coercion between the types
   kind(s) ~N kind (t)
1262 1263 1264 1265 1266 1267 1268 1269 1270 1271 1272 1273 1274 1275

Note [Coercion holes]
~~~~~~~~~~~~~~~~~~~~~~~~
During typechecking, constraint solving for type classes works by
  - Generate an evidence Id,  d7 :: Num a
  - Wrap it in a Wanted constraint, [W] d7 :: Num a
  - Use the evidence Id where the evidence is needed
  - Solve the constraint later
  - When solved, add an enclosing let-binding  let d7 = .... in ....
    which actually binds d7 to the (Num a) evidence

For equality constraints we use a different strategy.  See Note [The
equality types story] in TysPrim for background on equality constraints.
  - For boxed equality constraints, (t1 ~N t2) and (t1 ~R t2), it's just
1276 1277
    like type classes above. (Indeed, boxed equality constraints *are* classes.)
  - But for /unboxed/ equality constraints (t1 ~R# t2) and (t1 ~N# t2)
1278 1279 1280 1281 1282
    we use a different plan

For unboxed equalities:
  - Generate a CoercionHole, a mutable variable just like a unification
    variable
1283
  - Wrap the CoercionHole in a Wanted constraint; see TcRnTypes.TcEvDest
1284 1285 1286 1287 1288 1289 1290 1291 1292 1293 1294 1295 1296 1297 1298 1299 1300 1301 1302 1303 1304 1305 1306 1307 1308 1309 1310 1311 1312 1313 1314 1315 1316 1317 1318 1319 1320
  - Use the CoercionHole in a Coercion, via HoleProv
  - Solve the constraint later
  - When solved, fill in the CoercionHole by side effect, instead of
    doing the let-binding thing

The main reason for all this is that there may be no good place to let-bind
the evidence for unboxed equalities:
  - We emit constraints for kind coercions, to be used
    to cast a type's kind. These coercions then must be used in types. Because
    they might appear in a top-level type, there is no place to bind these
   (unlifted) coercions in the usual way.

  - A coercion for (forall a. t1) ~ forall a. t2) will look like
       forall a. (coercion for t1~t2)
    But the coercion for (t1~t2) may mention 'a', and we don't have let-bindings
    within coercions.  We could add them, but coercion holes are easier.

Other notes about HoleCo:

 * INVARIANT: CoercionHole and HoleProv are used only during type checking,
   and should never appear in Core. Just like unification variables; a Type
   can contain a TcTyVar, but only during type checking. If, one day, we
   use type-level information to separate out forms that can appear during
   type-checking vs forms that can appear in core proper, holes in Core will
   be ruled out.

 * The Unique carried with a coercion hole is used solely for debugging.

 * Coercion holes can be compared for equality only like other coercions:
   only by looking at the types coerced.

 * We don't use holes for other evidence because other evidence wants to
   be /shared/. But coercions are entirely erased, so there's little
   benefit to sharing.

Note [ProofIrrelProv]
~~~~~~~~~~~~~~~~~~~~~
1321
A ProofIrrelProv is a coercion between coercions. For example:
1322 1323 1324 1325 1326 1327 1328 1329 1330 1331 1332 1333 1334 1335 1336 1337 1338 1339 1340 1341 1342 1343 1344 1345 1346 1347 1348 1349

  data G a where
    MkG :: G Bool

In core, we get

  G :: * -> *
  MkG :: forall (a :: *). (a ~ Bool) -> G a

Now, consider 'MkG -- that is, MkG used in a type -- and suppose we want
a proof that ('MkG co1 a1) ~ ('MkG co2 a2). This will have to be

  TyConAppCo Nominal MkG [co3, co4]
  where
    co3 :: co1 ~ co2
    co4 :: a1 ~ a2

Note that
  co1 :: a1 ~ Bool
  co2 :: a2 ~ Bool

Here,
  co3 = UnivCo (ProofIrrelProv co5) Nominal (CoercionTy co1) (CoercionTy co2)
  where
    co5 :: (a1 ~ Bool) ~ (a2 ~ Bool)
    co5 = TyConAppCo Nominal (~) [<*>, <*>, co4, <Bool>]


1350 1351 1352 1353 1354 1355 1356
%************************************************************************
%*                                                                      *
                 Free variables of types and coercions
%*                                                                      *
%************************************************************************
-}

1357 1358 1359 1360 1361 1362 1363 1364 1365 1366 1367 1368 1369 1370 1371 1372
{- Note [Free variables of types]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The family of functions tyCoVarsOfType, tyCoVarsOfTypes etc, returns
a VarSet that is closed over the types of its variables.  More precisely,
  if    S = tyCoVarsOfType( t )
  and   (a:k) is in S
  then  tyCoVarsOftype( k ) is a subset of S

Example: The tyCoVars of this ((a:* -> k) Int) is {a, k}.

We could /not/ close over the kinds of the variable occurrences, and
instead do so at call sites, but it seems that we always want to do
so, so it's easiest to do it here.
-}


1373 1374 1375 1376
-- | Returns free variables of a type, including kind variables as
-- a non-deterministic set. For type synonyms it does /not/ expand the
-- synonym.
tyCoVarsOfType :: Type -> TyCoVarSet
1377
-- See Note [Free variables of types]
niteria's avatar
niteria committed
1378
tyCoVarsOfType ty = fvVarSet $ tyCoFVsOfType ty
1379 1380 1381 1382 1383

-- | `tyVarsOfType` that returns free variables of a type in a deterministic
-- set. For explanation of why using `VarSet` is not deterministic see
-- Note [Deterministic FV] in FV.
tyCoVarsOfTypeDSet :: Type -> DTyCoVarSet
1384
-- See Note [Free variables of types]
niteria's avatar
niteria committed
1385
tyCoVarsOfTypeDSet ty = fvDVarSet $ tyCoFVsOfType ty
1386 1387 1388 1389 1390

-- | `tyVarsOfType` that returns free variables of a type in deterministic
-- order. For explanation of why using `VarSet` is not deterministic see
-- Note [Deterministic FV] in FV.
tyCoVarsOfTypeList :: Type -> [TyCoVar]
1391
-- See Note [Free variables of types]
niteria's avatar
niteria committed
1392
tyCoVarsOfTypeList ty = fvVarList $ tyCoFVsOfType ty
1393 1394 1395 1396

-- | The worker for `tyVarsOfType` and `tyVarsOfTypeList`.
-- The previous implementation used `unionVarSet` which is O(n+m) and can
-- make the function quadratic.
1397 1398
-- It's exported, so that it can be composed with
-- other functions that compute free variables.
1399
-- See Note [FV naming conventions] in FV.
1400 1401
--
-- Eta-expanded because that makes it run faster (apparently)
1402
-- See Note [FV eta expansion] in FV for explanation.
niteria's avatar
niteria committed
1403
tyCoFVsOfType :: Type -> FV
1404
-- See Note [Free variables of types]
niteria's avatar
niteria committed
1405 1406 1407