Patching a GADT-and-phantom-types-heavy-library … what did I do wrong?

Learning
, ,
1

I’m trying to update a large, complex library that heavily uses GADTs and phantom types. Unfortunately, I seem to have ended up somewhat out of my depth — I just cannot get my patch to compile.

Here’s a “minimal” reproduction (I did my best to rip everything I could out; the original codebase is absurdly complex and confusing, sorry) of the starting state, which compiles:

module Phantom : sig
  type 'a number = private |
  type 'a int = private |
  type 'a date = private |
end = struct
  type 'a number = private |
  type 'a int = private |
  type 'a date = private |
end

module Prim = struct
  module Value = struct
    type (_, _) t =
      | Int : int64 -> (int64 Phantom.int Phantom.number, int64) t
      | Float : float -> (float Phantom.number, float) t
      | String : string -> (string, string) t
      | Domain : domain_value -> (domain, domain_value) t
      | Date : float -> (float Phantom.date, float) t
      | DateTime : float -> (float Phantom.date, float) t
  end

  module Type = struct
    type signed =
      | Signed
      | Unsigned

    type int_affinity =
      | Raw
      | Percent
      | Bytes

    type float_affinity =
      | Raw
      | Percent
      | Cent

    type (_, _) string_kind =
      | Domain : (domain, domain_value) string_kind
      | Plain : (string, string) string_kind

    type _ time_kind =
      | Time : float time_kind
      | DateOnly : float time_kind

    type (_, _) t =
      | Int : signed * int_affinity -> (int64 Phantom.int Phantom.number, int64) t
      | Float : float_affinity -> (float Phantom.number, float) t
      | String : ('kind, 'actual) string_kind -> ('kind, 'actual) t
      | Date : 'kind time_kind -> ('kind Phantom.date, 'kind) t
  end
end

module Ir = struct
  type loc = Lexing.position * Lexing.position
  type 'a with_loc = {
    loc : loc;
    v : 'a;
  }
  let dummy_loc = Lexing.dummy_pos, Lexing.dummy_pos

  module Expr = struct
    let e v = { v; loc = dummy_loc }

    type ('id, 'query) expr' =
      | EInt of int64
      | EFloat of float
      | EUnsignedInt of int64
      | EString of string
  end
end

module Foo = struct
  module Value = struct
    open Prim.Value

    let to_expr : type t t'. (t, t') Prim.Type.t -> (t, t') Prim.Value.t -> _ =
     fun t v ->
      let open Ir.Expr in
      match t, v with
      | Int (Signed, _), Int i -> e @@ EInt i
      | Int (Unsigned, _), Int i -> e @@ EUnsignedInt i
      | _, Float f -> e @@ EFloat f
      | _, String s -> e @@ EString s
      | _, Domain s -> e @@ EString (make_domain s)
      | _, Date s -> e @@ EInt (Int64.of_int (int_of_float s))
      | _, DateTime s -> e @@ EInt (Int64.of_int (int_of_float s))
      | _ -> .
  end
end

(playground)

However, after trying to add adding a new high-precision DateTime64 variant, along with a new date_with_time phantom to subsume it, I’m getting this error:

Line 99, characters 8-9:
Error: This match case could not be refuted.
       Here is an example of a value that would reach it:
       (Date HighPrecision, Int _)

The changes don’t seem very substantial:

@@ -12,10 +12,12 @@ module Phantom : sig
   type 'a number = private |
   type 'a int = private |
   type 'a date = private |
+  type 'a date_with_time = private |
 end = struct
   type 'a number = private |
   type 'a int = private |
   type 'a date = private |
+  type 'a date_with_time = private |
 end
 
@@ -27,7 +29,8 @@ module Prim = struct
       | String : string -> (string, string) t
       | Domain : domain_value -> (domain, domain_value) t
       | Date : float -> (float Phantom.date, float) t
-      | DateTime : float -> (float Phantom.date, float) t
+      | DateTime : float -> (float Phantom.date_with_time Phantom.date, float) t
+      | DateTime64 : int64 -> (int64 Phantom.date_with_time Phantom.date, int64) t
   end
 
   module Type = struct
@@ -49,15 +52,16 @@ module Prim = struct
       | Domain : (domain, domain_value) string_kind
       | Plain : (string, string) string_kind
 
-    type _ time_kind =
-      | Time : float time_kind
-      | DateOnly : float time_kind
+    type (_, _) time_kind =
+      | HighPrecision : (int64 Phantom.date_with_time, int64) time_kind
+      | Time : (float Phantom.date_with_time, float) time_kind
+      | DateOnly : (float, float) time_kind
 
     type (_, _) t =
       | Int : signed * int_affinity -> (int64 Phantom.int Phantom.number, int64) t
       | Float : float_affinity -> (float Phantom.number, float) t
       | String : ('kind, 'actual) string_kind -> ('kind, 'actual) t
-      | Date : 'kind time_kind -> ('kind Phantom.date, 'kind) t
+      | Date : ('kind, 'actual) time_kind -> ('kind Phantom.date, 'actual) t
   end
 end
 
@@ -96,6 +100,7 @@ module Foo = struct
       | _, Domain s -> e @@ EString (make_domain s)
       | _, Date s -> e @@ EInt (Int64.of_int (int_of_float s))
       | _, DateTime s -> e @@ EInt (Int64.of_int (int_of_float s))
+      | _, DateTime64 s -> e @@ EInt s
       | _ -> .
   end
 end

(playground)

The specific error above isn’t the only refutation error; if I hackily work around that, I get other things like …

File "sth.ml", line 56, characters 15-88:
56 |     let parser (Value.Int i) = check_bounds_and_convert ~name ?max ?min Int64.to_float i in
                    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error (warning 8 [partial-match]): this pattern-matching is not exhaustive.
Here is an example of a case that is not matched:
DateTime64 _

I’ve spent most of my day banging my head against this; I cannot, for the life of me, figure out what’s different about my DateTime64 type than the existing DateTime type (or different than the existing String type, for instance, w.r.t. the GADT; or different than the Int type re: the phantom types …)

Help? :skull:

2

Shouldn’t you have ('kind, 'actual) t here?

Cheers,
Nicolas

3

Looking at the definition of Value.t,

your patch introduces a second potential inhabitant of the type of Value.Int (int64 Phantom.int Phantom.number, int64), DateTime64 which is why any code relying on the Value.Int being the single inhabitant of this type fails.

The point which is unclear to me is why the type-level tags in the Phantom module has not been made distinguishable with:

module Phantom : sig
  type 'a number = private Number_tag
  type 'a int = private Int_tag
  type 'a date = private Date_tag
end = ...

As written the code make it impossible to prove that there are no type equalities between number, int, date` laying somewhere, which triggers the exhaustiveness issue.

3 Likes