polymorphic type from external module crashes type checker

[nyuichi]

This thread is a follow up to https://twitter.com/___yuni/status/1148284153126739968.

Combining polymorphic types from an external module with type aliasing crashes the type checker. For example, compiling the following code

module Hoge : sig
  type 'a t
end = struct
  type 'a t = Hoge
end

module Fuga : sig
  type 'a t
end = struct
  type 'a t = ('a Hoge.t) list
end

I got an assertion error of the type checker of satysfi.

$ satysfi crash1.satyh 
 ---- ---- ---- ----
  target file: 'crash1.pdf'
  dump file: 'crash1.satysfi-aux' (will be created)
  parsing 'crash1.satyh' ...
 ---- ---- ---- ----
  type checking 'crash1.satyh' ...
Fatal error: exception "Assert_failure src/frontend/typeenv.ml:575:24"
Raised at file "src/frontend/typeenv.ml", line 575, characters 24-36
Called from file "src/frontend/typeenv.ml", line 516, characters 56-69
Called from file "src/frontend/typeenv.ml", line 639, characters 14-82
Called from file "src/frontend/typeenv.ml", line 871, characters 31-91
Called from file "src/frontend/directedGraph.ml", line 201, characters 24-40
Called from file "src/frontend/typeenv.ml", line 910, characters 4-42
Called from file "src/frontend/typechecker.ml", line 894, characters 21-73
Called from file "src/frontend/typechecker.ml", line 899, characters 20-52
Called from file "src/frontend/typechecker.ml", line 902, characters 22-54
Called from file "src/frontend/typechecker.ml", line 1404, characters 18-112
Called from file "src/frontend/main.ml", line 278, characters 21-56
Called from file "src/frontend/main.ml", line 1048, characters 26-69
Called from file "list.ml", line 117, characters 24-34
Called from file "src/frontend/main.ml", line 1045, characters 10-528
Called from file "src/frontend/main.ml", line 425, characters 4-16
Called from file "src/frontend/main.ml", line 993, characters 2-1023

The version I used was e1e0270.

[elpinal]

No need to be "polymorphic": we can reproduce the same phenomenon with the following, smaller code.

module M = struct
  type t = int
end

type t = M.t

Note that if we choose another name for either type definition, no error is reported as expected:

module M = struct
  type t = int
end

type u = M.t