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

[flicky frans]

   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