Commit 40fa237e authored by Krzysztof Gogolewski's avatar Krzysztof Gogolewski Committed by Ben Gamari

Linear types (#15981)

This is the first step towards implementation of the linear types proposal
(https://github.com/ghc-proposals/ghc-proposals/pull/111).

It features

* A language extension -XLinearTypes
* Syntax for linear functions in the surface language
* Linearity checking in Core Lint, enabled with -dlinear-core-lint
* Core-to-core passes are mostly compatible with linearity
* Fields in a data type can be linear or unrestricted; linear fields
  have multiplicity-polymorphic constructors.
  If -XLinearTypes is disabled, the GADT syntax defaults to linear fields

The following items are not yet supported:

* a # m -> b syntax (only prefix FUN is supported for now)
* Full multiplicity inference (multiplicities are really only checked)
* Decent linearity error messages
* Linear let, where, and case expressions in the surface language
  (each of these currently introduce the unrestricted variant)
* Multiplicity-parametric fields
* Syntax for annotating lambda-bound or let-bound with a multiplicity
* Syntax for non-linear/multiple-field-multiplicity records
* Linear projections for records with a single linear field
* Linear pattern synonyms
* Multiplicity coercions (test LinearPolyType)

A high-level description can be found at
https://ghc.haskell.org/trac/ghc/wiki/LinearTypes/Implementation
Following the link above you will find a description of the changes made to Core.
This commit has been authored by

* Richard Eisenberg
* Krzysztof Gogolewski
* Matthew Pickering
* Arnaud Spiwack

With contributions from:

* Mark Barbone
* Alexander Vershilov

Updates haddock submodule.
parent 20616959
......@@ -197,7 +197,7 @@ module GHC (
-- ** Data constructors
DataCon,
dataConType, dataConTyCon, dataConFieldLabels,
dataConIsInfix, isVanillaDataCon, dataConUserType,
dataConIsInfix, isVanillaDataCon, dataConWrapperType,
dataConSrcBangs,
StrictnessMark(..), isMarkedStrict,
......
......@@ -1901,6 +1901,15 @@ typeSymbolAppendFamNameKey = mkPreludeTyConUnique 190
unsafeEqualityTyConKey :: Unique
unsafeEqualityTyConKey = mkPreludeTyConUnique 191
-- Linear types
multiplicityTyConKey :: Unique
multiplicityTyConKey = mkPreludeTyConUnique 192
unrestrictedFunTyConKey :: Unique
unrestrictedFunTyConKey = mkPreludeTyConUnique 193
multMulTyConKey :: Unique
multMulTyConKey = mkPreludeTyConUnique 194
---------------- Template Haskell -------------------
-- GHC.Builtin.Names.TH: USES TyConUniques 200-299
......@@ -2075,6 +2084,12 @@ typeLitNatDataConKey = mkPreludeDataConUnique 113
unsafeReflDataConKey :: Unique
unsafeReflDataConKey = mkPreludeDataConUnique 114
-- Multiplicity
oneDataConKey, manyDataConKey :: Unique
oneDataConKey = mkPreludeDataConUnique 115
manyDataConKey = mkPreludeDataConUnique 116
---------------- Template Haskell -------------------
-- GHC.Builtin.Names.TH: USES DataUniques 200-250
-----------------------------------------------------
......
......@@ -98,7 +98,7 @@ templateHaskellNames = [
-- Type
forallTName, forallVisTName, varTName, conTName, infixTName, appTName,
appKindTName, equalityTName, tupleTName, unboxedTupleTName,
unboxedSumTName, arrowTName, listTName, sigTName, litTName,
unboxedSumTName, arrowTName, mulArrowTName, listTName, sigTName, litTName,
promotedTName, promotedTupleTName, promotedNilTName, promotedConsTName,
wildCardTName, implicitParamTName,
-- TyLit
......@@ -438,8 +438,8 @@ recordPatSynName = libFun (fsLit "recordPatSyn") recordPatSynIdKey
-- data Type = ...
forallTName, forallVisTName, varTName, conTName, infixTName, tupleTName,
unboxedTupleTName, unboxedSumTName, arrowTName, listTName, appTName,
appKindTName, sigTName, equalityTName, litTName, promotedTName,
unboxedTupleTName, unboxedSumTName, arrowTName, mulArrowTName, listTName,
appTName, appKindTName, sigTName, equalityTName, litTName, promotedTName,
promotedTupleTName, promotedNilTName, promotedConsTName,
wildCardTName, implicitParamTName :: Name
forallTName = libFun (fsLit "forallT") forallTIdKey
......@@ -450,6 +450,7 @@ tupleTName = libFun (fsLit "tupleT") tupleTIdKey
unboxedTupleTName = libFun (fsLit "unboxedTupleT") unboxedTupleTIdKey
unboxedSumTName = libFun (fsLit "unboxedSumT") unboxedSumTIdKey
arrowTName = libFun (fsLit "arrowT") arrowTIdKey
mulArrowTName = libFun (fsLit "mulArrowT") mulArrowTIdKey
listTName = libFun (fsLit "listT") listTIdKey
appTName = libFun (fsLit "appT") appTIdKey
appKindTName = libFun (fsLit "appKindT") appKindTIdKey
......@@ -1046,6 +1047,10 @@ interruptibleIdKey = mkPreludeMiscIdUnique 442
funDepIdKey :: Unique
funDepIdKey = mkPreludeMiscIdUnique 445
-- mulArrow
mulArrowTIdKey :: Unique
mulArrowTIdKey = mkPreludeMiscIdUnique 446
-- data TySynEqn = ...
tySynEqnIdKey :: Unique
tySynEqnIdKey = mkPreludeMiscIdUnique 460
......
......@@ -579,7 +579,7 @@ primOpType op
Compare _occ ty -> compare_fun_ty ty
GenPrimOp _occ tyvars arg_tys res_ty ->
mkSpecForAllTys tyvars (mkVisFunTys arg_tys res_ty)
mkSpecForAllTys tyvars (mkVisFunTysMany arg_tys res_ty)
primOpOcc :: PrimOp -> OccName
primOpOcc op = case primOpInfo op of
......@@ -739,9 +739,9 @@ commutableOp :: PrimOp -> Bool
-- Utils:
dyadic_fun_ty, monadic_fun_ty, compare_fun_ty :: Type -> Type
dyadic_fun_ty ty = mkVisFunTys [ty, ty] ty
monadic_fun_ty ty = mkVisFunTy ty ty
compare_fun_ty ty = mkVisFunTys [ty, ty] intPrimTy
dyadic_fun_ty ty = mkVisFunTysMany [ty, ty] ty
monadic_fun_ty ty = mkVisFunTyMany ty ty
compare_fun_ty ty = mkVisFunTysMany [ty, ty] intPrimTy
-- Output stuff:
......
......@@ -125,7 +125,17 @@ module GHC.Builtin.Types (
int8ElemRepDataConTy, int16ElemRepDataConTy, int32ElemRepDataConTy,
int64ElemRepDataConTy, word8ElemRepDataConTy, word16ElemRepDataConTy,
word32ElemRepDataConTy, word64ElemRepDataConTy, floatElemRepDataConTy,
doubleElemRepDataConTy
doubleElemRepDataConTy,
-- * Multiplicity and friends
multiplicityTyConName, oneDataConName, manyDataConName, multiplicityTy,
multiplicityTyCon, oneDataCon, manyDataCon, oneDataConTy, manyDataConTy,
oneDataConTyCon, manyDataConTyCon,
multMulTyCon,
unrestrictedFunTyCon, unrestrictedFunTyConName
) where
#include "HsVersions.h"
......@@ -142,6 +152,7 @@ import {-# SOURCE #-} GHC.Builtin.Uniques
-- others:
import GHC.Core.Coercion.Axiom
import GHC.Types.Id
import GHC.Types.Var (VarBndr (Bndr))
import GHC.Settings.Constants ( mAX_TUPLE_SIZE, mAX_CTUPLE_SIZE, mAX_SUM_SIZE )
import GHC.Unit.Module ( Module )
import GHC.Core.Type
......@@ -150,6 +161,7 @@ import GHC.Core.DataCon
import {-# SOURCE #-} GHC.Core.ConLike
import GHC.Core.TyCon
import GHC.Core.Class ( Class, mkClass )
import GHC.Core.Multiplicity
import GHC.Types.Name.Reader
import GHC.Types.Name as Name
import GHC.Types.Name.Env ( NameEnv, mkNameEnv, lookupNameEnv, lookupNameEnv_NF )
......@@ -240,6 +252,7 @@ wiredInTyCons = [ -- Units are not treated like other tuples, because they
, vecElemTyCon
, constraintKindTyCon
, liftedTypeKindTyCon
, multiplicityTyCon
]
mkWiredInTyConName :: BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
......@@ -461,6 +474,20 @@ constraintKindTyConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "Constr
liftedTypeKindTyConName :: Name
liftedTypeKindTyConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "Type") liftedTypeKindTyConKey liftedTypeKindTyCon
multiplicityTyConName :: Name
multiplicityTyConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "Multiplicity")
multiplicityTyConKey multiplicityTyCon
oneDataConName, manyDataConName :: Name
oneDataConName = mkWiredInDataConName BuiltInSyntax gHC_TYPES (fsLit "One") oneDataConKey oneDataCon
manyDataConName = mkWiredInDataConName BuiltInSyntax gHC_TYPES (fsLit "Many") manyDataConKey manyDataCon
-- It feels wrong to have One and Many be BuiltInSyntax. But otherwise,
-- `Many`, in particular, is considered out of scope unless an appropriate
-- file is open. The problem with this is that `Many` appears implicitly in
-- types every time there is an `(->)`, hence out-of-scope errors get
-- reported. Making them built-in make it so that they are always considered in
-- scope.
runtimeRepTyConName, vecRepDataConName, tupleRepDataConName, sumRepDataConName :: Name
runtimeRepTyConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "RuntimeRep") runtimeRepTyConKey runtimeRepTyCon
vecRepDataConName = mkWiredInDataConName UserSyntax gHC_TYPES (fsLit "VecRep") vecRepDataConKey vecRepDataCon
......@@ -544,16 +571,20 @@ pcTyCon name cType tyvars cons
False -- Not in GADT syntax
pcDataCon :: Name -> [TyVar] -> [Type] -> TyCon -> DataCon
pcDataCon n univs = pcDataConWithFixity False n univs
pcDataCon n univs tys = pcDataConW n univs (map linear tys)
pcDataConW :: Name -> [TyVar] -> [Scaled Type] -> TyCon -> DataCon
pcDataConW n univs tys = pcDataConWithFixity False n univs
[] -- no ex_tvs
univs -- the univs are precisely the user-written tyvars
tys
pcDataConWithFixity :: Bool -- ^ declared infix?
-> Name -- ^ datacon name
-> [TyVar] -- ^ univ tyvars
-> [TyCoVar] -- ^ ex tycovars
-> [TyCoVar] -- ^ user-written tycovars
-> [Type] -- ^ args
-> [Scaled Type] -- ^ args
-> TyCon
-> DataCon
pcDataConWithFixity infx n = pcDataConWithFixity' infx n (dataConWorkerUnique (nameUnique n))
......@@ -567,7 +598,7 @@ pcDataConWithFixity infx n = pcDataConWithFixity' infx n (dataConWorkerUnique (n
pcDataConWithFixity' :: Bool -> Name -> Unique -> RuntimeRepInfo
-> [TyVar] -> [TyCoVar] -> [TyCoVar]
-> [Type] -> TyCon -> DataCon
-> [Scaled Type] -> TyCon -> DataCon
-- The Name should be in the DataName name space; it's the name
-- of the DataCon itself.
--
......@@ -625,7 +656,7 @@ mkDataConWorkerName data_con wrk_key =
pcSpecialDataCon :: Name -> [Type] -> TyCon -> RuntimeRepInfo -> DataCon
pcSpecialDataCon dc_name arg_tys tycon rri
= pcDataConWithFixity' False dc_name (dataConWorkerUnique (nameUnique dc_name)) rri
[] [] [] arg_tys tycon
[] [] [] (map linear arg_tys) tycon
{-
************************************************************************
......@@ -651,7 +682,7 @@ constraintKindTyCon = pcTyCon constraintKindTyConName Nothing [] []
liftedTypeKind, typeToTypeKind, constraintKind :: Kind
liftedTypeKind = tYPE liftedRepTy
typeToTypeKind = liftedTypeKind `mkVisFunTy` liftedTypeKind
typeToTypeKind = liftedTypeKind `mkVisFunTyMany` liftedTypeKind
constraintKind = mkTyConApp constraintKindTyCon []
{-
......@@ -791,7 +822,8 @@ isBuiltInOcc_maybe occ =
"~" -> Just eqTyConName
-- function tycon
"->" -> Just funTyConName
"FUN" -> Just funTyConName
"->" -> Just unrestrictedFunTyConName
-- boxed tuple data/tycon
-- We deliberately exclude Solo (the boxed 1-tuple).
......@@ -1149,7 +1181,7 @@ eqSCSelId, heqSCSelId, coercibleSCSelId :: Id
rhs klass
(mkPrelTyConRepName eqTyConName)
klass = mk_class tycon sc_pred sc_sel_id
datacon = pcDataCon eqDataConName tvs [sc_pred] tycon
datacon = pcDataConW eqDataConName tvs [unrestricted sc_pred] tycon
-- Kind: forall k. k -> k -> Constraint
binders = mkTemplateTyConBinders [liftedTypeKind] (\[k] -> [k,k])
......@@ -1167,7 +1199,7 @@ eqSCSelId, heqSCSelId, coercibleSCSelId :: Id
rhs klass
(mkPrelTyConRepName heqTyConName)
klass = mk_class tycon sc_pred sc_sel_id
datacon = pcDataCon heqDataConName tvs [sc_pred] tycon
datacon = pcDataConW heqDataConName tvs [unrestricted sc_pred] tycon
-- Kind: forall k1 k2. k1 -> k2 -> Constraint
binders = mkTemplateTyConBinders [liftedTypeKind, liftedTypeKind] id
......@@ -1185,7 +1217,7 @@ eqSCSelId, heqSCSelId, coercibleSCSelId :: Id
rhs klass
(mkPrelTyConRepName coercibleTyConName)
klass = mk_class tycon sc_pred sc_sel_id
datacon = pcDataCon coercibleDataConName tvs [sc_pred] tycon
datacon = pcDataConW coercibleDataConName tvs [unrestricted sc_pred] tycon
-- Kind: forall k. k -> k -> Constraint
binders = mkTemplateTyConBinders [liftedTypeKind] (\[k] -> [k,k])
......@@ -1203,6 +1235,67 @@ mk_class tycon sc_pred sc_sel_id
{- *********************************************************************
* *
Multiplicity Polymorphism
* *
********************************************************************* -}
{- Multiplicity polymorphism is implemented very similarly to levity
polymorphism. We write in the multiplicity kind and the One and Many
types which can appear in user programs. These are defined properly in GHC.Types.
data Multiplicity = One | Many
-}
multiplicityTy :: Type
multiplicityTy = mkTyConTy multiplicityTyCon
multiplicityTyCon :: TyCon
multiplicityTyCon = pcTyCon multiplicityTyConName Nothing []
[oneDataCon, manyDataCon]
oneDataCon, manyDataCon :: DataCon
oneDataCon = pcDataCon oneDataConName [] [] multiplicityTyCon
manyDataCon = pcDataCon manyDataConName [] [] multiplicityTyCon
oneDataConTy, manyDataConTy :: Type
oneDataConTy = mkTyConTy oneDataConTyCon
manyDataConTy = mkTyConTy manyDataConTyCon
oneDataConTyCon, manyDataConTyCon :: TyCon
oneDataConTyCon = promoteDataCon oneDataCon
manyDataConTyCon = promoteDataCon manyDataCon
multMulTyConName :: Name
multMulTyConName =
mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "MultMul") multMulTyConKey multMulTyCon
multMulTyCon :: TyCon
multMulTyCon = mkFamilyTyCon multMulTyConName binders multiplicityTy Nothing
(BuiltInSynFamTyCon trivialBuiltInFamily)
Nothing
NotInjective
where
binders = mkTemplateAnonTyConBinders [multiplicityTy, multiplicityTy]
unrestrictedFunTy :: Type
unrestrictedFunTy = functionWithMultiplicity manyDataConTy
unrestrictedFunTyCon :: TyCon
unrestrictedFunTyCon = buildSynTyCon unrestrictedFunTyConName [] arrowKind [] unrestrictedFunTy
where arrowKind = mkTyConKind binders liftedTypeKind
-- See also funTyCon
binders = [ Bndr runtimeRep1TyVar (NamedTCB Inferred)
, Bndr runtimeRep2TyVar (NamedTCB Inferred)
]
++ mkTemplateAnonTyConBinders [ tYPE runtimeRep1Ty
, tYPE runtimeRep2Ty
]
unrestrictedFunTyConName :: Name
unrestrictedFunTyConName = mkWiredInTyConName BuiltInSyntax gHC_TYPES (fsLit "->") unrestrictedFunTyConKey unrestrictedFunTyCon
{- *********************************************************************
* *
Kinds and RuntimeRep
......@@ -1576,7 +1669,7 @@ consDataCon :: DataCon
consDataCon = pcDataConWithFixity True {- Declared infix -}
consDataConName
alpha_tyvar [] alpha_tyvar
[alphaTy, mkTyConApp listTyCon alpha_ty] listTyCon
(map linear [alphaTy, mkTyConApp listTyCon alpha_ty]) listTyCon
-- Interesting: polymorphic recursion would help here.
-- We can't use (mkListTy alphaTy) in the defn of consDataCon, else mkListTy
-- gets the over-specific type (Type -> Type)
......
......@@ -44,4 +44,13 @@ anyTypeOfKind :: Kind -> Type
unboxedTupleKind :: [Type] -> Type
mkPromotedListTy :: Type -> [Type] -> Type
multiplicityTyCon :: TyCon
multiplicityTy :: Type
oneDataConTy :: Type
oneDataConTyCon :: TyCon
manyDataConTy :: Type
manyDataConTyCon :: TyCon
unrestrictedFunTyCon :: TyCon
multMulTyCon :: TyCon
tupleTyConName :: TupleSort -> Arity -> Name
......@@ -26,12 +26,16 @@ module GHC.Builtin.Types.Prim(
runtimeRep1TyVar, runtimeRep2TyVar, runtimeRep1Ty, runtimeRep2Ty,
openAlphaTy, openBetaTy, openAlphaTyVar, openBetaTyVar,
multiplicityTyVar,
multiplicityTyVarList,
-- Kind constructors...
tYPETyCon, tYPETyConName,
-- Kinds
tYPE, primRepToRuntimeRep,
functionWithMultiplicity,
funTyCon, funTyConName,
unexposedPrimTyCons, exposedPrimTyCons, primTyCons,
......@@ -108,7 +112,7 @@ import {-# SOURCE #-} GHC.Builtin.Types
, int64ElemRepDataConTy, word8ElemRepDataConTy, word16ElemRepDataConTy
, word32ElemRepDataConTy, word64ElemRepDataConTy, floatElemRepDataConTy
, doubleElemRepDataConTy
, mkPromotedListTy )
, mkPromotedListTy, multiplicityTy )
import GHC.Types.Var ( TyVar, mkTyVar )
import GHC.Types.Name
......@@ -385,6 +389,14 @@ openAlphaTy, openBetaTy :: Type
openAlphaTy = mkTyVarTy openAlphaTyVar
openBetaTy = mkTyVarTy openBetaTyVar
multiplicityTyVar :: TyVar
multiplicityTyVar = mkTemplateTyVars (repeat multiplicityTy) !! 13 -- selects 'n'
-- Create 'count' multiplicity TyVars
multiplicityTyVarList :: Int -> [TyVar]
multiplicityTyVarList count = take count $
drop 13 $ -- selects 'n', 'o'...
mkTemplateTyVars (repeat multiplicityTy)
{-
************************************************************************
* *
......@@ -394,13 +406,13 @@ openBetaTy = mkTyVarTy openBetaTyVar
-}
funTyConName :: Name
funTyConName = mkPrimTyConName (fsLit "->") funTyConKey funTyCon
funTyConName = mkPrimTyConName (fsLit "FUN") funTyConKey funTyCon
-- | The @(->)@ type constructor.
-- | The @FUN@ type constructor.
--
-- @
-- (->) :: forall {rep1 :: RuntimeRep} {rep2 :: RuntimeRep}.
-- TYPE rep1 -> TYPE rep2 -> Type
-- FUN :: forall {m :: Multiplicity} {rep1 :: RuntimeRep} {rep2 :: RuntimeRep}.
-- TYPE rep1 -> TYPE rep2 -> *
-- @
--
-- The runtime representations quantification is left inferred. This
......@@ -413,13 +425,15 @@ funTyConName = mkPrimTyConName (fsLit "->") funTyConKey funTyCon
-- @
-- type Arr :: forall (rep1 :: RuntimeRep) (rep2 :: RuntimeRep).
-- TYPE rep1 -> TYPE rep2 -> Type
-- type Arr = (->)
-- type Arr = FUN
-- @
--
funTyCon :: TyCon
funTyCon = mkFunTyCon funTyConName tc_bndrs tc_rep_nm
where
tc_bndrs = [ mkNamedTyConBinder Inferred runtimeRep1TyVar
-- See also unrestrictedFunTyCon
tc_bndrs = [ mkNamedTyConBinder Required multiplicityTyVar
, mkNamedTyConBinder Inferred runtimeRep1TyVar
, mkNamedTyConBinder Inferred runtimeRep2TyVar ]
++ mkTemplateAnonTyConBinders [ tYPE runtimeRep1Ty
, tYPE runtimeRep2Ty
......@@ -543,6 +557,10 @@ mkPrimTcName built_in_syntax occ key tycon
tYPE :: Type -> Type
tYPE rr = TyConApp tYPETyCon [rr]
-- Given a Multiplicity, applies FUN to it.
functionWithMultiplicity :: Type -> Type
functionWithMultiplicity mul = TyConApp funTyCon [mul]
{-
************************************************************************
* *
......
......@@ -194,17 +194,15 @@ section "The word size story."
-- This type won't be exported directly (since there is no concrete
-- syntax for this sort of export) so we'll have to manually patch
-- export lists in both GHC and Haddock.
primtype (->) a b
{The builtin function type, written in infix form as {\tt a -> b} and
in prefix form as {\tt (->) a b}. Values of this type are functions
taking inputs of type {\tt a} and producing outputs of type {\tt b}.
primtype FUN m a b
{The builtin function type, written in infix form as {\tt a # m -> b}.
Values of this type are functions taking inputs of type {\tt a} and
producing outputs of type {\tt b}. The multiplicity of the input is
{\tt m}.
Note that {\tt a -> b} permits levity-polymorphism in both {\tt a} and
Note that {\tt FUN m a b} permits levity-polymorphism in both {\tt a} and
{\tt b}, so that types like {\tt Int\# -> Int\#} can still be well-kinded.
}
with fixity = infixr -1
-- This fixity is only the one picked up by Haddock. If you
-- change this, do update 'ghcPrimIface' in 'GHC.Iface.Load'.
------------------------------------------------------------------------
section "Char#"
......
......@@ -19,6 +19,7 @@ import GHC.Types.Name ( Name, getName )
import GHC.Types.Name.Env
import GHC.Core.DataCon ( DataCon, dataConRepArgTys, dataConIdentity )
import GHC.Core.TyCon ( TyCon, tyConFamilySize, isDataTyCon, tyConDataCons )
import GHC.Core.Multiplicity ( scaledThing )
import GHC.Types.RepType
import GHC.StgToCmm.Layout ( mkVirtConstrSizes )
import GHC.StgToCmm.Closure ( tagForCon, NonVoid (..) )
......@@ -58,7 +59,7 @@ make_constr_itbls hsc_env cons =
mk_itbl dcon conNo = do
let rep_args = [ NonVoid prim_rep
| arg <- dataConRepArgTys dcon
, prim_rep <- typePrimRep arg ]
, prim_rep <- typePrimRep (scaledThing arg) ]
(tot_wds, ptr_wds) =
mkVirtConstrSizes dflags rep_args
......
......@@ -518,6 +518,10 @@ checked by Core Lint.
7. The type of the scrutinee must be the same as the type
of the case binder, obviously. Checked in lintCaseExpr.
8. The multiplicity of the binders in constructor patterns must be the
multiplicity of the corresponding field /scaled by the multiplicity of the
case binder/. Checked in lintCoreAlt.
Note [Core type and coercion invariant]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We allow a /non-recursive/, /non-top-level/ let to bind type and
......
......@@ -112,6 +112,8 @@ module GHC.Core.Coercion (
-- * Other
promoteCoercion, buildCoercion,
multToCo,
simplifyArgsWorker,
badCoercionHole, badCoercionHoleCo
......@@ -147,6 +149,7 @@ import GHC.Builtin.Types.Prim
import GHC.Data.List.SetOps
import GHC.Data.Maybe
import GHC.Types.Unique.FM
import GHC.Core.Multiplicity
import Control.Monad (foldM, zipWithM)
import Data.Function ( on )
......@@ -298,9 +301,9 @@ whose `RuntimeRep' arguments are intentionally marked inferred to
avoid type application.
Hence
FunCo r co1 co2 :: (s1->t1) ~r (s2->t2)
FunCo r mult co1 co2 :: (s1->t1) ~r (s2->t2)
is short for
TyConAppCo (->) co_rep1 co_rep2 co1 co2