Better error messages

[roboguy13]

Right now, we don't print any context information for errors. For instance, we might just have a message saying catchesT failed instead of providing information about which particular expression caused the failure. Here is an example using examples/laws/ListLaws.hs:

HERMIT> eval "rule-to-lemma nil-append"
nil-append (Not Proven)
  ∀ △ xs. (++) ▲ ([] ▲) xs ≡ xs
[Done]

HERMIT> proveLemma "nil-append"
Goal:
  ∀ △ xs. (++) ▲ ([] ▲) xs ≡ xs
[Done]

HERMIT> rhsR unfold
catchesT failed
*** Exception: failed to parse result value: Null : Object not returned from Server
HERMIT> 

The equivalent commands executed in the original hermit will also give the message Error in expression: rhs unfold.

When you are trying to debug a large script file, this lack of context can make things pretty difficult.

I believe that in the original hermit shell, the current expression was passed around in the form of an ExprH, but it seems as though we can't use this in hermit-shell (the stubExprHs in hermit-shell never seem to be printed). Also, unfortunately, the Value in parseTopLevel (from HERMIT.Server.Parser) seems to be a little too top level to be useful (it looks like it has the entire script, or most of the script, rather than just the current expression).

I think you know the specific, current expression inside of a parseExternal call but I'm not sure how you'd use this information since RewriteH LCore, etc are not instances of MonadCatch (so you couldn't use something like setFailMsg).

[ecaustin]

I'll look into this since it goes hand-in-hand with the return value stuff I'm working on.

There's basically three reasons something would fail from the client's view:

1. The provided method call is ill-typed.
2. The provided method call failed to parse.
3. The provided method call fails on the server side so we don't get a valid return result.

Reason 1 is handled for us already by GHCI because of the way we developed our API.

Reason 2 is a little harder to catch, but the Parse monad does propagate error strings, so I should be able to modify parseCLT to use parseEither instead of parseMaybe and trickle those changes through for better error messages.

Reason 3 is basically impossible to handle right now until we get return values pegged down, i.e. we can't throw the same exception that the server does client-side until we figure out how to return that exception to the client.

In the short term, I can modify the send method to at least tell you what method call caused the error along with what parameters were used to make the call since all of that information is obviously available. Hopefully that's useful for you.

[ecaustin]

Sorry, I wasn't feeling well today (yesterday?) so I didn't get much work done. I wanted to get something in place for error messages so that @roboguy13's work wasn't slowed down, though.

I modified send to print out a crudely pretty-printed form of a method call in the case that a shell exception is thrown. For example:

Cannot find path: binding-of failed: No matching nodes found.
*** Exception: failed to parse result value for setPath (bindingOf bad): Null : Object not returned from Server

For your given example, this is the produced output:

catchesT failed
*** Exception: failed to parse result value for rewrite (rhs unfold ): Null : Object not returned from Server

Not perfect, but hopefully you can infer rhsR unfold from rewrite (rhs unfold).

Interestingly, if you attempt this command outside of "proof mode" you'll see an actual exception, not just catchesT failed. I'm assuming this means that my earlier hunch about needing return values was wrong. What's more likely happening is that we're not properly propagating exceptions from "proof mode" back to the client.

David, maybe that's something you can look into since you've been focusing on that area lately?

[roboguy13]

With ku-fpg/kure@66b9d735 we get a lot more detailed messages, but there are a couple issues at this point:

1. We get lots of messages about crumbs that obscure the real errors (this looks like it's due to ku-fpg/hermit#133).
2. We get the error message in a tree format:

(there is no child matching the crumb. <+ (there is no child matching the crumb. <+ (there is no child matching the crumb. <+ (there is no child matching the crumb. <+ (there is no child matching the crumb. <+ (there is no child matching the crumb. <+ (unfold failed: (not an application. <+ Inline failed: variable is not bound to an expression.) <+ (there is no child matching the crumb. <+ catchesT failed))))))))

This tree should be parsed, destructured and and probably flattened into a list (although there might be some useful structure to keep. Notice how not an application and Inline failed: ... are structured relative to unfold failed) and we should decide where we want to provide that functionality (hermit-shell, hermit or kure).

[ecaustin]

Do we really want the user to see every single error message? Is returning the root, e.g. unfold failed: not an application not sufficient?

[roboguy13]

That would be an improvement, but it would be nice to see the Inline failed: variable is not bound to an expression. message too. If I'm understanding @Sculthorpen correctly, fixing ku-fpg/hermit#133 will get rid of all those crumb errors though, leaving (hopefully) only the useful messages.

For the moment, though, I could just print the root or filter out all the crumb messages. Either way would definitely be more readable, but I would like to see if we can get rid of those crumb messages at some point.

[Sculthorpen]

My proposal to override the default childL implementation is a fairly heavyweight solution.

However, I think there is a smaller problem, with a lightweight solution. Somewhere all the crumb error messages are getting aggregated. Just above that point, they should be overridden with a higher-level message. I'm not sure if this point is in KURE or HERMIT.

I've just improved the error message in KURE. Can you test that and see if we're getting lots of reported "childL failures", or a single "childL failure" with lots of crumb failures? If the former, the fault probably lies with something that's invoking childL.

[ecaustin]

Sorry @roboguy13, I read your message before you edited it to include all of the crumb error messages.

Assuming that is fixed somehow (I'll leave that to you two to figure out), I'd like to reiterate my earlier point that we should only be returning the top-most error message.

If that doesn't contain enough information, then we need to change the message itself, not get fancy with exception combinators.

[roboguy13]

@Sculthorpen It looks like there's a lot of "childL failures":

HERMIT> rhsR unfold (childL failed: there is no child matching the crumb. <+ (childL failed: there is no child matching the crumb. <+ (childL failed: there is no child matching the crumb. <+ (childL failed: there is no child matching the crumb. <+ (childL failed: there is no child matching the crumb. <+ (childL failed: there is no child matching the crumb. <+ (unfold failed: (not an application. <+ Inline failed: variable is not bound to an expression.) <+ (childL failed: there is no child matching the crumb. <+ catchesT failed))))))))

@ecaustin There are suberrors that may be helpful though. I believe Inline failed... is a "suberror" of unfold failed.... The way it's set up at the moment, these things are naturally structured in a tree which is given pretty freely based on how the (<+) applications ended up fitting together (there isn't anything fancy going on with how (<+) generates these messages), and this shows a relationship between the errors. Now, maybe we should end up throwing out everything except for the top-level message, but I feel like we should take a look at it without the crumb clutter before we make a completely final decision on that.

[ecaustin]

The original intention of the (<+) operator was an to catch a message thrown by a MonadCatch computation and ignore it. I don't understand why we're suddenly modifying its behavior to solve a problem that is unrelated to the operator itself.

If you do not like the error message thrown by unfoldR then change its definition to use modFailMsg instead of prefixFailMsg.

If you do not like the error message, or lack of error message, thrown by catchesT then change its definition to use a combinator that doesn't discard error messages.

Or better yet, go back to where catchesT is used and try and figure out why we're using a combinator that assumes success when there's the obvious chance of failure.

[roboguy13]

The issue here, I think, is whether or not it makes sense, in the most general case, for (<+) to collect error messages when both arguments fail. With my limited understanding of library, it seems to make sense but I'm not familiar enough with KURE to really know whether that's true. For this one, I'll have to defer that to other people who are more familiar with it.

[ecaustin]

Go back to the root of this issue: You wanted to see a detailed error message instead of catchesT failed.

The problem with that is that catchesT is implemented under the assumption that the list argument you provide it with contains at least one transformation that will succeed. Thus, catchesT should never fail when used properly. This is why it used (<+) internally; it doesn't care about the error messages.

If you want similar behavior but maintaining the error messages then you should be using a combinator that uses catchM internally, not (<+).

The proper fix here is to revert your changes to (<+) and implement your own version of catchesT for debugging purposes. While doing this, you can easily filter out the crumb error messages you don't care about by testing the String value that catchM handles, e.g. (\ e -> if "childL failed"isPrefixOfe then ...)

[roboguy13]

I have to wonder though, do we really want a combinator that is expected to never fail and as part of its expected behavior, gives back very little in the way of useful error messages when it does fail? It feels like a lot of the KURE library is designed around handling failures gracefully and this seems to me to be in conflict with that goal.

What this reminds me of are the issues with using partial functions. With a partial function like head, you get almost no information to go off of it when it fails. If you use an irrefutable pattern match instead, it at least gives you some more information (the source location of the failure). The latter is typically preferable.

Also note the behavior with the change is exactly the same as the behavior without the change, if the original precondition holds (that one of the transformations must succeed). It only gives error messages back if all of them fail.

I don't have a problem with being overridden on this issue, but I think we should at least discuss this change a bit further rather than saying it is invalid only because it differs from how it worked before.

What is the benefit of the original behavior over the behavior with the change? Also, given those pros and cons, which behavior would someone want more often? I suspect that it would be the behavior with the change, but I could be missing something I'm not thinking of.

If we do go with the original behavior, we should update the documentation for catchesT to make it a bit more clear that it has the precondition that one of the transformations should succeed.

[ecaustin]

The combinator language provided in the https://hackage.haskell.org/package/kure-2.16.10/docs/Language-KURE-MonadCatch.html module corresponds to a fairly standardized notion of a strategic programming language. Specifically, I believe it's an implementation of the System S calculus.

These concepts are shared among other languages too. For example, in HOL the (<+) combinator corresponds to "or else" and the catchesM combinator corresponds to "first" and is derived from (<+).

As a motivating example, imagine a basic expression language that has Lam, App, and Var constructors with methods to lift a transformation to operate over each constructor. The expression \ t -> catchesT [lamT t, appT, varT t] is total in a sense, in that it attempts to apply a given transformation to an expression of every possible form. Per the definition of catchesT, this expression expands to lamT t <+ appT t <+ varT t <+ fail "catchesT".

In the simplest case where a transformation handles only a single form of expression at a time, we expect the provided argument to fail for 2 of the 3 cases. Maintaining the error messages for those failures doesn't make sense because they were expected. Furthermore, when all of the cases fail, it's not due to the definition of of catchesT, (<+), or any of the expression combinators, but rather due to providing a bad argument. In that case, the best practice would be to wrap the main transformation with a catch statement to throw a meaningful error message.

For example, setFailMsg "bad transformation provided" $ \ t -> catchesT ....

After digging through the code relevant to your original example, the issue is that rhsR and its related rewrite combinators lack this wrapping message so when unfold fails for every enumerated case then catchesT failed is the error that is thrown.

As for the change you made to the definition of (<+), it's technically semantic preserving in that all failures are semantically equivalent regardless of the error message they carry. My main issue with the change is that it adds a significant amount of overhead as you are allocating and mutating strings that were previously ignored due to laziness. Additionally, I don't think the resultant message actually provides any helpful information. It just enumerates all of the sub-transformation failures that we could already infer from the main failure.

[Sculthorpen]

I agree with Evan on this: the higher-level transformations (e.g. rhsR) should provide their own error message rather than relying on messages propagated from lower-level combinators. If that error message could useful propagate information from a specific failed sub-transformations, then this could be encoded directly (rather than trying to parse the aggregated error string later). E.g.

lamT t catchM \ s1 -> varT t catchM \s2 -> (lamT (fail s1) <+ varT (fail s2))

Regarding the specific KURE combinators:

When I implemented (<+), I chose to have it emit the error message of the second operand if both failed, as this was both simplest, and consistent with "catch" semantics generally. Arguably though, a reasonable choice would be to have it combine both error messages, as David suggests, or to return neither and instead emit its own "<+ failed" message.

In practice, we often tend to write alternatives using (r1 <+ r2 <+ r3), but when really we don't care about the order of the alternatives as they're mutually exclusive. In those situations returning the error message of the final rewrite isn't very useful, but then, as Evan says, the transformation that is invoking the sequence of alternatives should be overriding the error message with something more useful anyway. Really what's needed is a separate combinator (e.g. <+>) for combining a set of mutually exclusive (but total in aggregate) transformations. This could then produce a more sensible error message for such situations (such as my first example in this post). Exploring this was on my TODO list, but I never got around to it.

My inclination right now is to keep the old definition of (<+), because apart from anything else it's the most efficient. If you find you do need alternative combinators that aggregate the error messages, then I suggest you define them in HERMIT and trial them. If they do prove useful in practice, then we can migrate them into KURE (which is the natural home for them).

Also, I noticed that there is both a catchesT and a catchesM. I believe the former is just a specialisation of the latter, so I've redefined it as catchesM, and deprecated it. (I probably forgot to delete it when I generalised a load of the Transform combinators to MonadCatch.)

I've pushed the catchesT change, and the reversion of (<+).

[roboguy13]

Oh, those are good points. I didn't fully understand it before, but that makes sense to me now. You're right, each combinator should provide its own error message.