#3584: type signature involving a type family rejected
-----------------------------+----------------------------------------------
Reporter: baramoglo | Owner:
Type: bug | Status: new
Priority: normal | Component: Compiler (Type checker)
Version: 6.10.2 | Severity: normal
Keywords: | Testcase:
Os: Unknown/Multiple | Architecture: x86
-----------------------------+----------------------------------------------
`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
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/3584>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
