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
>