Opened 5 years ago

Last modified 4 years ago

#10183 new bug

Warning for redundant constraints: interaction with pattern matching

Reported by: simonpj Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.11
Keywords: redundant-constraints, GADTs Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Incorrect warning at compile-time Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by thomie)

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.

Change History (4)

comment:1 Changed 5 years ago by simonpj

Description: modified (diff)

comment:2 Changed 5 years ago by goldfire

Does the fancy new pattern-match completeness checker help out here? Can GHC record somehow that a constraint is used when the completeness checker is thinking?

In the meantime, does this mean the flag should be excluded from -Wall for 7.10?

comment:3 Changed 5 years ago by hvr

Version: 7.8.47.11

Afaik this only occurs on GHC HEAD

comment:4 Changed 4 years ago by thomie

Description: modified (diff)
Keywords: redundant-constraints GADTs added
Type of failure: None/UnknownIncorrect warning at compile-time
Note: See TracTickets for help on using tickets.