Ctype.Unify(_) error with higher-order example

[yallop]

I expect this can be simplified further:

module type S = sig type _ t end
implicit module Id = struct type 'a t = 'a end

module R = struct type 'a t = (implicit T: S) -> 'a T.t ->  unit end

let g (f : (implicit X: S) -> _ X.t -> unit) (implicit U:S) =
  let module RU = struct type 'a t = 'a R.t U.t end in f (implicit RU) 

let j (implicit T: S) _ = ()
let h f = g f j

[yallop]

The following code also raises Ctype.Unify(_). Perhaps it's the same issue:

module type T1 = sig type _ t end
implicit module Id = struct type 'a t = 'a end
let g : (implicit C:T1) -> (<f:'g. 'g -> 'g C.t>) -> unit = assert false
let _  = g (object method f : 'g. 'g -> 'g = assert false end)

[let-def]

After https://github.com/ocamllabs/ocaml-modular-implicits/commit/b81ea304825810f5ea0367bb95ca725c6e707852 fix, I think it is the same issue.

I don't know how these unifications should be handled. The code dealing with this is: typeimplicit.ml:165.

Here, tyvar is a type variable introduced during instantiation of the implicit arrow, ty is a type referring to the implicit module that should be unified with tyvar. E.g when instantiating f : (implicit M : T) -> M.t -> unit a type variable 'a is introduced and the tuple (M.t,'a) is added to the constraint list.

This code is quite naive as I don't know enough about OCaml unification to properly handle all the cases… The environment and the unification function should be properly setup and selected so that call on line 168 succeed.

[let-def]

We spend some time looking at that issue with @lpw25 .

The unify error is likely because of unification with a univar which was put in the constraint list. During normal typechecking this is an error as the univar will be ill-scoped (unifiying something under the forall quantifier with some variables potentially from the outside).

Luckily, with implicits, we can make sure by construction that all type variables introduced appear only in the correct scope.

typeimplicit.ml:62 is about sharing of introduced type variables: we introduce only one fresh type variable per equal types. This is correct except for types which are syntactically equal but interpreted in different scopes, e.g. (<f:'g. 'g -> 'g C.t>) -> (<f:'g. 'g -> 'g C.t>) -> unit, or even more tricky, (<f:'g. 'g -> 'g C.t -> (<f:'g. 'g -> 'g C.t>) >) -> unit

The solution is:

• keep track of scope in typeimplicit.ml:73, when entering and exiting a Tpoly.
• relax unification typeimplicit.ml:165 now that we know that unification of Tunivar with fresh variable is correct.

[let-def]

Leo suggested we introduce a new constructor for type variables which are allowed to unify with some univars, something like:

Tpolyvar of string list (* allowed univars *) * string option (* like usual Tvar *)