add error messages on some call failures

[fdupress]

When using call with invariant on procedures whose argument or return types do not match, we raised an exception without catching it. This adds an error message.

Fix #983.

[fdupress]

This needs improved further to print out at least the offending types. Ran out of time.

[fdupress]

@ahuelsing Are you happy with the error message? (This should address #983.)

[ahuelsing]

looks good

[fdupress]

Big Pickle thinks the error message does not look like the other error messages in the code base and that it is a problem.

I agree with the first part (it is not like the other error messages in the codebase), but disagree that it is a problem. In fact, I am tempted to add a suggestion that call (: ... ==> ...) should be used so the relation between arguments/returns can be given explicitly.

I also think we should have a way of specifying contracts that allows us to avoid repeating the part that is invariant between pre and post. (But that should be a separate issue.)

[strub]

@fdupress If you start to add detailed error messages and ask the question "hey, do you think this is in line with the current error messages?", of course you are going to obtain "no" as an answer. This should not forbid you to continue in this direction.

[fdupress]

I was asking it about the format string and boxes :)

After I merge this, I'll start a general pass to improve our error messages to get an idea of what infra we could have to make it easier to write good ones throughout in the first place, then make a plan.

[alleystoughton]

I was asking it about the format string and boxes :)

After I merge this, I'll start a general pass to improve our error messages to get an idea of what infra we could have to make it easier to write good ones throughout in the first place, then make a plan.

One of my recent favorites is apply saying:

the module Top.DDHOrAdv(Adv) is not allowed to use the modules(s) Adv

There was a missing module restriction. So the longer error message could at least say check your module restrictions for Adv.