Unnecessary error

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.

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