Applying a function to too few arguments produces a difficult to understand error

[bboston7]

Assume a helper function:

let pointer_to_fresh (type : LLVMType) (name : String) = do { ... }

If a developer forgets to pass in the name argument, they get an error like:

[23:14:52.267] /workspaces/exercises/functional-correctness/swap/solution/solution.saw:87:27-99:2: Type Mismatch, expected: t.1 (t.2, t.3) but got: String -> LLVMSetup (Term, SetupValue)
 at "swap_array_spec" (/workspaces/exercises/functional-correctness/swap/solution/solution.saw:87:5-87:20)
Type constructors mismatch. Expected: <Block> but got (->) at "swap_array_spec" (/workspaces/exercises/functional-correctness/swap/solution/solution.saw:87:5-87:20)

In my experience, new users have no idea what this is trying to say. Some specific problems with it:

1. The error buries the lede. The important part is Type Mismatch, expected: t.1 (t.2, t.3) but got: String -> LLVMSetup (Term, SetupValue) which communicates that the proof writer failed to provide a String argument. Unfortunately, this error message is attached to many lines of SAW source (87:27-99:2), while the somewhat useless Type constructors mismatch is attached to a much narrower code range leading new users to focus on that error.
2. Learners do not know what any of these types mean. In some cases, they cannot even look it up. LLVMSetup doesn't appear at all in the SAW manual. Neither does <Block>.
3. The line numbers are misleading. In the example that produced this error, the pointer_to_fresh call with a missing argument is on line 88. However, the error directs users to lines 87-99 (a broad range that hardly helps to narrow things down) and line 87 (the declaration for the function that contains the bad pointer_to_fresh call). Learners might be able to fix these errors more easily if they're pointed to the right line.

When applying a function to too many arguments, you get the helpful suggestion:

(maybe a function is applied to too many arguments?)

It would be great to do the same when applying a function to too few arguments.

[sauclovian-g]

#2046 will help with this some, but not really fix it properly.

[sauclovian-g]

The position lossage was fixed in #2076, but the problems with Block remain, and something needs to be done about the docs as well.