Left-to-right bias in type checking GADT functions

[Stefan Holdermans]

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                -- !!!