Plugin can turn a tractable proof into an unsatisfiable wanted

[pieter-bos]

The plugin is careful with how it handles types involving subtractions. This makes sense to me, as it is helpful that we can show things like d - n + n <= d when we can also show n <= d.

Accordingly, there are proofs that are valid, but are not solved by natnormalise, e.g.:

given: n - d <= 1
wanted: n - d <= 2

Note that although the value of n - d is unspecified in the case that d > n, it should be considered an arbitrary but fixed Nat.

I don't think that is a problem by itself (it's fine that the plugin is incomplete), but it is inconvenient that in this case the wanted is resolved, but an additional wanted is emitted: d <= n. The plugin has thus transformed a tractable proof into an intractable one (we can't show d <= n here), meaning subsequent plugins like proof-assist have no chance to solve the constraint.

I think it would be helpful if we could consider abandoning the resolution of a wanted (like n - d <= 2) altogether in the case that not all side conditions (like d <= n) follow from the givens, rather than passing along the side conditions, which may be more restrictive than the original wanted.

[christiaanb]

I wonder how we can decide that no other solver will be able to solve wanted we emit.

For example, if we have:

[G] Max n (1 + n) - n <= 1
[W] Max n (1 + n) - n <= 2

Then we would solve the wanted [W] Max n (1 + n) - n <= 2, and emit the [W] n <= Max n (1+n), then the ghc-typelits-extra solver would instantly solve the emitted wanted.

So unless we have a good solution/heuristic, the best we can do is add a flag to the plugin to toggle between the current behavior and the behavior you desire.

[rowanG077]

Isn't it possible to safely emit a d <= n given if an n - d is encountered in a given constraint?