Hi all,
I have to admit that I haven't checked if this is a known issue...
The following is tested with both GHC 6.4.1 and 6.4.2; I have not
checked the HEAD.
Let me define a simple GADT |F|,
-- a simple GADT
data F :: * -> * where F :: Int -> F ()
and a more or less trivial function |g| operating on it:
-- type checks
g :: F a -> a -> Int
g (F n) () = n
No problems up to here. But then let me just flip the parameters of |
g|---and call the resulting function |h|:
-- does not type check
h :: a -> F a -> Int
h () (F n) = n -- !!!
Now, this definition of h does not type check:
Couldn't match the rigid variable `a' against `()'
`a' is bound by the type signature for `h'
Expected type: a
Inferred type: ()
When checking the pattern: ()
In the definition of `h': h () (F n) = n
So, it seems that there's a left-to-right bias in type checking
functions over GADTs. I cannot imagine this being by design, for it
certainly seems possible to type check functions of this sort in a
conceptually unbiased fashion.
Anyone to shine a light on this?
TIA,
Stefan
------------------------------------------
Bias.lhs:
> {-# OPTIONS -fglasgow-exts #-}
> -- a simple GADT
> data F :: * -> * where F :: Int -> F ()
> -- type checks
> g :: F a -> a -> Int
> g (F n) () = n
> -- does not type check
> h :: a -> F a -> Int
> h () (F n) = n -- !!!
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
