Pattern matching and GADTs

[Gabor Greif]

This might be off-topic for your paper, but possibly relevant for
GADT-based programming:

In the below snippet
-----------------------------------------------------------------
{-# LANGUAGE GADTs, PatternGuards #-}

data Bar a where
  Listy :: Bar [Int]

{-
foo :: a -> Bar a -> Int
foo [0] Listy = 1

gadtTest.hs:8:5:
    Couldn't match expected type `a' with actual type `[a0]'
      `a' is a rigid type variable bound by
          the type signature for: foo :: a -> Bar a -> Int
          at /home/ggreif/gadtTest.hs:7:8
    Relevant bindings include
      foo :: a -> Bar a -> Int (bound at /home/ggreif/gadtTest.hs:8:1)
    In the pattern: [0]
    In an equation for `foo': foo [0] Listy = 1
-}

foo' :: Bar a -> a -> Int
foo' Listy [a] = a

foo'' :: a -> Bar a -> Int
foo'' l Listy | [a] <- l = a
-----------------------------------------------------------------

the "wrong" order of pattern matches (i.e. foo) causes an error,
the flipped order works (i.e. foo') and pattern guards remedy the
situation (e.g. foo'').

Since the type signatures are isomorphic this is a bit disturbing. Why
is it like this?
My guess is that patterns are matched left-to-right and refinements
become available "too late". Or is the reason buried in the OutsideIn
algorithm (and function arrow associativity: a -> (Bar a -> Int)) ?

Would it be a big deal to forward-propagate type information in from
GADT pattern matches?

Thanks and cheers,

    Gabor

On 3/2/15, Simon Peyton Jones <simonpj at microsoft.com> wrote:
> GHC developers
> You may be interested in this paper, submitted to ICFP
> GADTs meet their match: pattern-matching warnings that account for GADTs,
> guards, and
> laziness<http://research.microsoft.com/%7Esimonpj/papers/pattern-matching>,
> with Georgios Karachalias, Tom Schrijvers, and Dimitrios Vytiniotis.
> It describes a GADT-aware algorithm for detecting missing and redundant
> patterns.
> The implementation is not yet up to production quality, but it will be!
> If you feel able to give us any feedback about the paper itself, that would
> be incredibly useful. Thanks
> Simon
>
>