Yes, it's quite deliberate. See 5.4 of http://research.microsoft.com/%7Esimonpj/papers/gadt/gadt-icfp.pdf The alternative design choice is to reject both programs, but in Haskell (because of laziness) the evaluation order is prescribed, so accepting the former seems right. Simon | -----Original Message----- | From: glasgow-haskell-users-bounces@haskell.org [mailto:glasgow-haskell-users-bounces@haskell.org] | On Behalf Of Stefan Holdermans | Sent: 20 June 2006 08:53 | To: Glasgow Haskell Users | Subject: Left-to-right bias in type checking GADT functions | | 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