[Haskell-cafe] Spurious pattern match warnings with GADTs

[MigMit]

Type classes are inherently open. The compiler uses only the facts that there ARE some instances of the classes it needs, but it doesn't attempt to use information that some types AREN'T instances of certain classes. So, it can't use information that T0 isn't an instance of C1. And that's right thing to do — it could happen that there is "instance C1 T0" in another module, which imports this one.

On 13 Jan 2012, at 00:40, Tom Hawkins wrote:

> Let's say I have:
> 
> data T0
> data T1
> 
> data T a where
>  A :: T T0
>  B :: T T1
> 
> Then I can write the following without getting any non-exhaustive
> pattern match warnings:
> 
> t :: T T0 -> String
> t a = case a of
>  A -> "A"
> 
> However, if I use type classes to constrain the constructors, instead
> of using the phantom types directly:
> 
> class C0 a
> instance C0 T0
> 
> class C1 a
> instance C1 T1
> 
> data T a where
>  A :: C0 a => T a
>  B :: C1 a => T a
> 
> Then I get a non-exhaustive pattern match warning on 't'.  How come?
> (I'm using GHC 7.0.4)
> 
> It appears that the intelligent pattern analysis of the first example
> is a relatively recent addition [1].
> 
> -Tom
> 
> [1] http://hackage.haskell.org/trac/ghc/ticket/3476
> 
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe