Totality checker case hinting and assuming in proofs

[plredmond]

Currently if you want to write a proof with a lot of cases, you have no way of knowing which ones are necessary. The process that I've used is to write out all the cases and then whittle down to necessary cases. This can be time consuming. This PR changes how we elaborate cases to make this process easier:

• Case_Hinting -- When a user writes a proof that pattern matches one constructor but doesn't handle all of them, we'll tell them which additional cases require proofs. Eg. See test Totality00 and compare with the error expected by Totality02.

• Case_Assuming -- When a user writes a proof with a lot of cases, LH won't require them to write down trivially-discharged cases. Eg. See test Totality00 and compare with cases in Totality03.

Implementation

• In ANF transform normalize: For a case .. of expression of type () we replace the body of a GHC generated case alternative (patError) with ().
• In ANF transformcloneCase: Inject a Tick with a unique RealSrcSpan into the body of the case alternative to mark the injected case.
• In solveCs: Extract all the unique RealSrcSpan values injected by cloneCase and compare them with the spans on constraint errors returned by liquid fixpoint. If there's a match, produce an ErrOther that explains there's a missing case.

Followup

TODO before merging

• [ ] I don't know what the coding conventions are, and I duplicated some code here and there. Please comment on any TODOs/FIXMEs to let me know how to resolve them.
• [ ] Case_Hinting -- Need to make it show an error for each missing case, not just one. Currently solveCs has errors for all the cases which should be added, but only one is displayed to the user. (Essentially, it only shows you the "next" missing case, but would be quicker if it showed you all missing cases.)
• [ ] Fix conflicts

Possible future concerns

• [ ] Case_Hinting -- The span used for the missing cases is one that is anchored to the first pattern clause, and so it's not very helpful for determining which match needs additional cases.
• [ ] Case_Hinting -- With our change, hints are displayed after the user pattern matches on a constructor. If they just use the wildcard, then no elaboration takes place and no hints are given.
• [ ] Case_Assuming -- Essentially, we're allowing possible cases to be undefined in the code. This could cause crashes if somebody forces the value returned by a proof.

[plredmond]

My original branch passed CI/CD: https://github.com/plredmond/liquidhaskell/commit/e5af8eb2ab5bbb3c13bd99f66ff8ad6553a9beec. I'm looking at why this rebased branch doesn't pass.

[plredmond]

Thanks for joining the demo meeting. In the PR description above, I've un-hidden the bit which describes the changes to LH at a high-level, and I've split the TODO list according to our discussion to indicate some of the TODOs should happen before merging.

[facundominguez]

Hello @plredmond, would you still like to have this PR merged?

[plredmond]

No, this PR should be closed. I never merged it originally b/c the implementation is a very awkward hack (encoding arbitrary show/read data into Tick/RealSrcSpan and relying on the ability to parse that data out in order to detect a specific condition). Additionally, there didn't seem to be much enthusiasm for the feature. Thanks for following up.

[plredmond]

Closed per discussion and staleness.