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

2 files changed, 48 insertions, 0 deletions

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, [''])