type signature involving a type family rejected

[baramoglo]

add1 is rejected in the following program:

{-# LANGUAGE EmptyDataDecls, FlexibleContexts, FlexibleInstances, GADTs, TypeFamilies, TypeOperators, UndecidableInstances #-}

data False

type family IsNegative x

type family x :+: y

class Natural x
instance (IsNegative x ~ False) => Natural x

data A n
  where
    A :: Natural n => Int -> A n

getA :: A n -> Int
getA (A n) = n

add1 :: Natural (m:+:n) => A m -> A n -> A (m:+:n)
add1 (A a) (A b) = A (a+b)

add2 (A a) (A b) = A (a+b)

add3 :: (IsNegative (m:+:n) ~ False) => A m -> A n -> A (m:+:n)
add3 (A a) (A b) = A (a+b)

add4 :: Natural (m:+:n) => A m -> A n -> A (m:+:n)
add4 a b = A (getA a + getA b)

add5 :: Natural (m:+:n) => A m -> A n -> A (m:+:n)
add5 (A a) _ = A a

The following modifications of add1 work fine:

• Removing the type signature (add2)
• Using the type inferred for add2 (add3)
• Using the projection function getA instead of pattern matching (add4)
• Only pattern match on the first argument

[simonpj]

The problem is your instance for Natural x. You are saying "If you want to prove Natural x, then please prove (IsNegative x ~ False)". Now in the RHS of add1, GHC is faced with thee following problem:

 From   (Natural (m:+:n),     -- From signature
         Natural n,           -- From first pattern match
         Natural m)           -- From second pattern match
please prove
         Natural (m:+:n)

That seems easy enough, since the thing to prove is one of the premises. But a possible reasoning step is to use the instance declaration first, leading to

please prove
         IsNegative (m:+:n) ~ False

which we obviously can't do. Your instance declaration promises an alternative way to prove a constraint (Natural ty), but one which turns out to be a blind alley. But GHC does not search for a proof; it follows just one path. (In general the search could be very complicated.)

Nevertheless, I think there is a bug here: GHC should really not use an instance declaration if there is any possibility that one of the local premises might match, rather in the same way that it refrains from committing to one instance if more than one matches. Thanks for pointing this out.

Simon

[simonpj]

Hmm. Since there is only one instance for Natural GHC is right to use the (only) instance declaration. So I think there is no bug here and I'm therefore closing it.

Simon