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
RESULT_INJmodule 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
valto manipulate the
Any one knows of a better workaround?