Left-to-right bias in type checking GADT functions

20 Jun 2006

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

Left-to-right bias in type checking GADT functions

Stefan Holdermans