Generalize bindings

[pieter-bos]

This PR generalizes the representation of bindings as proposed in #2572, together with ucsd-progsys/liquid-fixpoint#763. Other than that, I made a few associated changes:

• I split up the functionality of Reftable into the already existing ToReft(V) and PPrint, and added Top, Meet, and IsReft. I replaced isTauto and mempty->trueReft with a fixed implementation. All this was helpful in divorcing various functionalities from Symbol :)
• After going through the sites that could no longer use Reftable, I noticed that Reftable and UReftable did not have many remaining uses, so I've replaced them entirely here.
• Most places that want an unrefined RType have r as (). I replaced this with a unit type NoReftB b in order to have a sensible assignment for ToReft.ReftVar and Subable.Variable.
• I (hopefully temporarily) added a class CompatibleBinder to arrange that a tv from a RAllT is included in scope-aware traversals like emapReftM.
• Similarly I added PredicateCompat for b, v that can express papp (?). I have to say I'm not sure what that is for or whether it's needed.

[facundominguez]

Thanks @pieter-bos!

I hope to review this next week.

There are some test failures in the liquidhaskell-parser testsuite. [link]

They look like some tests need to be updated.

[facundominguez]

LGTM!

[facundominguez]

After fixing the liquidhaskell-parser tests we would be good to merge. Perhaps some of them require tweaking the printing of expressions.