Wildcard pattern overriding subtype constraint on polymorphic variant

Question

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:

1. Why is it no longer able to accept a subtype? I understand the wildcard means it now CAN accept a supertype, but that shouldn't mean it MUST.
2. Is there some way of getting around this, to avoid having to enumerate a million or so variants that aren't relevant?

Belgian

Answer 1

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.

Preglacial

Answer 2

The type of the second version of pp is [< b > `A `B ] -> string. In other words, `A and `B must appear in the type. I guess it seems reasonable that if you want to compare a value against `B then `B should appear in the type of the value.

You can write pp (a :> b).

Class

In itself it might seem reasonable, but wouldn't it be just as reasonable for the function that enumerates all the variants? +1 for :> though, I didn't realize it could be used for poly-variants too! – Belgian