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