Re: [Haskell-cafe] Injective type families for GHC - syntax proposals

2014-09-18 21:38 GMT+04:00, Brent Yorgey :

On Thu, Sep 18, 2014 at 11:02 AM, flicky frans wrote:

...

Plus a b :: (result :: Nat)

That looks quite unintuitive to me, since `result' reads like a variable of type Nat.

But isn't that exactly what it is supposed to be?

At least (Plus a b :: Nat) /= (Plus a b :: (result :: Nat)), since a variable of type Nat is not the type of Plus a b. In (a :: (b :: c)) `a' is a variable, `b' is a type, `c' is a kind (in System F, of course) But yes, I made a mistake, `result' should be a variable. Maybe this? type family Plus a b = r :: * | r a -> b, r b -> a where