Re: [Caml-list] When is a function polymorphic?

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

From: Yaron Minsky <yminsky@gmail.com>

> I don't understand the following results.  It seems like these two
> examples should have the same type.  In this example, there isn't much
> of a difference between the two cases, but there are cases where this
> idiom is quite convenient.  Any idea how to salvage it?
> 
> # function Some x -> Some () | None as x -> x;;
> - : 'a option -> unit option = <fun>
> # function Some x -> Some () | x -> x;;
> - : unit option -> unit option = <fun>

The typechecker does something special about "as x" patterns.
Namely, rather than unifying the type of x with the type of the whole
input, it types the aliased pattern twice, and only unifies type
parameters which appear in the pattern. So this means that
  # function Some _ as x -> x | None -> Some () ;;
  - : unit option -> unit option = <fun>
since the type parameter appears in the argument to Some, while
  # function Some x -> Some () | None as x -> x;;
  - : 'a option -> unit option = <fun>
since it doesn't appear in None.
This clever typing only happens with "<pat> as <var>" patterns, so
your second example gets the standard result (it is assumed that x
could be anything, including Some, as the typing does not use the
result of the exhaustiveness analysis.)

Jacques Garrigue