Warning for redundant constraints: interaction with pattern matching
Herbert gives this example:
{-# LANGUAGE GADTs, DataKinds, TypeOperators, UnicodeSyntax #-}
import GHC.TypeLits
data List l t where
Nil ∷ List 0 t
(:-) ∷ t → List l t → List (l+1) t
head' ∷ (1<=l) ⇒ List l t → t
head' (x :- _) = x
We get the warning
typelits1.hs:9:9: Warning:
Redundant constraint: 1 <= l
In the type signature for: head' ∷ (1 <= l) ⇒ List l t → t
But of course the warning is not redundant if we want to exclude the (head' Nil)
case.
Here's an example that only depends on GADTs
:
{-# LANGUAGE GADTs #-}
data T a where
TT :: T Bool
TF :: T Int
f :: T Bool -> Bool
f TT = True
g :: (a ~ Bool) => T a -> Bool
g TT = True
Here f
compiles fine, but g
warns about a redundant constraint, even though the two types are isomorphic! And indeed the evidence for (a~Bool)
is not used in the code for g
. But that evidence is used to prove that the un-matched pattern (g TF)
is unreachable.
I'm not sure how to fix this. Bother.