This PR fixes a bug in Syntax.pp_sign, where field labels were not bound during pretty printing, leading to this code
def bad : type := sig (A : type) (a : A) (b : A)
def test (x : bad) : type :=
let y := x in
?
causing this error
test.cooltt:5.2-5.3 [Info]:
Emitted hole:
x : bad
y : sub {sig (A : type) (a : x)
(y : cooltt: internal error, uncaught exception:
Failure("Pp printer: tried to resolve bound variable out of range")
This PR fixes a bug in
Syntax.pp_sign
, where field labels were not bound during pretty printing, leading to this codecausing this error