Standalone deriving for GADTs should avoid impossible cases
One solution to bringing recursion schemes to mutually-recursive types is to combine the different types into a single GADT `T`, parameterized by a tag type. To really make this ergonomic, it would be nice to be able to derive instances for individual tags. And this almost works! But not always:
```hs
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# OPTIONS_GHC -Wall -Werror -ddump-deriv #-}
module M where
data T = T -- no Show instance
data Good a where
A :: Good Int
B :: T -> Good Char
data Fine a where
P :: Fine Int
Q :: Fine Char
data Bad a where
X :: Bad Int
Y :: T -> Bad Char
instance Show (Good Int) where -- OK and warning-free
show A = "A"
deriving instance Show (Fine Int) -- OK, because of suppressed warnings
deriving instance Show (Bad Int) -- Fails!
```
This fails with the error
```
example.hs:25:1: error:
• Could not deduce (Show T) arising from a use of ‘showsPrec’
from the context: Int ~ Char
bound by a pattern with constructor: Y :: T -> Bad Char,
in an equation for ‘showsPrec’
at example.hs:25:1-33
```
The derived code is as follows:
```
==================== Derived instances ====================
Derived class instances:
instance GHC.Show.Show (M.Bad GHC.Types.Int) where
GHC.Show.showsPrec _ M.X = GHC.Show.showString "X"
GHC.Show.showsPrec a_a1cf (M.Y b1_a1cg)
= GHC.Show.showParen
(a_a1cf GHC.Classes.>= 11)
((GHC.Base..)
(GHC.Show.showString "Y ") (GHC.Show.showsPrec 11 b1_a1cg))
instance GHC.Show.Show (M.Fine GHC.Types.Int) where
GHC.Show.showsPrec _ M.P = GHC.Show.showString "P"
GHC.Show.showsPrec _ M.Q = GHC.Show.showString "Q"
```
Is there a way that the derived `Show` code for `Bad Int` could avoid emitting cases for `Bad Char` terms? A solution that worked even for a limited set of tags would be still be interesting; for example, restricting to situations where the GADT was indexed by a sum kind like `data K = Ix1 | Ix2 | ... | IxN`.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.6.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Standalone deriving for GADTs should avoid impossible cases","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"One solution to bringing recursion schemes to mutually-recursive types is to combine the different types into a single GADT `T`, parameterized by a tag type. To really make this ergonomic, it would be nice to be able to derive instances for individual tags. And this almost works! But not always:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE FlexibleInstances #-}\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE StandaloneDeriving #-}\r\n{-# OPTIONS_GHC -Wall -Werror -ddump-deriv #-}\r\n\r\nmodule M where\r\n\r\ndata T = T -- no Show instance\r\n\r\ndata Good a where\r\n A :: Good Int\r\n B :: T -> Good Char\r\n\r\ndata Fine a where\r\n P :: Fine Int\r\n Q :: Fine Char\r\n\r\ndata Bad a where\r\n X :: Bad Int\r\n Y :: T -> Bad Char\r\n\r\ninstance Show (Good Int) where -- OK and warning-free\r\n show A = \"A\"\r\nderiving instance Show (Fine Int) -- OK, because of suppressed warnings\r\nderiving instance Show (Bad Int) -- Fails!\r\n}}}\r\n\r\nThis fails with the error\r\n{{{\r\nexample.hs:25:1: error:\r\n • Could not deduce (Show T) arising from a use of ‘showsPrec’\r\n from the context: Int ~ Char\r\n bound by a pattern with constructor: Y :: T -> Bad Char,\r\n in an equation for ‘showsPrec’\r\n at example.hs:25:1-33\r\n}}}\r\n\r\nThe derived code is as follows:\r\n{{{\r\n==================== Derived instances ====================\r\nDerived class instances:\r\n instance GHC.Show.Show (M.Bad GHC.Types.Int) where\r\n GHC.Show.showsPrec _ M.X = GHC.Show.showString \"X\"\r\n GHC.Show.showsPrec a_a1cf (M.Y b1_a1cg)\r\n = GHC.Show.showParen\r\n (a_a1cf GHC.Classes.>= 11)\r\n ((GHC.Base..)\r\n (GHC.Show.showString \"Y \") (GHC.Show.showsPrec 11 b1_a1cg))\r\n\r\n instance GHC.Show.Show (M.Fine GHC.Types.Int) where\r\n GHC.Show.showsPrec _ M.P = GHC.Show.showString \"P\"\r\n GHC.Show.showsPrec _ M.Q = GHC.Show.showString \"Q\"\r\n}}}\r\n\r\nIs there a way that the derived `Show` code for `Bad Int` could avoid emitting cases for `Bad Char` terms? A solution that worked even for a limited set of tags would be still be interesting; for example, restricting to situations where the GADT was indexed by a sum kind like `data K = Ix1 | Ix2 | ... | IxN`.","type_of_failure":"OtherFailure","blocking":[]} -->
issue