type signature involving a type family rejected

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

Trac metadata

Trac field	Value
Version	6.10.2
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC	78emil@gmail.com
Operating system
Architecture