Fix bogus type of case expression

This MR fixes #17056 (closed). The commit message is:

Issue #17056 revealed that we were sometimes building a case
expression whose type field (in the Case constructor) was bogus.

Consider a phantom type synonym
   type S a = Int
and we want to form the case expression
   case x of K (a::*) -> (e :: S a)
We must not make the type field of the Case constructor be (S a)
because 'a' isn't in scope.  We must instead expand the synonym.

Changes in this patch:

* Expand synonyms in the new function CoreUtils.mkSingleAltCase.

* Use mkSingleAltCase in MkCore.wrapFloat, which was the proximate
  source of the bug (when called by exprIsConApp_maybe)

* Use mkSingleAltCase elsewhere

* Documentation
    CoreSyn   new invariant (6) in Note [Case expression invariants]
    CoreSyn   Note [Why does Case have a 'Type' field?]
    CoreUtils Note [Care with the type of a case expression]

* I improved Core Lint's error reporting, which was pretty
  confusing in this case, because it didn't mention that the offending
  type was the return type of a case expression.

* A little bit of cosmetic refactoring in CoreUtils