[Git][ghc/ghc][master] Unification of Nat and Naturals
Marge Bot
gitlab at gitlab.haskell.org
Wed Oct 14 07:42:23 UTC 2020
Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC
Commits:
8f4f5794 by HaskellMouse at 2020-10-13T13:05:49+03:00
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.
- - - - -
29 changed files:
- compiler/GHC/Builtin/Names.hs
- compiler/GHC/Builtin/Types.hs
- compiler/GHC/Builtin/Types.hs-boot
- compiler/GHC/Builtin/Types/Literals.hs
- compiler/GHC/Core/Type.hs
- compiler/GHC/HsToCore/Binds.hs
- compiler/GHC/Tc/Gen/HsType.hs
- compiler/GHC/Tc/Instance/Class.hs
- docs/users_guide/9.2.1-notes.rst
- docs/users_guide/exts/type_literals.rst
- libraries/base/Data/Typeable/Internal.hs
- libraries/base/GHC/Event/PSQ.hs
- libraries/base/GHC/Generics.hs
- libraries/base/GHC/TypeLits.hs
- libraries/base/GHC/TypeNats.hs
- libraries/base/changelog.md
- libraries/ghc-prim/GHC/Types.hs
- testsuite/tests/ghci/scripts/T9181.stdout
- testsuite/tests/indexed-types/should_compile/T13398b.hs
- testsuite/tests/indexed-types/should_compile/T15322a.stderr
- testsuite/tests/th/T15360b.stderr
- + testsuite/tests/typecheck/should_compile/T10776.hs
- testsuite/tests/typecheck/should_fail/T15799.stderr
- testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail1.stderr
- testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail2.stderr
- testsuite/tests/typecheck/should_run/TestTypeableBinary.stdout
- testsuite/tests/typecheck/should_run/TypeOf.stdout
- testsuite/tests/typecheck/should_run/TypeRep.stdout
- utils/haddock
Changes:
=====================================
compiler/GHC/Builtin/Names.hs
=====================================
@@ -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
=====================================
compiler/GHC/Builtin/Types.hs
=====================================
@@ -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
=====================================
compiler/GHC/Builtin/Types.hs-boot
=====================================
@@ -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
=====================================
compiler/GHC/Builtin/Types/Literals.hs
=====================================
@@ -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
=====================================
compiler/GHC/Core/Type.hs
=====================================
@@ -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
=====================================
compiler/GHC/HsToCore/Binds.hs
=====================================
@@ -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"
=====================================
compiler/GHC/Tc/Gen/HsType.hs
=====================================
@@ -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
=====================================
compiler/GHC/Tc/Instance/Class.hs
=====================================
@@ -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
=====================================
docs/users_guide/9.2.1-notes.rst
=====================================
@@ -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``.
+
=====================================
docs/users_guide/exts/type_literals.rst
=====================================
@@ -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: ::
=====================================
libraries/base/Data/Typeable/Internal.hs
=====================================
@@ -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
=====================================
libraries/base/GHC/Event/PSQ.hs
=====================================
@@ -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(..))
=====================================
libraries/base/GHC/Generics.hs
=====================================
@@ -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
=====================================
libraries/base/GHC/TypeLits.hs
=====================================
@@ -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
--------------------------------------------------------------------------------
=====================================
libraries/base/GHC/TypeNats.hs
=====================================
@@ -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 at .
+
+type Nat = Natural
--------------------------------------------------------------------------------
-- | This class gives the integer associated with a type-level natural.
=====================================
libraries/base/changelog.md
=====================================
@@ -1,5 +1,13 @@
# 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
=====================================
libraries/ghc-prim/GHC/Types.hs
=====================================
@@ -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
=====================================
testsuite/tests/ghci/scripts/T9181.stdout
=====================================
@@ -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) =>
=====================================
testsuite/tests/indexed-types/should_compile/T13398b.hs
=====================================
@@ -1,5 +1,6 @@
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds, PolyKinds #-}
+{-# LANGUAGE TypeSynonymInstances #-}
module T13398b where
import GHC.TypeLits
=====================================
testsuite/tests/indexed-types/should_compile/T15322a.stderr
=====================================
@@ -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
=====================================
testsuite/tests/th/T15360b.stderr
=====================================
@@ -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)
=====================================
testsuite/tests/typecheck/should_compile/T10776.hs
=====================================
@@ -0,0 +1,17 @@
+{-# 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
=====================================
testsuite/tests/typecheck/should_fail/T15799.stderr
=====================================
@@ -1,4 +1,5 @@
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’
=====================================
testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail1.stderr
=====================================
@@ -1,5 +1,5 @@
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’
=====================================
testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail2.stderr
=====================================
@@ -1,10 +1,10 @@
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’
=====================================
testsuite/tests/typecheck/should_run/TestTypeableBinary.stdout
=====================================
@@ -12,4 +12,4 @@ good: *
good: Int -> Int
good: 5
good: "hello world"
-good: 'Just Nat 5
+good: 'Just Natural 5
=====================================
testsuite/tests/typecheck/should_run/TypeOf.stdout
=====================================
@@ -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) ((~~) * *)
=====================================
testsuite/tests/typecheck/should_run/TypeRep.stdout
=====================================
@@ -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 * *
=====================================
utils/haddock
=====================================
@@ -1 +1 @@
-Subproject commit 6f16399e0320d0ef5e6c3dd0329ce7ed3715b6b2
+Subproject commit f7d9e0bb987ca31c3b15cbe63198dafbeee3a395
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/8f4f5794eb3504bf2ca093dc5895742395fdbde9
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/8f4f5794eb3504bf2ca093dc5895742395fdbde9
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20201014/f3df1189/attachment-0001.html>
More information about the ghc-commits
mailing list