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:

{-# 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.

Trac metadata

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