Incapability of realizing the definitions of the abstract types when defining a module

[elpinal]

Description

It turns out that the typechecker cannot equate two abstract types when defining a module which defines the abstract types.

How to reproduce

test.saty:

@require: stdjareport

module M : sig
  type t
  type s
  val f : s -> t list
end = struct
  type t = int
  type s = t list
  let f x = x
end in

StdJaReport.document (|
  title = {};
  author = {};
|) '<
>

Then, execute satysfi:

$ satysfi test.saty
 ---- ---- ---- ----
  target file: 'test.pdf'
  dump file: 'test.satysfi-aux' (already exists)
  parsing 'test.saty' ...
  parsing 'stdjareport.satyh' ...
  parsing 'pervasives.satyh' ...
  parsing 'gr.satyh' ...
  parsing 'geom.satyh' ...
  parsing 'list.satyg' ...
  parsing 'math.satyh' ...
  parsing 'color.satyh' ...
  parsing 'footnote-scheme.satyh' ...
 ---- ---- ---- ----
  reading 'pervasives.satyh' ...
  type check passed.
 ---- ---- ---- ----
  reading 'list.satyg' ...
  type check passed.
 ---- ---- ---- ----
  reading 'color.satyh' ...
  type check passed.
 ---- ---- ---- ----
  reading 'geom.satyh' ...
  type check passed.
 ---- ---- ---- ----
  reading 'gr.satyh' ...
  type check passed.
 ---- ---- ---- ----
  reading 'footnote-scheme.satyh' ...
  type check passed.
 ---- ---- ---- ----
  reading 'math.satyh' ...
  type check passed.
 ---- ---- ---- ----
  reading 'stdjareport.satyh' ...
  type check passed.
 ---- ---- ---- ----
  reading 'test.saty' ...
! [Type Error] at "test.saty", line 3, character 0 to line 11, character 3:
    The implementation of value 'f' has type
      '#a -> '#a
    which is inconsistent with the type required by the signature
      M.s -> M.t list

In this situation, M.s and M.t list should be deemed equivalent; It is outside M that they should be considered incompatible. So typechecking the example should pass.

Moreover, the above module definition is well-typed in both OCaml and Standard ML.

[elpinal]

In contrast, the following, a bit modified version is considered well-typed by the typechecker.

@require: stdjareport

module M : sig
  type t
  type s
  val f : s -> t list
end = struct
  type t = int
  type s = t list
  let f x =
    let _ = List.length x in  % The addition of this line makes typechecking succeed!
      x
end in

StdJaReport.document (|
  title = {};
  author = {};
|) '<
>

Since this second example is well-typed, the first example also should be well-typed. So I believe this is a bug.