[Haskell-cafe] Why do I need UndecidableInstances?

[adam vogt]

On Thu, Oct 24, 2013 at 9:08 AM, Stijn van Drongelen <rhymoid at gmail.com> wrote:
> 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