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

13 files changed, 397 insertions, 177 deletions

diff --git a/compiler/basicTypes/MkId.hs b/compiler/basicTypes/MkId.hs
index 741b48e58b..bc7d0f57c9 100644
--- a/compiler/basicTypes/MkId.hs
+++ b/compiler/basicTypes/MkId.hs
@@ -48,7 +48,7 @@ import FamInstEnv
 import Coercion
 import TcType
 import MkCore
-import CoreUtils        ( exprType, mkCast )
+import CoreUtils        ( mkCast, mkDefaultCase )
 import CoreUnfold
 import Literal
 import TyCon
@@ -463,8 +463,8 @@ mkDictSelRhs clas val_index
 
     rhs_body | new_tycon = unwrapNewTypeBody tycon (mkTyVarTys tyvars)
                                                    (Var dict_id)
-             | otherwise = Case (Var dict_id) dict_id (idType the_arg_id)
-                                [(DataAlt data_con, arg_ids, varToCoreExpr the_arg_id)]
+             | otherwise = mkSingleAltCase (Var dict_id) dict_id (DataAlt data_con)
+                                           arg_ids (varToCoreExpr the_arg_id)
                                 -- varToCoreExpr needed for equality superclass selectors
                                 --   sel a b d = case x of { MkC _ (g:a~b) _ -> CO g }
 
@@ -987,7 +987,7 @@ wrapCo co rep_ty (unbox_rep, box_rep)  -- co :: arg_ty ~ rep_ty
 
 ------------------------
 seqUnboxer :: Unboxer
-seqUnboxer v = return ([v], \e -> Case (Var v) v (exprType e) [(DEFAULT, [], e)])
+seqUnboxer v = return ([v], mkDefaultCase (Var v) v)
 
 unitUnboxer :: Unboxer
 unitUnboxer v = return ([v], \e -> e)
@@ -1014,8 +1014,8 @@ dataConArgUnpack arg_ty
     ,( \ arg_id ->
        do { rep_ids <- mapM newLocal rep_tys
           ; let unbox_fn body
-                  = Case (Var arg_id) arg_id (exprType body)
-                         [(DataAlt con, rep_ids, body)]
+                  = mkSingleAltCase (Var arg_id) arg_id
+                             (DataAlt con) rep_ids body
           ; return (rep_ids, unbox_fn) }
      , Boxer $ \ subst ->
        do { rep_ids <- mapM (newLocal . TcType.substTyUnchecked subst) rep_tys
diff --git a/compiler/coreSyn/CoreLint.hs b/compiler/coreSyn/CoreLint.hs
index 86943e2ba7..e0f4dda2aa 100644
--- a/compiler/coreSyn/CoreLint.hs
+++ b/compiler/coreSyn/CoreLint.hs
@@ -3,7 +3,8 @@
 (c) The GRASP/AQUA Project, Glasgow University, 1993-1998
 
 
-A ``lint'' pass to check for Core correctness
+A ``lint'' pass to check for Core correctness.
+See Note [Core Lint guarantee].
 -}
 
 {-# LANGUAGE CPP #-}
@@ -78,6 +79,23 @@ import Pair
 import qualified GHC.LanguageExtensions as LangExt
 
 {-
+Note [Core Lint guarantee]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+Core Lint is the type-checker for Core. Using it, we get the following guarantee:
+
+If all of:
+1. Core Lint passes,
+2. there are no unsafe coercions (i.e. UnsafeCoerceProv),
+3. all plugin-supplied coercions (i.e. PluginProv) are valid, and
+4. all case-matches are complete
+then running the compiled program will not seg-fault, assuming no bugs downstream
+(e.g. in the code generator). This guarantee is quite powerful, in that it allows us
+to decouple the safety of the resulting program from the type inference algorithm.
+
+However, do note point (4) above. Core Lint does not check for incomplete case-matches;
+see Note [Case expression invariants] in CoreSyn, invariant (4). As explained there,
+an incomplete case-match might slip by Core Lint and cause trouble at runtime.
+
 Note [GHC Formalism]
 ~~~~~~~~~~~~~~~~~~~~
 This file implements the type-checking algorithm for System FC, the "official"
@@ -392,6 +410,7 @@ interactiveInScope hsc_env
               --   f :: [t] -> [t]
               -- where t is a RuntimeUnk (see TcType)
 
+-- | Type-check a 'CoreProgram'. See Note [Core Lint guarantee].
 lintCoreBindings :: DynFlags -> CoreToDo -> [Var] -> CoreProgram -> (Bag MsgDoc, Bag MsgDoc)
 --   Returns (warnings, errors)
 -- If you edit this function, you may need to update the GHC formalism
@@ -786,50 +805,8 @@ lintCoreExpr (Lam var expr)
     do { body_ty <- lintCoreExpr expr
        ; return $ mkLamType var' body_ty }
 
-lintCoreExpr e@(Case scrut var alt_ty alts) =
-       -- Check the scrutinee
-  do { scrut_ty <- markAllJoinsBad $ lintCoreExpr scrut
-          -- See Note [Join points are less general than the paper]
-          -- in CoreSyn
-
-     ; (alt_ty, _) <- lintInTy alt_ty
-     ; (var_ty, _) <- lintInTy (idType var)
-
-     -- We used to try to check whether a case expression with no
-     -- alternatives was legitimate, but this didn't work.
-     -- See Note [No alternatives lint check] for details.
-
-     -- See Note [Rules for floating-point comparisons] in PrelRules
-     ; let isLitPat (LitAlt _, _ , _) = True
-           isLitPat _                 = False
-     ; checkL (not $ isFloatingTy scrut_ty && any isLitPat alts)
-         (ptext (sLit $ "Lint warning: Scrutinising floating-point " ++
-                        "expression with literal pattern in case " ++
-                        "analysis (see #9238).")
-          $$ text "scrut" <+> ppr scrut)
-
-     ; case tyConAppTyCon_maybe (idType var) of
-         Just tycon
-              | debugIsOn
-              , isAlgTyCon tycon
-              , not (isAbstractTyCon tycon)
-              , null (tyConDataCons tycon)
-              , not (exprIsBottom scrut)
-              -> pprTrace "Lint warning: case binder's type has no constructors" (ppr var <+> ppr (idType var))
-                        -- This can legitimately happen for type families
-                      $ return ()
-         _otherwise -> return ()
-
-        -- Don't use lintIdBndr on var, because unboxed tuple is legitimate
-
-     ; subst <- getTCvSubst
-     ; ensureEqTys var_ty scrut_ty (mkScrutMsg var var_ty scrut_ty subst)
-
-     ; lintBinder CaseBind var $ \_ ->
-       do { -- Check the alternatives
-            mapM_ (lintCoreAlt scrut_ty alt_ty) alts
-          ; checkCaseAlts e scrut_ty alts
-          ; return alt_ty } }
+lintCoreExpr (Case scrut var alt_ty alts)
+  = lintCaseExpr scrut var alt_ty alts
 
 -- This case can't happen; linting types in expressions gets routed through
 -- lintCoreArgs
@@ -1095,6 +1072,60 @@ lintTyKind tyvar arg_ty
 ************************************************************************
 -}
 
+lintCaseExpr :: CoreExpr -> Id -> Type -> [CoreAlt] -> LintM OutType
+lintCaseExpr scrut var alt_ty alts =
+  do { let e = Case scrut var alt_ty alts   -- Just for error messages
+
+     -- Check the scrutinee
+     ; scrut_ty <- markAllJoinsBad $ lintCoreExpr scrut
+          -- See Note [Join points are less general than the paper]
+          -- in CoreSyn
+
+     ; (alt_ty, _) <- addLoc (CaseTy scrut) $
+                      lintInTy alt_ty
+     ; (var_ty, _) <- addLoc (IdTy var) $
+                      lintInTy (idType var)
+
+     -- We used to try to check whether a case expression with no
+     -- alternatives was legitimate, but this didn't work.
+     -- See Note [No alternatives lint check] for details.
+
+     -- Check that the scrutinee is not a floating-point type
+     -- if there are any literal alternatives
+     -- See CoreSyn Note [Case expression invariants] item (5)
+     -- See Note [Rules for floating-point comparisons] in PrelRules
+     ; let isLitPat (LitAlt _, _ , _) = True
+           isLitPat _                 = False
+     ; checkL (not $ isFloatingTy scrut_ty && any isLitPat alts)
+         (ptext (sLit $ "Lint warning: Scrutinising floating-point " ++
+                        "expression with literal pattern in case " ++
+                        "analysis (see #9238).")
+          $$ text "scrut" <+> ppr scrut)
+
+     ; case tyConAppTyCon_maybe (idType var) of
+         Just tycon
+              | debugIsOn
+              , isAlgTyCon tycon
+              , not (isAbstractTyCon tycon)
+              , null (tyConDataCons tycon)
+              , not (exprIsBottom scrut)
+              -> pprTrace "Lint warning: case binder's type has no constructors" (ppr var <+> ppr (idType var))
+                        -- This can legitimately happen for type families
+                      $ return ()
+         _otherwise -> return ()
+
+        -- Don't use lintIdBndr on var, because unboxed tuple is legitimate
+
+     ; subst <- getTCvSubst
+     ; ensureEqTys var_ty scrut_ty (mkScrutMsg var var_ty scrut_ty subst)
+       -- See CoreSyn Note [Case expression invariants] item (7)
+
+     ; lintBinder CaseBind var $ \_ ->
+       do { -- Check the alternatives
+            mapM_ (lintCoreAlt scrut_ty alt_ty) alts
+          ; checkCaseAlts e scrut_ty alts
+          ; return alt_ty } }
+
 checkCaseAlts :: CoreExpr -> OutType -> [CoreAlt] -> LintM ()
 -- a) Check that the alts are non-empty
 -- b1) Check that the DEFAULT comes first, if it exists
@@ -1106,7 +1137,10 @@ checkCaseAlts :: CoreExpr -> OutType -> [CoreAlt] -> LintM ()
 
 checkCaseAlts e ty alts =
   do { checkL (all non_deflt con_alts) (mkNonDefltMsg e)
+         -- See CoreSyn Note [Case expression invariants] item (2)
+
      ; checkL (increasing_tag con_alts) (mkNonIncreasingAltsMsg e)
+         -- See CoreSyn Note [Case expression invariants] item (3)
 
           -- For types Int#, Word# with an infinite (well, large!) number of
           -- possible values, there should usually be a DEFAULT case
@@ -1136,6 +1170,7 @@ lintAltExpr :: CoreExpr -> OutType -> LintM ()
 lintAltExpr expr ann_ty
   = do { actual_ty <- lintCoreExpr expr
        ; ensureEqTys actual_ty ann_ty (mkCaseAltMsg expr actual_ty ann_ty) }
+         -- See CoreSyn Note [Case expression invariants] item (6)
 
 lintCoreAlt :: OutType          -- Type of scrutinee
             -> OutType          -- Type of the alternative
@@ -1246,7 +1281,8 @@ lintIdBndr top_lvl bind_site id linterF
        ; checkL (not (isExternalName (Var.varName id)) || is_top_lvl)
            (mkNonTopExternalNameMsg id)
 
-       ; (ty, k) <- lintInTy (idType id)
+       ; (ty, k) <- addLoc (IdTy id) $
+                    lintInTy (idType id)
 
           -- See Note [Levity polymorphism invariants] in CoreSyn
        ; lintL (isJoinId id || not (isKindLevPoly k))
@@ -2180,6 +2216,9 @@ data LintLocInfo
   | BodyOfLetRec [Id]   -- One of the binders
   | CaseAlt CoreAlt     -- Case alternative
   | CasePat CoreAlt     -- The *pattern* of the case alternative
+  | CaseTy CoreExpr     -- The type field of a case expression
+                        -- with this scrutinee
+  | IdTy Id             -- The type field of an Id binder
   | AnExpr CoreExpr     -- Some expression
   | ImportedUnfolding SrcLoc -- Some imported unfolding (ToDo: say which)
   | TopLevelBindings
@@ -2237,17 +2276,23 @@ addWarnL msg = LintM $ \ env (warns,errs) ->
 
 addMsg :: LintEnv ->  Bag MsgDoc -> MsgDoc -> Bag MsgDoc
 addMsg env msgs msg
-  = ASSERT( notNull locs )
+  = ASSERT( notNull loc_msgs )
     msgs `snocBag` mk_msg msg
   where
-   locs = le_loc env
-   (loc, cxt1) = dumpLoc (head locs)
-   cxts        = [snd (dumpLoc loc) | loc <- locs]
-   context     = ifPprDebug (vcat (reverse cxts) $$ cxt1 $$
-                             text "Substitution:" <+> ppr (le_subst env))
-                            cxt1
+   loc_msgs :: [(SrcLoc, SDoc)]  -- Innermost first
+   loc_msgs = map dumpLoc (le_loc env)
+
+   cxt_doc = vcat $ reverse $ map snd loc_msgs
+   context = cxt_doc $$ whenPprDebug extra
+   extra   = text "Substitution:" <+> ppr (le_subst env)
 
-   mk_msg msg = mkLocMessage SevWarning (mkSrcSpan loc loc) (context $$ msg)
+   msg_span = case [ span | (loc,_) <- loc_msgs
+                          , let span = srcLocSpan loc
+                          , isGoodSrcSpan span ] of
+               []    -> noSrcSpan
+               (s:_) -> s
+   mk_msg msg = mkLocMessage SevWarning msg_span
+                             (msg $$ context)
 
 addLoc :: LintLocInfo -> LintM a -> LintM a
 addLoc extra_loc m
@@ -2345,7 +2390,8 @@ lintTyCoVarInScope :: TyCoVar -> LintM ()
 lintTyCoVarInScope var
   = do { subst <- getTCvSubst
        ; lintL (var `isInScope` subst)
-               (pprBndr LetBind var <+> text "is out of scope") }
+               (hang (text "The variable" <+> pprBndr LetBind var)
+                   2 (text "is out of scope")) }
 
 ensureEqTys :: OutType -> OutType -> MsgDoc -> LintM ()
 -- check ty2 is subtype of ty1 (ie, has same structure but usage
@@ -2375,19 +2421,19 @@ lintRole co r1 r2
 dumpLoc :: LintLocInfo -> (SrcLoc, SDoc)
 
 dumpLoc (RhsOf v)
-  = (getSrcLoc v, brackets (text "RHS of" <+> pp_binders [v]))
+  = (getSrcLoc v, text "In the RHS of" <+> pp_binders [v])
 
 dumpLoc (LambdaBodyOf b)
-  = (getSrcLoc b, brackets (text "in body of lambda with binder" <+> pp_binder b))
+  = (getSrcLoc b, text "In the body of lambda with binder" <+> pp_binder b)
 
 dumpLoc (UnfoldingOf b)
-  = (getSrcLoc b, brackets (text "in the unfolding of" <+> pp_binder b))
+  = (getSrcLoc b, text "In the unfolding of" <+> pp_binder b)
 
 dumpLoc (BodyOfLetRec [])
-  = (noSrcLoc, brackets (text "In body of a letrec with no binders"))
+  = (noSrcLoc, text "In body of a letrec with no binders")
 
 dumpLoc (BodyOfLetRec bs@(_:_))
-  = ( getSrcLoc (head bs), brackets (text "in body of letrec with binders" <+> pp_binders bs))
+  = ( getSrcLoc (head bs), text "In the body of letrec with binders" <+> pp_binders bs)
 
 dumpLoc (AnExpr e)
   = (noSrcLoc, text "In the expression:" <+> ppr e)
@@ -2398,8 +2444,15 @@ dumpLoc (CaseAlt (con, args, _))
 dumpLoc (CasePat (con, args, _))
   = (noSrcLoc, text "In the pattern of a case alternative:" <+> parens (ppr con <+> pp_binders args))
 
+dumpLoc (CaseTy scrut)
+  = (noSrcLoc, hang (text "In the result-type of a case with scrutinee:")
+                  2 (ppr scrut))
+
+dumpLoc (IdTy b)
+  = (getSrcLoc b, text "In the type of a binder:" <+> ppr b)
+
 dumpLoc (ImportedUnfolding locn)
-  = (locn, brackets (text "in an imported unfolding"))
+  = (locn, text "In an imported unfolding")
 dumpLoc TopLevelBindings
   = (noSrcLoc, Outputable.empty)
 dumpLoc (InType ty)
diff --git a/compiler/coreSyn/CorePrep.hs b/compiler/coreSyn/CorePrep.hs
index 6be5346ab5..9d4044cf57 100644
--- a/compiler/coreSyn/CorePrep.hs
+++ b/compiler/coreSyn/CorePrep.hs
@@ -1274,7 +1274,7 @@ wrapBinds :: Floats -> CpeBody -> CpeBody
 wrapBinds (Floats _ binds) body
   = foldrOL mk_bind body binds
   where
-    mk_bind (FloatCase bndr rhs _) body = Case rhs bndr (exprType body) [(DEFAULT, [], body)]
+    mk_bind (FloatCase bndr rhs _) body = mkDefaultCase rhs bndr body
     mk_bind (FloatLet bind)        body = Let bind body
     mk_bind (FloatTick tickish)    body = mkTick tickish body
 
diff --git a/compiler/coreSyn/CoreSyn.hs b/compiler/coreSyn/CoreSyn.hs
index f8fb9ef971..d94761b237 100644
--- a/compiler/coreSyn/CoreSyn.hs
+++ b/compiler/coreSyn/CoreSyn.hs
@@ -201,40 +201,7 @@ These data types are the heart of the compiler
 --    The binder gets bound to the value of the scrutinee,
 --    and the 'Type' must be that of all the case alternatives
 --
---    #case_invariants#
---    This is one of the more complicated elements of the Core language,
---    and comes with a number of restrictions:
---
---    1. The list of alternatives may be empty;
---       See Note [Empty case alternatives]
---
---    2. The 'DEFAULT' case alternative must be first in the list,
---       if it occurs at all.
---
---    3. The remaining cases are in order of increasing
---         tag  (for 'DataAlts') or
---         lit  (for 'LitAlts').
---       This makes finding the relevant constructor easy,
---       and makes comparison easier too.
---
---    4. The list of alternatives must be exhaustive. An /exhaustive/ case
---       does not necessarily mention all constructors:
---
---       @
---            data Foo = Red | Green | Blue
---       ... case x of
---            Red   -> True
---            other -> f (case x of
---                            Green -> ...
---                            Blue  -> ... ) ...
---       @
---
---       The inner case does not need a @Red@ alternative, because @x@
---       can't be @Red@ at that program point.
---
---    5. Floating-point values must not be scrutinised against literals.
---       See #9238 and Note [Rules for floating-point comparisons]
---       in PrelRules for rationale.
+--    IMPORTANT: see Note [Case expression invariants]
 --
 -- *  Cast an expression to a particular type.
 --    This is used to implement @newtype@s (a @newtype@ constructor or
@@ -247,6 +214,41 @@ These data types are the heart of the compiler
 --
 -- *  A coercion
 
+{- Note [Why does Case have a 'Type' field?]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The obvious alternative is
+   exprType (Case scrut bndr alts)
+     | (_,_,rhs1):_ <- alts
+     = exprType rhs1
+
+But caching the type in the Case constructor
+  exprType (Case scrut bndr ty alts) = ty
+is better for at least three reasons:
+
+* It works when there are no alternatives (see case invarant 1 above)
+
+* It might be faster in deeply-nested situations.
+
+* It might not be quite the same as (exprType rhs) for one
+  of the RHSs in alts. 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) }
+   Then exprType of the RHS is (S a), but we cannot make that be
+   the 'ty' in the Case constructor because 'a' is simply not in
+   scope there. Instead we must expand the synonym to Int before
+   putting it in the Case constructor.  See CoreUtils.mkSingleAltCase.
+
+   So we'd have to do synonym expansion in exprType which would
+   be inefficient.
+
+* The type stored in the case is checked with lintInTy. This checks
+  (among other things) that it does not mention any variables that are
+  not in scope. If we did not have the type there, it would be a bit
+  harder for Core Lint to reject case blah of Ex x -> x where
+      data Ex = forall a. Ex a.
+-}
+
 -- If you edit this type, you may need to update the GHC formalism
 -- See Note [GHC Formalism] in coreSyn/CoreLint.hs
 data Expr b
@@ -255,7 +257,8 @@ data Expr b
   | App   (Expr b) (Arg b)
   | Lam   b (Expr b)
   | Let   (Bind b) (Expr b)
-  | Case  (Expr b) b Type [Alt b]       -- See #case_invariants#
+  | Case  (Expr b) b Type [Alt b]   -- See Note [Case expression invariants]
+                                    -- and Note [Why does Case have a 'Type' field?]
   | Cast  (Expr b) Coercion
   | Tick  (Tickish Id) (Expr b)
   | Type  Type
@@ -448,6 +451,71 @@ coreSyn/MkCore.
 For discussion of some implications of the let/app invariant primops see
 Note [Checking versus non-checking primops] in PrimOp.
 
+Note [Case expression invariants]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Case expressions are one of the more complicated elements of the Core
+language, and come with a number of invariants.  All of them should be
+checked by Core Lint.
+
+1. The list of alternatives may be empty;
+   See Note [Empty case alternatives]
+
+2. The 'DEFAULT' case alternative must be first in the list,
+   if it occurs at all.  Checked in CoreLint.checkCaseAlts.
+
+3. The remaining cases are in order of (strictly) increasing
+     tag  (for 'DataAlts') or
+     lit  (for 'LitAlts').
+   This makes finding the relevant constructor easy, and makes
+   comparison easier too.   Checked in CoreLint.checkCaseAlts.
+
+4. The list of alternatives must be exhaustive. An /exhaustive/ case
+   does not necessarily mention all constructors:
+
+   @
+        data Foo = Red | Green | Blue
+        ... case x of
+              Red   -> True
+              other -> f (case x of
+                              Green -> ...
+                              Blue  -> ... ) ...
+   @
+
+   The inner case does not need a @Red@ alternative, because @x@
+   can't be @Red@ at that program point.
+
+   This is not checked by Core Lint -- it's very hard to do so.
+   E.g. suppose that inner case was floated out, thus:
+         let a = case x of
+                   Green -> ...
+                   Blue  -> ... )
+         case x of
+           Red   -> True
+           other -> f a
+   Now it's really hard to see that the Green/Blue case is
+   exhaustive.  But it is.
+
+   If you have a case-expression that really /isn't/ exhaustive,
+   we may generate seg-faults.  Consider the Green/Blue case
+   above.  Since there are only two branches we may generate
+   code that tests for Green, and if not Green simply /assumes/
+   Blue (since, if the case is exhaustive, that's all that
+   remains).  Of course, if it's not Blue and we start fetching
+   fields that should be in a Blue constructor, we may die
+   horribly. See also Note [Core Lint guarantee] in CoreLint.
+
+5. Floating-point values must not be scrutinised against literals.
+   See #9238 and Note [Rules for floating-point comparisons]
+   in PrelRules for rationale.  Checked in lintCaseExpr;
+   see the call to isFloatingTy.
+
+6. The 'ty' field of (Case scrut bndr ty alts) is the type of the
+   /entire/ case expression.  Checked in lintAltExpr.
+   See also Note [Why does Case have a 'Type' field?].
+
+7. The type of the scrutinee must be the same as the type
+   of the case binder, obviously.  Checked in lintCaseExpr.
+
 Note [CoreSyn type and coercion invariant]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We allow a /non-recursive/, /non-top-level/ let to bind type and
@@ -1748,8 +1816,8 @@ ltAlt a1 a2 = (a1 `cmpAlt` a2) == LT
 
 cmpAltCon :: AltCon -> AltCon -> Ordering
 -- ^ Compares 'AltCon's within a single list of alternatives
--- DEFAULT comes out smallest, so that sorting by AltCon
--- puts alternatives in the order required by #case_invariants#
+-- DEFAULT comes out smallest, so that sorting by AltCon puts
+-- alternatives in the order required: see Note [Case expression invariants]
 cmpAltCon DEFAULT      DEFAULT     = EQ
 cmpAltCon DEFAULT      _           = LT
 
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.
diff --git a/compiler/coreSyn/MkCore.hs b/compiler/coreSyn/MkCore.hs
index e2c881a1c4..b451e61a63 100644
--- a/compiler/coreSyn/MkCore.hs
+++ b/compiler/coreSyn/MkCore.hs
@@ -7,6 +7,7 @@ module MkCore (
         mkCoreApp, mkCoreApps, mkCoreConApps,
         mkCoreLams, mkWildCase, mkIfThenElse,
         mkWildValBinder, mkWildEvBinder,
+        mkSingleAltCase,
         sortQuantVars, castBottomExpr,
 
         -- * Constructing boxed literals
@@ -57,7 +58,7 @@ import Id
 import Var      ( EvVar, setTyVarUnique )
 
 import CoreSyn
-import CoreUtils        ( exprType, needsCaseBinding, bindNonRec )
+import CoreUtils        ( exprType, needsCaseBinding, mkSingleAltCase, bindNonRec )
 import Literal
 import HscTypes
 
@@ -111,29 +112,34 @@ mkCoreLet (NonRec bndr rhs) body        -- See Note [CoreSyn let/app invariant]
 mkCoreLet bind body
   = Let bind body
 
+-- | Create a lambda where the given expression has a number of variables
+-- bound over it. The leftmost binder is that bound by the outermost
+-- lambda in the result
+mkCoreLams :: [CoreBndr] -> CoreExpr -> CoreExpr
+mkCoreLams = mkLams
+
 -- | Bind a list of binding groups over an expression. The leftmost binding
 -- group becomes the outermost group in the resulting expression
 mkCoreLets :: [CoreBind] -> CoreExpr -> CoreExpr
 mkCoreLets binds body = foldr mkCoreLet body binds
 
--- | Construct an expression which represents the application of one expression
--- paired with its type to an argument. The result is paired with its type. This
--- function is not exported and used in the definition of 'mkCoreApp' and
--- 'mkCoreApps'.
+-- | Construct an expression which represents the application of a number of
+-- expressions to that of a data constructor expression. The leftmost expression
+-- in the list is applied first
+mkCoreConApps :: DataCon -> [CoreExpr] -> CoreExpr
+mkCoreConApps con args = mkCoreApps (Var (dataConWorkId con)) args
+
+-- | Construct an expression which represents the application of a number of
+-- expressions to another. The leftmost expression in the list is applied first
 -- Respects the let/app invariant by building a case expression where necessary
 --   See CoreSyn Note [CoreSyn let/app invariant]
-mkCoreAppTyped :: SDoc -> (CoreExpr, Type) -> CoreExpr -> (CoreExpr, Type)
-mkCoreAppTyped _ (fun, fun_ty) (Type ty)
-  = (App fun (Type ty), piResultTy fun_ty ty)
-mkCoreAppTyped _ (fun, fun_ty) (Coercion co)
-  = (App fun (Coercion co), res_ty)
-  where
-    (_, res_ty) = splitFunTy fun_ty
-mkCoreAppTyped d (fun, fun_ty) arg
-  = ASSERT2( isFunTy fun_ty, ppr fun $$ ppr arg $$ d )
-    (mk_val_app fun arg arg_ty res_ty, res_ty)
+mkCoreApps :: CoreExpr -> [CoreExpr] -> CoreExpr
+mkCoreApps fun args
+  = fst $
+    foldl' (mkCoreAppTyped doc_string) (fun, fun_ty) args
   where
-    (arg_ty, res_ty) = splitFunTy fun_ty
+    doc_string = ppr fun_ty $$ ppr fun $$ ppr args
+    fun_ty = exprType fun
 
 -- | Construct an expression which represents the application of one expression
 -- to the other
@@ -143,47 +149,40 @@ mkCoreApp :: SDoc -> CoreExpr -> CoreExpr -> CoreExpr
 mkCoreApp s fun arg
   = fst $ mkCoreAppTyped s (fun, exprType fun) arg
 
--- | Construct an expression which represents the application of a number of
--- expressions to another. The leftmost expression in the list is applied first
+-- | Construct an expression which represents the application of one expression
+-- paired with its type to an argument. The result is paired with its type. This
+-- function is not exported and used in the definition of 'mkCoreApp' and
+-- 'mkCoreApps'.
 -- Respects the let/app invariant by building a case expression where necessary
 --   See CoreSyn Note [CoreSyn let/app invariant]
-mkCoreApps :: CoreExpr -> [CoreExpr] -> CoreExpr
-mkCoreApps fun args
-  = fst $
-    foldl' (mkCoreAppTyped doc_string) (fun, fun_ty) args
+mkCoreAppTyped :: SDoc -> (CoreExpr, Type) -> CoreExpr -> (CoreExpr, Type)
+mkCoreAppTyped _ (fun, fun_ty) (Type ty)
+  = (App fun (Type ty), piResultTy fun_ty ty)
+mkCoreAppTyped _ (fun, fun_ty) (Coercion co)
+  = (App fun (Coercion co), funResultTy fun_ty)
+mkCoreAppTyped d (fun, fun_ty) arg
+  = ASSERT2( isFunTy fun_ty, ppr fun $$ ppr arg $$ d )
+    (mkValApp fun arg arg_ty res_ty, res_ty)
   where
-    doc_string = ppr fun_ty $$ ppr fun $$ ppr args
-    fun_ty = exprType fun
-
--- | Construct an expression which represents the application of a number of
--- expressions to that of a data constructor expression. The leftmost expression
--- in the list is applied first
-mkCoreConApps :: DataCon -> [CoreExpr] -> CoreExpr
-mkCoreConApps con args = mkCoreApps (Var (dataConWorkId con)) args
+    (arg_ty, res_ty) = splitFunTy fun_ty
 
-mk_val_app :: CoreExpr -> CoreExpr -> Type -> Type -> CoreExpr
+mkValApp :: CoreExpr -> CoreExpr -> Type -> Type -> CoreExpr
 -- Build an application (e1 e2),
 -- or a strict binding  (case e2 of x -> e1 x)
 -- using the latter when necessary to respect the let/app invariant
 --   See Note [CoreSyn let/app invariant]
-mk_val_app fun arg arg_ty res_ty
+mkValApp fun arg arg_ty res_ty
   | not (needsCaseBinding arg_ty arg)
   = App fun arg                -- The vastly common case
-
   | otherwise
-  = Case arg arg_id res_ty [(DEFAULT,[],App fun (Var arg_id))]
-  where
-    arg_id = mkWildValBinder arg_ty
-        -- Lots of shadowing, but it doesn't matter,
-        -- because 'fun ' should not have a free wild-id
-        --
-        -- This is Dangerous.  But this is the only place we play this
-        -- game, mk_val_app returns an expression that does not have
-        -- a free wild-id.  So the only thing that can go wrong
-        -- is if you take apart this case expression, and pass a
-        -- fragment of it as the fun part of a 'mk_val_app'.
+  = mkStrictApp fun arg arg_ty res_ty
+
+{- *********************************************************************
+*                                                                      *
+              Building case expressions
+*                                                                      *
+********************************************************************* -}
 
------------
 mkWildEvBinder :: PredType -> EvVar
 mkWildEvBinder pred = mkWildValBinder pred
 
@@ -197,10 +196,29 @@ mkWildValBinder ty = mkLocalIdOrCoVar wildCardName ty
 
 mkWildCase :: CoreExpr -> Type -> Type -> [CoreAlt] -> CoreExpr
 -- Make a case expression whose case binder is unused
--- The alts should not have any occurrences of WildId
+-- The alts and res_ty should not have any occurrences of WildId
 mkWildCase scrut scrut_ty res_ty alts
   = Case scrut (mkWildValBinder scrut_ty) res_ty alts
 
+mkStrictApp :: CoreExpr -> CoreExpr -> Type -> Type -> CoreExpr
+-- Build a strict application (case e2 of x -> e1 x)
+mkStrictApp fun arg arg_ty res_ty
+  = Case arg arg_id res_ty [(DEFAULT,[],App fun (Var arg_id))]
+       -- mkDefaultCase looks attractive here, and would be sound.
+       -- But it uses (exprType alt_rhs) to compute the result type,
+       -- whereas here we already know that the result type is res_ty
+  where
+    arg_id = mkWildValBinder arg_ty
+        -- Lots of shadowing, but it doesn't matter,
+        -- because 'fun' and 'res_ty' should not have a free wild-id
+        --
+        -- This is Dangerous.  But this is the only place we play this
+        -- game, mkStrictApp returns an expression that does not have
+        -- a free wild-id.  So the only way 'fun' could get a free wild-id
+        -- would be if you take apart this case expression (or some other
+        -- expression that uses mkWildValBinder, of which there are not
+        -- many), and pass a fragment of it as the fun part of a 'mkStrictApp'.
+
 mkIfThenElse :: CoreExpr -> CoreExpr -> CoreExpr -> CoreExpr
 mkIfThenElse guard then_expr else_expr
 -- Not going to be refining, so okay to take the type of the "then" clause
@@ -219,17 +237,6 @@ castBottomExpr e res_ty
     e_ty = exprType e
 
 {-
-The functions from this point don't really do anything cleverer than
-their counterparts in CoreSyn, but they are here for consistency
--}
-
--- | Create a lambda where the given expression has a number of variables
--- bound over it. The leftmost binder is that bound by the outermost
--- lambda in the result
-mkCoreLams :: [CoreBndr] -> CoreExpr -> CoreExpr
-mkCoreLams = mkLams
-
-{-
 ************************************************************************
 *                                                                      *
 \subsection{Making literals}
@@ -558,7 +565,7 @@ instance Outputable FloatBind where
 
 wrapFloat :: FloatBind -> CoreExpr -> CoreExpr
 wrapFloat (FloatLet defns)       body = Let defns body
-wrapFloat (FloatCase e b con bs) body = Case e b (exprType body) [(con, bs, body)]
+wrapFloat (FloatCase e b con bs) body = mkSingleAltCase e b con bs body
 
 -- | Applies the floats from right to left. That is @wrapFloats [b1, b2, …, bn]
 -- u = let b1 in let b2 in … in let bn in u@
diff --git a/compiler/deSugar/DsUtils.hs b/compiler/deSugar/DsUtils.hs
index 7d39b4a3c6..14dab29b30 100644
--- a/compiler/deSugar/DsUtils.hs
+++ b/compiler/deSugar/DsUtils.hs
@@ -243,8 +243,7 @@ wrapBind new old body   -- NB: this function must deal with term
   | otherwise   = Let (NonRec new (varToCoreExpr old)) body
 
 seqVar :: Var -> CoreExpr -> CoreExpr
-seqVar var body = Case (Var var) var (exprType body)
-                        [(DEFAULT, [], body)]
+seqVar var body = mkDefaultCase (Var var) var body
 
 mkCoLetMatchResult :: CoreBind -> MatchResult -> MatchResult
 mkCoLetMatchResult bind = adjustMatchResult (mkCoreLet bind)
diff --git a/compiler/simplCore/SimplUtils.hs b/compiler/simplCore/SimplUtils.hs
index 63c216fce2..4eeb51ceaa 100644
--- a/compiler/simplCore/SimplUtils.hs
+++ b/compiler/simplCore/SimplUtils.hs
@@ -2212,8 +2212,10 @@ mkCase2 dflags scrut bndr alts_ty alts
            ; return (ex_tvs ++ arg_ids) }
     mk_new_bndrs _ _ = return []
 
-    re_sort :: [CoreAlt] -> [CoreAlt]  -- Re-sort the alternatives to
-    re_sort alts = sortBy cmpAlt alts  -- preserve the #case_invariants#
+    re_sort :: [CoreAlt] -> [CoreAlt]
+    -- Sort the alternatives to re-establish
+    -- CoreSyn Note [Case expression invariants]
+    re_sort alts = sortBy cmpAlt alts
 
     add_default :: [CoreAlt] -> [CoreAlt]
     -- See Note [Literal cases]
diff --git a/compiler/stranal/WwLib.hs b/compiler/stranal/WwLib.hs
index f346324f4d..5e4d22857a 100644
--- a/compiler/stranal/WwLib.hs
+++ b/compiler/stranal/WwLib.hs
@@ -16,7 +16,7 @@ module WwLib ( mkWwBodies, mkWWstr, mkWorkerArgs
 import GhcPrelude
 
 import CoreSyn
-import CoreUtils        ( exprType, mkCast )
+import CoreUtils        ( exprType, mkCast, mkDefaultCase, mkSingleAltCase )
 import Id
 import IdInfo           ( JoinArity )
 import DataCon
@@ -1027,7 +1027,7 @@ mkWWcpr_help (data_con, inst_tys, arg_tys, co)
              con_app   = mkConApp2 data_con inst_tys [arg] `mkCast` mkSymCo co
 
        ; return ( True
-                , \ wkr_call -> Case wkr_call arg (exprType con_app) [(DEFAULT, [], con_app)]
+                , \ wkr_call -> mkDefaultCase wkr_call arg con_app
                 , \ body     -> mkUnpackCase body co work_uniq data_con [arg] (varToCoreExpr arg)
                                 -- varToCoreExpr important here: arg can be a coercion
                                 -- Lacking this caused #10658
@@ -1042,9 +1042,11 @@ mkWWcpr_help (data_con, inst_tys, arg_tys, co)
              ubx_tup_ty  = exprType ubx_tup_app
              ubx_tup_app = mkCoreUbxTup (map fst arg_tys) (map varToCoreExpr args)
              con_app     = mkConApp2 data_con inst_tys args `mkCast` mkSymCo co
+             tup_con     = tupleDataCon Unboxed (length arg_tys)
 
        ; return (True
-                , \ wkr_call -> Case wkr_call wrap_wild (exprType con_app)  [(DataAlt (tupleDataCon Unboxed (length arg_tys)), args, con_app)]
+                , \ wkr_call -> mkSingleAltCase wkr_call wrap_wild
+                                                (DataAlt tup_con) args con_app
                 , \ body     -> mkUnpackCase body co work_uniq data_con args ubx_tup_app
                 , ubx_tup_ty ) }
 
@@ -1056,8 +1058,8 @@ mkUnpackCase ::  CoreExpr -> Coercion -> Unique -> DataCon -> [Id] -> CoreExpr -
 mkUnpackCase (Tick tickish e) co uniq con args body   -- See Note [Profiling and unpacking]
   = Tick tickish (mkUnpackCase e co uniq con args body)
 mkUnpackCase scrut co uniq boxing_con unpk_args body
-  = Case casted_scrut bndr (exprType body)
-         [(DataAlt boxing_con, unpk_args, body)]
+  = mkSingleAltCase casted_scrut bndr
+                    (DataAlt boxing_con) unpk_args body
   where
     casted_scrut = scrut `mkCast` co
     bndr = mk_ww_local uniq (exprType casted_scrut, MarkedStrict)
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index 39a07c2fed..d8664eba62 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -2825,6 +2825,10 @@ occCheckExpand :: [Var] -> Type -> Maybe Type
 -- of the given type variable.  If the type is already syntactically
 -- free of the variable, then the same type is returned.
 occCheckExpand vs_to_avoid ty
+  | null vs_to_avoid  -- Efficient shortcut
+  = Just ty           -- Can happen, eg. CoreUtils.mkSingleAltCase
+
+  | otherwise
   = go (mkVarSet vs_to_avoid, emptyVarEnv) ty
   where
     go :: (VarSet, VarEnv TyCoVar) -> Type -> Maybe Type
diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index bbc32c8115..823244ebca 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -40,7 +40,7 @@ test('T12742', normal, compile, [''])
 #       (1) Use -fexternal-interpreter, or
 #       (2) Build the program twice: once with -dynamic, and then
 #           with -prof using -osuf to set a different object file suffix.
-test('T13910', [expect_broken_for(16537, ['optasm']), omit_ways(['profasm'])], compile, [''])
+test('T13910', [omit_ways(['profasm'])], compile, [''])
 test('T13938', [req_th, extra_files(['T13938a.hs'])], makefile_test, ['T13938'])
 test('T14556', normal, compile, [''])
 test('T14720', normal, compile, [''])
diff --git a/testsuite/tests/indexed-types/should_compile/T17056.hs b/testsuite/tests/indexed-types/should_compile/T17056.hs
new file mode 100644
index 0000000000..d22d1dfcdc
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T17056.hs
@@ -0,0 +1,47 @@
+-- This test tripped Core Lint by producing a
+-- case expression whose 'type' field included an
+-- out of scope variable because of a phantom type
+-- synonym
+
+{-# OPTIONS_GHC -O #-}
+
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+module Bug where
+
+import Data.Kind (Type)
+import Data.Type.Equality ((:~:)(..))
+
+type IsInt a = Int :~: a
+
+data Sing :: forall (b :: Type). IsInt b -> Type where
+  SRefl :: Sing Refl
+
+data SomeSing :: Type -> Type where
+  SomeSing :: Sing (x :: IsInt b) -> SomeSing b
+
+type WhyCastWith    (e :: IsInt b) = b
+-- Type /synonym/
+--   WhyCastWith b (e :: IsInt b) = b
+
+type family   Apply (e :: IsInt b) :: Type
+type instance Apply (e :: IsInt b) = WhyCastWith e
+
+-- axiom   Apply (b :: *) (e :: IsInt b) ~ WhyCastWith e
+
+(~>:~:) :: forall (b :: Type) (r :: IsInt b).
+           Sing r
+        -> Apply r
+(~>:~:) SRefl = let w = w in w
+
+castWith :: forall b. IsInt b ->  b
+castWith eq
+  = case (case eq of Refl -> SomeSing SRefl) :: SomeSing b of
+      SomeSing SRefl -> (~>:~:) @b SRefl
diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T
index 7eeeda6d59..1ee797ca41 100644
--- a/testsuite/tests/indexed-types/should_compile/all.T
+++ b/testsuite/tests/indexed-types/should_compile/all.T
@@ -292,3 +292,4 @@ test('T16356_Compile2', normal, compile, [''])
 test('T16632', normal, compile, ['-Wunused-type-patterns -fdiagnostics-show-caret'])
 test('T16828', normal, compile, [''])
 test('T17008b', normal, compile, [''])
+test('T17056', normal, compile, [''])