id,summary,reporter,owner,description,type,status,priority,milestone,component,version,resolution,keywords,cc,os,architecture,failure,difficulty,testcase,blockedby,blocking,related
3584,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",bug,closed,normal,7.0.1,Compiler (Type checker),6.10.2,invalid,,78emil@…,Unknown/Multiple,x86,None/Unknown,Unknown,,,,