gfngfn / SATySFi

A statically-typed, functional typesetting system
GNU Lesser General Public License v3.0
1.16k stars 82 forks source link

Can we shadow primitive types? #81

Open nekketsuuu opened 6 years ago

nekketsuuu commented 6 years ago

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.

gfngfn commented 6 years ago

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).

nekketsuuu commented 6 years ago

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.