[GHC] #15868: Standard deriving should be less conservative when `UndecidableInstances` is enabled

#15868: Standard deriving should be less conservative when `UndecidableInstances` is enabled -------------------------------------+------------------------------------- Reporter: edsko | Owner: (none) Type: feature | Status: new request | Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- The following program {{{#!hs {-# 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... #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 {{{#!hs 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: {{{#!hs 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15868 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15868: Standard deriving should be less conservative when `UndecidableInstances` is enabled -------------------------------------+------------------------------------- Reporter: edsko | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by kosmikus): * cc: kosmikus (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15868#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15868: Standard deriving should be less conservative when `UndecidableInstances` is enabled -------------------------------------+------------------------------------- Reporter: edsko | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by adamgundry): * cc: adamgundry (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15868#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15868: Standard deriving should be less conservative when `UndecidableInstances` is enabled -------------------------------------+------------------------------------- Reporter: edsko | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Resolution: | Keywords: deriving Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * keywords: => deriving Comment: 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: {{{#!hs 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: {{{#!hs 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15868#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15868: Standard deriving should be less conservative when `UndecidableInstances` is enabled -------------------------------------+------------------------------------- Reporter: edsko | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Resolution: | Keywords: deriving 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: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * related: => #11008 Comment: #11008 is a similar ticket. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15868#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15868: Standard deriving should be less conservative when `UndecidableInstances` is enabled -------------------------------------+------------------------------------- Reporter: edsko | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Resolution: | Keywords: deriving 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: | -------------------------------------+------------------------------------- Comment (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? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15868#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15868: Standard deriving should be less conservative when `UndecidableInstances` is enabled -------------------------------------+------------------------------------- Reporter: edsko | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Resolution: | Keywords: deriving 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: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Replying to [comment:5 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15868#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC