[GHC] #10183: Warning for redundant constraints: interaction with pattern matching
GHC
ghc-devs at haskell.org
Mon Mar 23 13:30:09 UTC 2015
#10183: Warning for redundant constraints: interaction with pattern matching
-------------------------------------+-------------------------------------
Reporter: simonpj | Owner:
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 7.8.4
Resolution: | Keywords:
Operating System: Unknown/Multiple | Architecture:
Type of failure: None/Unknown | Unknown/Multiple
Blocked By: | Test Case:
Related Tickets: | Blocking:
| Differential Revisions:
-------------------------------------+-------------------------------------
Description changed by simonpj:
Old description:
> 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 doesn't depend on `TypeLits`:
> {{{
> data T a where
> TT :: T True
> TF :: T False
>
> f :: T True -> Bool
> f TT = True
>
> g :: (a ~ True) => T a -> Bool
> g TT = True
> }}}
> Here `f` compiles fine, but `g` warns about a redundant constraint! And
> indeed the evidence for `(a~True)` 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.
New description:
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 doesn't depend on `TypeLits`:
{{{
data T a where
TT :: T True
TF :: T False
f :: T True -> Bool
f TT = True
g :: (a ~ True) => 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~True)` 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.
--
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/10183#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
More information about the ghc-tickets
mailing list