Can't publish constructor

[puripuri2100]

module test : sig
  type t = Hoge | Fuga
end = struct
  type t = Hoge | Fuga
end

% ==>
% ! [Syntax Error at Parser] at "file.satyh", line 2, characters 9-10:

[yuhr]

Same here, is this by design?

[nekketsuuu]

Currently this is a limitation of SATySFi; a type including public constructors must be defined in the top level. But this is not by design, I suppose. @gfngfn said this is just "not implemented yet": https://twitter.com/bd_gfngfn/status/1178332243514646528.

[gfngfn]

Currently this is a limitation of SATySFi; a type including public constructors must be defined in the top level.

Yes, it is. As said above, a simple workaround is to define the type in the top-level scope.

These days, however, I plan to extend SATySFi’s module system into the one based on F-ing modules [1]. Since this formalization supports the exposure of type definitions in modules, we will probably be able to provide such functionality.

References

1. Andreas Rossberg, Claudio Russo, and Derek Dreyer. F-ing modules. Journal of Functional Programming, 24(5), pp. 529–607, 2014.