[GHC] #16341: Standalone deriving for GADTs should avoid impossible cases

20 Feb 2019

      #16341: Standalone deriving for GADTs should avoid impossible cases
-------------------------------------+-------------------------------------
           Reporter:  mnoonan        |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.6.3
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
                                     |  https://ghc.haskell.org/trac/ghc/ticket/15398
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 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`.

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16341
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler