`PPAbsyn` raises exception when pattern matching on infix constructor

[zbyrn]

Version

110.99.7.1 (Latest)

Operating System

• Any
• Linux
• macOS
• Windows
• Other Unix

OS Version

No response

Processor

• Any
• Arm (using Rosetta)
• PowerPC
• Sparc
• x86 (32-bit)
• x86-64 (64-bit)
• Other

System Component

Core system

Severity

Cosmetic

Description

When an infix constructor is not used as an infix, the pretty printer raises an exception when the following pattern is not a tuple pattern. @bquiring originally discovered this bug.

Example,

case [1] of op:: x => x;

When the pretty printer is invoked to report the match non-exhaustiveness warning, it throws an exception.

Transcript

Standard ML of New Jersey [Version 110.99.7.1; 64-bit; January 17, 2025]
- case [1] of op:: x => x;
Error: Compiler bug: PPAbsyn: ppDconPat'[APPpat]
-

Expected Behavior

No response

Steps to Reproduce

case [1] of op:: x => x;

Additional Information

No response

Email address

byronzhong@cs.uchicago.edu

[dmacqueen]

This is certainly a valid bug. I will try to find a fix, assuming there is one that does not involve the internals of the old PP pretty print library.

[JohnReppy]

I think that the error is generated at line 234 of ElabData/syntax/ppabsyn.sml. Note that it is also a bug in the development branch.

[JohnReppy]

I've looked into this bug and the problem is that the current code uses the fixity of the data constructor to determine the expected shape of the argument pattern. While the op keyword allows :: to be used as a prefix constructor, the fixity of :: is not affected. One possible solution might be to add a INFIXpat constructor to the Absyn.pat type (a similar change would have to be made to the AST). One advantage of this approach is that we would get better syntactic fidelity in our error messages. Alternatively, we should the code to not rely on a symbol's fixity being a predictor of the shape of its argument.

[dmacqueen]

The parsing of patterns in ElabCore is currently incomplete and buggy, and I have been working on rewriting it in the dbm2 branch of legacy. When I have finished (probably today), I'll take a look at this bug and the related pretty printing strategy for infix data constructors. The trick is how to remember the infix status of :: in the original source pattern when prettyprinting the pattern (or not! - another option). For prettyprinting an operator (constructor) as an infix, it should have an explicit pair (2-tuple) of patterns as its argument, and when that isn't the case, as in this example, we should probably print the operator as nonfat with an op keyword, as in the original code.

[JohnReppy]

I've pushed a fix for this issue.