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
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 lazinesshttp://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