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 usecase, 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
usecase 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
andRESULT_INJ
module types with the injectivity annotation and thenMakeInj(P:PARAM_INJ) : RESULT_INJ with … = Make(P)
. This workaround avoids duplication in the implementation. But it requires significant duplication in the signature (in the real example, the module types have a lot ofval
to manipulate theSeq
like values).Any one knows of a better workaround?