Commit 8f4f5794 authored by Rinat Striungis's avatar Rinat Striungis

Unification of Nat and Naturals

This commit removes the separate kind 'Nat' and enables promotion
of type 'Natural' for using as type literal.
It partially solves #10776

Now the following code will be successfully typechecked:
    data C = MkC Natural
    type CC = MkC 1

Before this change we had to create the separate type for promotion
    data C = MkC Natural
    data CP = MkCP Nat
    type CC = MkCP 1

But CP is uninhabited in terms.

For backward compatibility type synonym `Nat` has been made:
    type Nat = Natural

The user's documentation and tests have been updated.
The haddock submodule also have been updated.
parent 0a5f2918
Pipeline #26273 passed with stages
in 323 minutes and 5 seconds
......@@ -1872,7 +1872,7 @@ uIntTyConKey = mkPreludeTyConUnique 162
uWordTyConKey = mkPreludeTyConUnique 163
-- Type-level naturals
typeNatKindConNameKey, typeSymbolKindConNameKey,
typeSymbolKindConNameKey,
typeNatAddTyFamNameKey, typeNatMulTyFamNameKey, typeNatExpTyFamNameKey,
typeNatLeqTyFamNameKey, typeNatSubTyFamNameKey
, typeSymbolCmpTyFamNameKey, typeNatCmpTyFamNameKey
......@@ -1880,7 +1880,6 @@ typeNatKindConNameKey, typeSymbolKindConNameKey,
, typeNatModTyFamNameKey
, typeNatLogTyFamNameKey
:: Unique
typeNatKindConNameKey = mkPreludeTyConUnique 164
typeSymbolKindConNameKey = mkPreludeTyConUnique 165
typeNatAddTyFamNameKey = mkPreludeTyConUnique 166
typeNatMulTyFamNameKey = mkPreludeTyConUnique 167
......
......@@ -96,7 +96,7 @@ module GHC.Builtin.Types (
mkSumTy, sumTyCon, sumDataCon,
-- * Kinds
typeNatKindCon, typeNatKind, typeSymbolKindCon, typeSymbolKind,
typeSymbolKindCon, typeSymbolKind,
isLiftedTypeKindTyConName, liftedTypeKind,
typeToTypeKind, constraintKind,
liftedTypeKindTyCon, constraintKindTyCon, constraintKindTyConName,
......@@ -256,7 +256,6 @@ wiredInTyCons = [ -- Units are not treated like other tuples, because they
, heqTyCon
, eqTyCon
, coercibleTyCon
, typeNatKindCon
, typeSymbolKindCon
, runtimeRepTyCon
, vecCountTyCon
......@@ -477,8 +476,7 @@ makeRecoveryTyCon tc
-- at (promoted) use-sites of MkT.
-- Kinds
typeNatKindConName, typeSymbolKindConName :: Name
typeNatKindConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "Nat") typeNatKindConNameKey typeNatKindCon
typeSymbolKindConName :: Name
typeSymbolKindConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "Symbol") typeSymbolKindConNameKey typeSymbolKindCon
constraintKindTyConName :: Name
......@@ -679,14 +677,11 @@ pcSpecialDataCon dc_name arg_tys tycon rri
************************************************************************
-}
typeNatKindCon, typeSymbolKindCon :: TyCon
-- data Nat
typeSymbolKindCon :: TyCon
-- data Symbol
typeNatKindCon = pcTyCon typeNatKindConName Nothing [] []
typeSymbolKindCon = pcTyCon typeSymbolKindConName Nothing [] []
typeNatKind, typeSymbolKind :: Kind
typeNatKind = mkTyConTy typeNatKindCon
typeSymbolKind :: Kind
typeSymbolKind = mkTyConTy typeSymbolKindCon
constraintKindTyCon :: TyCon
......
......@@ -8,7 +8,7 @@ import GHC.Types.Basic (Arity, TupleSort, Boxity, ConTag)
import {-# SOURCE #-} GHC.Types.Name (Name)
listTyCon :: TyCon
typeNatKind, typeSymbolKind :: Type
typeSymbolKind :: Type
mkBoxedTupleTy :: [Type] -> Type
coercibleTyCon, heqTyCon :: TyCon
......
......@@ -236,7 +236,7 @@ typeNatLogTyCon = mkTypeNatFunTyCon1 name
typeNatLeqTyCon :: TyCon
typeNatLeqTyCon =
mkFamilyTyCon name
(mkTemplateAnonTyConBinders [ typeNatKind, typeNatKind ])
(mkTemplateAnonTyConBinders [ naturalTy, naturalTy ])
boolTy
Nothing
(BuiltInSynFamTyCon ops)
......@@ -255,7 +255,7 @@ typeNatLeqTyCon =
typeNatCmpTyCon :: TyCon
typeNatCmpTyCon =
mkFamilyTyCon name
(mkTemplateAnonTyConBinders [ typeNatKind, typeNatKind ])
(mkTemplateAnonTyConBinders [ naturalTy, naturalTy ])
orderingKind
Nothing
(BuiltInSynFamTyCon ops)
......@@ -301,14 +301,12 @@ typeSymbolAppendTyCon = mkTypeSymbolFunTyCon2 name
name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "AppendSymbol")
typeSymbolAppendFamNameKey typeSymbolAppendTyCon
-- Make a unary built-in constructor of kind: Nat -> Nat
mkTypeNatFunTyCon1 :: Name -> BuiltInSynFamily -> TyCon
mkTypeNatFunTyCon1 op tcb =
mkFamilyTyCon op
(mkTemplateAnonTyConBinders [ typeNatKind ])
typeNatKind
(mkTemplateAnonTyConBinders [ naturalTy ])
naturalTy
Nothing
(BuiltInSynFamTyCon tcb)
Nothing
......@@ -319,8 +317,8 @@ mkTypeNatFunTyCon1 op tcb =
mkTypeNatFunTyCon2 :: Name -> BuiltInSynFamily -> TyCon
mkTypeNatFunTyCon2 op tcb =
mkFamilyTyCon op
(mkTemplateAnonTyConBinders [ typeNatKind, typeNatKind ])
typeNatKind
(mkTemplateAnonTyConBinders [ naturalTy, naturalTy ])
naturalTy
Nothing
(BuiltInSynFamTyCon tcb)
Nothing
......
......@@ -253,7 +253,7 @@ import GHC.Types.Unique.Set
import GHC.Core.TyCon
import GHC.Builtin.Types.Prim
import {-# SOURCE #-} GHC.Builtin.Types
( listTyCon, typeNatKind
( naturalTy, listTyCon
, typeSymbolKind, liftedTypeKind
, constraintKind
, unrestrictedFunTyCon
......@@ -2599,7 +2599,7 @@ tcReturnsConstraintKind _ = False
--------------------------
typeLiteralKind :: TyLit -> Kind
typeLiteralKind (NumTyLit {}) = typeNatKind
typeLiteralKind (NumTyLit {}) = naturalTy
typeLiteralKind (StrTyLit {}) = typeSymbolKind
-- | Returns True if a type is levity polymorphic. Should be the same
......
......@@ -53,7 +53,7 @@ import GHC.Tc.Utils.TcType
import GHC.Core.Type
import GHC.Core.Coercion
import GHC.Core.Multiplicity
import GHC.Builtin.Types ( typeNatKind, typeSymbolKind )
import GHC.Builtin.Types ( naturalTy, typeSymbolKind )
import GHC.Types.Id
import GHC.Types.Id.Make(proxyHashId)
import GHC.Types.Name
......@@ -1306,7 +1306,7 @@ ds_ev_typeable ty (EvTypeableTyLit ev)
-- tr_fun is the Name of
-- typeNatTypeRep :: KnownNat a => Proxy# a -> TypeRep a
-- of typeSymbolTypeRep :: KnownSymbol a => Proxy# a -> TypeRep a
tr_fun | ty_kind `eqType` typeNatKind = typeNatTypeRepName
tr_fun | ty_kind `eqType` naturalTy = typeNatTypeRepName
| ty_kind `eqType` typeSymbolKind = typeSymbolTypeRepName
| otherwise = panic "dsEvTypeable: unknown type lit kind"
......
......@@ -1192,8 +1192,8 @@ tc_hs_type _ rn_ty@(HsStarTy _ _) exp_kind
--------- Literals
tc_hs_type _ rn_ty@(HsTyLit _ (HsNumTy _ n)) exp_kind
= do { checkWiredInTyCon typeNatKindCon
; checkExpectedKind rn_ty (mkNumLitTy n) typeNatKind exp_kind }
= do { checkWiredInTyCon naturalTyCon
; checkExpectedKind rn_ty (mkNumLitTy n) naturalTy exp_kind }
tc_hs_type _ rn_ty@(HsTyLit _ (HsStrTy _ s)) exp_kind
= do { checkWiredInTyCon typeSymbolKindCon
......
......@@ -418,7 +418,7 @@ matchTypeable clas [k,t] -- clas = Typeable
| isJust (tcSplitPredFunTy_maybe t) = return NoInstance -- Qualified type
-- Now cases that do work
| k `eqType` typeNatKind = doTyLit knownNatClassName t
| k `eqType` naturalTy = doTyLit knownNatClassName t
| k `eqType` typeSymbolKind = doTyLit knownSymbolClassName t
| tcIsConstraintKind t = doTyConApp clas t constraintKindTyCon []
| Just (mult,arg,ret) <- splitFunTy_maybe t = doFunTy clas t mult arg ret
......
......@@ -28,8 +28,24 @@ Compiler
since the argument was already forced in the first equation. For more
details see :ghc-flag:`-Wredundant-bang-patterns`.
- Type checker plugins which work with the natural numbers now
should use ``naturalTy`` kind instead of ``typeNatKind``, which has been removed.
``ghc-prim`` library
~~~~~~~~~~~~~~~~~~~~
- ``Void#`` is now a type synonym for the unboxed tuple ``(# #)``.
Code using ``Void#`` now has to enable :extension:`UnboxedTuples`.
``base`` library
~~~~~~~~~~~~~~~~
- It's possible now to promote the ``Natural`` type: ::
data Coordinate = Mk2D Natural Natural
type MyCoordinate = Mk2D 1 10
The separate kind ``Nat`` is removed and now it is just a type synonym for
``Natural``. As a consequence, one must enable ``TypeSynonymInstances``
in order to define instances for ``Nat``.
......@@ -5,7 +5,7 @@ Type-Level Literals
GHC supports numeric and string literals at the type level, giving
convenient access to a large number of predefined type-level constants.
Numeric literals are of kind ``Nat``, while string literals are of kind
Numeric literals are of kind ``Natural``, while string literals are of kind
``Symbol``. This feature is enabled by the :extension:`DataKinds` language
extension.
......@@ -23,11 +23,17 @@ safe interface to a low-level function: ::
import Data.Word
import Foreign
newtype ArrPtr (n :: Nat) a = ArrPtr (Ptr a)
newtype ArrPtr (n :: Natural) a = ArrPtr (Ptr a)
clearPage :: ArrPtr 4096 Word8 -> IO ()
clearPage (ArrPtr p) = ...
Also type-level naturals could be promoted from the ``Natural`` data type
using `DataKinds`, for example: ::
data Point = MkPoint Natural Natural
type MyCoordinates = MkPoint 95 101
Here is an example of using type-level string literals to simulate
simple record operations: ::
......
......@@ -91,7 +91,7 @@ import GHC.List ( splitAt, foldl', elem )
import GHC.Word
import GHC.Show
import GHC.TypeLits ( KnownSymbol, symbolVal', AppendSymbol )
import GHC.TypeNats ( KnownNat, natVal' )
import GHC.TypeNats ( KnownNat, Nat, natVal' )
import Unsafe.Coerce ( unsafeCoerce )
import GHC.Fingerprint.Type
......
......@@ -40,7 +40,7 @@ module GHC.Event.PSQ
, atMost
) where
import GHC.Base hiding (Nat, empty)
import GHC.Base hiding (empty)
import GHC.Event.Unique
import GHC.Word (Word64)
import GHC.Num (Num(..))
......
......@@ -748,7 +748,7 @@ import GHC.Fingerprint.Type ( Fingerprint(..) )
-- Needed for metadata
import Data.Proxy ( Proxy(..) )
import GHC.TypeLits ( KnownSymbol, KnownNat, symbolVal, natVal )
import GHC.TypeLits ( KnownSymbol, KnownNat, Nat, symbolVal, natVal )
--------------------------------------------------------------------------------
-- Representation types
......
......@@ -31,7 +31,7 @@ working with type-level data will be defined in a separate library.
module GHC.TypeLits
( -- * Kinds
Nat, Symbol -- Both declared in GHC.Types in package ghc-prim
Natural, Nat, Symbol -- Symbol is declared in GHC.Types in package ghc-prim
-- * Linking type and value level
, N.KnownNat, natVal, natVal'
......@@ -54,7 +54,7 @@ module GHC.TypeLits
) where
import GHC.Base(Eq(..), Ord(..), Ordering(..), String, otherwise)
import GHC.Types( Nat, Symbol )
import GHC.Types(Symbol)
import GHC.Num(Integer, fromInteger)
import GHC.Show(Show(..))
import GHC.Read(Read(..))
......@@ -65,7 +65,7 @@ import Data.Proxy (Proxy(..))
import Data.Type.Equality((:~:)(Refl))
import Unsafe.Coerce(unsafeCoerce)
import GHC.TypeNats (KnownNat)
import GHC.TypeNats (Natural, Nat, KnownNat)
import qualified GHC.TypeNats as N
--------------------------------------------------------------------------------
......
......@@ -22,8 +22,8 @@ for working with type-level naturals should be defined in a separate library.
module GHC.TypeNats
( -- * Nat Kind
Nat -- declared in GHC.Types in package ghc-prim
Natural -- declared in GHC.Num.Natural in package ghc-bignum
, Nat
-- * Linking type and value level
, KnownNat, natVal, natVal'
, SomeNat(..)
......@@ -37,8 +37,8 @@ module GHC.TypeNats
) where
import GHC.Base(Eq(..), Ord(..), Bool(True), Ordering(..), otherwise)
import GHC.Types( Nat )
import GHC.Base(Eq(..), Ord(..), otherwise)
import GHC.Types
import GHC.Num.Natural(Natural)
import GHC.Show(Show(..))
import GHC.Read(Read(..))
......@@ -48,6 +48,13 @@ import Data.Proxy (Proxy(..))
import Data.Type.Equality((:~:)(Refl))
import Unsafe.Coerce(unsafeCoerce)
-- | A type synonym for 'Natural'.
--
-- Prevously, this was an opaque data type, but it was changed to a type synonym
-- @since @base-4.15.0.0@.
type Nat = Natural
--------------------------------------------------------------------------------
-- | This class gives the integer associated with a type-level natural.
......
# Changelog for [`base` package](http://hackage.haskell.org/package/base)
## 4.16.0.0 *TBA*
* Make it possible to promote `Natural`s and remove the separate `Nat` kind.
For backwards compatibility, `Nat` is now a type synonym for `Natural`.
As a consequence, one must enable `TypeSynonymInstances`
in order to define instances for `Nat`. Also, different instances for `Nat` and `Natural`
won't typecheck anymore.
## 4.15.0.0 *TBA*
* `openFile` now calls the `open` system call with an `interruptible` FFI
......@@ -35,7 +43,7 @@
* `catMaybes` is now implemented using `mapMaybe`, so that it is both a "good
consumer" and "good producer" for list-fusion (#18574)
## 4.14.0.0 *TBA*
* Bundled with GHC 8.10.1
......
......@@ -30,7 +30,7 @@ module GHC.Types (
Ordering(..), IO(..),
isTrue#,
SPEC(..),
Nat, Symbol,
Symbol,
Any,
type (~~), Coercible,
TYPE, RuntimeRep(..), Type, Constraint,
......@@ -98,13 +98,10 @@ type family MultMul (a :: Multiplicity) (b :: Multiplicity) :: Multiplicity wher
{- *********************************************************************
* *
Nat and Symbol
Symbol
* *
********************************************************************* -}
-- | (Kind) This is the kind of type-level natural numbers.
data Nat
-- | (Kind) This is the kind of type-level symbols.
-- Declared here because class IP needs it
data Symbol
......
......@@ -39,47 +39,53 @@ GHC.TypeLits.symbolVal ::
GHC.TypeLits.KnownSymbol n => proxy n -> String
GHC.TypeLits.symbolVal' ::
GHC.TypeLits.KnownSymbol n => GHC.Prim.Proxy# n -> String
type (GHC.TypeNats.*) :: GHC.Types.Nat
-> GHC.Types.Nat -> GHC.Types.Nat
type (GHC.TypeNats.*) :: GHC.Num.Natural.Natural
-> GHC.Num.Natural.Natural -> GHC.Num.Natural.Natural
type family (GHC.TypeNats.*) a b
type (GHC.TypeNats.+) :: GHC.Types.Nat
-> GHC.Types.Nat -> GHC.Types.Nat
type (GHC.TypeNats.+) :: GHC.Num.Natural.Natural
-> GHC.Num.Natural.Natural -> GHC.Num.Natural.Natural
type family (GHC.TypeNats.+) a b
type (GHC.TypeNats.-) :: GHC.Types.Nat
-> GHC.Types.Nat -> GHC.Types.Nat
type (GHC.TypeNats.-) :: GHC.Num.Natural.Natural
-> GHC.Num.Natural.Natural -> GHC.Num.Natural.Natural
type family (GHC.TypeNats.-) a b
type (GHC.TypeNats.<=) :: GHC.Types.Nat
-> GHC.Types.Nat -> Constraint
type (GHC.TypeNats.<=) :: GHC.Num.Natural.Natural
-> GHC.Num.Natural.Natural -> Constraint
type (GHC.TypeNats.<=) x y =
(x GHC.TypeNats.<=? y) ~ 'True :: Constraint
type (GHC.TypeNats.<=?) :: GHC.Types.Nat -> GHC.Types.Nat -> Bool
type (GHC.TypeNats.<=?) :: GHC.Num.Natural.Natural
-> GHC.Num.Natural.Natural -> Bool
type family (GHC.TypeNats.<=?) a b
type GHC.TypeNats.CmpNat :: GHC.Types.Nat
-> GHC.Types.Nat -> Ordering
type GHC.TypeNats.CmpNat :: GHC.Num.Natural.Natural
-> GHC.Num.Natural.Natural -> Ordering
type family GHC.TypeNats.CmpNat a b
type GHC.TypeNats.Div :: GHC.Types.Nat
-> GHC.Types.Nat -> GHC.Types.Nat
type GHC.TypeNats.Div :: GHC.Num.Natural.Natural
-> GHC.Num.Natural.Natural -> GHC.Num.Natural.Natural
type family GHC.TypeNats.Div a b
type GHC.TypeNats.KnownNat :: GHC.Types.Nat -> Constraint
type GHC.TypeNats.KnownNat :: GHC.TypeNats.Nat -> Constraint
class GHC.TypeNats.KnownNat n where
GHC.TypeNats.natSing :: GHC.TypeNats.SNat n
{-# MINIMAL natSing #-}
type GHC.TypeNats.Log2 :: GHC.Types.Nat -> GHC.Types.Nat
type GHC.TypeNats.Log2 :: GHC.Num.Natural.Natural
-> GHC.Num.Natural.Natural
type family GHC.TypeNats.Log2 a
type GHC.TypeNats.Mod :: GHC.Types.Nat
-> GHC.Types.Nat -> GHC.Types.Nat
type GHC.TypeNats.Mod :: GHC.Num.Natural.Natural
-> GHC.Num.Natural.Natural -> GHC.Num.Natural.Natural
type family GHC.TypeNats.Mod a b
type GHC.Types.Nat :: *
data GHC.Types.Nat
type GHC.TypeNats.Nat :: *
type GHC.TypeNats.Nat = GHC.Num.Natural.Natural
type GHC.Num.Natural.Natural :: *
data GHC.Num.Natural.Natural
= GHC.Num.Natural.NS GHC.Prim.Word#
| GHC.Num.Natural.NB GHC.Prim.ByteArray#
type GHC.TypeNats.SomeNat :: *
data GHC.TypeNats.SomeNat
= forall (n :: GHC.Types.Nat).
= forall (n :: GHC.TypeNats.Nat).
GHC.TypeNats.KnownNat n =>
GHC.TypeNats.SomeNat (Data.Proxy.Proxy n)
type GHC.Types.Symbol :: *
data GHC.Types.Symbol
type (GHC.TypeNats.^) :: GHC.Types.Nat
-> GHC.Types.Nat -> GHC.Types.Nat
type (GHC.TypeNats.^) :: GHC.Num.Natural.Natural
-> GHC.Num.Natural.Natural -> GHC.Num.Natural.Natural
type family (GHC.TypeNats.^) a b
GHC.TypeNats.sameNat ::
(GHC.TypeNats.KnownNat a, GHC.TypeNats.KnownNat b) =>
......
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds, PolyKinds #-}
{-# LANGUAGE TypeSynonymInstances #-}
module T13398b where
import GHC.TypeLits
......
......@@ -4,7 +4,7 @@ T15322a.hs:12:7: error:
arising from a use of ‘typeRep’
from the context: KnownNat n
bound by the type signature for:
f :: forall (n :: GHC.Types.Nat).
f :: forall (n :: GHC.TypeNats.Nat).
KnownNat n =>
Proxy n -> TypeRep (n + 1)
at T15322a.hs:11:1-56
......
......@@ -5,7 +5,7 @@ T15360b.hs:10:13: error:
In the type signature: x :: Proxy (Type Double)
T15360b.hs:13:13: error:
• Expected kind ‘* -> k2’, but ‘1’ has kind ‘GHC.Types.Nat
• Expected kind ‘* -> k2’, but ‘1’ has kind ‘GHC.Num.Natural.Natural
• In the first argument of ‘Proxy’, namely ‘(1 Int)’
In the type signature: y :: Proxy (1 Int)
......
{-# LANGUAGE TypeFamilies, DataKinds, KindSignatures, TypeOperators #-}
module T10776 where
import GHC.TypeLits (Nat, Natural, Symbol, KnownNat)
import Data.Type.Equality ((:~:)(..))
import Data.Proxy
nat_is_natural :: Nat :~: Natural
nat_is_natural = Refl
data NatPair = TN Natural Natural
type X = TN 1 101
type family SecondNat (a :: NatPair) :: Nat where
SecondNat ('TN _ a) = a
T15799.hs:46:62: error:
Couldn't match kind ‘TypeLits.Natural’ with ‘Op Nat’
• Expected kind ‘Op Nat’, but ‘UnOp b’ has kind ‘Nat’
• In the first argument of ‘(<=)’, namely ‘UnOp b’
UnliftedNewtypesFamilyKindFail1.hs:11:31: error:
• Expected a type, but ‘5’ has kind ‘GHC.Types.Nat
• Expected a type, but ‘5’ has kind ‘GHC.Num.Natural.Natural
• In the kind ‘5’
In the data family declaration for ‘DF’
UnliftedNewtypesFamilyKindFail2.hs:12:20:
Expected a type, but ‘5’ has kind ‘GHC.Types.Nat
Expected a type, but ‘5’ has kind ‘GHC.Num.Natural.Natural
In the first argument of ‘F’, namely ‘5’
In the newtype instance declaration for ‘F’
UnliftedNewtypesFamilyKindFail2.hs:12:31:
Expected a type, but ‘5’ has kind ‘GHC.Types.Nat
Expected a type, but ‘5’ has kind ‘GHC.Num.Natural.Natural
In the first argument of ‘F’, namely ‘5’
In the type ‘(F 5)’
In the definition of data constructor ‘MkF’
......
......@@ -12,4 +12,4 @@ good: *
good: Int -> Int
good: 5
good: "hello world"
good: 'Just Nat 5
good: 'Just Natural 5
......@@ -12,13 +12,13 @@ Int -> Int
Proxy Constraint (Eq Int)
Proxy * (Int,Int)
Proxy Symbol "hello world"
Proxy Nat 1
Proxy [Nat] (': Nat 1 (': Nat 2 (': Nat 3 ('[] Nat))))
Proxy Natural 1
Proxy [Natural] (': Natural 1 (': Natural 2 (': Natural 3 ('[] Natural))))
Proxy Ordering 'EQ
Proxy (RuntimeRep -> *) TYPE
Proxy * *
Proxy * *
Proxy * *
Proxy RuntimeRep 'LiftedRep
Proxy (Nat,Symbol) ('(,) Nat Symbol 1 "hello")
Proxy (Natural,Symbol) ('(,) Natural Symbol 1 "hello")
Proxy (* -> * -> Constraint) ((~~) * *)
......@@ -17,8 +17,8 @@ Int#
Proxy Constraint (Eq Int)
Proxy * (Int,Int)
Proxy Symbol "hello world"
Proxy Nat 1
Proxy [Nat] (': Nat 1 (': Nat 2 (': Nat 3 ('[] Nat))))
Proxy Natural 1
Proxy [Natural] (': Natural 1 (': Natural 2 (': Natural 3 ('[] Natural))))
Proxy Ordering 'EQ
Proxy (RuntimeRep -> *) TYPE
Proxy * *
......
Subproject commit 6f16399e0320d0ef5e6c3dd0329ce7ed3715b6b2
Subproject commit f7d9e0bb987ca31c3b15cbe63198dafbeee3a395
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment