Fix bogus type of case expressionwip/T17056

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

1 files changed, 41 insertions, 4 deletions

diff --git a/compiler/coreSyn/CoreUtils.hs b/compiler/coreSyn/CoreUtils.hs
index d3ed00f783..95aae22b58 100644
--- a/compiler/coreSyn/CoreUtils.hs
+++ b/compiler/coreSyn/CoreUtils.hs
@@ -14,7 +14,7 @@ module CoreUtils (
         mkCast,
         mkTick, mkTicks, mkTickNoHNF, tickHNFArgs,
         bindNonRec, needsCaseBinding,
-        mkAltExpr,
+        mkAltExpr, mkDefaultCase, mkSingleAltCase,
 
         -- * Taking expressions apart
         findDefault, addDefault, findAlt, isDefaultAlt,
@@ -488,7 +488,7 @@ bindNonRec bndr rhs body
   | needsCaseBinding (idType bndr) rhs = case_bind
   | otherwise                          = let_bind
   where
-    case_bind = Case rhs bndr (exprType body) [(DEFAULT, [], body)]
+    case_bind = mkDefaultCase rhs bndr body
     let_bind  = Let (NonRec bndr rhs) body
 
 -- | Tests whether we have to use a @case@ rather than @let@ binding for this expression
@@ -512,8 +512,45 @@ mkAltExpr (LitAlt lit) [] []
 mkAltExpr (LitAlt _) _ _ = panic "mkAltExpr LitAlt"
 mkAltExpr DEFAULT _ _ = panic "mkAltExpr DEFAULT"
 
-{- Note [Binding coercions]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~
+mkDefaultCase :: CoreExpr -> Id -> CoreExpr -> CoreExpr
+-- Make (case x of y { DEFAULT -> e }
+mkDefaultCase scrut case_bndr body
+  = Case scrut case_bndr (exprType body) [(DEFAULT, [], body)]
+
+mkSingleAltCase :: CoreExpr -> Id -> AltCon -> [Var] -> CoreExpr -> CoreExpr
+-- Use this function if possible, when building a case,
+-- because it ensures that the type on the Case itself
+-- doesn't mention variables bound by the case
+-- See Note [Care with the type of a case expression]
+mkSingleAltCase scrut case_bndr con bndrs body
+  = Case scrut case_bndr case_ty [(con,bndrs,body)]
+  where
+    body_ty = exprType body
+
+    case_ty -- See Note [Care with the type of a case expression]
+      | Just body_ty' <- occCheckExpand bndrs body_ty
+      = body_ty'
+
+      | otherwise
+      = pprPanic "mkSingleAltCase" (ppr scrut $$ ppr bndrs $$ ppr body_ty)
+
+{- Note [Care with the type of a case expression]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+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-expression (S a) because
+'a' isn't in scope.  Hence the call to occCheckExpand.  This caused
+issue #17056.
+
+NB: this situation can only arise with type synonyms, which can
+falsely "mention" type variables that aren't "really there", and which
+can be eliminated by expanding the synonym.
+
+Note [Binding coercions]
+~~~~~~~~~~~~~~~~~~~~~~~~
 Consider binding a CoVar, c = e.  Then, we must atisfy
 Note [CoreSyn type and coercion invariant] in CoreSyn,
 which allows only (Coercion co) on the RHS.