On Thu, Oct 24, 2013 at 9:08 AM, Stijn van Drongelen
I'm not familiar enough (yet) with the reasons behind this rule to explain why it's there (if anyone can explain this in detail, please do!), but this should be a direct answer to your question: it's against the rules.
Hello, Perhaps those rules are unnecessarily restrictive? Maybe the check could be changed to something like "at least one of the types is shrinking if all the other are not growing", rather than the current rule that seems to be "all types must be smaller in the recursive call". The equivalent code using type families doesn't need undecidable instances in my ghc-7.6.2. {-# LANGUAGE DataKinds #-} {-# LANGUAGE TypeFamilies #-} data Nat = Zero | Succ Nat type family Plus (a :: Nat) (b :: Nat) :: Nat type instance Plus Zero x = x type instance Plus (Succ x) y = Succ (Plus x y) type family Max (x :: Nat) (y :: Nat) :: Nat type instance Max Zero y = y type instance Max (Succ x) Zero = Succ x type instance Max (Succ a) (Succ b) = Succ (Max a b) Also using normal data types instead of the datakinds doesn't make a difference. Regards, Adam