Given these types
type a = [ `A ]
type b = [ a | `B | `C ]
and this function
let pp: [< b] -> string =
function | `A -> "A"
| `B -> "B"
| `C -> "C"
applying a value of type a
works without issue, as expected:
let a: a = `A
let _ = pp a
However, if the function is modified to include a wildcard pattern
let pp: [< b] -> string =
function | `A -> "A"
| `B -> "B"
| _ -> "?"
even though everything else remains the same, it now yields the following error (on let _ = pp a
):
This expression has type b -> string but an expression was expected of type a -> 'a Type b = [ `A | `B ] is not compatible with type a = [ `A ] The second variant type does not allow tag(s) `B
Questions:
The underlying question is why the type of
let pp= function
| `A -> "A"
| `B -> "B"
| _ -> "?"
is infered as [> `A| `B] -> string
and not as [< `A| `B | ... ] -> string
(where ...
stands for any constructor). The answer is that is a design choice and a question of compromise between false positive and false negative : https://www.math.nagoya-u.ac.jp/~garrigue/papers/matching.pdf .
More precisely, the second type was deemed too weak since it was too easy to lose the information that `A
and `B
were present in pp
. For instance, consider the following code where `b
is a spelling mistake and should have been `B
:
let restrict (`A | `b) = ()
let dual x = restrict x, pp x
Currently, this code fails with
Error: This expression has type [< `A | `b] but an expression was expected of type [> `A | `B ]
The first variant type does not allow tag(s) `B
At this point, if `b
was a spelling mistake, it becomes possible to catch the mistake here. If pp
had been typed [< `A|`B |..]
, the type of dual would have been restricted to [`A] -> unit * string
silently, with no chance of catching this mistake. Moreover, with the current typing, if `b
was not a spelling mistake, it is perfectly possible to make dual
valid by adding some coercions
let dual x = restrict x, pp (x:[`A]:>[>`A]);;
(* or *)
let dual x = restrict x, (pp:>[`A] -> _) x
making it very explicit that restrict
and pp
works on different sets of polymorphic variants.