## #10836 closed bug (fixed)

# Better error reporting for closed type families

Reported by: | jstolarek | Owned by: | |
---|---|---|---|

Priority: | normal | Milestone: | 8.0.1 |

Component: | Compiler | Version: | 7.11 |

Keywords: | Cc: | ||

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

Type of failure: | Incorrect warning at compile-time | Test Case: | typecheck/should_fail/T10836 |

Blocked By: | Blocking: | ||

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

Wiki Page: |

### Description

Consider this code:

{-# LANGUAGE TypeFamilies #-} module Bug where type family Foo a = r | r -> a type instance Foo Int = Int type instance Foo Bool = Int type family Bar a = r | r -> a type instance Bar Int = Int type instance Bar Bool = Int

Both definitions are incorrect as they violate their injectivity annotation. When I compile the module GHC reports errors on both definitons:

Bug.hs:9:15: error: Type family equations violate injectivity annotation: Foo Bool = Int Foo Int = Int Bug.hs:13:15: error: Type family equations violate injectivity annotation: Bar Bool = Int Bar Int = Int

When I convert these to closed type families:

{-# LANGUAGE TypeFamilies #-} module Bug where type family Foo a = r | r -> a where Foo Int = Int Foo Bool = Int type family Bar a = r | r -> a where Bar Int = Int Bar Bool = Int

GHC only reports error on `Foo`

but not on `Bar`

:

Bug.hs:8:5: error: Type family equations violate injectivity annotation: Foo Int = Int Foo Bool = Int In the equations for closed type family ‘Foo’ In the type family declaration for ‘Foo’

Only when I fix the error on `Foo`

I get the error on `Bar`

. This is mostly annoying. A spectacular example of when this is really a problem can be seen in the testsuite: for open type families all the failing injectivity tests are in one test `T6018fail`

but for closed type families there are twelve separate tests (`T6018closedfail01`

through `T6018closedfail12`

).

I pinned down the problem to these lines in `TcTyClsDecls.tcTyClGroup`

:

; checkNoErrs $ mapM_ (recoverM (return ()) . checkValidTyCl) tyclss -- We recover, which allows us to report multiple validity errors -- the checkNoErrs is necessary to fix #7175.

As stated by the comment, removing `checkNoErrs`

fixes the problem but breaks #7175. Commit message for d0ddde58f928a6b156d8061c406226c4fbb7cd22 suggests that this can't be easily fixed. Richard Eisenberg also remarks: "It's all about the irrefutable pattern in `rejigConRes`

for matching up result types of GADTs."

### Change History (7)

### comment:1 Changed 3 years ago by

Test Case: | → T10836 |
---|

### comment:3 Changed 3 years ago by

Resolution: | → fixed |
---|---|

Status: | new → closed |

Test Case: | T10836 → typecheck/should_fail/T10836 |

### comment:4 follow-up: 6 Changed 3 years ago by

Simon, this change is a huge improvement over the previous situation, but not everything is yet perfect. Consider this:

type family FClosed a b c = (result :: *) | result -> a b c where FClosed Int Char Bool = Bool FClosed Char Bool Int = Int FClosed Bool Int Char = Int type family Bar a = r | r -> a where Bar Int = Bool Bar Bool = Int Bar Bool = Char bar :: Bar a -> Bar a bar x = x barapp :: Char barapp = bar 'c'

I would expect to get two errors:

T6018.hs:8:5: error: Type family equations violate injectivity annotation: FClosed Char Bool Int = Int FClosed Bool Int Char = Int In the equations for closed type family ‘FClosed’ In the type family declaration for ‘FClosed’ T6018.hs:20:14: error: Couldn't match expected type ‘Bar a0’ with actual type ‘Char’ The type variable ‘a0’ is ambiguous In the first argument of ‘bar’, namely ‘'c'’ In the expression: bar 'c' In an equation for ‘barapp’: barapp = bar 'c'

But I only get the first one. Is this expected?

### comment:6 Changed 3 years ago by

Replying to jstolarek:

But I only get the first one. Is this expected?

I think so. GHC gives up if type-checking the type & class definitions fails. Otherwise, who knows what terrible type errors might happen?

### comment:7 Changed 2 years ago by

Milestone: | → 8.0.1 |
---|

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

I added a test case (expected to fail).