Generalised abstract data types, phantom types and modules

Learning
, ,
1

Consider the two following code snippets

type atp
type smt
type _ config =
  | ConfigSmt : smt config
  | ConfigAtp : atp config

let digest : smt config -> unit =
  fun cfg -> match cfg with ConfigSmt -> ()

and

module M = struct
  type atp
  type smt
  type _ config =
    | ConfigSmt : smt config
    | ConfigAtp : atp config
end

let digest : M.smt M.config -> unit = fun cfg ->
  match cfg with ConfigSmt -> ()

and let’s call nomod.ml a file that contains the first snippet and mod.ml another file that contains the second snippet.

I’d expect both files to compile, and in particular in both cases I’d expect the type checker to infer that the case ConfigAtp isn’t possible,

  • either because ConfigAtp is of type M.atp, which isn’t M.smt in mod.ml and
  • because ConfigAtp is of type atp which isn’t smt in mod.ml.

However, nomod.ml type checks but not mod.ml doesn’t: using ocaml 4.14.1,

$ ocamlc nomod.ml

but

$ ocamlc mod.ml
File "mod.ml", line 10, characters 2-32:
10 |   match cfg with ConfigSmt -> ()
       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Warning 8 [partial-match]: this pattern-matching is not exhaustive.
Here is an example of a case that is not matched:
ConfigAtp

Why does the type checker fails to infer that ConfigAtp is of type M.atp M.config which shouldn’t be equivalent to M.smt M.config?

1 Like
2

This is because atp and smt have no representation outside the current module, so the compiler cannot deduce that they are different. One trick is to give them a form in the :

type atp = Atp
type smt = Smt
3

My bad, this is a duplicate of Unable to refute impossible GADT pattern when phantom types belong to a module