When to thunk to remove type error in OCaml

Question

The following code displays an mismatch error for the val refl : ('a, 'a) eq component

Error: Signature mismatch:
       ...
       Values do not match:
         val refl : ('_a, '_a) eq
       is not included in
         val refl : ('a, 'a) eq
       File "lib/SO_typenoarg.ml", line 38, characters 2-24:
         Expected declaration
       File "lib/SO_typenoarg.ml", line 62, characters 6-10:
         Actual declaration

module Leibniz_ERROR : sig
  type ('a, 'b) eq

  val refl : ('a, 'a) eq
end = struct
  module type m = sig
    type 'a m
  end

  module type TyEq = sig
    type a
    type b
  end

  module Refl (X : sig
    type x
  end) : TyEq with type a = X.x and type b = X.x = struct
    type a = X.x
    type b = X.x
  end

  type ('a, 'b) eq = (module TyEq with type a = 'a and type b = 'b)

  module R = Refl (struct
    type x = int
  end)

  let refl (type a) : (a, a) eq =
    (module Refl (struct
      type x = a
    end))
end

It is solved (a bit mysteriously to me) by delaying refl

module Leibniz : sig
  type ('a, 'b) eq

  val refl : unit -> ('a, 'a) eq
end = struct
  module type m = sig
    type 'a m
  end

  module type TyEq = sig
    type a
    type b
  end

  module Refl (X : sig
    type x
  end) : TyEq with type a = X.x and type b = X.x = struct
    type a = X.x
    type b = X.x
  end

  type ('a, 'b) eq = (module TyEq with type a = 'a and type b = 'b)

  module R = Refl (struct
    type x = int
  end)

  let refl (type a) : unit -> (a, a) eq =
   fun _ ->
    (module Refl (struct
      type x = a
    end))
end

What's your practical rule of thumb for when to add a thunk ?

Answer 1

It is called eta-expansion and it is done to turn a value (which could be anything including a closure that does some nasty stuff) into a syntactic value for which it is guaranteed that it is fully defined in static time (i.e., that it is not a computed question).

In other words, weak variables are introduced when a type variable doesn't have a ground type and it is ascribed to a value that is either non-syntactic (i.e., a result of computation) or to a value to which the relaxed value restriction doesn't apply. The relaxed value restriction part is rather interesting but convoluted. It allows generalization (turning type variables into polymorphic types) for values that are not syntactic constants. See this article for the high-level overview of weak variables it has a part about the value restriction and its interaction with subtyping and covariance. And here's more academic read on the topic.

Finally, your eq type could be easily defined without any computations using constant syntactic values, i.e., with the GADT, type ('a,'b) eq = T : ('a,'a) eq, e.g.,

module Leibniz : sig
  type ('a, 'b) eq

  val refl : ('a, 'a) eq
end = struct
  module type m = sig
    type 'a m
  end

  module type TyEq = sig
    type a
    type b
  end

  module Refl (X : sig
      type x
    end) : TyEq with type a = X.x and type b = X.x = struct
    type a = X.x
    type b = X.x
  end

  type ('a,'b) eq = T : ('a,'a) eq


  module R = Refl (struct
      type x = int
    end)

  let refl (type a) : (a, a) eq = T
end

Answer 2

This is the value restriction at work

   (module Refl (struct
      type x = a
    end))

is a computation and not a syntactic value and it thus cannot be generalized by a let-binding.