On Thu, 31 Mar 2005 09:37:24 +0900 (JST), Jacques Garrigue
<garrigue@math.nagoya-u.ac.jp> wrote:
> 
> 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.)
> 

I think I screwed up the original examples a bit.  I think the effect
I'm looking at doesn't depend on the "as" notation in particular. 
Here's another example that doesn't use "as":

# function Some x -> Some () | None -> None;;
- : 'a option -> unit option = <fun>
# function Some x -> Some () | x -> x;;
- : unit option -> unit option = <fun>

The reason I want this is for the following example.  Consider some
complicated union type with a single parameter:

type 'a foo = A of 'a | B of int | C of string * string | ... | ZZ of float

I want a function that converts an 'a foo to a unit foo.  I tried to
write it this way:

function A _ -> A () | x -> x

But this ends up having type: unit foo -> unit foo, which isn't what I
want at all.  Any idea of how to achieve this cleanly?

Yaron