On Fri, 19 Sep 2014 00:17:49 +0400, flicky frans <flickyfrans at gmail.com> wrote: > Sorry. > > type family Plus a b = r :: Nat | r a -> b, r b -> a where +1 Simple, intuitive and backwards compatible. I don't have to introduce a variable if I don't want to, either.