[Haskell] Re: GHC Error question

[oleg at pobox.com]

>  > Or, one may use the local type variable to the same end
>  > 
>  > >  compile1 :: forall b t box. (Builder b box) => t -> Name -> Ir.ANF -> b
>  > >  t compile1 f x body = do env <- compile body empty
>  > >                          wire ((Arg W)::Source box) (env x)
>  > >                          return f
>  > 
>  > the explicit `forall' binder is required.
>
> This suggestion, I like.  I have always hated that ML and Haskell
> leave the foralls implicit.  Bad design.

I'm afraid I may disagree about the quantification. Also, I'm cautious
about the phrase "ML and Haskell". In GHC 6.4, local type variables
behave pretty much like those in ML (actually, GHC 6.2 was closer). In
GHC 6.6, the behavior is completely different!

Regarding the quantification: in ML (OCaml) we can write
	let foo (x:'a) y = (x+1,(y:'a))
That does not mean that foo has the type forall 'a. 'a -> 'a -> ...
Indeed, foo is not polymorphic and its inferred type is int -> int ->
int * int. If there should be a quantifier in the above type, it
probably should be 'exists' rather than 'forall'.  It seems in ML, the
type variables are better understood as names of some types; if two
subterms are annotated with the same type variable, these two subterms
must have the same type. Thus the annotation adds an
equation/constraint to the pool of type equations to solve. I must
admit I find that constraint-based view quite intuitive.

GHC 6.6 has changed things dramatically for the sake of wobbly
inference and boxy types (or boxy inference and wobbly types...). Now, a
type variable is a rigid type variable. The new GHC rules are described in
 http://www.haskell.org/ghc/docs/latest/html/users_guide/type-extensions.html
in Section 7.4.10, Lexically scoped type variables. In particular,
Subsection 7.4.10.2 confirms your understanding for the need of the
explicit forall. Incidentally, as far as your example is concerned,
forall as a binder is required already in GHC 6.4.