Better error reporting for closed type families

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 (closed). Commit message for d0ddde58 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."

Trac metadata

Trac field	Value
Version	7.11
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture