#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

#10183: Warning for redundant constraints: interaction with pattern matching -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.11 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by hvr): * version: 7.8.4 => 7.11 Comment: Afaik this only occurs on GHC HEAD -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10183#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler