SATySFi icon indicating copy to clipboard operation
SATySFi copied to clipboard

Arity mismatch of type constructors should be detected as soon as possible

Open elpinal opened this issue 5 years ago • 0 comments

As written in a comment in typeenv.ml, SATySFi does not check whether a type constructor has the same arity in the structure and the signature: https://github.com/gfngfn/SATySFi/blob/69e62f66056b5644461f73c5fe841003602b0938/src/frontend/typeenv.ml#L1221

For example, SATySFi does not complain about the following code:

module M : sig
  type t
end = struct
  type 'a t = int
end

The type t expects 1 argument in the structure while in the signature it expects 0 arguments.

Although this situation does not make anything unfavorable (e.g., breach of soundness), early error reports are preferable.

elpinal avatar Sep 15 '19 06:09 elpinal