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

Plus a b :: (result :: Nat) That looks quite unintuitive to me, since `result' reads like a variable of type Nat. This is similar to legal (with KindSignatures) (5 :: (Int :: *)). Maybe it would be better to use something like associated type synonyms? type family (r ~ *) => Id a :: r | r -> a where type family (res ~ *) => G a b c :: r | res -> a b where type family (result ~ Nat) => Plus a b :: result | result a -> b, result b -> a where