Hi Gabor,

On Fri, Jan 3, 2014 at 9:33 AM, Gabor Greif <ggreif@gmail.com> wrote:

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.

Indeed, there is no way to construct `KnownNumber (a + b)` from `(Known a, Known b)`. This is not something that we lost, it was just never implemented. We could make something like it work, I think, but it'd make things a bit more complex: the representation of `KnownNumber` dictionaries would have to be expressions, rather than a simple constant.

I'd be inclined to leave this as is for now---let's see what we can do with the current system, before we add more functionality.

Declaring the function thus

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

only dodges the problem around.

Dodging problems is good! :-) I don't fully understand from the type what the function is supposed to do, but I'd write something like this:

addNumbers :: (KnownNat a, KnownNat b)

=> (Integer -> Integer -> Bool) -- ^ Some constraint?

Proxy a -> Proxy b -> Maybe (Proxy (a + b))

addNumber p x y =

do guard (p (natVal x) (natVal y))

return Proxy

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.

Ah yes, I thought that this was supposed to be added to some other library, but I guess that never happened. It was implemented like this, if you need it right now.

sameNumber :: (KnownNat a, KnownNat b)

=> Proxy a -> Proxy b -> Maybe (a :~: b)

sameNumber x y

| natVal x == natVal y = Just (unsafeCoerce Refl)

| otherwise = Nothing

This doesn't fit the pattern for the `TestEquality` class (due to the constraints on the parameters), so perhaps I'll add it back to GHC.TypeLits.

-Iavor