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 |