The expression:

  let a = assert false in
    fun x -> 1

is not a syntactic value, so because of the value restriction it has type:

    '_a -> int

That '_a comes from the `x` parameter.

> the variable a is not used in fun x -> 1

OCaml doesn't take account of whether `a` is used in deciding if something is a value, although if you had written:

  ignore (assert false);
  fun x -> 1

then it would have been a value.

I suspect the part you are missing is that generalization happens as part of `let` (and `match`, class definitions, polymorphic record creation, etc...). If you had written:

  let a = assert false in
  let f = fun x -> 1 in
  f

then the type associated with `x` would have been generalized as part of the definition of `f` although the resulting function would still have type:

  '_a -> int

Regards,

Leo
  

On 20 April 2017 at 01:15, Kenichi Asai <asai@is.ocha.ac.jp> wrote:
> Without looking too closely at your question I would assume that is just the
> value restriction.

But both in the expressions:

>     let a = 1 in fun x -> 1
>     let a = assert false in fun x -> 1

the variable a is not used in fun x -> 1.  How can the type of x be
affected by an unused binding for a around fun x -> 1?

It also seems that assert false can be used polymorphically (because
of the relaxed value restriction?):

# fun () -> let a = assert false in (a 1, a true);;
Warning 20: this argument will not be used by the function.
Warning 20: this argument will not be used by the function.
- : unit -> 'a * 'b = <fun>

--
Kenichi Asai