Allow visible type application for levity-poly data cons

This patch was driven by #18481, to allow visible type application
for levity-polymorphic newtypes. As so often, it started simple
but grew:

* Significant refactor: I removed HsConLikeOut from the
  client-independent Language.Haskell.Syntax.Expr, and put it where it
  belongs, as a new constructor `ConLikeTc` in the GHC-specific extension
  data type for expressions, `GHC.Hs.Expr.XXExprGhcTc`.

  That changed touched a lot of files in a very superficial way.

* Note [Typechecking data constructors] explains the main payload.
  The eta-expansion part is no longer done by the typechecker, but
  instead deferred to the desugarer, via `ConLikeTc`

* A little side benefit is that I was able to restore VTA for
  data types with a "stupid theta": #19775.  Not very important,
  but the code in GHC.Tc.Gen.Head.tcInferDataCon is is much, much
  more elegant now.

* I had to refactor the levity-polymorphism checking code in
  GHC.HsToCore.Expr, see
     Note [Checking for levity-polymorphic functions]
     Note [Checking levity-polymorphic data constructors]

9 files changed, 234 insertions, 103 deletions

diff --git a/testsuite/tests/codeGen/should_fail/T13233.stderr b/testsuite/tests/codeGen/should_fail/T13233.stderr
index 6f1636e544..0208b2695a 100644
--- a/testsuite/tests/codeGen/should_fail/T13233.stderr
+++ b/testsuite/tests/codeGen/should_fail/T13233.stderr
@@ -1,9 +1,23 @@
 
+T13233.hs:14:11: error:
+    Cannot use function with levity-polymorphic arguments:
+      (#,#) :: a -> a -> (# a, a #)
+    (Note that levity-polymorphic primops such as 'coerce' and unboxed tuples
+    are eta-expanded internally because they must occur fully saturated.
+    Use -fprint-typechecker-elaboration to display the full expression.)
+    Levity-polymorphic arguments:
+      a :: TYPE rep
+      a :: TYPE rep
+
 T13233.hs:22:16: error:
-    A levity-polymorphic type is not allowed here:
-      Type: a
-      Kind: TYPE rep1
-    When trying to create a variable of type: a
+    Cannot use function with levity-polymorphic arguments:
+      (#,#) :: a -> b -> (# a, b #)
+    (Note that levity-polymorphic primops such as 'coerce' and unboxed tuples
+    are eta-expanded internally because they must occur fully saturated.
+    Use -fprint-typechecker-elaboration to display the full expression.)
+    Levity-polymorphic arguments:
+      a :: TYPE rep1
+      b :: TYPE rep2
 
 T13233.hs:27:10: error:
     Cannot use function with levity-polymorphic arguments:
diff --git a/testsuite/tests/codeGen/should_fail/T13233_elab.stderr b/testsuite/tests/codeGen/should_fail/T13233_elab.stderr
index 6a069752f7..ec9a04d726 100644
--- a/testsuite/tests/codeGen/should_fail/T13233_elab.stderr
+++ b/testsuite/tests/codeGen/should_fail/T13233_elab.stderr
@@ -1,15 +1,24 @@
 
+T13233_elab.hs:17:11: error:
+    Cannot use function with levity-polymorphic arguments:
+      (#,#) @rep @rep @a @a :: a -> a -> (# a, a #)
+    Levity-polymorphic arguments:
+      a :: TYPE rep
+      a :: TYPE rep
+
 T13233_elab.hs:25:16: error:
-    A levity-polymorphic type is not allowed here:
-      Type: a
-      Kind: TYPE rep1
-    When trying to create a variable of type: a
+    Cannot use function with levity-polymorphic arguments:
+      (#,#) @rep1 @rep2 @a @b :: a -> b -> (# a, b #)
+    Levity-polymorphic arguments:
+      a :: TYPE rep1
+      b :: TYPE rep2
 
 T13233_elab.hs:33:10: error:
     Cannot use function with levity-polymorphic arguments:
-      mkWeak# @rep @a @b @c :: a
-                               -> b
-                               -> (State# RealWorld -> (# State# RealWorld, c #))
-                               -> State# RealWorld
-                               -> (# State# RealWorld, Weak# b #)
+      mkWeak# @rep @a @b @c
+        :: a
+           -> b
+           -> (State# RealWorld -> (# State# RealWorld, c #))
+           -> State# RealWorld
+           -> (# State# RealWorld, Weak# b #)
     Levity-polymorphic arguments: a :: TYPE rep
diff --git a/testsuite/tests/parser/should_compile/DumpTypecheckedAst.stderr b/testsuite/tests/parser/should_compile/DumpTypecheckedAst.stderr
index 1ba86ee6ef..5302fd7e7b 100644
--- a/testsuite/tests/parser/should_compile/DumpTypecheckedAst.stderr
+++ b/testsuite/tests/parser/should_compile/DumpTypecheckedAst.stderr
@@ -69,9 +69,11 @@
                   []))
                 (L
                  (SrcSpanAnn (EpAnnNotUsed) { <no location info> })
-                 (HsConLikeOut
-                  (NoExtField)
-                  ({abstract:ConLike})))
+                 (XExpr
+                  (ConLikeTc
+                   ({abstract:ConLike})
+                   []
+                   [])))
                 (L
                  (SrcSpanAnn (EpAnnNotUsed) { <no location info> })
                  (HsLit
@@ -117,9 +119,11 @@
                 []))
               (L
                (SrcSpanAnn (EpAnnNotUsed) { <no location info> })
-               (HsConLikeOut
-                (NoExtField)
-                ({abstract:ConLike})))
+               (XExpr
+                (ConLikeTc
+                 ({abstract:ConLike})
+                 []
+                 [])))
               (L
                (SrcSpanAnn (EpAnnNotUsed) { <no location info> })
                (HsLit
@@ -219,9 +223,11 @@
                   []))
                 (L
                  (SrcSpanAnn (EpAnnNotUsed) { <no location info> })
-                 (HsConLikeOut
-                  (NoExtField)
-                  ({abstract:ConLike})))
+                 (XExpr
+                  (ConLikeTc
+                   ({abstract:ConLike})
+                   []
+                   [])))
                 (L
                  (SrcSpanAnn (EpAnnNotUsed) { <no location info> })
                  (HsLit
@@ -267,9 +273,11 @@
                 []))
               (L
                (SrcSpanAnn (EpAnnNotUsed) { <no location info> })
-               (HsConLikeOut
-                (NoExtField)
-                ({abstract:ConLike})))
+               (XExpr
+                (ConLikeTc
+                 ({abstract:ConLike})
+                 []
+                 [])))
               (L
                (SrcSpanAnn (EpAnnNotUsed) { <no location info> })
                (HsLit
@@ -369,9 +377,11 @@
                   []))
                 (L
                  (SrcSpanAnn (EpAnnNotUsed) { <no location info> })
-                 (HsConLikeOut
-                  (NoExtField)
-                  ({abstract:ConLike})))
+                 (XExpr
+                  (ConLikeTc
+                   ({abstract:ConLike})
+                   []
+                   [])))
                 (L
                  (SrcSpanAnn (EpAnnNotUsed) { <no location info> })
                  (HsLit
@@ -417,9 +427,11 @@
                 []))
               (L
                (SrcSpanAnn (EpAnnNotUsed) { <no location info> })
-               (HsConLikeOut
-                (NoExtField)
-                ({abstract:ConLike})))
+               (XExpr
+                (ConLikeTc
+                 ({abstract:ConLike})
+                 []
+                 [])))
               (L
                (SrcSpanAnn (EpAnnNotUsed) { <no location info> })
                (HsLit
@@ -519,9 +531,11 @@
                   []))
                 (L
                  (SrcSpanAnn (EpAnnNotUsed) { <no location info> })
-                 (HsConLikeOut
-                  (NoExtField)
-                  ({abstract:ConLike})))
+                 (XExpr
+                  (ConLikeTc
+                   ({abstract:ConLike})
+                   []
+                   [])))
                 (L
                  (SrcSpanAnn (EpAnnNotUsed) { <no location info> })
                  (HsLit
@@ -567,9 +581,11 @@
                 []))
               (L
                (SrcSpanAnn (EpAnnNotUsed) { <no location info> })
-               (HsConLikeOut
-                (NoExtField)
-                ({abstract:ConLike})))
+               (XExpr
+                (ConLikeTc
+                 ({abstract:ConLike})
+                 []
+                 [])))
               (L
                (SrcSpanAnn (EpAnnNotUsed) { <no location info> })
                (HsLit
@@ -669,9 +685,11 @@
                   []))
                 (L
                  (SrcSpanAnn (EpAnnNotUsed) { <no location info> })
-                 (HsConLikeOut
-                  (NoExtField)
-                  ({abstract:ConLike})))
+                 (XExpr
+                  (ConLikeTc
+                   ({abstract:ConLike})
+                   []
+                   [])))
                 (L
                  (SrcSpanAnn (EpAnnNotUsed) { <no location info> })
                  (HsLit
@@ -717,9 +735,11 @@
                 []))
               (L
                (SrcSpanAnn (EpAnnNotUsed) { <no location info> })
-               (HsConLikeOut
-                (NoExtField)
-                ({abstract:ConLike})))
+               (XExpr
+                (ConLikeTc
+                 ({abstract:ConLike})
+                 []
+                 [])))
               (L
                (SrcSpanAnn (EpAnnNotUsed) { <no location info> })
                (HsLit
@@ -769,9 +789,11 @@
         []))
       (L
        (SrcSpanAnn (EpAnnNotUsed) { <no location info> })
-       (HsConLikeOut
-        (NoExtField)
-        ({abstract:ConLike})))
+       (XExpr
+        (ConLikeTc
+         ({abstract:ConLike})
+         []
+         [])))
       (L
        (SrcSpanAnn (EpAnnNotUsed) { <no location info> })
        (HsLit
@@ -805,9 +827,11 @@
         []))
       (L
        (SrcSpanAnn (EpAnnNotUsed) { <no location info> })
-       (HsConLikeOut
-        (NoExtField)
-        ({abstract:ConLike})))
+       (XExpr
+        (ConLikeTc
+         ({abstract:ConLike})
+         []
+         [])))
       (L
        (SrcSpanAnn (EpAnnNotUsed) { <no location info> })
        (HsLit
@@ -841,9 +865,11 @@
         []))
       (L
        (SrcSpanAnn (EpAnnNotUsed) { <no location info> })
-       (HsConLikeOut
-        (NoExtField)
-        ({abstract:ConLike})))
+       (XExpr
+        (ConLikeTc
+         ({abstract:ConLike})
+         []
+         [])))
       (L
        (SrcSpanAnn (EpAnnNotUsed) { <no location info> })
        (HsLit
@@ -887,9 +913,11 @@
           []))
         (L
          (SrcSpanAnn (EpAnnNotUsed) { <no location info> })
-         (HsConLikeOut
-          (NoExtField)
-          ({abstract:ConLike})))
+         (XExpr
+          (ConLikeTc
+           ({abstract:ConLike})
+           []
+           [])))
         (L
          (SrcSpanAnn (EpAnnNotUsed) { <no location info> })
          (HsVar
@@ -931,9 +959,11 @@
           []))
         (L
          (SrcSpanAnn (EpAnnNotUsed) { <no location info> })
-         (HsConLikeOut
-          (NoExtField)
-          ({abstract:ConLike})))
+         (XExpr
+          (ConLikeTc
+           ({abstract:ConLike})
+           []
+           [])))
         (L
          (SrcSpanAnn (EpAnnNotUsed) { <no location info> })
          (HsVar
@@ -975,9 +1005,11 @@
           []))
         (L
          (SrcSpanAnn (EpAnnNotUsed) { <no location info> })
-         (HsConLikeOut
-          (NoExtField)
-          ({abstract:ConLike})))
+         (XExpr
+          (ConLikeTc
+           ({abstract:ConLike})
+           []
+           [])))
         (L
          (SrcSpanAnn (EpAnnNotUsed) { <no location info> })
          (HsVar
@@ -1019,9 +1051,11 @@
           []))
         (L
          (SrcSpanAnn (EpAnnNotUsed) { <no location info> })
-         (HsConLikeOut
-          (NoExtField)
-          ({abstract:ConLike})))
+         (XExpr
+          (ConLikeTc
+           ({abstract:ConLike})
+           []
+           [])))
         (L
          (SrcSpanAnn (EpAnnNotUsed) { <no location info> })
          (HsVar
@@ -1063,9 +1097,11 @@
           []))
         (L
          (SrcSpanAnn (EpAnnNotUsed) { <no location info> })
-         (HsConLikeOut
-          (NoExtField)
-          ({abstract:ConLike})))
+         (XExpr
+          (ConLikeTc
+           ({abstract:ConLike})
+           []
+           [])))
         (L
          (SrcSpanAnn (EpAnnNotUsed) { <no location info> })
          (HsVar
@@ -1107,9 +1143,11 @@
           []))
         (L
          (SrcSpanAnn (EpAnnNotUsed) { <no location info> })
-         (HsConLikeOut
-          (NoExtField)
-          ({abstract:ConLike})))
+         (XExpr
+          (ConLikeTc
+           ({abstract:ConLike})
+           []
+           [])))
         (L
          (SrcSpanAnn (EpAnnNotUsed) { <no location info> })
          (HsVar
@@ -1150,9 +1188,11 @@
                  (TyConApp
                   ({abstract:TyCon})
                   []))
-                (HsConLikeOut
-                 (NoExtField)
-                 ({abstract:ConLike}))))))
+                (XExpr
+                 (ConLikeTc
+                  ({abstract:ConLike})
+                  []
+                  []))))))
             (L
              (SrcSpanAnn (EpAnnNotUsed) { <no location info> })
              (HsVar
@@ -1193,9 +1233,11 @@
                      (TyConApp
                       ({abstract:TyCon})
                       []))
-                    (HsConLikeOut
-                     (NoExtField)
-                     ({abstract:ConLike}))))))
+                    (XExpr
+                     (ConLikeTc
+                      ({abstract:ConLike})
+                      []
+                      []))))))
                 (L
                  (SrcSpanAnn (EpAnnNotUsed) { <no location info> })
                  (HsVar
@@ -1236,9 +1278,11 @@
                          (TyConApp
                           ({abstract:TyCon})
                           []))
-                        (HsConLikeOut
-                         (NoExtField)
-                         ({abstract:ConLike}))))))
+                        (XExpr
+                         (ConLikeTc
+                          ({abstract:ConLike})
+                          []
+                          []))))))
                     (L
                      (SrcSpanAnn (EpAnnNotUsed) { <no location info> })
                      (HsVar
@@ -1255,9 +1299,11 @@
                        (TyConApp
                         ({abstract:TyCon})
                         []))
-                      (HsConLikeOut
-                       (NoExtField)
-                       ({abstract:ConLike}))))))))))))))))))))))
+                      (XExpr
+                       (ConLikeTc
+                        ({abstract:ConLike})
+                        []
+                        []))))))))))))))))))))))
  ,(L
    (SrcSpanAnn (EpAnnNotUsed) { <no location info> })
    (VarBind
@@ -1285,9 +1331,11 @@
           []))
         (L
          (SrcSpanAnn (EpAnnNotUsed) { <no location info> })
-         (HsConLikeOut
-          (NoExtField)
-          ({abstract:ConLike})))
+         (XExpr
+          (ConLikeTc
+           ({abstract:ConLike})
+           []
+           [])))
         (L
          (SrcSpanAnn (EpAnnNotUsed) { <no location info> })
          (HsVar
@@ -1304,9 +1352,11 @@
            (TyConApp
             ({abstract:TyCon})
             []))
-          (HsConLikeOut
-           (NoExtField)
-           ({abstract:ConLike}))))))))))
+          (XExpr
+           (ConLikeTc
+            ({abstract:ConLike})
+            []
+            []))))))))))
  ,(L
    (SrcSpanAnn (EpAnnNotUsed) { <no location info> })
    (VarBind
@@ -1334,9 +1384,11 @@
           []))
         (L
          (SrcSpanAnn (EpAnnNotUsed) { <no location info> })
-         (HsConLikeOut
-          (NoExtField)
-          ({abstract:ConLike})))
+         (XExpr
+          (ConLikeTc
+           ({abstract:ConLike})
+           []
+           [])))
         (L
          (SrcSpanAnn (EpAnnNotUsed) { <no location info> })
          (HsPar
@@ -1353,9 +1405,11 @@
               []))
             (L
              (SrcSpanAnn (EpAnnNotUsed) { <no location info> })
-             (HsConLikeOut
-              (NoExtField)
-              ({abstract:ConLike})))
+             (XExpr
+              (ConLikeTc
+               ({abstract:ConLike})
+               []
+               [])))
             (L
              (SrcSpanAnn (EpAnnNotUsed) { <no location info> })
              (HsLit
@@ -1385,9 +1439,11 @@
             []))
           (L
            (SrcSpanAnn (EpAnnNotUsed) { <no location info> })
-           (HsConLikeOut
-            (NoExtField)
-            ({abstract:ConLike})))
+           (XExpr
+            (ConLikeTc
+             ({abstract:ConLike})
+             []
+             [])))
           (L
            (SrcSpanAnn (EpAnnNotUsed) { <no location info> })
            (HsLit
@@ -1486,4 +1542,6 @@
                (NoExtField)))))])
          (FromSource))
         []))]}
-    (False)))]}
\ No newline at end of file
+    (False)))]}
+
+
diff --git a/testsuite/tests/typecheck/should_compile/T18481.hs b/testsuite/tests/typecheck/should_compile/T18481.hs
new file mode 100644
index 0000000000..8cf8362899
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T18481.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE UnliftedNewtypes #-}
+module Bug where
+
+import GHC.Exts
+
+type Id :: TYPE r -> TYPE r
+newtype Id a where
+  MkId :: forall r (a :: TYPE r). a -> Id a
+
+idBool :: Id Bool
+idBool = MkId @LiftedRep @Bool True
diff --git a/testsuite/tests/typecheck/should_compile/T18481a.hs b/testsuite/tests/typecheck/should_compile/T18481a.hs
new file mode 100644
index 0000000000..b5b29a8af7
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T18481a.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE UnliftedDatatypes, PolyKinds, DataKinds, TypeApplications #-}
+
+module T18481a where
+
+import Data.Kind
+import GHC.Types( Levity(..), RuntimeRep(..), TYPE )
+
+type T :: TYPE (BoxedRep r) -> TYPE (BoxedRep r)
+data T a = MkT Int
+
+f :: T Bool
+f = MkT @Lifted @Bool 42
diff --git a/testsuite/tests/typecheck/should_compile/T19775.hs b/testsuite/tests/typecheck/should_compile/T19775.hs
new file mode 100644
index 0000000000..9c048d79c5
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T19775.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE DatatypeContexts, TypeApplications #-}
+{-# OPTIONS_GHC -Wno-deprecated-flags #-}
+
+module T19775 where
+
+data Ord a => T a = MkT (Maybe a)
+
+foo = MkT @Int
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 9d0225a6c2..868771542e 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -785,3 +785,6 @@ test('T19315', normal, compile, [''])
 test('T19535', normal, compile, [''])
 test('T19738', normal, compile, [''])
 test('T19742', normal, compile, [''])
+test('T18481', normal, compile, [''])
+test('T18481a', normal, compile, [''])
+test('T19775', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/T17021.stderr b/testsuite/tests/typecheck/should_fail/T17021.stderr
index 96c700c4b7..52f48d2bed 100644
--- a/testsuite/tests/typecheck/should_fail/T17021.stderr
+++ b/testsuite/tests/typecheck/should_fail/T17021.stderr
@@ -1,6 +1,14 @@
 
 T17021.hs:18:5: error:
+    Cannot use function with levity-polymorphic arguments:
+      MkT :: Int -> T
+    (Note that levity-polymorphic primops such as 'coerce' and unboxed tuples
+    are eta-expanded internally because they must occur fully saturated.
+    Use -fprint-typechecker-elaboration to display the full expression.)
+    Levity-polymorphic arguments: Int :: TYPE (Id ('BoxedRep 'Lifted))
+
+T17021.hs:18:9: error:
     A levity-polymorphic type is not allowed here:
       Type: Int
       Kind: TYPE (Id ('BoxedRep 'Lifted))
-    When trying to create a variable of type: Int
+    In the type of expression: 42
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesLevityBinder.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesLevityBinder.stderr
index a33a957e9d..70746fd60a 100644
--- a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesLevityBinder.stderr
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesLevityBinder.stderr
@@ -1,6 +1,8 @@
 
 UnliftedNewtypesLevityBinder.hs:16:7: error:
-    A levity-polymorphic type is not allowed here:
-      Type: a
-      Kind: TYPE r
-    When trying to create a variable of type: a
+    Cannot use function with levity-polymorphic arguments:
+      IdentC :: a -> Ident a
+    (Note that levity-polymorphic primops such as 'coerce' and unboxed tuples
+    are eta-expanded internally because they must occur fully saturated.
+    Use -fprint-typechecker-elaboration to display the full expression.)
+    Levity-polymorphic arguments: a :: TYPE r