Eta-expand remaining ValArgs in rebuildHsAppswip/datacon-eta

This patch expands the scope of hasFixedRuntimeRep_remainingValArgs:
instead of simply checking that eta-expansion is possible, actually
perform the eta-expansion then and there.

Changes:

  1. hasFixedRuntimeRep_remainingValArgs renamed to tcRemainingValArgs.
  2. tcRemainingValArgs is now called at the end of tcApp within
     rebuildHsApps; this fills a hole as the logic in the implementation
     of quick-look impredicativity (in quickLookArg1/tcEValArg) mirrors
     in some important aspects the implementation in tcApp.
  3. tcRemainingValArgs now performs eta-expansion (instead of only
     checking whether eta expansion is possible). In particular, it
     eta-expands data constructors up to their arity, allowing us to
     remove the problematic implementation of dsConLike which introduced
     representation-polymorphic lambdas.

Consequences:

  A. rebuildHsApps is now monadic, as necessitated by (2)+(3)
  B. Introduce WpHsLet, a wrapper that creates a let binding.
     This is because we might need to let-bind existing value
     arguments when eta-expanding, to avoid loss of sharing.
     We rename the existing WpLet to WpEvLet, being more specific
     about its nature.
     Some Data and Outputable instances had to be moved to avoid
     recursive imports now HsWrapper, through WpHsLet, mentions HsExpr.
  C. We drop stupid-theta dictionaries in the wrapper for the data
     constructor, which is the only other sensible place for this logic
     to go now that we got rid of dsConLike.

For the moment, the FixedRuntimeRep check in tcRemainingValArgs
is kept as a syntactic check, as a full on PHASE 2 check doesn't jibe
well with the rest of the compiler, which doesn't look at application
chains in a single go.

Fixes #21346.

1 files changed, 32 insertions, 253 deletions

diff --git a/compiler/GHC/Tc/Gen/App.hs b/compiler/GHC/Tc/Gen/App.hs
index 8f59daf24a..ecb79b8248 100644
--- a/compiler/GHC/Tc/Gen/App.hs
+++ b/compiler/GHC/Tc/Gen/App.hs
@@ -2,7 +2,6 @@
 {-# LANGUAGE DataKinds           #-}
 {-# LANGUAGE FlexibleContexts    #-}
 {-# LANGUAGE GADTs               #-}
-{-# LANGUAGE LambdaCase          #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies        #-}
 {-# LANGUAGE UndecidableInstances #-} -- Wrinkle in Note [Trees That Grow]
@@ -22,21 +21,14 @@ module GHC.Tc.Gen.App
 
 import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcPolyExpr )
 
-import GHC.Types.Basic ( Arity, ExprOrPat(Expression) )
-import GHC.Types.Id ( idArity, idName, hasNoBinding )
-import GHC.Types.Name ( isWiredInName )
 import GHC.Types.Var
 import GHC.Builtin.Types ( multiplicityTy )
-import GHC.Core.ConLike  ( ConLike(..) )
-import GHC.Core.DataCon ( dataConRepArity
-                        , isNewDataCon, isUnboxedSumDataCon, isUnboxedTupleDataCon )
 import GHC.Tc.Gen.Head
 import GHC.Hs
 import GHC.Tc.Errors.Types
 import GHC.Tc.Utils.Monad
 import GHC.Tc.Utils.Unify
 import GHC.Tc.Utils.Instantiate
-import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep_syntactic )
 import GHC.Tc.Instance.Family ( tcGetFamInstEnvs, tcLookupDataFamInst_maybe )
 import GHC.Tc.Gen.HsType
 import GHC.Tc.Utils.TcMType
@@ -331,28 +323,16 @@ tcApp :: HsExpr GhcRn -> ExpRhoType -> TcM (HsExpr GhcTc)
 -- See Note [tcApp: typechecking applications]
 tcApp rn_expr exp_res_ty
   | (fun@(rn_fun, fun_ctxt), rn_args) <- splitHsApps rn_expr
-  = do { (tc_fun, fun_sigma) <- tcInferAppHead fun rn_args
+  = do { traceTc "tcApp {" $
+           vcat [ text "rn_fun:" <+> ppr rn_fun
+                , text "rn_args:" <+> ppr rn_args ]
+
+       ; (tc_fun, fun_sigma) <- tcInferAppHead fun rn_args
 
        -- Instantiate
        ; do_ql <- wantQuickLook rn_fun
        ; (delta, inst_args, app_res_rho) <- tcInstFun do_ql True fun fun_sigma rn_args
 
-       -- Check for representation polymorphism in the case that
-       -- the head of the application is a primop or data constructor
-       -- which has argument types that are representation-polymorphic.
-       -- This amounts to checking that the leftover argument types,
-       -- up until the arity, are not representation-polymorphic,
-       -- so that we can perform eta-expansion later without introducing
-       -- representation-polymorphic binders.
-       --
-       -- See Note [Checking for representation-polymorphic built-ins]
-       ; traceTc "tcApp FRR" $
-           vcat
-             [ text "tc_fun =" <+> ppr tc_fun
-             , text "inst_args =" <+> ppr inst_args
-             , text "app_res_rho =" <+> ppr app_res_rho ]
-       ; hasFixedRuntimeRep_remainingValArgs inst_args app_res_rho tc_fun
-
        -- Quick look at result
        ; app_res_rho <- if do_ql
                         then quickLookResultType delta app_res_rho exp_res_ty
@@ -375,239 +355,33 @@ tcApp rn_expr exp_res_ty
        ; res_co <- perhaps_add_res_ty_ctxt $
                    unifyExpectedType rn_expr app_res_rho exp_res_ty
 
-       ; whenDOptM Opt_D_dump_tc_trace $
-         do { inst_args <- mapM zonkArg inst_args  -- Only when tracing
-            ; traceTc "tcApp" (vcat [ text "rn_fun"       <+> ppr rn_fun
-                               , text "inst_args"    <+> brackets (pprWithCommas pprHsExprArgTc inst_args)
-                               , text "do_ql:  "     <+> ppr do_ql
-                               , text "fun_sigma:  " <+> ppr fun_sigma
-                               , text "delta:      " <+> ppr delta
-                               , text "app_res_rho:" <+> ppr app_res_rho
-                               , text "exp_res_ty:"  <+> ppr exp_res_ty
-                               , text "rn_expr:"     <+> ppr rn_expr ]) }
-
        -- Typecheck the value arguments
        ; tc_args <- tcValArgs do_ql inst_args
 
-       -- Reconstruct, with a special cases for tagToEnum#.
+       -- Reconstruct, with a special case for tagToEnum#.
        ; tc_expr <-
           if isTagToEnum rn_fun
           then tcTagToEnum tc_fun fun_ctxt tc_args app_res_rho
-          else do return (rebuildHsApps tc_fun fun_ctxt tc_args)
+          else do rebuildHsApps tc_fun fun_ctxt tc_args app_res_rho
+
+       ; whenDOptM Opt_D_dump_tc_trace $
+         do { inst_args <- mapM zonkArg inst_args  -- Only when tracing
+            ; traceTc "tcApp }" (vcat [ text "rn_fun:"      <+> ppr rn_fun
+                                      , text "rn_args:"     <+> ppr rn_args
+                                      , text "inst_args"    <+> brackets (pprWithCommas pprHsExprArgTc inst_args)
+                                      , text "do_ql:  "     <+> ppr do_ql
+                                      , text "fun_sigma:  " <+> ppr fun_sigma
+                                      , text "delta:      " <+> ppr delta
+                                      , text "app_res_rho:" <+> ppr app_res_rho
+                                      , text "exp_res_ty:"  <+> ppr exp_res_ty
+                                      , text "rn_expr:"     <+> ppr rn_expr
+                                      , text "tc_fun:"      <+> ppr tc_fun
+                                      , text "tc_args:"     <+> ppr tc_args
+                                      , text "tc_expr:"     <+> ppr tc_expr ]) }
 
        -- Wrap the result
        ; return (mkHsWrapCo res_co tc_expr) }
 
-{-
-Note [Checking for representation-polymorphic built-ins]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We cannot have representation-polymorphic or levity-polymorphic
-function arguments. See Note [Representation polymorphism invariants]
-in GHC.Core.  That is checked by the calls to `hasFixedRuntimeRep` in
-`tcEValArg`.
-
-But some /built-in/ functions have representation-polymorphic argument
-types. Users can't define such Ids; they are all GHC built-ins or data
-constructors.  Specifically they are:
-
-1. A few wired-in Ids like unsafeCoerce#, with compulsory unfoldings.
-2. Primops, such as raise#.
-3. Newtype constructors with `UnliftedNewtypes` that have
-   a representation-polymorphic argument.
-4. Representation-polymorphic data constructors: unboxed tuples
-   and unboxed sums.
-
-For (1) consider
-  badId :: forall r (a :: TYPE r). a -> a
-  badId = unsafeCoerce# @r @r @a @a
-
-The wired-in function
-  unsafeCoerce# :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
-                   (a :: TYPE r1) (b :: TYPE r2).
-                   a -> b
-has a convenient but representation-polymorphic type. It has no
-binding; instead it has a compulsory unfolding, after which we
-would have
-  badId = /\r /\(a :: TYPE r). \(x::a). ...body of unsafeCorece#...
-And this is no good because of that rep-poly \(x::a).  So we want
-to reject this.
-
-On the other hand
-  goodId :: forall (a :: Type). a -> a
-  goodId = unsafeCoerce# @LiftedRep @LiftedRep @a @a
-
-is absolutely fine, because after we inline the unfolding, the \(x::a)
-is representation-monomorphic.
-
-Test cases: T14561, RepPolyWrappedVar2.
-
-For primops (2) the situation is similar; they are eta-expanded in
-CorePrep to be saturated, and that eta-expansion must not add a
-representation-polymorphic lambda.
-
-Test cases: T14561b, RepPolyWrappedVar, UnliftedNewtypesCoerceFail.
-
-For (3), consider a representation-polymorphic newtype with
-UnliftedNewtypes:
-
-  type Id :: forall r. TYPE r -> TYPE r
-  newtype Id a where { MkId :: a }
-
-  bad :: forall r (a :: TYPE r). a -> Id a
-  bad = MkId @r @a             -- Want to reject
-
-  good :: forall (a :: Type). a -> Id a
-  good = MkId @LiftedRep @a   -- Want to accept
-
-Test cases: T18481, UnliftedNewtypesLevityBinder
-
-So these three cases need special treatment. We add a special case
-in tcApp to check whether an application of an Id has any remaining
-representation-polymorphic arguments, after instantiation and application
-of previous arguments.  This is achieved by the hasFixedRuntimeRep_remainingValArgs
-function, which computes the types of the remaining value arguments, and checks
-that each of these have a fixed runtime representation using hasFixedRuntimeRep.
-
-Wrinkles
-
-* Because of Note [Typechecking data constructors] in GHC.Tc.Gen.Head,
-  we desugar a representation-polymorphic data constructor application
-  like this:
-     (/\(r :: RuntimeRep) (a :: TYPE r) \(x::a). K r a x) @LiftedRep Int 4
-  That is, a rep-poly lambda applied to arguments that instantiate it in
-  a rep-mono way.  It's a bit like a compulsory unfolding that has been
-  inlined, but not yet beta-reduced.
-
-  Because we want to accept this, we switch off Lint's representation
-  polymorphism checks when Lint checks the output of the desugarer;
-  see the lf_check_fixed_rep flag in GHC.Core.Lint.lintCoreBindings.
-
-  We then rely on the simple optimiser to beta reduce these
-  representation-polymorphic lambdas (e.g. GHC.Core.SimpleOpt.simple_app).
-
-* Arity.  We don't want to check for arguments past the
-  arity of the function.  For example
-
-      raise# :: forall {r :: RuntimeRep} (a :: Type) (b :: TYPE r). a -> b
-
-  has arity 1, so an instantiation such as:
-
-      foo :: forall w r (z :: TYPE r). w -> z -> z
-      foo = raise# @w @(z -> z)
-
-  is unproblematic.  This means we must take care not to perform a
-  representation-polymorphism check on `z`.
-
-  To achieve this, we consult the arity of the 'Id' which is the head
-  of the application (or just use 1 for a newtype constructor),
-  and keep track of how many value-level arguments we have seen,
-  to ensure we stop checking once we reach the arity.
-  This is slightly complicated by the need to include both visible
-  and invisible arguments, as the arity counts both:
-  see GHC.Tc.Gen.Head.countVisAndInvisValArgs.
-
-  Test cases: T20330{a,b}
-
--}
-
--- | Check for representation-polymorphism in the remaining argument types
--- of a variable or data constructor, after it has been instantiated and applied to some arguments.
---
--- See Note [Checking for representation-polymorphic built-ins]
-hasFixedRuntimeRep_remainingValArgs :: [HsExprArg 'TcpInst] -> TcRhoType -> HsExpr GhcTc -> TcM ()
-hasFixedRuntimeRep_remainingValArgs applied_args app_res_rho = \case
-
-  HsVar _ (L _ fun_id)
-
-    -- (1): unsafeCoerce#
-    -- 'unsafeCoerce#' is peculiar: it is patched in manually as per
-    -- Note [Wiring in unsafeCoerce#] in GHC.HsToCore.
-    -- Unfortunately, even though its arity is set to 1 in GHC.HsToCore.mkUnsafeCoercePrimPair,
-    -- at this stage, if we query idArity, we get 0. This is because
-    -- we end up looking at the non-patched version of unsafeCoerce#
-    -- defined in Unsafe.Coerce, and that one indeed has arity 0.
-    --
-    -- We thus manually specify the correct arity of 1 here.
-    | idName fun_id == unsafeCoercePrimName
-    -> check_thing fun_id 1 (FRRNoBindingResArg fun_id)
-
-    -- (2): primops and other wired-in representation-polymorphic functions,
-    -- such as 'rightSection', 'oneShot', etc; see bindings with Compulsory unfoldings
-    -- in GHC.Types.Id.Make
-    | isWiredInName (idName fun_id) && hasNoBinding fun_id
-    -> check_thing fun_id (idArity fun_id) (FRRNoBindingResArg fun_id)
-       -- NB: idArity consults the IdInfo of the Id. This can be a problem
-       -- in the presence of hs-boot files, as we might not have finished
-       -- typechecking; inspecting the IdInfo at this point can cause
-       -- strange Core Lint errors (see #20447).
-       -- We avoid this entirely by only checking wired-in names,
-       -- as those are the only ones this check is applicable to anyway.
-
-
-  XExpr (ConLikeTc (RealDataCon con) _ _)
-  -- (3): Representation-polymorphic newtype constructors.
-    | isNewDataCon con
-  -- (4): Unboxed tuples and unboxed sums
-    || isUnboxedTupleDataCon con
-    || isUnboxedSumDataCon con
-    -> check_thing con (dataConRepArity con) (FRRDataConArg Expression con)
-
-  _ -> return ()
-
-  where
-    nb_applied_vis_val_args :: Int
-    nb_applied_vis_val_args = count isHsValArg applied_args
-
-    nb_applied_val_args :: Int
-    nb_applied_val_args = countVisAndInvisValArgs applied_args
-
-    arg_tys :: [(Type,AnonArgFlag)]
-    arg_tys = getRuntimeArgTys app_res_rho
-    -- We do not need to zonk app_res_rho first, because the number of arrows
-    -- in the (possibly instantiated) inferred type of the function will
-    -- be at least the arity of the function.
-
-    check_thing :: Outputable thing
-                => thing
-                -> Arity
-                -> (Int -> FixedRuntimeRepContext)
-                -> TcM ()
-    check_thing thing arity mk_frr_orig = do
-      traceTc "tcApp remainingValArgs check_thing" (debug_msg thing arity)
-      go (nb_applied_vis_val_args + 1) (nb_applied_val_args + 1) arg_tys
-      where
-        go :: Int -- visible value argument index, starting from 1
-                  -- only used to report the argument position in error messages
-           -> Int -- value argument index, starting from 1
-                  -- used to count up to the arity to ensure we don't check too many argument types
-           -> [(Type, AnonArgFlag)] -- run-time argument types
-           -> TcM ()
-        go _ i_val _
-          | i_val > arity
-          = return ()
-        go _ _ []
-          -- Should never happen: it would mean that the arity is higher
-          -- than the number of arguments apparent from the type
-          = pprPanic "hasFixedRuntimeRep_remainingValArgs" (debug_msg thing arity)
-        go i_visval !i_val ((arg_ty, af) : tys)
-          = case af of
-              InvisArg ->
-                go i_visval (i_val + 1) tys
-              VisArg   -> do
-                hasFixedRuntimeRep_syntactic (mk_frr_orig i_visval) arg_ty
-                go (i_visval + 1) (i_val + 1) tys
-
-    -- A message containing all the relevant info, in case this functions
-    -- needs to be debugged again at some point.
-    debug_msg :: Outputable thing => thing -> Arity -> SDoc
-    debug_msg thing arity =
-      vcat
-        [ text "thing =" <+> ppr thing
-        , text "arity =" <+> ppr arity
-        , text "applied_args =" <+> ppr applied_args
-        , text "nb_applied_val_args =" <+> ppr nb_applied_val_args
-        , text "arg_tys =" <+> ppr arg_tys ]
-
 --------------------
 wantQuickLook :: HsExpr GhcRn -> TcM Bool
 -- GHC switches on impredicativity all the time for ($)
@@ -645,6 +419,7 @@ zonkArg arg = return arg
 
 
 ----------------
+
 tcValArgs :: Bool                    -- Quick-look on?
           -> [HsExprArg 'TcpInst]    -- Actual argument
           -> TcM [HsExprArg 'TcpTc]  -- Resulting argument
@@ -694,9 +469,13 @@ tcEValArg ctxt (ValArgQL { va_expr = larg@(L arg_loc _)
   = addArgCtxt ctxt larg $
     do { traceTc "tcEValArgQL {" (vcat [ ppr inner_fun <+> ppr inner_args ])
        ; tc_args <- tcValArgs True inner_args
-       ; co      <- unifyType Nothing app_res_rho exp_arg_sigma
-       ; let arg' = mkHsWrapCo co $ rebuildHsApps inner_fun fun_ctxt tc_args
-       ; traceTc "tcEValArgQL }" empty
+
+       ; co   <- unifyType Nothing app_res_rho exp_arg_sigma
+       ; arg' <- mkHsWrapCo co <$> rebuildHsApps inner_fun fun_ctxt tc_args app_res_rho
+       ; traceTc "tcEValArgQL }" $
+           vcat [ text "inner_fun:" <+> ppr inner_fun
+                , text "app_res_rho:" <+> ppr app_res_rho
+                , text "exp_arg_sigma:" <+> ppr exp_arg_sigma ]
        ; return (L arg_loc arg') }
 
 {- *********************************************************************
@@ -1418,15 +1197,15 @@ tcTagToEnum tc_fun fun_ctxt tc_args res_ty
          check_enumeration res_ty rep_tc
        ; let rep_ty  = mkTyConApp rep_tc rep_args
              tc_fun' = mkHsWrap (WpTyApp rep_ty) tc_fun
-             tc_expr = rebuildHsApps tc_fun' fun_ctxt [val_arg]
              df_wrap = mkWpCastR (mkTcSymCo coi)
+       ; tc_expr <- rebuildHsApps tc_fun' fun_ctxt [val_arg] res_ty
        ; return (mkHsWrap df_wrap tc_expr) }}}}}
 
   | otherwise
   = failWithTc TcRnTagToEnumMissingValArg
 
   where
-    vanilla_result = return (rebuildHsApps tc_fun fun_ctxt tc_args)
+    vanilla_result = rebuildHsApps tc_fun fun_ctxt tc_args res_ty
 
     check_enumeration ty' tc
       | isEnumerationTyCon tc = return ()