typesocamltype-inferencesubtypingpolymorphic-variants

Wildcard pattern overriding subtype constraint on polymorphic variant


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?

Solution

  • 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.