SATySFi
SATySFi copied to clipboard
Application of {inline, block, math} commands does not take type synonyms into account
The following code causes SATySFi to crash.
type t = [inline-text] inline-cmd
module M : sig
val \x : t
end = struct
let-inline \x it = it
end
let _ = {\M.x{}}
With the output:
---- ---- ---- ----
target file: 'test.pdf'
dump file: 'test.satysfi-aux' (will be created)
parsing 'test.saty' ...
---- ---- ---- ----
type checking 'test.saty' ...
Fatal error: exception "Assert_failure src/frontend/typechecker.ml:1147:14"
Raised at file "src/frontend/typechecker.ml", line 1147, characters 14-26
Called from file "src/frontend/typechecker.ml", line 573, characters 18-60
Called from file "src/frontend/typechecker.ml", line 774, characters 22-51
Called from file "src/frontend/typechecker.ml", line 902, characters 22-54
Called from file "src/frontend/typechecker.ml", line 1404, characters 18-112
Called from file "src/frontend/main.ml", line 278, characters 21-56
Called from file "src/frontend/main.ml", line 1048, characters 26-69
Called from file "list.ml", line 111, characters 24-34
Called from file "src/frontend/main.ml", line 1045, characters 10-528
Called from file "src/frontend/main.ml", line 425, characters 4-16
Called from file "src/frontend/main.ml", line 993, characters 2-1023
The type of \M.x
is t
, but the typechecker does not consider the possibility that t
is equal to [inline-text] inline-cmd
.
Similar situations arise when t
is [block-text] block-cmd
or [math] math-cmd
, mutatis mutandis.