Comment author: @lpw25

I noticed this one a while ago and tried to use it to break soundness, but it appears that this bug is not sufficient to break soundness. Of course it is still a bug.

Comment author: @garrigue

Thanks for the report.

Indeed, there is no soundness problem here, since what this code says is just that "if there were values of type F(List).t, then we would be able to compare them". However, the code for generative functor does not allow to create values of this type.

A more correct statement would be "generative functors can be used as applicative constructors in type paths".

I agree that allowing to write this meaningless type is confusing, and this should be eventually rejected.

Comment author: @lpw25

Well, you can actually create values of some of these nonsense types:

  # module F () = struct
      type t = T
    end;;
      module F : functor () -> sig type t = T end

  # let x : F(List).t = T;;
  Characters 20-21:
    let x : F(List).t = T;;
                        ^
  Warning 40: T was selected from type F(List).t.
  It is not visible in the current scope, and will not 
  be selected if the type becomes unknown.
  val x : F(List).t = F(List).T

but I think it is still not enough to break soundness.

Comment author: @Octachron

This was fixed in #1491,

module F () = struct type t end
let f (x: F(List).t) (y: F(List).t) = x=y;;

now raises an error:

Error: The functor F is generative, it cannot be applied in type expressions