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]

2 files changed, 36 insertions, 13 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