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]

17 files changed, 473 insertions, 277 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)
diff --git a/compiler/GHC/Hs/Expr.hs b/compiler/GHC/Hs/Expr.hs
index fb523bb74a..f812c66540 100644
--- a/compiler/GHC/Hs/Expr.hs
+++ b/compiler/GHC/Hs/Expr.hs
@@ -52,6 +52,7 @@ import GHC.Types.Basic
 import GHC.Types.Fixity
 import GHC.Types.SourceText
 import GHC.Types.SrcLoc
+import GHC.Types.Var( InvisTVBinder )
 import GHC.Core.ConLike
 import GHC.Unit.Module (ModuleName)
 import GHC.Utils.Misc
@@ -218,7 +219,6 @@ data EpAnnUnboundVar = EpAnnUnboundVar
      } deriving Data
 
 type instance XVar           (GhcPass _) = NoExtField
-type instance XConLikeOut    (GhcPass _) = NoExtField
 type instance XRecFld        (GhcPass _) = NoExtField
 type instance XLam           (GhcPass _) = NoExtField
 
@@ -240,7 +240,6 @@ type instance XUnboundVar    GhcTc = HoleExprRef
   -- Much, much easier just to define HoleExprRef with a Data instance and
   -- store the whole structure.
 
-type instance XConLikeOut    (GhcPass _) = NoExtField
 type instance XRecFld        (GhcPass _) = NoExtField
 type instance XIPVar         (GhcPass _) = EpAnnCO
 type instance XOverLitE      (GhcPass _) = EpAnnCO
@@ -361,21 +360,9 @@ type instance XBinTick       (GhcPass _) = NoExtField
 
 type instance XPragE         (GhcPass _) = NoExtField
 
-type instance XXExpr         GhcPs       = NoExtCon
-
--- See Note [Rebindable syntax and HsExpansion] below
-type instance XXExpr         GhcRn       = HsExpansion (HsExpr GhcRn)
-                                                       (HsExpr GhcRn)
-type instance XXExpr         GhcTc       = XXExprGhcTc
-
-
 type instance Anno [LocatedA ((StmtLR (GhcPass pl) (GhcPass pr) (LocatedA (body (GhcPass pr)))))] = SrcSpanAnnL
 type instance Anno (StmtLR GhcRn GhcRn (LocatedA (body GhcRn))) = SrcSpanAnnA
 
-data XXExprGhcTc
-  = WrapExpr {-# UNPACK #-} !(HsWrap HsExpr)
-  | ExpansionExpr {-# UNPACK #-} !(HsExpansion (HsExpr GhcRn) (HsExpr GhcTc))
-
 data AnnExplicitSum
   = AnnExplicitSum {
       aesOpen       :: EpaLocation,
@@ -421,6 +408,40 @@ tupArgPresent :: HsTupArg (GhcPass p) -> Bool
 tupArgPresent (Present {}) = True
 tupArgPresent (Missing {}) = False
 
+
+{- *********************************************************************
+*                                                                      *
+            XXExpr: the extension constructor of HsExpr
+*                                                                      *
+********************************************************************* -}
+
+type instance XXExpr GhcPs = NoExtCon
+type instance XXExpr GhcRn = HsExpansion (HsExpr GhcRn) (HsExpr GhcRn)
+type instance XXExpr GhcTc = XXExprGhcTc
+-- HsExpansion: see Note [Rebindable syntax and HsExpansion] below
+
+
+data XXExprGhcTc
+  = WrapExpr        -- Type and evidence application and abstractions
+      {-# UNPACK #-} !(HsWrap HsExpr)
+
+  | ExpansionExpr   -- See Note [Rebindable syntax and HsExpansion] below
+      {-# UNPACK #-} !(HsExpansion (HsExpr GhcRn) (HsExpr GhcTc))
+
+  | ConLikeTc      -- Result of typechecking a data-con
+                   -- See Note [Typechecking data constructors] in
+                   --     GHC.Tc.Gen.Head
+                   -- The two arguments describe how to eta-expand
+                   -- the data constructor when desugaring
+        ConLike [InvisTVBinder] [Scaled TcType]
+
+
+{- *********************************************************************
+*                                                                      *
+            Pretty-printing expressions
+*                                                                      *
+********************************************************************* -}
+
 instance (OutputableBndrId p) => Outputable (HsExpr (GhcPass p)) where
     ppr expr = pprExpr expr
 
@@ -457,7 +478,6 @@ ppr_expr :: forall p. (OutputableBndrId p)
          => HsExpr (GhcPass p) -> SDoc
 ppr_expr (HsVar _ (L _ v))   = pprPrefixOcc v
 ppr_expr (HsUnboundVar _ uv) = pprPrefixOcc uv
-ppr_expr (HsConLikeOut _ c)  = pprPrefixOcc c
 ppr_expr (HsRecFld _ f)      = pprPrefixOcc f
 ppr_expr (HsIPVar _ v)       = ppr v
 ppr_expr (HsOverLabel _ l)   = char '#' <> ppr l
@@ -638,27 +658,41 @@ ppr_expr (XExpr x) = case ghcPass @p of
   GhcPs -> ppr x
 #endif
   GhcRn -> ppr x
-  GhcTc -> case x of
-    WrapExpr (HsWrap co_fn e) -> pprHsWrapper co_fn
-      (\parens -> if parens then pprExpr e else pprExpr e)
-    ExpansionExpr e -> ppr e -- e is an HsExpansion, we print the original
-                             -- expression (LHsExpr GhcPs), not the
-                             -- desugared one (LHsExpr GhcT).
+  GhcTc -> ppr x
+
+instance Outputable XXExprGhcTc where
+  ppr (WrapExpr (HsWrap co_fn e))
+    = pprHsWrapper co_fn (\_parens -> pprExpr e)
+
+  ppr (ExpansionExpr e)
+    = ppr e -- e is an HsExpansion, we print the original
+            -- expression (LHsExpr GhcPs), not the
+            -- desugared one (LHsExpr GhcTc).
+
+  ppr (ConLikeTc con _ _) = pprPrefixOcc con
+   -- Used in error messages generated by
+   -- the pattern match overlap checker
 
 ppr_infix_expr :: forall p. (OutputableBndrId p) => HsExpr (GhcPass p) -> Maybe SDoc
 ppr_infix_expr (HsVar _ (L _ v))    = Just (pprInfixOcc v)
-ppr_infix_expr (HsConLikeOut _ c)   = Just (pprInfixOcc (conLikeName c))
 ppr_infix_expr (HsRecFld _ f)       = Just (pprInfixOcc f)
 ppr_infix_expr (HsUnboundVar _ occ) = Just (pprInfixOcc occ)
-ppr_infix_expr (XExpr x)            = case (ghcPass @p, x) of
+ppr_infix_expr (XExpr x)            = case ghcPass @p of
 #if __GLASGOW_HASKELL__ < 901
-  (GhcPs, _)                              -> Nothing
+                                        GhcPs -> Nothing
 #endif
-  (GhcRn, HsExpanded a _)                 -> ppr_infix_expr a
-  (GhcTc, WrapExpr (HsWrap _ e))          -> ppr_infix_expr e
-  (GhcTc, ExpansionExpr (HsExpanded a _)) -> ppr_infix_expr a
+                                        GhcRn -> ppr_infix_expr_rn x
+                                        GhcTc -> ppr_infix_expr_tc x
 ppr_infix_expr _ = Nothing
 
+ppr_infix_expr_rn :: HsExpansion (HsExpr GhcRn) (HsExpr GhcRn) -> Maybe SDoc
+ppr_infix_expr_rn (HsExpanded a _) = ppr_infix_expr a
+
+ppr_infix_expr_tc :: XXExprGhcTc -> Maybe SDoc
+ppr_infix_expr_tc (WrapExpr (HsWrap _ e))          = ppr_infix_expr e
+ppr_infix_expr_tc (ExpansionExpr (HsExpanded a _)) = ppr_infix_expr a
+ppr_infix_expr_tc (ConLikeTc {})                   = Nothing
+
 ppr_apps :: (OutputableBndrId p)
          => HsExpr (GhcPass p)
          -> [Either (LHsExpr (GhcPass p)) (LHsWcType (NoGhcTc (GhcPass p)))]
@@ -698,67 +732,70 @@ pprParendExpr p expr
 -- | @'hsExprNeedsParens' p e@ returns 'True' if the expression @e@ needs
 -- parentheses under precedence @p@.
 hsExprNeedsParens :: forall p. IsPass p => PprPrec -> HsExpr (GhcPass p) -> Bool
-hsExprNeedsParens p = go
+hsExprNeedsParens prec = go
   where
+    go :: HsExpr (GhcPass p) -> Bool
     go (HsVar{})                      = False
     go (HsUnboundVar{})               = False
-    go (HsConLikeOut{})               = False
     go (HsIPVar{})                    = False
     go (HsOverLabel{})                = False
-    go (HsLit _ l)                    = hsLitNeedsParens p l
-    go (HsOverLit _ ol)               = hsOverLitNeedsParens p ol
+    go (HsLit _ l)                    = hsLitNeedsParens prec l
+    go (HsOverLit _ ol)               = hsOverLitNeedsParens prec ol
     go (HsPar{})                      = False
-    go (HsApp{})                      = p >= appPrec
-    go (HsAppType {})                 = p >= appPrec
-    go (OpApp{})                      = p >= opPrec
-    go (NegApp{})                     = p > topPrec
+    go (HsApp{})                      = prec >= appPrec
+    go (HsAppType {})                 = prec >= appPrec
+    go (OpApp{})                      = prec >= opPrec
+    go (NegApp{})                     = prec > topPrec
     go (SectionL{})                   = True
     go (SectionR{})                   = True
     -- Special-case unary boxed tuple applications so that they are
     -- parenthesized as `Identity (Solo x)`, not `Identity Solo x` (#18612)
     -- See Note [One-tuples] in GHC.Builtin.Types
     go (ExplicitTuple _ [Present{}] Boxed)
-                                      = p >= appPrec
+                                      = prec >= appPrec
     go (ExplicitTuple{})              = False
     go (ExplicitSum{})                = False
-    go (HsLam{})                      = p > topPrec
-    go (HsLamCase{})                  = p > topPrec
-    go (HsCase{})                     = p > topPrec
-    go (HsIf{})                       = p > topPrec
-    go (HsMultiIf{})                  = p > topPrec
-    go (HsLet{})                      = p > topPrec
+    go (HsLam{})                      = prec > topPrec
+    go (HsLamCase{})                  = prec > topPrec
+    go (HsCase{})                     = prec > topPrec
+    go (HsIf{})                       = prec > topPrec
+    go (HsMultiIf{})                  = prec > topPrec
+    go (HsLet{})                      = prec > topPrec
     go (HsDo _ sc _)
       | isComprehensionContext sc     = False
-      | otherwise                     = p > topPrec
+      | otherwise                     = prec > topPrec
     go (ExplicitList{})               = False
     go (RecordUpd{})                  = False
-    go (ExprWithTySig{})              = p >= sigPrec
+    go (ExprWithTySig{})              = prec >= sigPrec
     go (ArithSeq{})                   = False
-    go (HsPragE{})                    = p >= appPrec
+    go (HsPragE{})                    = prec >= appPrec
     go (HsSpliceE{})                  = False
     go (HsBracket{})                  = False
     go (HsRnBracketOut{})             = False
     go (HsTcBracketOut{})             = False
-    go (HsProc{})                     = p > topPrec
-    go (HsStatic{})                   = p >= appPrec
+    go (HsProc{})                     = prec > topPrec
+    go (HsStatic{})                   = prec >= appPrec
     go (HsTick _ _ (L _ e))           = go e
     go (HsBinTick _ _ _ (L _ e))      = go e
     go (RecordCon{})                  = False
     go (HsRecFld{})                   = False
     go (HsProjection{})               = True
     go (HsGetField{})                 = False
-    go (XExpr x)
-      | GhcTc <- ghcPass @p
-      = case x of
-          WrapExpr      (HsWrap _ e)     -> go e
-          ExpansionExpr (HsExpanded a _) -> hsExprNeedsParens p a
-      | GhcRn <- ghcPass @p
-      = case x of HsExpanded a _ -> hsExprNeedsParens p a
+    go (XExpr x) = case ghcPass @p of
+                     GhcTc -> go_x_tc x
+                     GhcRn -> go_x_rn x
 #if __GLASGOW_HASKELL__ <= 900
-      | otherwise
-      = True
+                     GhcPs -> True
 #endif
 
+    go_x_tc :: XXExprGhcTc -> Bool
+    go_x_tc (WrapExpr (HsWrap _ e))          = hsExprNeedsParens prec e
+    go_x_tc (ExpansionExpr (HsExpanded a _)) = hsExprNeedsParens prec a
+    go_x_tc (ConLikeTc {})                   = False
+
+    go_x_rn :: HsExpansion (HsExpr GhcRn) (HsExpr GhcRn) -> Bool
+    go_x_rn (HsExpanded a _) = hsExprNeedsParens prec a
+
 
 -- | @'parenthesizeHsExpr' p e@ checks if @'hsExprNeedsParens' p e@ is true,
 -- and if so, surrounds @e@ with an 'HsPar'. Otherwise, it simply returns @e@.
@@ -778,7 +815,6 @@ stripParensHsExpr e = e
 isAtomicHsExpr :: forall p. IsPass p => HsExpr (GhcPass p) -> Bool
 -- True of a single token
 isAtomicHsExpr (HsVar {})        = True
-isAtomicHsExpr (HsConLikeOut {}) = True
 isAtomicHsExpr (HsLit {})        = True
 isAtomicHsExpr (HsOverLit {})    = True
 isAtomicHsExpr (HsIPVar {})      = True
@@ -786,12 +822,16 @@ isAtomicHsExpr (HsOverLabel {})  = True
 isAtomicHsExpr (HsUnboundVar {}) = True
 isAtomicHsExpr (HsRecFld{})      = True
 isAtomicHsExpr (XExpr x)
-  | GhcTc <- ghcPass @p          = case x of
-      WrapExpr      (HsWrap _ e)     -> isAtomicHsExpr e
-      ExpansionExpr (HsExpanded a _) -> isAtomicHsExpr a
-  | GhcRn <- ghcPass @p          = case x of
-      HsExpanded a _         -> isAtomicHsExpr a
-isAtomicHsExpr _                 = False
+  | GhcTc <- ghcPass @p          = go_x_tc x
+  | GhcRn <- ghcPass @p          = go_x_rn x
+  where
+    go_x_tc (WrapExpr      (HsWrap _ e))     = isAtomicHsExpr e
+    go_x_tc (ExpansionExpr (HsExpanded a _)) = isAtomicHsExpr a
+    go_x_tc (ConLikeTc {})                   = True
+
+    go_x_rn (HsExpanded a _) = isAtomicHsExpr a
+
+isAtomicHsExpr _ = False
 
 instance Outputable (HsPragE (GhcPass p)) where
   ppr (HsPragSCC _ st (StringLiteral stl lbl _)) =
@@ -1108,21 +1148,27 @@ ppr_cmd (HsCmdArrApp _ arrow arg HsHigherOrderApp True)
 ppr_cmd (HsCmdArrApp _ arrow arg HsHigherOrderApp False)
   = hsep [ppr_lexpr arg, arrowtt, ppr_lexpr arrow]
 
-ppr_cmd (HsCmdArrForm _ (L _ (HsVar _ (L _ v))) _ (Just _) [arg1, arg2])
-  = hang (pprCmdArg (unLoc arg1)) 4 (sep [ pprInfixOcc v
-                                         , pprCmdArg (unLoc arg2)])
-ppr_cmd (HsCmdArrForm _ (L _ (HsVar _ (L _ v))) Infix _    [arg1, arg2])
-  = hang (pprCmdArg (unLoc arg1)) 4 (sep [ pprInfixOcc v
-                                         , pprCmdArg (unLoc arg2)])
-ppr_cmd (HsCmdArrForm _ (L _ (HsConLikeOut _ c)) _ (Just _) [arg1, arg2])
-  = hang (pprCmdArg (unLoc arg1)) 4 (sep [ pprInfixOcc (conLikeName c)
-                                         , pprCmdArg (unLoc arg2)])
-ppr_cmd (HsCmdArrForm _ (L _ (HsConLikeOut _ c)) Infix _    [arg1, arg2])
-  = hang (pprCmdArg (unLoc arg1)) 4 (sep [ pprInfixOcc (conLikeName c)
-                                         , pprCmdArg (unLoc arg2)])
-ppr_cmd (HsCmdArrForm _ op _ _ args)
-  = hang (text "(|" <+> ppr_lexpr op)
-         4 (sep (map (pprCmdArg.unLoc) args) <+> text "|)")
+ppr_cmd (HsCmdArrForm _ (L _ op) ps_fix rn_fix args)
+  | HsVar _ (L _ v) <- op
+  = ppr_cmd_infix v
+  | GhcTc <- ghcPass @p
+  , XExpr (ConLikeTc c _ _) <- op
+  = ppr_cmd_infix (conLikeName c)
+  | otherwise
+  = fall_through
+  where
+    fall_through = hang (text "(|" <+> ppr_expr op)
+                      4 (sep (map (pprCmdArg.unLoc) args) <+> text "|)")
+
+    ppr_cmd_infix :: OutputableBndr v => v -> SDoc
+    ppr_cmd_infix v
+      | [arg1, arg2] <- args
+      , isJust rn_fix || ps_fix == Infix
+      = hang (pprCmdArg (unLoc arg1))
+           4 (sep [ pprInfixOcc v, pprCmdArg (unLoc arg2)])
+      | otherwise
+      = fall_through
+
 ppr_cmd (XCmd x) = case ghcPass @p of
 #if __GLASGOW_HASKELL__ < 811
   GhcPs -> ppr x
diff --git a/compiler/GHC/Hs/Utils.hs b/compiler/GHC/Hs/Utils.hs
index 43be3749ad..34120f56cd 100644
--- a/compiler/GHC/Hs/Utils.hs
+++ b/compiler/GHC/Hs/Utils.hs
@@ -44,7 +44,7 @@ module GHC.Hs.Utils(
   mkHsDictLet, mkHsLams,
   mkHsOpApp, mkHsDo, mkHsDoAnns, mkHsComp, mkHsCompAnns, mkHsWrapPat, mkHsWrapPatCo,
   mkLHsPar, mkHsCmdWrap, mkLHsCmdWrap,
-  mkHsCmdIf,
+  mkHsCmdIf, mkConLikeTc,
 
   nlHsTyApp, nlHsTyApps, nlHsVar, nl_HsVar, nlHsDataCon,
   nlHsLit, nlHsApp, nlHsApps, nlHsSyntaxApps,
@@ -468,6 +468,8 @@ mkHsStringPrimLit fs = HsStringPrim NoSourceText (bytesFS fs)
 mkHsCharPrimLit :: Char -> HsLit (GhcPass p)
 mkHsCharPrimLit c = HsChar NoSourceText c
 
+mkConLikeTc :: ConLike -> HsExpr GhcTc
+mkConLikeTc con = XExpr (ConLikeTc con [] [])
 
 {-
 ************************************************************************
@@ -487,7 +489,7 @@ nl_HsVar n = HsVar noExtField (noLocA n)
 
 -- | NB: Only for 'LHsExpr' 'Id'.
 nlHsDataCon :: DataCon -> LHsExpr GhcTc
-nlHsDataCon con = noLocA (HsConLikeOut noExtField (RealDataCon con))
+nlHsDataCon con = noLocA (mkConLikeTc (RealDataCon con))
 
 nlHsLit :: HsLit (GhcPass p) -> LHsExpr (GhcPass p)
 nlHsLit n = noLocA (HsLit noComments n)
diff --git a/compiler/GHC/HsToCore/Arrows.hs b/compiler/GHC/HsToCore/Arrows.hs
index 8017fc65f6..f1dee3f3b4 100644
--- a/compiler/GHC/HsToCore/Arrows.hs
+++ b/compiler/GHC/HsToCore/Arrows.hs
@@ -553,8 +553,8 @@ dsCmd ids local_vars stack_ty res_ty
     left_con <- dsLookupDataCon leftDataConName
     right_con <- dsLookupDataCon rightDataConName
     let
-        left_id  = HsConLikeOut noExtField (RealDataCon left_con)
-        right_id = HsConLikeOut noExtField (RealDataCon right_con)
+        left_id  = mkConLikeTc (RealDataCon left_con)
+        right_id = mkConLikeTc (RealDataCon right_con)
         left_expr  ty1 ty2 e = noLocA $ HsApp noComments
                            (noLocA $ mkHsWrap (mkWpTyApps [ty1, ty2]) left_id ) e
         right_expr ty1 ty2 e = noLocA $ HsApp noComments
diff --git a/compiler/GHC/HsToCore/Coverage.hs b/compiler/GHC/HsToCore/Coverage.hs
index 8a6bb4e160..4f9b85a53f 100644
--- a/compiler/GHC/HsToCore/Coverage.hs
+++ b/compiler/GHC/HsToCore/Coverage.hs
@@ -521,10 +521,6 @@ addTickHsExpr e@(HsUnboundVar {})   = return e
 addTickHsExpr e@(HsRecFld _ (Ambiguous id _))   = do freeVar id; return e
 addTickHsExpr e@(HsRecFld _ (Unambiguous id _)) = do freeVar id; return e
 
-addTickHsExpr e@(HsConLikeOut {}) = return e
-  -- We used to do a freeVar on a pat-syn builder, but actually
-  -- such builders are never in the inScope env, which
-  -- doesn't include top level bindings
 addTickHsExpr e@(HsIPVar {})     = return e
 addTickHsExpr e@(HsOverLit {})   = return e
 addTickHsExpr e@(HsOverLabel{})  = return e
@@ -649,6 +645,11 @@ addTickHsExpr (XExpr (ExpansionExpr (HsExpanded a b))) =
         liftM (XExpr . ExpansionExpr . HsExpanded a) $
               (addTickHsExpr b)
 
+addTickHsExpr e@(XExpr (ConLikeTc {})) = return e
+  -- We used to do a freeVar on a pat-syn builder, but actually
+  -- such builders are never in the inScope env, which
+  -- doesn't include top level bindings
+
 addTickTupArg :: HsTupArg GhcTc -> TM (HsTupArg GhcTc)
 addTickTupArg (Present x e)  = do { e' <- addTickLHsExpr e
                                   ; return (Present x e') }
diff --git a/compiler/GHC/HsToCore/Expr.hs b/compiler/GHC/HsToCore/Expr.hs
index 565132aed3..176aa1bc02 100644
--- a/compiler/GHC/HsToCore/Expr.hs
+++ b/compiler/GHC/HsToCore/Expr.hs
@@ -275,7 +275,6 @@ dsExpr (HsUnboundVar (HER ref _ _) _)  = dsEvTerm =<< readMutVar ref
 dsExpr (HsPar _ e)            = dsLExpr e
 dsExpr (ExprWithTySig _ e _)  = dsLExpr e
 
-dsExpr (HsConLikeOut _ con)   = dsConLike con
 dsExpr (HsIPVar {})           = panic "dsExpr: HsIPVar"
 
 dsExpr (HsGetField x _ _)     = absurd x
@@ -289,10 +288,11 @@ dsExpr (HsOverLit _ lit)
   = do { warnAboutOverflowedOverLit lit
        ; dsOverLit lit }
 
-dsExpr e@(XExpr expansion)
-  = case expansion of
+dsExpr e@(XExpr ext_expr_tc)
+  = case ext_expr_tc of
       ExpansionExpr (HsExpanded _ b) -> dsExpr b
       WrapExpr {}                    -> dsHsWrapped e
+      ConLikeTc {}                   -> dsHsWrapped e
 
 dsExpr (NegApp _ (L loc
                     (HsOverLit _ lit@(OverLit { ol_val = HsIntegral i})))
@@ -671,7 +671,7 @@ dsExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = Left fields
                  mk_val_arg fl pat_arg_id
                      = nlHsVar (lookupNameEnv upd_fld_env (flSelector fl) `orElse` pat_arg_id)
 
-                 inst_con = noLocA $ mkHsWrap wrap (HsConLikeOut noExtField con)
+                 inst_con = noLocA $ mkHsWrap wrap (mkConLikeTc con)
                         -- Reconstruct with the WrapId so that unpacking happens
                  wrap = mkWpEvVarApps theta_vars                                <.>
                         dict_req_wrap                                           <.>
@@ -1042,13 +1042,18 @@ dsDo ctx stmts
 -}
 
 dsHsVar :: Id -> DsM CoreExpr
+-- We could just call dsHsUnwrapped; but this is a short-cut
+-- for the very common case of a variable with no wrapper.
+-- NB: withDict is always instantiated by a wrapper, so we need
+--     only check for it in dsHsUnwrapped
 dsHsVar var
-  = do { checkLevPolyFunction (ppr var) var (idType var)
+  = do { checkLevPolyFunction var var (idType var)
        ; return (varToCoreExpr var) }   -- See Note [Desugaring vars]
 
-dsConLike :: ConLike -> DsM CoreExpr
-dsConLike (RealDataCon dc) = dsHsVar (dataConWrapId dc)
-dsConLike (PatSynCon ps)
+dsHsConLike :: ConLike -> DsM CoreExpr
+dsHsConLike (RealDataCon dc)
+  = return (varToCoreExpr (dataConWrapId dc))
+dsHsConLike (PatSynCon ps)
   | Just (builder_name, _, add_void) <- patSynBuilder ps
   = do { builder_id <- dsLookupGlobalId builder_name
        ; return (if add_void
@@ -1058,6 +1063,26 @@ dsConLike (PatSynCon ps)
   | otherwise
   = pprPanic "dsConLike" (ppr ps)
 
+dsConLike :: ConLike -> [TcInvisTVBinder] -> [Scaled Type] -> DsM CoreExpr
+-- This function desugars ConLikeTc
+-- See Note [Typechecking data constructors] in GHC.Tc.Gen.Head
+--     for what is going on here
+dsConLike con tvbs tys
+  = do { ds_con <- dsHsConLike con
+       ; ids    <- newSysLocalsDs tys
+                   -- newSysLocalDs: /can/ be lev-poly; see
+                   -- Note [Checking levity-polymorphic data constructors]
+       ; return (mkLams tvs $
+                 mkLams ids $
+                 ds_con `mkTyApps` mkTyVarTys tvs
+                        `mkVarApps` drop_stupid ids) }
+  where
+    tvs = binderVars tvbs
+
+    drop_stupid = dropList (conLikeStupidTheta con)
+    -- drop_stupid: see Note [Instantiating stupid theta]
+    --              in GHC.Tc.Gen.Head
+
 {-
 ************************************************************************
 *                                                                      *
@@ -1135,7 +1160,7 @@ Note that if `f :: forall r (a :: Type r). blah`, then
 is absolutely fine.  Here `f` is a function, represented by a
 pointer, and we can pass it to `const` (or anything else).  (See
 #12708 for an example.)  It's only the Id.hasNoBinding functions
-that are a problem.
+that are a problem.  See checkLevPolyFunction.
 
 Interestingly, this approach does not look to see whether the Id in
 question will be eta expanded. The logic is this:
@@ -1146,6 +1171,62 @@ question will be eta expanded. The logic is this:
     argument. If its wrapped type contains levity polymorphic arguments, reject.
 So, either way, we're good to reject.
 
+Note [Nasty wrinkle in levity-polymorphic function check]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+A nasty wrinkle came up in T13244
+   type family Rep x
+   type instance Rep Int = IntRep
+
+   type Unboxed x :: TYPE (Rep x)
+   type instance Unboxed Int = Int#
+
+   box :: Unboxed Int -> Int
+   box = I#
+
+Here the function I# is wrapped in a /cast/, thus
+   box = I# |> (co :: (Int# -> Int) ~ (Unboxed Int -> Int))
+If we look only at final type of the expression,
+  namely: Unboxed Int -> Int,
+the kind of the argument type is TYPE (Rep Int), and that needs
+type-family reduction to say whether it is lifted or unlifted.
+
+So we split the wrapper into the instantiating part (which is what
+we really want) and everything else; see splitWrapper.  This is
+very disgusting.
+
+But it also improves the error message in an example like T13233_elab:
+  obscure :: (forall (rep1 :: RuntimeRep) (rep2 :: RuntimeRep)
+                     (a :: TYPE rep1) (b :: TYPE rep2).
+                     a -> b -> (# a, b #)) -> ()
+  obscure _ = ()
+
+  quux = obscure (#,#)
+
+Around the (#,#) we'll get some type /abstractions/ wrapping some type
+/instantiations/. In the levity-poly error message we really only want
+to report the instantiations.  Hence passing (mkHsWrap w_inner e) to
+checkLevPolyArgs.
+
+
+Note [Checking levity-polymorphic data constructors]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Similarly, generated by a newtype data constructor, we might get this:
+  (/\(r :: RuntimeRep) (a :: TYPE r) \(x::a). K r a x) @LiftedRep Int 4
+
+which we want to accept. See Note [Typechecking data constructors] in
+GHC.Tc.Gen.Head.
+
+Because we want to accept this, we switch off Lint's levity-poly checks
+when Lint checks the output of the desugarer; see the lf_check_levity_poly
+flag in GHC.Core.Lint.lintCoreBindings.
+
+We can get this situation both for levity-polymorphic newtype constructors
+(T18481), and for levity-polymorphic algebraic data types, e.g (T18481a)
+    type T :: TYPE (BoxedRep r) -> TYPE (BoxedRep r)
+    data T a = MkT Int
+
+    f :: T Bool
+    f = MkT @Lifted @Bool 42
 -}
 
 ------------------------------
@@ -1154,38 +1235,72 @@ dsHsWrapped :: HsExpr GhcTc -> DsM CoreExpr
 -- or wrappers (HsWrap), and checks that any hasNoBinding function
 -- is not levity polymorphic, *after* instantiation with those wrappers
 dsHsWrapped orig_hs_expr
-  = go id orig_hs_expr
+  = go idHsWrapper orig_hs_expr
   where
-    go wrap (XExpr (WrapExpr (HsWrap co_fn hs_e)))
-       = do { wrap' <- dsHsWrapper co_fn
-            ; addTyCs FromSource (hsWrapDictBinders co_fn) $
-              go (wrap . wrap') hs_e }
-    go wrap (HsConLikeOut _ (RealDataCon dc))
-      = go_head wrap (dataConWrapId dc)
-    go wrap (HsAppType ty hs_e _) = go_l (wrap . (\e -> App e (Type ty))) hs_e
-    go wrap (HsPar _ hs_e)        = go_l wrap hs_e
-    go wrap (HsVar _ (L _ var))   = go_head wrap var
-    go wrap hs_e                  = do { e <- dsExpr hs_e; return (wrap e) }
-
-    go_l wrap (L _ hs_e) = go wrap hs_e
-
-    go_head wrap var
+    go wrap (HsPar _ (L _ hs_e))
+       = go wrap hs_e
+    go wrap1 (XExpr (WrapExpr (HsWrap wrap2 hs_e)))
+       = go (wrap1 <.> wrap2) hs_e
+    go wrap (HsAppType ty (L _ hs_e) _)
+       = go (wrap <.> WpTyApp ty) hs_e
+
+    go wrap e@(XExpr (ConLikeTc con tvs tys))
+      = do { let (w_outer, w_inner) = splitWrapper wrap
+           ; w_outer' <- dsHsWrapper w_outer
+           ; w_inner' <- dsHsWrapper w_inner
+           ; ds_con <- dsConLike con tvs tys
+           ; let inst_e  = w_inner' ds_con
+                 inst_ty = exprType inst_e
+           ; checkLevPolyArgs (mkHsWrap w_inner e) inst_ty
+           ; return (w_outer' inst_e) }
+
+    go wrap e@(HsVar _ (L _ var))
       | var `hasKey` withDictKey
-      = ds_withDict wrapped_ty
+      = do { wrap' <- dsHsWrapper wrap
+           ; ds_withDict (exprType (wrap' (varToCoreExpr var))) }
 
       | otherwise
-      = do { checkLevPolyFunction (ppr orig_hs_expr) var wrapped_ty
-             -- See Note [Checking for levity-polymorphic functions]
-             -- Pass orig_hs_expr, so that the user can see entire
-             -- expression with -fprint-typechecker-elaboration
-
+      = do { let (w_outer, w_inner) = splitWrapper wrap
+           ; w_outer' <- dsHsWrapper w_outer
+           ; w_inner' <- dsHsWrapper w_inner
+           ; let inst_e  = w_inner' (varToCoreExpr var)
+                 inst_ty = exprType inst_e
+           ; checkLevPolyFunction (mkHsWrap w_inner e) var inst_ty
            ; dflags <- getDynFlags
-           ; warnAboutIdentities dflags var wrapped_ty
+           ; warnAboutIdentities dflags var inst_ty
+           ; return (w_outer' inst_e) }
+
+    go wrap hs_e
+       = do { wrap' <- dsHsWrapper wrap
+            ; addTyCs FromSource (hsWrapDictBinders wrap) $
+              do { e <- dsExpr hs_e
+                 ; return (wrap' e) } }
+
+splitWrapper :: HsWrapper -> (HsWrapper, HsWrapper)
+-- Split a wrapper w into (outer_wrap <.> inner_wrap), where
+-- inner_wrap does instantiation (type and evidence application)
+-- and outer_wrap is everything else, such as a final cast
+-- See Note [Nasty wrinkle in levity-polymorphic function check]
+splitWrapper wrap
+  = go WpHole wrap
+  where
+    go :: HsWrapper -> HsWrapper -> (HsWrapper, HsWrapper)
+    -- If (go w1 w2) = (w3,w4) then
+    --    - w1 <.> w2  = w3 <.> w4
+    --    - w4 does instantiation only ("instantiator" below)
+    -- 'go' mainly dispatches on w2, using w1 as a work-list
+    -- onto which it pushes stuff in w2 to come back to later
+    go WpHole WpHole              = (WpHole,WpHole)
+    go w      WpHole              = splitWrapper w
+    go w1     (w2 `WpCompose` w3) = go (w1 <.> w2) w3
+
+    go w1 w2 | instantiator w2  = liftSnd (<.> w2) (splitWrapper w1)
+             | otherwise        = (w1 <.> w2, WpHole)
+
+    instantiator (WpTyApp {}) = True
+    instantiator (WpEvApp {}) = True
+    instantiator _            = False
 
-           ; return wrapped_e }
-      where
-        wrapped_e  = wrap (Var var)
-        wrapped_ty = exprType wrapped_e
 
 -- See Note [withDict]
 ds_withDict :: Type -> DsM CoreExpr
@@ -1204,18 +1319,17 @@ ds_withDict wrapped_ty
   , Just (inst_meth_ty, co) <- instNewTyCon_maybe dict_tc dict_args
     -- Check that `st` is equal to `meth_ty[t_i/a_i]`.
   , st `eqType` inst_meth_ty
-  = let sv = mkScaledTemplateLocal 1 $ mkScaled mult1 st
-        k  = mkScaledTemplateLocal 2 $ mkScaled mult2 dt_to_r in
-    pure $ mkLams [sv, k] $ Var k `App` Cast (Var sv) (mkSymCo co)
+  = do { sv <- newSysLocalDs mult1 st
+       ; k  <- newSysLocalDs mult2 dt_to_r
+       ; pure $ mkLams [sv, k] $ Var k `App` Cast (Var sv) (mkSymCo co) }
 
   | otherwise
   = errDsCoreExpr $ hang (text "Invalid instantiation of" <+>
                           quotes (ppr withDictName) <+> text "at type:")
                        4 (ppr wrapped_ty)
 
-{-
-Note [withDict]
-~~~~~~~~~~~~~~~
+{- Note [withDict]
+~~~~~~~~~~~~~~~~~~
 The identifier `withDict` is just a place-holder, which is used to
 implement a primitive that we cannot define in Haskell but we can write
 in Core.  It is declared with a place-holder type:
@@ -1346,13 +1460,29 @@ Some further observations about `withDict`:
 -- instantiated type.  If the function is a hasNoBinding op, and the
 -- type has levity-polymorphic arguments, issue an error.
 -- Note [Checking for levity-polymorphic functions]
-checkLevPolyFunction :: SDoc -> Id -> Type -> DsM ()
-checkLevPolyFunction pp_hs_expr var ty
-  | let bad_tys = isBadLevPolyFunction var ty
+checkLevPolyFunction :: Outputable e => e -> Id -> Type -> DsM ()
+checkLevPolyFunction orig_hs_expr var ty
+  | hasNoBinding var
+  = checkLevPolyArgs orig_hs_expr ty
+  | otherwise
+  = return ()
+
+checkLevPolyArgs :: Outputable e => e -> Type -> DsM ()
+-- Check that there are no levity-polymorphic arguments in
+-- the supplied type
+-- E.g. Given (forall a. t1 -> t2 -> blah), ensure that t1,t2
+--      are not levity-polymorhic
+--
+-- Pass orig_hs_expr, so that the user can see entire thing
+-- Note [Checking for levity-polymorphic functions]
+checkLevPolyArgs orig_hs_expr ty
+  | let (binders, _) = splitPiTys ty
+        arg_tys      = mapMaybe binderRelevantType_maybe binders
+        bad_tys      = filter isTypeLevPoly arg_tys
   , not (null bad_tys)
   = errDs $ vcat
     [ hang (text "Cannot use function with levity-polymorphic arguments:")
-         2 (pp_hs_expr <+> dcolon <+> pprWithTYPE ty)
+         2 (hang (ppr orig_hs_expr) 2 (dcolon <+> pprWithTYPE ty))
     , ppUnlessOption sdocPrintTypecheckerElaboration $ vcat
         [ text "(Note that levity-polymorphic primops such as 'coerce' and unboxed tuples"
         , text "are eta-expanded internally because they must occur fully saturated."
@@ -1364,18 +1494,4 @@ checkLevPolyFunction pp_hs_expr var ty
            bad_tys
     ]
 
-checkLevPolyFunction _ _ _ = return ()
-
--- | Is this a hasNoBinding Id with a levity-polymorphic type?
--- Returns the arguments that are levity polymorphic if they are bad;
--- or an empty list otherwise
--- Note [Checking for levity-polymorphic functions]
-isBadLevPolyFunction :: Id -> Type -> [Type]
-isBadLevPolyFunction id ty
-  | hasNoBinding id
-  = filter isTypeLevPoly arg_tys
-  | otherwise
-  = []
-  where
-    (binders, _) = splitPiTys ty
-    arg_tys      = mapMaybe binderRelevantType_maybe binders
+  | otherwise = return ()
diff --git a/compiler/GHC/HsToCore/Match.hs b/compiler/GHC/HsToCore/Match.hs
index 6bd3860e42..a5960529c5 100644
--- a/compiler/GHC/HsToCore/Match.hs
+++ b/compiler/GHC/HsToCore/Match.hs
@@ -1062,7 +1062,7 @@ viewLExprEq (e1,_) (e2,_) = lexp e1 e2
     exp (XExpr (ExpansionExpr (HsExpanded _ b))) (XExpr (ExpansionExpr (HsExpanded _ b'))) =
       exp b b'
     exp (HsVar _ i) (HsVar _ i') =  i == i'
-    exp (HsConLikeOut _ c) (HsConLikeOut _ c') = c == c'
+    exp (XExpr (ConLikeTc c _ _)) (XExpr (ConLikeTc c' _ _)) = c == c'
     -- the instance for IPName derives using the id, so this works if the
     -- above does
     exp (HsIPVar _ i) (HsIPVar _ i') = i == i'
diff --git a/compiler/GHC/HsToCore/Utils.hs b/compiler/GHC/HsToCore/Utils.hs
index 75dab7680f..002cf8d4b2 100644
--- a/compiler/GHC/HsToCore/Utils.hs
+++ b/compiler/GHC/HsToCore/Utils.hs
@@ -1076,7 +1076,7 @@ isTrueLHsExpr (L _ (HsVar _ (L _ v)))
      || v `hasKey` getUnique trueDataConId
                                               = Just return
         -- trueDataConId doesn't have the same unique as trueDataCon
-isTrueLHsExpr (L _ (HsConLikeOut _ con))
+isTrueLHsExpr (L _ (XExpr (ConLikeTc con _ _)))
   | con `hasKey` getUnique trueDataCon = Just return
 isTrueLHsExpr (L _ (HsTick _ tickish e))
     | Just ticks <- isTrueLHsExpr e
diff --git a/compiler/GHC/Iface/Ext/Ast.hs b/compiler/GHC/Iface/Ext/Ast.hs
index 5a787f5b94..692e4a2213 100644
--- a/compiler/GHC/Iface/Ext/Ast.hs
+++ b/compiler/GHC/Iface/Ext/Ast.hs
@@ -175,9 +175,6 @@ Here is an extract from the `ToHie` instance for (LHsExpr (GhcPass p)):
         [ toHie $ C Use (L mspan var)
              -- Patch up var location since typechecker removes it
         ]
-      HsConLikeOut _ con ->
-        [ toHie $ C Use $ L mspan $ conLikeName con
-        ]
       ...
       HsApp _ a b ->
         [ toHie a
@@ -738,7 +735,7 @@ instance HiePass p => HasType (LocatedA (HsExpr (GhcPass p))) where
               HsLit _ l -> Just (hsLitType l)
               HsOverLit _ o -> Just (overLitType o)
 
-              HsConLikeOut _ (RealDataCon con) -> Just (dataConNonlinearType con)
+              XExpr (ConLikeTc (RealDataCon con) _ _) -> Just (dataConNonlinearType con)
 
               HsLam     _ (MG { mg_ext = groupTy }) -> Just (matchGroupType groupTy)
               HsLamCase _ (MG { mg_ext = groupTy }) -> Just (matchGroupType groupTy)
@@ -775,7 +772,6 @@ instance HiePass p => HasType (LocatedA (HsExpr (GhcPass p))) where
           skipDesugaring :: HsExpr GhcTc -> Bool
           skipDesugaring e = case e of
             HsVar{}             -> False
-            HsConLikeOut{}      -> False
             HsRecFld{}          -> False
             HsOverLabel{}       -> False
             HsIPVar{}           -> False
@@ -1087,9 +1083,6 @@ instance HiePass p => ToHie (LocatedA (HsExpr (GhcPass p))) where
              -- Patch up var location since typechecker removes it
         ]
       HsUnboundVar _ _ -> []  -- there is an unbound name here, but that causes trouble
-      HsConLikeOut _ con ->
-        [ toHie $ C Use $ L mspan $ conLikeName con
-        ]
       HsRecFld _ fld ->
         [ toHie $ RFC RecFieldOcc Nothing (L (locA mspan) fld)
         ]
@@ -1216,14 +1209,14 @@ instance HiePass p => ToHie (LocatedA (HsExpr (GhcPass p))) where
       HsProjection {} -> []
       XExpr x
         | GhcTc <- ghcPass @p
-        , WrapExpr (HsWrap w a) <- x
-        -> [ toHie $ L mspan a
-           , toHie (L mspan w)
-           ]
-        | GhcTc <- ghcPass @p
-        , ExpansionExpr (HsExpanded _ b) <- x
-        -> [ toHie (L mspan b)
-           ]
+        -> case x of
+             WrapExpr (HsWrap w a)
+               -> [ toHie $ L mspan a
+                  , toHie (L mspan w) ]
+             ExpansionExpr (HsExpanded _ b)
+               -> [ toHie (L mspan b) ]
+             ConLikeTc con _ _
+               -> [ toHie $ C Use $ L mspan $ conLikeName con ]
         | otherwise -> []
 
 -- NOTE: no longer have the location
diff --git a/compiler/GHC/Tc/Gen/Expr.hs b/compiler/GHC/Tc/Gen/Expr.hs
index 98d8e8c278..0ff73863cc 100644
--- a/compiler/GHC/Tc/Gen/Expr.hs
+++ b/compiler/GHC/Tc/Gen/Expr.hs
@@ -329,10 +329,9 @@ tcExpr expr@(ExplicitTuple x tup_args boxity) res_ty
        ; let expr'       = ExplicitTuple x tup_args1 boxity
              missing_tys = [Scaled mult ty | (Missing (Scaled mult _), ty) <- zip tup_args1 arg_tys]
 
-             -- See Note [Linear fields generalization] in GHC.Tc.Gen.App
-             act_res_ty
-                 = mkVisFunTys missing_tys (mkTupleTy1 boxity arg_tys)
-                   -- See Note [Don't flatten tuples from HsSyn] in GHC.Core.Make
+             -- See Note [Typechecking data constructors] in GHC.Tc.Gen.Head
+             -- See Note [Don't flatten tuples from HsSyn] in GHC.Core.Make
+             act_res_ty = mkVisFunTys missing_tys (mkTupleTy1 boxity arg_tys)
 
        ; traceTc "ExplicitTuple" (ppr act_res_ty $$ ppr res_ty)
 
@@ -870,7 +869,6 @@ tcExpr e@(HsRnBracketOut _ brack ps) res_ty = tcUntypedBracket e brack ps res_ty
 ************************************************************************
 -}
 
-tcExpr (HsConLikeOut {})   ty = pprPanic "tcExpr:HsConLikeOut" (ppr ty)
 tcExpr (HsOverLabel {})    ty = pprPanic "tcExpr:HsOverLabel"  (ppr ty)
 tcExpr (SectionL {})       ty = pprPanic "tcExpr:SectionL"    (ppr ty)
 tcExpr (SectionR {})       ty = pprPanic "tcExpr:SectionR"    (ppr ty)
diff --git a/compiler/GHC/Tc/Gen/Head.hs b/compiler/GHC/Tc/Gen/Head.hs
index feb984fc26..feef214055 100644
--- a/compiler/GHC/Tc/Gen/Head.hs
+++ b/compiler/GHC/Tc/Gen/Head.hs
@@ -33,7 +33,6 @@ module GHC.Tc.Gen.Head
 import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcExpr, tcCheckMonoExprNC, tcCheckPolyExprNC )
 
 import GHC.Tc.Gen.HsType
-import GHC.Tc.Gen.Pat
 import GHC.Tc.Gen.Bind( chooseInferredQuantifiers )
 import GHC.Tc.Gen.Sig( tcUserTypeSig, tcInstSig, lhsSigWcTypeContextSpan )
 import GHC.Tc.TyCl.PatSyn( patSynBuilderOcc )
@@ -55,7 +54,8 @@ import GHC.Tc.Utils.TcType as TcType
 import GHC.Hs
 import GHC.Types.Id
 import GHC.Types.Id.Info
-import GHC.Core.ConLike
+import GHC.Core.PatSyn( PatSyn )
+import GHC.Core.ConLike( ConLike(..) )
 import GHC.Core.DataCon
 import GHC.Types.Name
 import GHC.Types.Name.Reader
@@ -897,12 +897,8 @@ tc_infer_id id_name
                -- Hence no checkTh stuff here
 
              AGlobal (AConLike cl) -> case cl of
-                 RealDataCon con -> return_data_con con
-                 PatSynCon ps
-                   | Just (expr, ty) <- patSynBuilderOcc ps
-                   -> return (expr, ty)
-                   | otherwise
-                   -> failWithTc (nonBidirectionalErr id_name)
+                 RealDataCon con -> tcInferDataCon con
+                 PatSynCon ps    -> tcInferPatSyn id_name ps
 
              AGlobal (ATyCon ty_con)
                -> fail_tycon global_env ty_con
@@ -931,49 +927,6 @@ tc_infer_id id_name
 
     return_id id = return (HsVar noExtField (noLocA id), idType id)
 
-    return_data_con con
-      = do { let tvs = dataConUserTyVarBinders con
-                 theta = dataConOtherTheta con
-                 args = dataConOrigArgTys con
-                 res = dataConOrigResTy con
-
-           -- See Note [Linear fields generalization]
-           ; mul_vars <- newFlexiTyVarTys (length args) multiplicityTy
-           ; let scaleArgs args' = zipWithEqual "return_data_con" combine mul_vars args'
-                 combine var (Scaled One ty) = Scaled var ty
-                 combine _   scaled_ty       = scaled_ty
-                   -- The combine function implements the fact that, as
-                   -- described in Note [Linear fields generalization], if a
-                   -- field is not linear (last line) it isn't made polymorphic.
-
-                 etaWrapper arg_tys = foldr (\scaled_ty wr -> WpFun WpHole wr scaled_ty empty) WpHole arg_tys
-
-           -- See Note [Instantiating stupid theta]
-           ; let shouldInstantiate = (not (null (dataConStupidTheta con)) ||
-                                      isKindLevPoly (tyConResKind (dataConTyCon con)))
-           ; case shouldInstantiate of
-               True -> do { (subst, tvs') <- newMetaTyVars (binderVars tvs)
-                           ; let tys'   = mkTyVarTys tvs'
-                                 theta' = substTheta subst theta
-                                 args'  = substScaledTys subst args
-                                 res'   = substTy subst res
-                           ; wrap <- instCall (OccurrenceOf id_name) tys' theta'
-                           ; let scaled_arg_tys = scaleArgs args'
-                                 eta_wrap = etaWrapper scaled_arg_tys
-                           ; addDataConStupidTheta con tys'
-                           ; return ( mkHsWrap (eta_wrap <.> wrap)
-                                               (HsConLikeOut noExtField (RealDataCon con))
-                                    , mkVisFunTys scaled_arg_tys res')
-                           }
-               False -> let scaled_arg_tys = scaleArgs args
-                            wrap1 = mkWpTyApps (mkTyVarTys $ binderVars tvs)
-                            eta_wrap = etaWrapper (map unrestricted theta ++ scaled_arg_tys)
-                            wrap2 = mkWpTyLams $ binderVars tvs
-                        in return ( mkHsWrap (wrap2 <.> eta_wrap <.> wrap1)
-                                             (HsConLikeOut noExtField (RealDataCon con))
-                                  , mkInvisForAllTys tvs $ mkInvisFunTysMany theta $ mkVisFunTys scaled_arg_tys res)
-           }
-
 check_local_id :: Id -> TcM ()
 check_local_id id
   = do { checkThLocalId id
@@ -984,47 +937,100 @@ check_naughty lbl id
   | isNaughtyRecordSelector id = failWithTc (naughtyRecordSel lbl)
   | otherwise                  = return ()
 
+tcInferDataCon :: DataCon -> TcM (HsExpr GhcTc, TcSigmaType)
+-- See Note [Typechecking data constructors]
+tcInferDataCon con
+  = do { let tvs   = dataConUserTyVarBinders con
+             theta = dataConOtherTheta con
+             args  = dataConOrigArgTys con
+             res   = dataConOrigResTy con
+             stupid_theta = dataConStupidTheta con
+
+       ; scaled_arg_tys <- mapM linear_to_poly args
+
+       ; let full_theta  = stupid_theta ++ theta
+             all_arg_tys = map unrestricted full_theta ++ scaled_arg_tys
+                -- stupid-theta must come first
+                -- See Note [Instantiating stupid theta]
+
+       ; return ( XExpr (ConLikeTc (RealDataCon con) tvs all_arg_tys)
+                , mkInvisForAllTys tvs $ mkPhiTy full_theta $
+                  mkVisFunTys scaled_arg_tys res ) }
+  where
+    linear_to_poly :: Scaled Type -> TcM (Scaled Type)
+    -- linear_to_poly implements point (3,4)
+    -- of Note [Typechecking data constructors]
+    linear_to_poly (Scaled One ty) = do { mul_var <- newFlexiTyVarTy multiplicityTy
+                                        ; return (Scaled mul_var ty) }
+    linear_to_poly scaled_ty       = return scaled_ty
+
+tcInferPatSyn :: Name -> PatSyn -> TcM (HsExpr GhcTc, TcSigmaType)
+tcInferPatSyn id_name ps
+  = case patSynBuilderOcc ps of
+       Just (expr,ty) -> return (expr,ty)
+       Nothing        -> failWithTc (nonBidirectionalErr id_name)
+
 nonBidirectionalErr :: Outputable name => name -> SDoc
 nonBidirectionalErr name = text "non-bidirectional pattern synonym"
                            <+> quotes (ppr name) <+> text "used in an expression"
 
-{-
-Note [Linear fields generalization]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-As per Note [Polymorphisation of linear fields], linear field of data
-constructors get a polymorphic type when the data constructor is used as a term.
+{- Note [Typechecking data constructors]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+As per Note [Polymorphisation of linear fields] in
+GHC.Core.Multiplicity, linear fields of data constructors get a
+polymorphic multiplicity when the data constructor is used as a term:
+
+    Just :: forall {p} a. a %p -> Maybe a
 
-    Just :: forall {p} a. a #p-> Maybe a
+So at an occurrence of a data constructor we do the following,
+mostly in tcInferDataCon:
 
-This rule is known only to the typechecker: Just keeps its linear type in Core.
+1. Get its type, say
+    K :: forall (r :: RuntimeRep) (a :: TYPE r). a %1 -> T r a
+   Note the %1: it is linear
 
-In order to desugar this generalised typing rule, we simply eta-expand:
+2. We are going to return a ConLikeTc, thus:
+     XExpr (ConLikeTc K [r,a] [Scaled p a])
+      :: forall (r :: RuntimeRep) (a :: Type r). a %p -> T r a
+   where 'p' is a fresh multiplicity unification variable.
 
-    \a (x # p :: a) -> Just @a x
+   To get the returned ConLikeTc, we allocate a fresh multiplicity
+   variable for each linear argument, and store the type, scaled by
+   the fresh multiplicity variable in the ConLikeTc; along with
+   the type of the ConLikeTc. This is done by linear_to_poly.
 
-has the appropriate type. We insert these eta-expansion with WpFun wrappers.
+3. If the argument is not linear (perhaps explicitly declared as
+   non-linear by the user), don't bother with this.
 
-A small hitch: if the constructor is levity-polymorphic (unboxed tuples, sums,
-certain newtypes with -XUnliftedNewtypes) then this strategy produces
+4. The (ConLikeTc K [r,a] [Scaled p a]) is later desugared by
+   GHC.HsToCore.Expr.dsConLike to:
+     (/\r a. \(x %p :: a). K @r @a x)
+   which has the desired type given in the previous bullet.
+   The 'p' is the multiplicity unification variable, which
+   will by now have been unified to something, or defaulted in
+   `GHC.Tc.Utils.Zonk.commitFlexi`. So it won't just be an
+   (unbound) variable.
 
-    \r1 r2 a b (x # p :: a) (y # q :: b) -> (# a, b #)
+Wrinkles
 
-Which has type
+* Why put [InvisTVBinder] in ConLikeTc, when we only need [TyVar] to
+  desugar?  It's a bit of a toss-up, but having [InvisTvBinder] supports
+  a future hsExprType :: HsExpr GhcTc -> Type
 
-    forall r1 r2 a b. a #p-> b #q-> (# a, b #)
+* Note that the [InvisTvBinder] is strictly redundant anyway; it's
+  just the dataConUserTyVarBinders of the data constructor.  Similarly
+  in the [Scaled TcType] field of ConLikeTc, the type comes directly
+  from the data constructor.  The only bit that /isn't/ redundant is the
+  fresh multiplicity variables!
 
-Which violates the levity-polymorphism restriction see Note [Levity polymorphism
-checking] in DsMonad.
+  So an alternative would be to define ConLikeTc like this:
+      | ConLikeTc [TcType]    -- Just the multiplicity variables
+  But then the desugarer (and hsExprType, when we implement it) would
+  need to repeat some of the work done here.  So for now at least
+  ConLikeTc records this strictly-redundant info.
 
-So we really must instantiate r1 and r2 rather than quantify over them.  For
-simplicity, we just instantiate the entire type, as described in Note
-[Instantiating stupid theta]. It breaks visible type application with unboxed
-tuples, sums and levity-polymorphic newtypes, but this doesn't appear to be used
-anywhere.
+* See Note [Instantiating stupid theta] for an extra wrinkle
 
-A better plan: let's force all representation variable to be *inferred*, so that
-they are not subject to visible type applications. Then we can instantiate
-inferred argument eagerly.
 
 Note [Adding the implicit parameter to 'assert']
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1037,15 +1043,31 @@ being able to reconstruct the exact original program.
 
 Note [Instantiating stupid theta]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Normally, when we infer the type of an Id, we don't instantiate,
-because we wish to allow for visible type application later on.
-But if a datacon has a stupid theta, we're a bit stuck. We need
-to emit the stupid theta constraints with instantiated types. It's
-difficult to defer this to the lazy instantiation, because a stupid
-theta has no spot to put it in a type. So we just instantiate eagerly
-in this case. Thus, users cannot use visible type application with
-a data constructor sporting a stupid theta. I won't feel so bad for
-the users that complain.
+Consider a data type with a "stupid theta":
+  data Ord a => T a = MkT (Maybe a)
+
+We want to generate an Ord constraint for every use of MkT; but
+we also want to allow visible type application, such as
+   MkT @Int
+
+So we generate (ConLikeTc MkT [a] [Ord a, Maybe a]), with type
+   forall a. Ord a => Maybe a -> T a
+
+Now visible type application will work fine. But we desugar the
+ConLikeTc to
+   /\a \(d:Ord a) (x:Maybe a). MkT x
+Notice that 'd' is dropped in this desugaring. We don't need it;
+it was only there to generate a Wanted constraint. (That is why
+it is stupid.)  To achieve this:
+
+* We put the stupid-thata at the front of the list of argument
+  types in ConLikeTc
+
+* GHC.HsToCore.Expr.dsConLike generates /lambdas/ for all the
+  arguments, but drops the stupid-theta arguments when building the
+  /application/.
+
+Nice.
 -}
 
 {-
diff --git a/compiler/GHC/Tc/TyCl/Instance.hs b/compiler/GHC/Tc/TyCl/Instance.hs
index 5a824b0e48..fb83e99583 100644
--- a/compiler/GHC/Tc/TyCl/Instance.hs
+++ b/compiler/GHC/Tc/TyCl/Instance.hs
@@ -1250,8 +1250,8 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds })
                      --    con_app_tys  = MkD ty1 ty2
                      --    con_app_scs  = MkD ty1 ty2 sc1 sc2
                      --    con_app_args = MkD ty1 ty2 sc1 sc2 op1 op2
-             con_app_tys  = mkHsWrap (mkWpTyApps inst_tys)
-                                  (HsConLikeOut noExtField (RealDataCon dict_constr))
+             con_app_tys  = mkHsWrap (mkWpTyApps inst_tys) $
+                            mkConLikeTc (RealDataCon dict_constr)
                        -- NB: We *can* have covars in inst_tys, in the case of
                        -- promoted GADT constructors.
 
diff --git a/compiler/GHC/Tc/TyCl/PatSyn.hs b/compiler/GHC/Tc/TyCl/PatSyn.hs
index 6f8e1ef901..2ba02e3584 100644
--- a/compiler/GHC/Tc/TyCl/PatSyn.hs
+++ b/compiler/GHC/Tc/TyCl/PatSyn.hs
@@ -959,7 +959,7 @@ tcPatSynBuilderBind prag_fn (PSB { psb_id = ps_lname@(L loc ps_name)
 patSynBuilderOcc :: PatSyn -> Maybe (HsExpr GhcTc, TcSigmaType)
 patSynBuilderOcc ps
   | Just (_, builder_ty, add_void_arg) <- patSynBuilder ps
-  , let builder_expr = HsConLikeOut noExtField (PatSynCon ps)
+  , let builder_expr = mkConLikeTc (PatSynCon ps)
   = Just $
     if add_void_arg
     then ( builder_expr   -- still just return builder_expr; the void# arg
diff --git a/compiler/GHC/Tc/Types/Origin.hs b/compiler/GHC/Tc/Types/Origin.hs
index 668dbb024c..b386c65a39 100644
--- a/compiler/GHC/Tc/Types/Origin.hs
+++ b/compiler/GHC/Tc/Types/Origin.hs
@@ -499,7 +499,6 @@ exprCtOrigin :: HsExpr GhcRn -> CtOrigin
 exprCtOrigin (HsVar _ (L _ name)) = OccurrenceOf name
 exprCtOrigin (HsGetField _ _ (L _ f)) = HasFieldOrigin (unLoc $ hflLabel f)
 exprCtOrigin (HsUnboundVar {})    = Shouldn'tHappenOrigin "unbound variable"
-exprCtOrigin (HsConLikeOut {})    = panic "exprCtOrigin HsConLikeOut"
 exprCtOrigin (HsRecFld _ f)       = OccurrenceOfRecSel (rdrNameAmbiguousFieldOcc f)
 exprCtOrigin (HsOverLabel _ l)    = OverLabelOrigin l
 exprCtOrigin (ExplicitList {})    = ListOrigin
diff --git a/compiler/GHC/Tc/Utils/Zonk.hs b/compiler/GHC/Tc/Utils/Zonk.hs
index 96118af3b3..bca87fb293 100644
--- a/compiler/GHC/Tc/Utils/Zonk.hs
+++ b/compiler/GHC/Tc/Utils/Zonk.hs
@@ -810,8 +810,6 @@ zonkExpr env (HsRecFld _ (Ambiguous v occ))
 zonkExpr env (HsRecFld _ (Unambiguous v occ))
   = return (HsRecFld noExtField (Unambiguous (zonkIdOcc env v) occ))
 
-zonkExpr _ e@(HsConLikeOut {}) = return e
-
 zonkExpr _ (HsIPVar x id)
   = return (HsIPVar x id)
 
@@ -1009,6 +1007,14 @@ zonkExpr env (XExpr (WrapExpr (HsWrap co_fn expr)))
 zonkExpr env (XExpr (ExpansionExpr (HsExpanded a b)))
   = XExpr . ExpansionExpr . HsExpanded a <$> zonkExpr env b
 
+zonkExpr env (XExpr (ConLikeTc con tvs tys))
+  = XExpr . ConLikeTc con tvs <$> mapM zonk_scale tys
+  where
+    zonk_scale (Scaled m ty) = Scaled <$> zonkTcTypeToTypeX env m <*> pure ty
+    -- Only the multiplicity can contain unification variables
+    -- The tvs come straight from the data-con, and so are strictly redundant
+    -- See Wrinkles of Note [Typechecking data constructors] in GHC.Tc.Gen.Head
+
 zonkExpr _ expr = pprPanic "zonkExpr" (ppr expr)
 
 -------------------------------------------------------------------------