A wildcard pattern that restricts a subtype of a polymorphic constraint

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 problems, as expected:

 let a: a = 'A let _ = pp a 

However, if the function is changed to include a lookup pattern

 let pp: [< b] -> string = function | 'A -> "A" | 'B -> "B" | _ -> "?" 

although everything else remains unchanged, now it gives the following error (on let _ = pp a ):

This expression is of type b → string, but an expression of type a → 'a was expected Type b = [' A | 'B] incompatible with type a = [' A] The second type of variant does not allow tags (s) 'B

Questions:

1. Why can he no longer accept the subtype? I understand that a wildcard means that MAY now accept a supertype, but that does not mean that it MUST.
2. Is there a way around this to avoid having to list a million or so options that are irrelevant?

Answer 1

The main question is why type

 let pp= function | `A -> "A" | `B -> "B" | _ -> "?" 

output as [> `A| `B] -> string [> `A| `B] -> string , not like [< `A| `B | ... ] -> string [< `A| `B | ... ] -> string [< `A| `B | ... ] -> string (where ... stands for any constructor). The answer is that this is a design choice and a compromise between false positive and false negative: https://www.math.nagoya-u.ac.jp/~garrigue/papers/matching.pdf .

More precisely, the second type was considered too weak, since it was too easy to lose information that `A `B were present in pp . For example, consider the following code, where `B is a spelling error and should `B :

 let restrict (`A | `b) = () let dual x = restrict x, pp x 

This code does not currently work with

Error: This expression is of type [<`A | `b], but an expression like [>` A | `B]
The first type of option does not allow the use of the `B tag

At this point, if `B was a spelling mistake, you can catch the mistake here. If pp were printed [< `A|`B |..] , the type of the double would be limited to [`A] -> unit * string without any chance of catching this error. Moreover, with the current character set, if `B not a spelling error, it is entirely possible to make dual valid by adding some coercion

 let dual x = restrict x, pp (x:[`A]:>[>`A]);; (* or *) let dual x = restrict x, (pp:>[`A] -> _) x 

makes it very clear that restrict and pp work with different sets of polymorphic variants.

Answer 2

The type of the second version of pp is [< b > `A `B ] -> string . In other words, `A `B should appear in type. I think it makes sense that if you want to compare the value with `B , `B should appear in the value type.

You can write pp (a :> b) .