[GHC] #16213: Unnecessary error

[GHC]

#16213: Unnecessary error
-------------------------------------+-------------------------------------
           Reporter:  pjljvdlaar     |             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:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 I don't know whether this is a bug or a feature request....

 When compiling
 {{{
 {-# LANGUAGE DataKinds           #-}
 {-# LANGUAGE FlexibleContexts    #-}
 {-# LANGUAGE GADTs               #-}
 {-# LANGUAGE KindSignatures      #-}
 {-# LANGUAGE TypeOperators       #-}
 {-# LANGUAGE TypeFamilies        #-}
 {-# LANGUAGE FlexibleInstances   #-}
 module Main where

 data Term (b::Bool) where
     Const :: Int -> Term 'True
     Sum  ::
             --Show (TermList v) =>
             TermList v -> Term 'False

 instance Show (Term b) where
     show (Const a) = "(Const " ++ show a ++ ")"
     show (Sum a) = "(Sum " ++ show a ++ ")"

 data TermList (xs :: [ Bool ]) where
     TNil :: TermList '[]
     TCons :: Term x -> TermList xs -> TermList (x ': xs)

 instance Show (TermList '[]) where
     show TNil = "Nil"

 instance Show (TermList xs) => Show (TermList (x ': xs)) where
     show (TCons a b) = "(Cons " ++ show a ++ " " ++ show b ++ ")"

 main :: IO ()
 main = do
         putStrLn "Hello world!"
 }}}

 one gets the error

 {{{
 src\Main.hs:37:31: error:
     * Could not deduce (Show (TermList v)) arising from a use of `show'
       from the context: b ~ 'False
         bound by a pattern with constructor:
                    Sum :: forall (v :: [Bool]). TermList v -> Term 'False,
                  in an equation for `show'
         at src\Main.hs:37:11-15
     * In the first argument of `(++)', namely `show a'
       In the second argument of `(++)', namely `show a ++ ")"'
       In the expression: "(Sum " ++ show a ++ ")"
    |
 37 |     show (Sum a) = "(Sum " ++ show a ++ ")"
    |                               ^^^^^^
 }}}

 Yet, both patterns are matched, i.e. '[] and (x ': xs),
 so I was surprised the compiler could not figure this out!

 By out commenting 'Show (TermList v) => ' the code complies fine.

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