SATySFi icon indicating copy to clipboard operation
SATySFi copied to clipboard

Application of {inline, block, math} commands does not take type synonyms into account

Open elpinal opened this issue 5 years ago • 0 comments

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.

elpinal avatar Dec 06 '19 11:12 elpinal