Type-level reasoning ability lost for TypeLits?

[Gabor Greif]

Hi devs,

with recent iterations of GHC.TypeLits (HEAD) I am struggling to get
something simple working. I have

> data Number nat = KnownNat nat => Number !(Proxy nat)

and want to write

> addNumbers :: Number a -> Number b -> Maybe (Number (a + b))

Unfortunately I cannot find a way to create the necessary KnownNat (a
+ b) constraint.

Declaring the function thus

> addNumbers :: KnownNat (a + b) => Number a -> Number b -> Maybe (Number (a + b))

only dodges the problem around.

Also I am wondering where the ability to perform a type equality check
went. I.e. I cannot find the relevant functionality to obtain

> sameNumber :: Number a -> Number b -> Maybe (a :~: b)

I guess there should be some TestEquality instance (for Proxy Nat?, is
this possible at all), but I cannot find it. Same applies for Symbols.

Any hints?

Thanks and cheers,

    Gabor