[GHC] #10836: Better error reporting for closed type families

3 Sep 2015

      #10836: Better error reporting for closed type families
-------------------------------------+-------------------------------------
              Reporter:  jstolarek   |             Owner:
                  Type:  bug         |            Status:  new
              Priority:  normal      |         Milestone:
             Component:  Compiler    |           Version:  7.11
              Keywords:              |  Operating System:  Unknown/Multiple
          Architecture:              |   Type of failure:  Incorrect
  Unknown/Multiple                   |  warning at compile-time
             Test Case:              |        Blocked By:
              Blocking:              |   Related Tickets:
Differential Revisions:              |
-------------------------------------+-------------------------------------
 Consider this code:

 {{{#!hs
 {-# 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:

 {{{#!hs
 {-# 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`:

 {{{#!hs
        ; 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."

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10836
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler