Commit 35ca1352 authored by Ryan Scott's avatar Ryan Scott Committed by Ben Gamari

Reexport CmpNat and friends (defined in GHC.TypeNats) from GHC.TypeLits

Previously, there were identical copies of `CmpNat`, `(<=?)`, `(+)`,
etc. spread across `GHC.TypeLits` and `GHC.TypeNats`. This makes
`GHC.TypeNats` the canonical home for them, and reexports them from
`GHC.TypeLits` to avoid confusion.

Test Plan: ./validate

Reviewers: bgamari, austin, hvr

Reviewed By: bgamari

Subscribers: thomie, phadej

Differential Revision: https://phabricator.haskell.org/D3272
parent 2e438482
......@@ -27,6 +27,7 @@ import Name ( Name, BuiltInSyntax(..) )
import TysWiredIn
import TysPrim ( mkTemplateAnonTyConBinders )
import PrelNames ( gHC_TYPELITS
, gHC_TYPENATS
, typeNatAddTyFamNameKey
, typeNatMulTyFamNameKey
, typeNatExpTyFamNameKey
......@@ -67,7 +68,7 @@ typeNatAddTyCon = mkTypeNatFunTyCon2 name
, sfInteractInert = interactInertAdd
}
where
name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "+")
name = mkWiredInTyConName UserSyntax gHC_TYPENATS (fsLit "+")
typeNatAddTyFamNameKey typeNatAddTyCon
typeNatSubTyCon :: TyCon
......@@ -78,7 +79,7 @@ typeNatSubTyCon = mkTypeNatFunTyCon2 name
, sfInteractInert = interactInertSub
}
where
name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "-")
name = mkWiredInTyConName UserSyntax gHC_TYPENATS (fsLit "-")
typeNatSubTyFamNameKey typeNatSubTyCon
typeNatMulTyCon :: TyCon
......@@ -89,7 +90,7 @@ typeNatMulTyCon = mkTypeNatFunTyCon2 name
, sfInteractInert = interactInertMul
}
where
name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "*")
name = mkWiredInTyConName UserSyntax gHC_TYPENATS (fsLit "*")
typeNatMulTyFamNameKey typeNatMulTyCon
typeNatExpTyCon :: TyCon
......@@ -100,7 +101,7 @@ typeNatExpTyCon = mkTypeNatFunTyCon2 name
, sfInteractInert = interactInertExp
}
where
name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "^")
name = mkWiredInTyConName UserSyntax gHC_TYPENATS (fsLit "^")
typeNatExpTyFamNameKey typeNatExpTyCon
typeNatLeqTyCon :: TyCon
......@@ -114,7 +115,7 @@ typeNatLeqTyCon =
NotInjective
where
name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "<=?")
name = mkWiredInTyConName UserSyntax gHC_TYPENATS (fsLit "<=?")
typeNatLeqTyFamNameKey typeNatLeqTyCon
ops = BuiltInSynFamily
{ sfMatchFam = matchFamLeq
......@@ -133,7 +134,7 @@ typeNatCmpTyCon =
NotInjective
where
name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "CmpNat")
name = mkWiredInTyConName UserSyntax gHC_TYPENATS (fsLit "CmpNat")
typeNatCmpTyFamNameKey typeNatCmpTyCon
ops = BuiltInSynFamily
{ sfMatchFam = matchFamCmpNat
......
......@@ -34,9 +34,9 @@ module GHC.TypeLits
-- * Functions on type literals
, type (<=), type (<=?), type (+), type (*), type (^), type (-)
, type (N.<=), type (N.<=?), type (N.+), type (N.*), type (N.^), type (N.-)
, AppendSymbol
, CmpNat, CmpSymbol
, N.CmpNat, CmpSymbol
-- * User-defined type errors
, TypeError
......@@ -129,44 +129,11 @@ type instance a == b = EqSymbol a b
--------------------------------------------------------------------------------
infix 4 <=?, <=
infixl 6 +, -
infixl 7 *
infixr 8 ^
-- | Comparison of type-level naturals, as a constraint.
type x <= y = (x <=? y) ~ 'True
-- | Comparison of type-level symbols, as a function.
--
-- @since 4.7.0.0
type family CmpSymbol (m :: Symbol) (n :: Symbol) :: Ordering
-- | Comparison of type-level naturals, as a function.
--
-- @since 4.7.0.0
type family CmpNat (m :: Nat) (n :: Nat) :: Ordering
{- | Comparison of type-level naturals, as a function.
NOTE: The functionality for this function should be subsumed
by 'CmpNat', so this might go away in the future.
Please let us know, if you encounter discrepancies between the two. -}
type family (m :: Nat) <=? (n :: Nat) :: Bool
-- | Addition of type-level naturals.
type family (m :: Nat) + (n :: Nat) :: Nat
-- | Multiplication of type-level naturals.
type family (m :: Nat) * (n :: Nat) :: Nat
-- | Exponentiation of type-level naturals.
type family (m :: Nat) ^ (n :: Nat) :: Nat
-- | Subtraction of type-level naturals.
--
-- @since 4.7.0.0
type family (m :: Nat) - (n :: Nat) :: Nat
-- | Concatenation of type-level symbols.
--
-- @since 4.10.0.0
......
type family (GHC.TypeLits.*) (a :: GHC.Types.Nat)
(b :: GHC.Types.Nat)
:: GHC.Types.Nat
type family (GHC.TypeLits.+) (a :: GHC.Types.Nat)
(b :: GHC.Types.Nat)
:: GHC.Types.Nat
type family (GHC.TypeLits.-) (a :: GHC.Types.Nat)
(b :: GHC.Types.Nat)
:: GHC.Types.Nat
type (GHC.TypeLits.<=) (x :: GHC.Types.Nat) (y :: GHC.Types.Nat) =
(x GHC.TypeLits.<=? y) ~ 'True :: Constraint
type family (GHC.TypeLits.<=?) (a :: GHC.Types.Nat)
(b :: GHC.Types.Nat)
:: Bool
type family GHC.TypeLits.AppendSymbol (a :: GHC.Types.Symbol)
(b :: GHC.Types.Symbol)
:: GHC.Types.Symbol
type family GHC.TypeLits.CmpNat (a :: GHC.Types.Nat)
(b :: GHC.Types.Nat)
:: Ordering
type family GHC.TypeLits.CmpSymbol (a :: GHC.Types.Symbol)
(b :: GHC.Types.Symbol)
:: Ordering
......@@ -36,9 +19,6 @@ data GHC.TypeLits.SomeSymbol where
(Data.Proxy.Proxy n) -> GHC.TypeLits.SomeSymbol
type family GHC.TypeLits.TypeError (a :: GHC.TypeLits.ErrorMessage)
:: b
type family (GHC.TypeLits.^) (a :: GHC.Types.Nat)
(b :: GHC.Types.Nat)
:: GHC.Types.Nat
GHC.TypeLits.natVal ::
GHC.TypeNats.KnownNat n => proxy n -> Integer
GHC.TypeLits.natVal' ::
......@@ -53,6 +33,23 @@ GHC.TypeLits.symbolVal ::
GHC.TypeLits.KnownSymbol n => proxy n -> String
GHC.TypeLits.symbolVal' ::
GHC.TypeLits.KnownSymbol n => GHC.Prim.Proxy# n -> String
type family (GHC.TypeNats.*) (a :: GHC.Types.Nat)
(b :: GHC.Types.Nat)
:: GHC.Types.Nat
type family (GHC.TypeNats.+) (a :: GHC.Types.Nat)
(b :: GHC.Types.Nat)
:: GHC.Types.Nat
type family (GHC.TypeNats.-) (a :: GHC.Types.Nat)
(b :: GHC.Types.Nat)
:: GHC.Types.Nat
type (GHC.TypeNats.<=) (x :: GHC.Types.Nat) (y :: GHC.Types.Nat) =
(x GHC.TypeNats.<=? y) ~ 'True :: Constraint
type family (GHC.TypeNats.<=?) (a :: GHC.Types.Nat)
(b :: GHC.Types.Nat)
:: Bool
type family GHC.TypeNats.CmpNat (a :: GHC.Types.Nat)
(b :: GHC.Types.Nat)
:: Ordering
class GHC.TypeNats.KnownNat (n :: GHC.Types.Nat) where
GHC.TypeNats.natSing :: GHC.TypeNats.SNat n
{-# MINIMAL natSing #-}
......@@ -61,6 +58,9 @@ data GHC.TypeNats.SomeNat where
GHC.TypeNats.SomeNat :: GHC.TypeNats.KnownNat n =>
(Data.Proxy.Proxy n) -> GHC.TypeNats.SomeNat
data GHC.Types.Symbol
type family (GHC.TypeNats.^) (a :: GHC.Types.Nat)
(b :: GHC.Types.Nat)
:: GHC.Types.Nat
GHC.TypeNats.sameNat ::
(GHC.TypeNats.KnownNat a, GHC.TypeNats.KnownNat b) =>
Data.Proxy.Proxy a
......
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