Opened 10 months ago

Last modified 10 months ago

#15868 new feature request

Standard deriving should be less conservative when `UndecidableInstances` is enabled

Reported by: edsko Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.6.1
Keywords: deriving Cc: kosmikus, adamgundry
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: #11008 Differential Rev(s):
Wiki Page:

Description

The following program

{-# LANGUAGE FlexibleContexts     #-}
{-# LANGUAGE FlexibleInstances    #-}
{-# LANGUAGE StandaloneDeriving   #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE UndecidableInstances #-}

module Exp where

type family F a

data T a = MkT (F a)

deriving instance Eq (F a) => Eq (T a)

data T2 a = T2 (T a)
  deriving (Eq)

results in a type error

    • No instance for (Eq (F a))
        arising from the first field of ‘T2’ (type ‘T a’)

According the manual this is expected behaviour (https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#inferred-context-for-deriving-clauses), but it is unfortunate; it seems to me that there is no deep reason that this instance should be rejected, other than an overly conservative check in the deriving machinery; I propose that this check is relaxed when the UndecidableInstances extension is enabled. Mind that I'm not proposing that it should also be able to infer the right constraints for T itself; but once I write such an explicit context myself once (for T), it seems to me that deriving the same constraints also for T2 should be easy.

Note that right now we can work-around this problem using

class Eq (F a) => EqF a

deriving instance EqF a => Eq (T a)

data T2 a = T2 (T a)
  deriving (Eq)

Normally however for such a class synonym we would then provide a single "authoritative" instance:

class Eq (F a) => EqF a
instance Eq (F a) => EqF a

but if we do that then we are back at the same error for T2, because ghc will go from the EqF a constraint to the Eq (F a) constraint, and then refuse to add that constraint.

Change History (6)

comment:1 Changed 10 months ago by kosmikus

Cc: kosmikus added

comment:2 Changed 10 months ago by adamgundry

Cc: adamgundry added

comment:3 Changed 10 months ago by RyanGlScott

Keywords: deriving added

I have mixed feelings on this. I'm reluctant to turn off this validity check entirely when UndecidableInstances is enabled since there are several situations where this can catch you when you're writing utterly bogus programs, such as this one:

data NotAShowInstance
data Foo = MkFoo Int NotAShowInstance deriving Show
Bug.hs:2:48: error:
    • No instance for (Show NotAShowInstance)
        arising from the second field of ‘MkFoo’ (type ‘NotAShowInstance’)
      Possible fix:
        use a standalone 'deriving instance' declaration,
          so you can specify the instance context yourself
    • When deriving the instance for (Show Foo)
  |
2 | data Foo = MkFoo Int NotAShowInstance deriving Show
  |                                                ^^^^

This is a relatively common mistake to make, and it's one that's caught by this validity check. If this check were relaxed, then GHC would generate this instance:

instance Show NotAShowInstance => Show Foo where ...

Which is almost surely not what you'd want.

At the same time, I can certainly understand wanting to relax this restriction when type families or fancy types (e.g., Show (f a b (g a b) (h a b))) get involved. Perhaps there's a way to write up a specification that permits T2 in your example but rejects Foo in my example. I'm not sure what such a specification would be yet, however.

comment:4 Changed 10 months ago by RyanGlScott

#11008 is a similar ticket.

comment:5 Changed 10 months ago by edsko

Would simply refusing to add constraints without any type variables be sufficient to rule out examples like the one you are worried about?

comment:6 in reply to:  5 Changed 10 months ago by RyanGlScott

Replying to edsko:

Would simply refusing to add constraints without any type variables be sufficient to rule out examples like the one you are worried about?

Not necessarily. Imagine if NotAShowInstance had a type parameter, for instance. Under your proposed scheme, we'd still allow data Foo a = MkFoo Int (NotAShowInstance a) deriving Show.

I think the right way to frame the discussion is to permit constraints that involve non–type constructors (such as type families or higher-kinded type variables) in certain ways. That's still not anything resembling a specification, but it's closer.

Note: See TracTickets for help on using tickets.