Hello,
I was surprised today to see that this code is rejected:
# let f (x : [< `A]) = ();;
val f : [< `A ] -> unit = <fun>
# let g (x : [< `B]) = ();;
val g : [< `B ] -> unit = <fun>
# fun b x -> if b then f x else g x;;
Error: This expression has type [< `A ]
but an expression was expected of type [< `B ]
These two variant types have no intersection
The type-checker rejects this code, even though it is safe,
and its type should be [< ] -> unit, where [< ] is the empty
variant type.
I imagine that the type-checker wants to be my friend and
wants to prevent me from defining a useless function.
However, in the real use case I have in mind, I am abusing
polymorphic variants to encode sets at the type level, and
the lack of an empty set is painful!
Just a random remark,
--
François Pottier
francois.pottier@inria.fr
http://cambium.inria.fr/~fpottier/