Opened 10 years ago

Closed 9 years ago

## #3584 closed bug (invalid)

# type signature involving a type family rejected

Reported by: | baramoglo | Owned by: | |
---|---|---|---|

Priority: | normal | Milestone: | 7.0.1 |

Component: | Compiler (Type checker) | Version: | 6.10.2 |

Keywords: | Cc: | 78emil@… | |

Operating System: | Unknown/Multiple | Architecture: | x86 |

Type of failure: | None/Unknown | Test Case: | |

Blocked By: | Blocking: | ||

Related Tickets: | Differential Rev(s): | ||

Wiki Page: |

### Description

`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

### Change History (3)

### comment:1 Changed 10 years ago by

difficulty: | → Unknown |
---|

### comment:2 Changed 10 years ago by

Milestone: | → 6.14.1 |
---|

### comment:3 Changed 9 years ago by

Resolution: | → invalid |
---|---|

Status: | new → closed |

Type of failure: | → None/Unknown |

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

**Note:**See TracTickets for help on using tickets.

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: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

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 notsearchfor 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

notuse 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