SATySFi icon indicating copy to clipboard operation
SATySFi copied to clipboard

Can we shadow primitive types?

Open nekketsuuu opened this issue 7 years ago • 2 comments

I noticed that the following code produces an odd error.

type int = A
module M : sig
  val a : A
end = struct
  let a = A
end
$ satysfi --type-check-only test.saty
 ---- ---- ---- ----
  target file: 'test.pdf'
  dump file: 'test.satysfi-aux' (will be created)
  parsing 'test.saty' ...
 ---- ---- ---- ----
  reading 'test.saty' ...
! [Type Error] at line 3, character 0 to line 7, character 3:
    The implementation of value 'a' has type
      int
    which is inconsistent with the type required by the signature
      int

This behavior may be related to the specification of shadowing of types. SATySFi can shadow user-defined types as follows. But can we shadow primitive types?

type t = A
module M : sig
  val a : t
end = struct
  let a = A
end

type t = B
module N : sig
  val a : t
end = struct
  let a = B
  % let a = A  % This produces a type error
end

Note that OCaml can shadow primitive types.

nekketsuuu avatar May 30 '18 15:05 nekketsuuu

To tell the truth, I have noticed the problem for a long time… It is mainly due to the implementation of the translation of manually written types to internal types (see here).

gfngfn avatar May 30 '18 15:05 gfngfn

So this is a kind of bug. Thanks for letting me know that. I'll change my type's name to differ from primitives as a workaround for the time being.

nekketsuuu avatar May 30 '18 16:05 nekketsuuu