Compiler crashes with assertion when constraining instances of an implicit functor

[ohad]

With the attached file path_error.ml.txt the following crashes:

$ ocamlbuild -use-ocamlfind path_error.byte
ocamlfind ocamldep -modules path_error.ml > path_error.ml.depends
ocamlfind ocamlc -c -o path_error.cmo path_error.ml
+ ocamlfind ocamlc -c -o path_error.cmo path_error.ml
Fatal error: exception File "typing/path.ml", line 57, characters 25-31: Assertion failed
Command exited with code 2.

[let-def]

I think the problem here is that foo takes an implicit module that contains a functor and add constraints on an instance of this functor (the B.R(INT).t parameter).

Constraints propagated from an instance of a functor are not yet supported.

[ohad]

OK, thanks. I think I'm giving up on using implicits for what I was trying to use.

I also think that if I change the implicit argument to the explicit argument, the program shouldn't type-check anyway, because a first class module cannot be bound in a type signature, right? I.e.:

val foo : (module B : BAR ) -> B.R(INT).t -> int

is not a valid OCaml program (with first-class modules).

(The above bug is still a bug, because the compiler shouldn't crash ;).)

[let-def]

Indeed, normal ocaml arrows don't bind anything in the environment. The correct syntax is then (module BAR) and there is no way to refer to the type of an applied functor. (let foo (module B : BAR) = ... is accepted, but the typechecker will enforce that no name from B escapes)