Internal error: [fmt_ppr_lf_infix_operator] spine length <> 2

[ryanakca]

Beluga v1.1.1 gives

$ beluga mwe.bel
## Type Reconstruction begin: mwe.bel ##
Internal error. Please report this as a bug.
[fmt_ppr_lf_infix_operator] spine length <> 2

on the following file

module Type = struct

tp : type.
mytp : tp.

rel : tp → tp → type. --infix rel.
rel : A rel B.
end;

--open Type.

test : tp → tp → type.
test/i : rel A B → test A B.
let broken : [⊢ test mytp mytp] = [⊢ test/i (Type.rel)];

[Ailrun]

Possibly because you used rel A B instead of A rel B in the test/i? But with that message it is a bug anyway. It should print a better error message for such a case.

[ryanakca]

Possibly. However, my understanding is that the --infix pragma is local to a module. Or at least, every time I've opened a module that contains --infix pragmas, I've had to explicitly respecify them after the --open pragma. (I think this is the most compositional approach: the explicit precedence levels declared in a module might clash with the precedence levels of relations already in scope at the --open pragma, so you should have to specify the precedence levels appropriate for the current context each time you open a module.)

[MartyO256]

Since version 1.1.1, there have been some bug fixes related to modules and fixity pragmas in commits e5adcb930ccea45eae84bb245a0e9f5adec60cd7 and 0e99fafc06d538172e5fd2e8127fa487c4cfcd32. A different error message is printed for that signature during parsing. A minor version release could be created and uploaded on the opam repository.

EDIT: Beluga version 1.1.2 has been released with those aforementioned bugfixes.