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 |