| data Bar a where
| Listy :: Bar [Int]
|
| {-
| foo :: a -> Bar a -> Int
| foo [0] Listy = 1
Well you'd get a seg-fault from the call (foo True (undefined :: Bar [Int])). So we really MUST match the (Bar a) arg before the 'a' arg. And Haskell only offers one way to do that, which is to put it first.
You don't have to change the argument order. Write
foo xs Listy | [0] <- xs = 1
Simon
| -----Original Message-----
| From: ghc-devs [mailto:ghc-devs-bounces@haskell.org] On Behalf Of Gabor
| Greif
| Sent: 03 March 2015 14:13
| To: ghc-devs@haskell.org
| Subject: Re: Pattern matching and GADTs
|
| 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