On Thu, Jul 16, 2009 at 12:40 PM, Andrew Coppin <andrewcoppin@btinternet.com> wrote:

Robert Greayer wrote:

f0 _ = (foo True, foo 'x') where foo = id

is well-typed.

Really? That actually works? How interesting... This suggests to me that where-clauses also do strange things to the type system.

You could think of it that way. You mentioned GADTs in your OP. Well, it turns out GADTs often do not play nicely with where/let and it happens to all be related. As I understand it, functions bind their parameters monomorphically and let/where bind things polymorphically. And then we have the misfeature known as the monomorphism restriction which adds special cases.

whereas

f1 foo = (foo True, foo 'x')

requires 'foo' to be polymorphic in its first argument. This does
require a higher rank type, which can't be inferred:

You could type f1 as
f1 :: (forall a . a -> a) -> (Bool, Char)

and apply it to 'id'.

Or you could type it as something like:
f1 :: (forall a . a -> ()) -> ((),())

and apply it to 'const ()'

...all of which is beyond Haskell-98, which is what I am limiting myself to at present.

(Actually, even that is a lie. I don't have type-classes yet...)

Congrats on the type inference engine you're writing. It's on my list of things to do, and I was even reading up on TaPL a month or two back, but I put it down and haven't picked it up again yet. I think writing one would help flush out my understand of all this stuff.

Jason