GADT + functor : a type variable cannot be deduced

I am trying to build a GADT where some of the type parameters are coming from the application of a functor. Despite the type of the functor parameter having an injectivity annotation (!'a) and the type being substituted from in the resulting module signature, the type system tells me that

a type variable cannot be deduced from the type parameters

Some code to reproduce because my explanation above is certainly full of misused technical terms.

(* A realistic parameter for the functor: quite close to what I 
   have in my use-case, just with fewer helper functions. *)
module type PARAM = sig
  type 'a t
  val inj : 'a -> 'a t
  val proj : 'a t -> 'a
end

(** A realistic signature for the functors' output: same as my
    use-case but without any of the functions to work on the
    produced type. *)
module type RESULT = sig
  type 'a param_t (* this type intended to be substituted *)

  (* same as ['a Seq.t] but the [->] returns a node wrapped in
     the functor's parameter type *)
  type 'a t = unit -> 'a node param_t
  and 'a node =
    | Nil
    | Cons of 'a * 'a t
end
(* Very simple functor implementation. Note the substitution in
   the type constraint. *)
module Make(P:PARAM) : RESULT with type 'a param_t := 'a P.t = struct
  type 'a t = unit -> 'a node P.t
  and 'a node =
    | Nil
    | Cons of 'a * 'a t
end
(* Instantiate the functor with an injective type *)
module M = Make(struct type !'a t = 'a let inj = Fun.id let proj = Fun.id end)

(* This doesn't work:
In this definition, a type variable cannot be deduced from the type parameters.
*)
type _ g =
  | Int : int g
  | Mt : 'a -> 'a M.t g

I can fix the issue by adding injectivity annotations to the 'a PARAM.t and the 'a RESULT.param_t declarations. But

  • Considering the type is destructively substituted by the functor application, I would expect the injectivity annotation of the functor application argument to carry over to the output.
  • This restrict what the functor can be used for: only injective types! I only want to build the GADT on a dummy parameter for tests, where I can get an injective type. But I want to expose an expressive functor to library users who might not have an injective type.

So my two questions are:

  • Why doesn’t the injective annotation carry through the subsitution constraint? Is there a theoretical reason or is it so that the code of the type checker is manageable in complexity or is it an implementation detail that could feasibly be changed?

  • As a workaround, I can define a separate PARAM_INJ and RESULT_INJ module types with the injectivity annotation and then MakeInj(P:PARAM_INJ) : RESULT_INJ with … = Make(P). This work-around avoids duplication in the implementation. But it requires significant duplication in the signature (in the real example, the module types have a lot of val to manipulate the Seq-like values).

    Any one knows of a better workaround?

The root issue is that neither variance nor injectivity information are refined after a functor application which is a long standing limitation: Variance information is not properly propagated through functor applications · Issue #5984 · ocaml/ocaml · GitHub .

2 Likes

Thanks!

I’ll keep the workaround for now and keep an eye on this issue.