David Allsopp wrote:
> Incidentally, if I use an annotation free version
>
> let f x = if x = `A then (true, `B) else (false, (x : [< `A | `C] :> [> `A |
> `C]))
>
> then the inferred type of x is [< `A | `C > `A ] ... what does that mean?
>   
This is a "point free" notation for what mathematicians would have written
`A <= x <= `A | `C

In other words, x is strictly bounded above and below by those 2 types.  
Translated into english, this means that the type from which x comes 
*must* contain an `A and *may* contain a `C and *must not* contain 
anything else.

For example, trying
let g x = f (snd (f x))
would not type.

Jacques