Left-to-right bias in type checking GADT functions

[Simon Peyton-Jones]

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 at haskell.org
[mailto:glasgow-haskell-users-bounces at 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 at haskell.org
| http://www.haskell.org/mailman/listinfo/glasgow-haskell-users