Trouble with polymorphic variants

Hey, I am declaring two types and one is the subset of the other. Snippet looks like

type dtype =
  [ `Int
  | `Bool
  | `Void
  | `NULL
  | `Pointer of dtype
  | `Array of dtype
  | `Struct of Symbol.t
  ]
let rec pp_dtype = function
    | `Int -> "int"
    | `Bool -> "bool"
    | `Void -> "void"
    | `Pointer ptr -> "*" ^ pp_dtype ptr
    | `Array arr -> pp_dtype arr ^ "[]"
    | `NULL -> "NULL"
    | `Struct s -> "struct " ^ Symbol.name s
  ;;

and parameter’s data type is the subset of dtype. It is a version without struct type.

type param =
  { t : [ `Int | `Bool | `Void | `NULL | `Pointer of dtype | `Array of dtype ]
  ; i : Symbol.t
  }

Since param.t is a subset of dtype, it should be okay to pp_dtype param.t. However, the error pops

This expression has type
  [ `Array of dtype | `Bool | `Int | `NULL | `Pointer of dtype | `Void ]
but an expression was expected of type
  [< `Array of 'a | `Bool | `Int | `NULL | `Pointer of 'a | `Void > `Void ]
  as 'a
Type
  dtype =
    [ `Array of dtype
    | `Bool
    | `Int
    | `NULL
    | `Pointer of dtype
    | `Struct of Symbol.t
    | `Void ]
is not compatible with type
  [< `Array of 'a | `Bool | `Int | `NULL | `Pointer of 'a | `Void > `Void ]
  as 'a 
Types for tag `Struct are incompatible

Is there anything I am missing :confused: ?

Oh, I figured it out. We need to explicitly indicate that param.t is a subset of dtype

pp_dtype (param.t :> dtype)

Bravo!

To spare your library users the work of figuring this out themselves and applying a coercion before every call, you can also annotate pp_dtype with a signature that allows arguments to be subtypes of dtype, not just instances of dtype itself:

let rec pp_dtype: 'a. ([< dtype] as 'a) -> string = function
   | `Int -> ...

There are two special function syntax features at work here.
'a. means “for every type a”. Sometimes the compiler infers a more specific type than you intend, and this says that the function definition must be general enough to support all types matching the type constraint (... as 'a), which here is dtype and all of its subtypes.

Polymorphic variants are powerful but their their treatment by the compiler is subtle. Often explicit function types help ensure that you get the behavior you intend.

4 Likes

You can also make the t field compatible as a subtype of dtype:

type param =
  { t :
      'a.
      ([< `Int | `Bool | `Void | `NULL | `Pointer of dtype | `Array of dtype]
       as
       'a);
    i : Symbol.t
  }
2 Likes

Since the error message was confusing (the error was that there is no tag `Struct in the second type, not that the argument type was mismatched), I decided to fix it . @Tom_H , do you want to be credited as reporter for the issue?

Sorry for the late reply… I was out town last week. I found that has already merged, is there anything I can do?

BTW, your PR is very comprehensive and concise, thank you for fixing!

Thank you for your suggestion! This constraint looks more intuitive to me.

Using param.t :> dtype is like param.t is a super set of dtype (because the symbol greater), and I have no idea why to use this notation.

'a. means “for every type a”.

I use 'a to indicate any type, but I find a subtle difference where you are using 'a. with an extra dot. Is this dot going to indicate the constraint for 'a?

I didn’t realize I can also add constraint in the type, not just function signature. Thank you for your idea :grinning: !

If you wish to be mentioned as the issue reporter, just tell me under which name: updating the changelog can be easily done, and this is really the kind of issue where consciously discovering the issue is half of the work.