Fix TypeData issues (fixes #22315 and #22332)

There were two bugs here:

1. Treating type-level constructors as PromotedDataCon doesn't always
   work, in particular because constructors promoted via DataKinds are
   called both T and 'T. (Tests T22332a, T22332b, T22315a, T22315b)
   Fix: guard these cases with isDataKindsPromotedDataCon.

2. Type-level constructors were sent to the code generator, producing
   things like constructor wrappers. (Tests T22332a, T22332b)
   Fix: test for them in isDataTyCon.

Other changes:

* changed the marking of "type data" DataCon's as suggested by SPJ.

* added a test TDGADT for a type-level GADT.

* comment tweaks

* change tcIfaceTyCon to ignore IfaceTyConInfo, so that IfaceTyConInfo
  is used only for pretty printing, not for typechecking. (SPJ)

14 files changed, 104 insertions, 0 deletions

diff --git a/testsuite/tests/type-data/should_compile/T22315a/Lib.hs b/testsuite/tests/type-data/should_compile/T22315a/Lib.hs
new file mode 100644
index 0000000000..a705db82f7
--- /dev/null
+++ b/testsuite/tests/type-data/should_compile/T22315a/Lib.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE DataKinds, TypeData #-}
+module T22315a.Lib where
+
+data TermLevel = Mk
+type data TypeLevel = Mk
+
+class C (a :: TypeLevel)
+instance C Mk where
+
+foo :: C a => proxy a -> ()
+foo _ = ()
diff --git a/testsuite/tests/type-data/should_compile/T22315a/Main.hs b/testsuite/tests/type-data/should_compile/T22315a/Main.hs
new file mode 100644
index 0000000000..6089f788d6
--- /dev/null
+++ b/testsuite/tests/type-data/should_compile/T22315a/Main.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+module T22315a.Main where
+
+import T22315a.Lib
+
+data Proxy (a :: TypeLevel)
+
+bar :: Proxy Mk -> ()
+bar = foo
diff --git a/testsuite/tests/type-data/should_compile/TDGADT.hs b/testsuite/tests/type-data/should_compile/TDGADT.hs
new file mode 100644
index 0000000000..a286e60680
--- /dev/null
+++ b/testsuite/tests/type-data/should_compile/TDGADT.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE TypeData #-}
+module TDGADT where
+
+import Data.Kind (Type)
+
+type data Nat = Zero | Succ Nat
+
+-- type level GADT
+type data Vec :: Nat -> Type -> Type where
+    VNil :: Vec Zero a
+    VCons :: a -> Vec n a -> Vec (Succ n) a
+
+type X = VCons Bool (VCons Int VNil)
diff --git a/testsuite/tests/type-data/should_compile/all.T b/testsuite/tests/type-data/should_compile/all.T
index 0f8294bee7..b5e9810b00 100644
--- a/testsuite/tests/type-data/should_compile/all.T
+++ b/testsuite/tests/type-data/should_compile/all.T
@@ -1,4 +1,6 @@
 test('TDDataConstructor', normal, compile, [''])
 test('TDExistential', normal, compile, [''])
+test('TDGADT', normal, compile, [''])
 test('TDGoodConsConstraints', normal, compile, [''])
 test('TDVector', normal, compile, [''])
+test('T22315a', [extra_files(['T22315a/'])], multimod_compile, ['T22315a.Lib T22315a.Main', '-v0'])
diff --git a/testsuite/tests/type-data/should_fail/T22332b.hs b/testsuite/tests/type-data/should_fail/T22332b.hs
new file mode 100644
index 0000000000..f13e15ba9c
--- /dev/null
+++ b/testsuite/tests/type-data/should_fail/T22332b.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE TypeData, DataKinds #-}
+module T22332b where
+
+type data X1 = T
+data X2 = T
+data Proxy a
+
+f :: Proxy T
+f = f :: Proxy 'T
diff --git a/testsuite/tests/type-data/should_fail/T22332b.stderr b/testsuite/tests/type-data/should_fail/T22332b.stderr
new file mode 100644
index 0000000000..26fd44a45f
--- /dev/null
+++ b/testsuite/tests/type-data/should_fail/T22332b.stderr
@@ -0,0 +1,7 @@
+
+T22332b.hs:9:5: error: [GHC-83865]
+    • Couldn't match type ‘T’ with ‘'T’
+      Expected: Proxy 'T
+        Actual: Proxy T
+    • In the expression: f :: Proxy 'T
+      In an equation for ‘f’: f = f :: Proxy 'T
diff --git a/testsuite/tests/type-data/should_fail/all.T b/testsuite/tests/type-data/should_fail/all.T
index ddf7bd86bd..82b257df22 100644
--- a/testsuite/tests/type-data/should_fail/all.T
+++ b/testsuite/tests/type-data/should_fail/all.T
@@ -11,3 +11,4 @@ test('TDRecordsH98', normal, compile_fail, [''])
 test('TDRecursive', normal, compile_fail, [''])
 test('TDStrictnessGADT', normal, compile_fail, [''])
 test('TDStrictnessH98', normal, compile_fail, [''])
+test('T22332b', normal, compile_fail, [''])
diff --git a/testsuite/tests/type-data/should_run/Makefile b/testsuite/tests/type-data/should_run/Makefile
new file mode 100644
index 0000000000..9101fbd40a
--- /dev/null
+++ b/testsuite/tests/type-data/should_run/Makefile
@@ -0,0 +1,3 @@
+TOP=../../..
+include $(TOP)/mk/boilerplate.mk
+include $(TOP)/mk/test.mk
diff --git a/testsuite/tests/type-data/should_run/T22315b.hs b/testsuite/tests/type-data/should_run/T22315b.hs
new file mode 100644
index 0000000000..ce58e8ae1c
--- /dev/null
+++ b/testsuite/tests/type-data/should_run/T22315b.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE TypeData #-}
+module T22315b where
+
+data TermLevel = Mk
+type data TypeLevel = Mk
+
+mk = Mk
+
+type Mk2 = Mk
diff --git a/testsuite/tests/type-data/should_run/T22315b.script b/testsuite/tests/type-data/should_run/T22315b.script
new file mode 100644
index 0000000000..fff5aa2d98
--- /dev/null
+++ b/testsuite/tests/type-data/should_run/T22315b.script
@@ -0,0 +1,5 @@
+:load T22315b.hs
+:type Mk
+:kind Mk
+:type mk
+:kind Mk2
diff --git a/testsuite/tests/type-data/should_run/T22315b.stdout b/testsuite/tests/type-data/should_run/T22315b.stdout
new file mode 100644
index 0000000000..f071fb1724
--- /dev/null
+++ b/testsuite/tests/type-data/should_run/T22315b.stdout
@@ -0,0 +1,4 @@
+Mk :: TermLevel
+Mk :: TypeLevel
+mk :: TermLevel
+Mk2 :: TypeLevel
diff --git a/testsuite/tests/type-data/should_run/T22332a.hs b/testsuite/tests/type-data/should_run/T22332a.hs
new file mode 100644
index 0000000000..bddb9065c5
--- /dev/null
+++ b/testsuite/tests/type-data/should_run/T22332a.hs
@@ -0,0 +1,27 @@
+{-# LANGUAGE TypeData, DataKinds, TypeFamilies #-}
+module Main where
+
+import Type.Reflection
+import Data.Type.Equality
+
+data Proxy a
+type data X1 = T -- defines type constructor T
+data X2 = T      -- defines type constructor 'T
+
+data family F p
+
+newtype instance F (Proxy T) = ID (forall a. a -> a)
+newtype instance F (Proxy 'T) = UC (forall a b. a -> b)
+
+-- This should fail at runtime because these are different types
+eq :: T :~~: 'T
+Just eq = eqTypeRep typeRep typeRep
+
+p :: a :~~: b -> F (Proxy a) :~: F (Proxy b)
+p HRefl = Refl
+
+uc :: a -> b
+uc = case castWith (p eq) (ID id) of UC a -> a
+
+main :: IO ()
+main = print (uc 'a' :: Int)
diff --git a/testsuite/tests/type-data/should_run/T22332a.stderr b/testsuite/tests/type-data/should_run/T22332a.stderr
new file mode 100644
index 0000000000..693ad69986
--- /dev/null
+++ b/testsuite/tests/type-data/should_run/T22332a.stderr
@@ -0,0 +1 @@
+T22332a: T22332a.hs:18:1-35: Non-exhaustive patterns in Just eq
diff --git a/testsuite/tests/type-data/should_run/all.T b/testsuite/tests/type-data/should_run/all.T
new file mode 100644
index 0000000000..f1faf7796e
--- /dev/null
+++ b/testsuite/tests/type-data/should_run/all.T
@@ -0,0 +1,2 @@
+test('T22332a', exit_code(1), compile_and_run, [''])
+test('T22315b', extra_files(['T22315b.hs']), ghci_script, ['T22315b.script'])