SATySFi
SATySFi copied to clipboard
Can we shadow primitive types?
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.
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).
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.