Opened 2 years ago

Closed 2 years ago

Last modified 23 months ago

#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 2 years ago by jstolarek

Test Case: T10836

I added a test case (expected to fail).

comment:2 Changed 2 years ago by Simon Peyton Jones <simonpj@…>

In a870738/ghc:

Improve rejigConRes (again)

I think this patch finally works around the delicacy in the strictness
of TcTyClsDecls.rejigConRes.   See the notes with that function and
Note [Checking GADT return types].

As a result, we fix Trac #10836, and improve Trac #7175

comment:3 Changed 2 years ago by simonpj

Resolution: fixed
Status: newclosed
Test Case: T10836typecheck/should_fail/T10836

comment:4 Changed 2 years ago by jstolarek

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:5 Changed 2 years ago by Jan Stolarek <jan.stolarek@…>

In f30a4925/ghc:

Testsuite cleanup

As a result of fixing #10836 it is now possible to merge 11 different
tests for #6018 into one

comment:6 in reply to:  4 Changed 2 years ago by goldfire

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 23 months ago by thomie

Milestone: 8.0.1
Note: See TracTickets for help on using tickets.