Add support for type-level integers

Similar to GHC.TypeNats, it would be nice to see something like the following:

newtype TypeInt (n :: Nat) = TypeInt Integer

class KnownInt (n :: k) where
  intSing :: TypeInt n

intVal :: forall n proxy. KnownInt n => proxy n -> Integer
intVal _ = case intSing :: TypeInt n of
  TypeInt x -> x

intVal' :: forall n. KnownInt n => Proxy# n -> Integer
intVal' _ = case intSing :: TypeInt n of
  TypeInt x -> x

Trac metadata

Trac field	Value
Version	8.4.3
Type	FeatureRequest
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

changed milestone to %8.6.1

changed weight to 5

added Tfeature request Trac import labels

We already have type-level Nat. Then you can emulate Integer by pairing a Nat with type-level Bool to hold the sign.

Do you have a stronger use case than "it would be nice to see"?

Ryan's comment to your previous request ticket:14922#comment:150377 applies here as well.

changed milestone to %8.8.1

These won't be addressed in GHC 8.6.

mentioned in issue #15488 (closed)

changed milestone to %8.10.1

Bumping milestones of low-priority tickets.

added core libraries label

added Pnormal label

removed milestone