Opened 2 years ago

Closed 16 months ago

Last modified 10 months ago

#14179 closed bug (fixed)

"Conflicting family instance" error pretty prints data family instances poorly

Reported by: RyanGlScott Owned by:
Priority: normal Milestone: 8.6.1
Component: Compiler (Type checker) Version: 8.2.1
Keywords: TypeFamilies Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Poor/confusing error message Test Case: indexed-types/should_fail/T14179
Blocked By: Blocking:
Related Tickets: Differential Rev(s): Phab:D4711
Wiki Page:

Description

This can be observed on GHC 8.0.1 or later:

{-# LANGUAGE TypeFamilies #-}
module Bug where

data family   Fam a
data instance Fam Int
data instance Fam Int
$ /opt/ghc/8.2.1/bin/ghci Bug.hs
GHCi, version 8.2.1: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )

Bug.hs:5:15: error:
    Conflicting family instance declarations:
      Fam Int = -- Defined at Bug.hs:5:15
      Fam Int = -- Defined at Bug.hs:6:15
  |
5 | data instance Fam Int
  |               ^^^

Notice how GHC attempts to pretty-print the RHS by using a = symbol, but there is no RHS!

This gets even more confusing with this program, which requires GHC HEAD:

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where

data family   Fam :: k -> *
data instance Fam :: * -> *
data instance Fam :: * -> *
$ ghc5/inplace/bin/ghc-stage2 --interactive Bug.hs
GHCi, version 8.3.20170818: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )

Bug.hs:6:15: error:
    Conflicting family instance declarations:
      Fam = -- Defined at Bug.hs:6:15
      Fam = -- Defined at Bug.hs:7:15
  |
6 | data instance Fam :: * -> *
  |               ^^^

Not only is there no RHS, but the kind signatures of each instance aren't printed either. This is an issue, since the entire reason why the two instances conflict are because of their kinds!

We should rethink how data family instances are pretty printer here to avoid this issue.

Change History (7)

comment:1 Changed 2 years ago by RyanGlScott

Indeed, the particular pretty printer that's being used in this error message is really broken. If you give GHC these conflicting instances:

module Bug where

data family   Fam a
data instance Fam [a] where
  Fam1 :: Fam [Int]
  Fam2 :: Fam [Bool]
data instance Fam [a] where
  Fam3 :: Fam [a]
  Fam4 :: Fam [Char]

Then the error message will print out information that's just plain wrong:

$ ghci Bug.hs
GHCi, version 8.2.1: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )

Bug.hs:6:15: error:
    Conflicting family instance declarations:
      Fam [a] = Fam1 | Fam2 -- Defined at Bug.hs:6:15
      Fam [a] = Fam3 | Fam4 -- Defined at Bug.hs:9:15
  |
6 | data instance Fam [a] where
  |               ^^^

I use the word "particular" above since the general-purpose data family instance pretty printer actually does the right thing:

λ> :i Fam
data family Fam a       -- Defined at Bug.hs:5:1
data instance Fam [a] where
  Fam3 :: Fam [a]
  Fam4 :: Fam [Char]
        -- Defined at Bug.hs:11:15

comment:2 Changed 16 months ago by RyanGlScott

This is an interesting one. I think that the solution here might be to pretty-print conflicting type family instances slightly differently than conflicting data family instances, for two reasons:

  1. Type family instances are unique in that you have can have duplicate instances (see #14440). Thus, the pretty-printer must show their right-hand sides, because otherwise a user wouldn't know why they were conflicting.

Data family instances, on the other hand, do not permit duplicates. These conflict, for instance:

data family Foo a
data instance Foo a
data instance Foo a
  1. The right-hand side of a data family instance can be quite large if there are many constructors. We could address this with pprDeeperList, but it's of questionable utility, since
    1. We might be suppressing the constructors in which two data family instance differ, and
    2. Part 1. brings into question whether it's worth going through this trouble in the first place, since the constructors themselves aren't the thing which causes data family instances to conflict.

In light of this, I would propose simply pretty-printing the data family instances without any constructors at all. In other words, for the programs in the original description, I would propose having these be the respective error messages:

Bug.hs:5:15: error:
    Conflicting family instance declarations:
      Fam Int -- Defined at Bug.hs:5:15
      Fam Int -- Defined at Bug.hs:6:15
  |
5 | data instance Fam Int
  |               ^^^
Bug.hs:6:15: error:
    Conflicting family instance declarations:
      Fam :: * -> * -- Defined at Bug.hs:6:15
      Fam :: * -> * -- Defined at Bug.hs:7:15
  |
6 | data instance Fam :: * -> *
  |               ^^^

And for the program in comment:1:

Bug.hs:6:15: error:
    Conflicting family instance declarations:
      Fam [a] -- Defined at Bug.hs:6:15
      Fam [a] -- Defined at Bug.hs:9:15
  |
6 | data instance Fam [a] where
  |               ^^^
Last edited 16 months ago by RyanGlScott (previous) (diff)

comment:3 Changed 16 months ago by simonpj

comment:2 sounds plausible to me.

PS: The first sentence of comment:2 doesn't make sense though: "pretty-print conflicting data family instances slightly differently than conflicting data family instances". Maybe needs an edit.

Last edited 16 months ago by simonpj (previous) (diff)

comment:4 in reply to:  3 Changed 16 months ago by RyanGlScott

Differential Rev(s): Phab:D4711
Status: newpatch

Replying to simonpj:

PS: The first sentence of comment:2 doesn't make sense though: "pretty-print conflicting data family instances slightly differently than conflicting data family instances". Maybe needs an edit.

Good catch. Fixed.

Alas, I wasn't able to do much about the kind signature thing, since by the time we call this error message, we've completely lost track of whether the original data family instance declaration was written with an explicit kind signature or not. Nevertheless, I've implemented the other suggestions in this thread in Phab:D4711, which substantially cleans up the error message (and will at the very least give results that make sense in some context).

comment:5 Changed 16 months ago by Ryan Scott <ryan.gl.scott@…>

In 979f085c/ghc:

Clean up the conflicting data family instances error message

Summary:
The way we were pretty-printing conflicting data family
instances in an error message was far from ideal:

1. If a data type had no constructors, it would print an equals sign
   with nothing to the right of it.
2. It would try to print GADTs using Haskell98 syntax.
3. It eta-reduced away some type variables from the LHS.

This patch addresses these three issues:

1. We no longer print constructors at all in this error message.
   There's really no reason to do so in the first place, since
   duplicate data family instances always conflict, regardless of
   their constructors.
2. Since we no longer print constructors, we no longer have to
   worry about whether we're using GADT or Haskell98 syntax.
3. I've put in a fix to ensure that type variables are no longer
   eta-reduced away from the LHS.

Test Plan: make test TEST=T14179

Reviewers: goldfire, bgamari

Reviewed By: bgamari

Subscribers: rwbarton, thomie, carter

GHC Trac Issues: #14179

Differential Revision: https://phabricator.haskell.org/D4711

comment:6 Changed 16 months ago by RyanGlScott

Milestone: 8.6.1
Resolution: fixed
Status: patchclosed
Test Case: indexed-types/should_fail/T14179

comment:7 Changed 10 months ago by Ryan Scott <ryan.gl.scott@…>

In 63a81707/ghc:

Fix #15845 by defining etaExpandFamInstLHS and using it

Summary:
Both #9692 and #14179 were caused by GHC being careless
about using eta-reduced data family instance axioms. Each of those
tickets were fixed by manually whipping up some code to eta-expand
the axioms. The same sort of issue has now caused #15845, so I
figured it was high time to factor out the code that each of these
fixes have in common.

This patch introduces the `etaExpandFamInstLHS` function, which takes
a family instance's type variables, LHS types, and RHS type, and
returns type variables and LHS types that have been eta-expanded if
necessary, in the case of a data family instance. (If it's a type
family instance, `etaExpandFamInstLHS` just returns the supplied type
variables and LHS types unchanged).

Along the way, I noticed that many references to
`Note [Eta reduction for data families]` (in `FamInstEnv`) had
slightly bitrotted (they either referred to a somewhat different
name, or claimed that the Note lived in a different module), so
I took the liberty of cleaning those up.

Test Plan: make test TEST="T9692 T15845"

Reviewers: goldfire, bgamari

Reviewed By: goldfire

Subscribers: rwbarton, carter

GHC Trac Issues: #15845

Differential Revision: https://phabricator.haskell.org/D5294
Note: See TracTickets for help on using tickets.