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]

3 files changed, 30 insertions, 17 deletions

diff --git a/compiler/GHC/Core/Lint.hs b/compiler/GHC/Core/Lint.hs
index b3ed2ce8eb..7eaec265a8 100644
--- a/compiler/GHC/Core/Lint.hs
+++ b/compiler/GHC/Core/Lint.hs
@@ -490,7 +490,18 @@ lintCoreBindings dflags pass local_in_scope binds
                { lf_check_global_ids = check_globals
                , lf_check_inline_loop_breakers = check_lbs
                , lf_check_static_ptrs = check_static_ptrs
-               , lf_check_linearity = check_linearity }
+               , lf_check_linearity = check_linearity
+               , lf_check_levity_poly = check_levity }
+
+    -- In the output of the desugarer, before optimisation,
+    -- we have eta-expanded data constructors with levity-polymorphic
+    -- bindings; so we switch off the lev-poly checks. The very simple
+    -- optimiser will beta-reduce them away.
+    -- See Note [Checking levity-polymorphic data constructors]
+    -- in GHC.HsToCore.Expr.
+    check_levity = case pass of
+                      CoreDesugar -> False
+                      _           -> True
 
     -- See Note [Checking for global Ids]
     check_globals = case pass of
@@ -541,7 +552,6 @@ lintCoreBindings dflags pass local_in_scope binds
 
 Note [Linting Unfoldings from Interfaces]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
 We use this to check all top-level unfoldings that come in from interfaces
 (it is very painful to catch errors otherwise).
 
@@ -922,9 +932,9 @@ lintCoreExpr e@(App _ _)
   , fun `hasKey` runRWKey
     -- N.B. we may have an over-saturated application of the form:
     --   runRW (\s -> \x -> ...) y
-  , arg_ty1 : arg_ty2 : arg3 : rest <- args
-  = do { fun_pair1 <- lintCoreArg (idType fun, zeroUE) arg_ty1
-       ; (fun_ty2, ue2) <- lintCoreArg fun_pair1      arg_ty2
+  , ty_arg1 : ty_arg2 : arg3 : rest <- args
+  = do { fun_pair1 <- lintCoreArg (idType fun, zeroUE) ty_arg1
+       ; (fun_ty2, ue2) <- lintCoreArg fun_pair1       ty_arg2
          -- See Note [Linting of runRW#]
        ; let lintRunRWCont :: CoreArg -> LintM (LintedType, UsageEnv)
              lintRunRWCont expr@(Lam _ _) =
@@ -1190,13 +1200,17 @@ lintCoreArg (fun_ty, fun_ue) arg
   = do { (arg_ty, arg_ue) <- markAllJoinsBad $ lintCoreExpr arg
            -- See Note [Levity polymorphism invariants] in GHC.Core
        ; flags <- getLintFlags
-       ; lintL (not (lf_check_levity_poly flags) || not (isTypeLevPoly arg_ty))
-           (text "Levity-polymorphic argument:" <+>
-             (ppr arg <+> dcolon <+> parens (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))))
-          -- check for levity polymorphism first, because otherwise isUnliftedType panics
 
-       ; checkL (not (isUnliftedType arg_ty) || exprOkForSpeculation arg)
-                (mkLetAppMsg arg)
+       ; when (lf_check_levity_poly flags) $
+         -- Only do these checks if lf_check_levity_poly is on,
+         -- because otherwise isUnliftedType panics
+         do { checkL (not (isTypeLevPoly arg_ty))
+                     (text "Levity-polymorphic argument:"
+                      <+> ppr arg <+> dcolon
+                      <+> parens (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty)))
+
+            ; checkL (not (isUnliftedType arg_ty) || exprOkForSpeculation arg)
+                     (mkLetAppMsg arg) }
 
        ; lintValApp arg fun_ty arg_ty fun_ue arg_ue }
 
diff --git a/compiler/GHC/Core/Multiplicity.hs b/compiler/GHC/Core/Multiplicity.hs
index 881966f8ff..42dc6c4b8b 100644
--- a/compiler/GHC/Core/Multiplicity.hs
+++ b/compiler/GHC/Core/Multiplicity.hs
@@ -237,9 +237,7 @@ Types don't match, we should get a type error. But this is legal Haskell 98
 code! Bad! Bad! Bad!
 
 It could be solved with subtyping, but subtyping doesn't combine well with
-polymorphism.
-
-Instead, we generalise the type of Just, when used as term:
+polymorphism. Instead, we generalise the type of Just, when used as term:
 
    Just :: forall {p}. a %p-> Just a
 
@@ -254,7 +252,8 @@ We only generalise linear fields this way: fields with multiplicity Many, or
 other multiplicity expressions are exclusive to -XLinearTypes, hence don't have
 backward compatibility implications.
 
-The implementation is described in Note [Linear fields generalization].
+The implementation is described in Note [Typechecking data constructors]
+in GHC.Tc.Gen.Head.
 
 More details in the proposal.
 -}
diff --git a/compiler/GHC/Core/SimpleOpt.hs b/compiler/GHC/Core/SimpleOpt.hs
index 9e3e92d247..53c239426a 100644
--- a/compiler/GHC/Core/SimpleOpt.hs
+++ b/compiler/GHC/Core/SimpleOpt.hs
@@ -338,11 +338,11 @@ simple_app env e@(Lam {}) as@(_:_)
   | (bndrs, body) <- collectBinders e
   , let zapped_bndrs = zapLamBndrs (length as) bndrs
     -- Be careful to zap the lambda binders if necessary
-    -- c.f. the Lam caes of simplExprF1 in GHC.Core.Opt.Simplify
+    -- c.f. the Lam case of simplExprF1 in GHC.Core.Opt.Simplify
     -- Lacking this zap caused #19347, when we had a redex
     --   (\ a b. K a b) e1 e2
     -- where (as it happens) the eta-expanded K is produced by
-    -- Note [Linear fields generalization] in GHC.Tc.Gen.Head
+    -- Note [Typechecking data constructors] in GHC.Tc.Gen.Head
   = do_beta env zapped_bndrs body as
   where
     do_beta env (b:bs) body (a:as)