# GADT + functor : a type variable cannot be deduced

**URL:** <https://discuss.ocaml.org/t/gadt-functor-a-type-variable-cannot-be-deduced/10651>\
**Category:** Learning\
**Tags:** type-system, gadt, types, functor\
**Created:** [October 17, 2022, 7:16am UTC](https://discuss.ocaml.org/t/gadt-functor-a-type-variable-cannot-be-deduced/10651 "2022-10-17T07:16:19Z")\
**Posts on this page:** 3\
**Page:** 1

<div class="post-metadata">

**Author:** ![raphael-proust](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/raphael-proust/32/415_2.png) [@raphael-proust](https://discuss.ocaml.org/u/raphael-proust)\
**Post date:** [October 17, 2022, 7:16am UTC](https://discuss.ocaml.org/t/gadt-functor-a-type-variable-cannot-be-deduced/10651/1 "2022-10-17T07:16:19Z")

</div>

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.

```auto
(* 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

```

```auto
(* 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

```

```auto
(* 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).

---

<div class="post-metadata">

**Author:** ![octachron](https://avatars.discourse-cdn.com/v4/letter/o/49beb7/32.png) [@octachron](https://discuss.ocaml.org/u/octachron)\
**Post date:** [October 17, 2022, 8:21am UTC](https://discuss.ocaml.org/t/gadt-functor-a-type-variable-cannot-be-deduced/10651/2 "2022-10-17T08:21:38Z")

</div>

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](https://github.com/ocaml/ocaml/issues/5984) .

---

<div class="post-metadata">

**Author:** ![raphael-proust](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/raphael-proust/32/415_2.png) [@raphael-proust](https://discuss.ocaml.org/u/raphael-proust)\
**Post date:** [October 17, 2022, 8:26am UTC](https://discuss.ocaml.org/t/gadt-functor-a-type-variable-cannot-be-deduced/10651/3 "2022-10-17T08:26:37Z")

</div>

Thanks!

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