Report delayed constraints in the REPL

[mb64]

When delayed higher-order unification problems remain unsolved, it would be useful to see the remaining constraints in the REPL.

Currently, asking a query such as eq (F 5) 5 ? gives back

Yes:
F := F.

There is no indication that there are still delayed unification problems.

For prior art on this, asking a similar query in Twelf, Teyjus, or ELPI with -delay-problems-outside-pattern-fragment, they all give a list of remaining constraints (or "disagreement pairs" for Teyjus).

[astampoulis]

Thanks for reporting this issue @mb64 ! Printing deferred constraints is opt-in behavior in Makam right now, by using the directive %constraints+..

Arguably it should be enabled by default. In my mind that should be bundled together with:

• testing query results should support validating that no deferred constraints exist, or what constraints do exist
• there are a few places in the standard library and in the examples where there are more constraints than there should be; using the testing support we could uncover why those happen and fix them.

[mb64]

Thanks! %constraints+. does what I want. Feel free to close this issue, unless you want to leave it open to track your other proposed UI improvements for inspecting constraints.