Treat coercions as arguments for floating and inlining

This reverts commit 8924224ecfa065ebc67b96a90d01cf9d2edd0e77
and fixes #17787.

8 files changed, 79 insertions, 18 deletions

diff --git a/compiler/GHC/CoreToStg.hs b/compiler/GHC/CoreToStg.hs
index ead7a12da0..a450f342b0 100644
--- a/compiler/GHC/CoreToStg.hs
+++ b/compiler/GHC/CoreToStg.hs
@@ -198,6 +198,26 @@ import Control.Monad (ap)
 --                 do we set CCCS from it; so we just slam in
 --                 dontCareCostCentre.
 
+-- Note [Coercion tokens]
+-- ~~~~~~~~~~~~~~~~~~~~~~
+-- In coreToStgArgs, we drop type arguments completely, but we replace
+-- coercions with a special coercionToken# placeholder. Why? Consider:
+--
+--   f :: forall a. Int ~# Bool -> a
+--   f = /\a. \(co :: Int ~# Bool) -> error "impossible"
+--
+-- If we erased the coercion argument completely, we’d end up with just
+-- f = error "impossible", but then f `seq` () would be ⊥!
+--
+-- This is an artificial example, but back in the day we *did* treat
+-- coercion lambdas like type lambdas, and we had bug reports as a
+-- result. So now we treat coercion lambdas like value lambdas, but we
+-- treat coercions themselves as zero-width arguments — coercionToken#
+-- has representation VoidRep — which gets the best of both worlds.
+--
+-- (For the gory details, see also the (unpublished) paper, “Practical
+-- aspects of evidence-based compilation in System FC.”)
+
 -- --------------------------------------------------------------
 -- Setting variable info: top-level, binds, RHSs
 -- --------------------------------------------------------------
@@ -357,8 +377,10 @@ coreToStgExpr (App (Lit LitRubbish) _some_unlifted_type)
   -- We lower 'LitRubbish' to @()@ here, which is much easier than doing it in
   -- a STG to Cmm pass.
   = coreToStgExpr (Var unitDataConId)
-coreToStgExpr (Var v)      = coreToStgApp v               [] []
-coreToStgExpr (Coercion _) = coreToStgApp coercionTokenId [] []
+coreToStgExpr (Var v) = coreToStgApp v [] []
+coreToStgExpr (Coercion _)
+  -- See Note [Coercion tokens]
+  = coreToStgApp coercionTokenId [] []
 
 coreToStgExpr expr@(App _ _)
   = coreToStgApp f args ticks
@@ -554,7 +576,7 @@ coreToStgArgs (Type _ : args) = do     -- Type argument
     (args', ts) <- coreToStgArgs args
     return (args', ts)
 
-coreToStgArgs (Coercion _ : args)  -- Coercion argument; replace with place holder
+coreToStgArgs (Coercion _ : args) -- Coercion argument; See Note [Coercion tokens]
   = do { (args', ts) <- coreToStgArgs args
        ; return (StgVarArg coercionTokenId : args', ts) }
 
diff --git a/compiler/basicTypes/MkId.hs b/compiler/basicTypes/MkId.hs
index 6fd99f2fa3..683d136b99 100644
--- a/compiler/basicTypes/MkId.hs
+++ b/compiler/basicTypes/MkId.hs
@@ -1693,7 +1693,7 @@ voidArgId :: Id       -- Local lambda-bound :: Void#
 voidArgId = mkSysLocal (fsLit "void") voidArgIdKey voidPrimTy
 
 coercionTokenId :: Id         -- :: () ~ ()
-coercionTokenId -- Used to replace Coercion terms when we go to STG
+coercionTokenId -- See Note [Coercion tokens] in CoreToStg.hs
   = pcMiscPrelId coercionTokenName
                  (mkTyConApp eqPrimTyCon [liftedTypeKind, liftedTypeKind, unitTy, unitTy])
                  noCafIdInfo
diff --git a/compiler/coreSyn/CoreUnfold.hs b/compiler/coreSyn/CoreUnfold.hs
index ab53451fa2..70f8715db3 100644
--- a/compiler/coreSyn/CoreUnfold.hs
+++ b/compiler/coreSyn/CoreUnfold.hs
@@ -444,8 +444,9 @@ inlineBoringOk e
     go :: Int -> CoreExpr -> Bool
     go credit (Lam x e) | isId x           = go (credit+1) e
                         | otherwise        = go credit e
-    go credit (App f a) | isTyCoArg a      = go credit f
-                        | credit > 0
+        -- See Note [Count coercion arguments in boring contexts]
+    go credit (App f (Type {}))            = go credit f
+    go credit (App f a) | credit > 0
                         , exprIsTrivial a  = go (credit-1) f
     go credit (Tick _ e)                   = go credit e -- dubious
     go credit (Cast e _)                   = go credit e
@@ -591,6 +592,29 @@ Things to note:
     NB: you might think that PostInlineUnconditionally would do this
     but it doesn't fire for top-level things; see SimplUtils
     Note [Top level and postInlineUnconditionally]
+
+Note [Count coercion arguments in boring contexts]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In inlineBoringOK, we ignore type arguments when deciding whether an
+expression is okay to inline into boring contexts. This is good, since
+if we have a definition like
+
+  let y = x @Int in f y y
+
+there’s no reason not to inline y at both use sites — no work is
+actually duplicated. It may seem like the same reasoning applies to
+coercion arguments, and indeed, in #17182 we changed inlineBoringOK to
+treat coercions the same way.
+
+However, this isn’t a good idea: unlike type arguments, which have
+no runtime representation, coercion arguments *do* have a runtime
+representation (albeit the zero-width VoidRep, see Note [Coercion tokens]
+in CoreToStg.hs). This caused trouble in #17787 for DataCon wrappers for
+nullary GADT constructors: the wrappers would be inlined and each use of
+the constructor would lead to a separate allocation instead of just
+sharing the wrapper closure.
+
+The solution: don’t ignore coercion arguments after all.
 -}
 
 uncondInline :: CoreExpr -> Arity -> Int -> Bool
diff --git a/compiler/simplCore/SetLevels.hs b/compiler/simplCore/SetLevels.hs
index 8f70df9d79..60cc676503 100644
--- a/compiler/simplCore/SetLevels.hs
+++ b/compiler/simplCore/SetLevels.hs
@@ -1007,18 +1007,17 @@ notWorthFloating e abs_vars
     go (Tick t e) n  = not (tickishIsCode t) && go e n
     go (Cast e _)  n = go e n
     go (App e arg) n
-       | Type {}     <- arg = go e n
-       | Coercion {} <- arg = go e n
-       | n==0               = False
-       | is_triv arg        = go e (n-1)
-       | otherwise          = False
-    go _ _                  = False
+       -- See Note [Floating applications to coercions]
+       | Type {} <- arg = go e n
+       | n==0           = False
+       | is_triv arg    = go e (n-1)
+       | otherwise      = False
+    go _ _              = False
 
     is_triv (Lit {})              = True        -- Treat all literals as trivial
     is_triv (Var {})              = True        -- (ie not worth floating)
     is_triv (Cast e _)            = is_triv e
-    is_triv (App e (Type {}))     = is_triv e
-    is_triv (App e (Coercion {})) = is_triv e
+    is_triv (App e (Type {}))     = is_triv e   -- See Note [Floating applications to coercions]
     is_triv (Tick t e)            = not (tickishIsCode t) && is_triv e
     is_triv _                     = False
 
@@ -1032,6 +1031,14 @@ Hence the litIsTrivial.
 Ditto literal strings (LitString), which we'd like to float to top
 level, which is now possible.
 
+Note [Floating applications to coercions]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We don’t float out variables applied only to type arguments, since the
+extra binding would be pointless: type arguments are completely erased.
+But *coercion* arguments aren’t (see Note [Coercion tokens] in
+CoreToStg.hs and Note [Count coercion arguments in boring contexts] in
+CoreUnfold.hs), so we still want to float out variables applied only to
+coercion arguments.
 
 Note [Escaping a value lambda]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/testsuite/tests/deSugar/should_compile/T2431.stderr b/testsuite/tests/deSugar/should_compile/T2431.stderr
index e2c903238c..608b26b793 100644
--- a/testsuite/tests/deSugar/should_compile/T2431.stderr
+++ b/testsuite/tests/deSugar/should_compile/T2431.stderr
@@ -10,7 +10,7 @@ T2431.$WRefl [InlPrag=INLINE[0]] :: forall a. a :~: a
  Cpr=m1,
  Unf=Unf{Src=InlineStable, TopLvl=True, Value=True, ConLike=True,
          WorkFree=True, Expandable=True,
-         Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=True)
+         Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=False)
          Tmpl= \ (@a) -> T2431.Refl @a @a @~(<a>_N :: a GHC.Prim.~# a)}]
 T2431.$WRefl
   = \ (@a) -> T2431.Refl @a @a @~(<a>_N :: a GHC.Prim.~# a)
@@ -110,6 +110,3 @@ T2431.$tc'Refl
       $tc'Refl2
       1#
       $krep3
-
-
-
diff --git a/testsuite/tests/simplCore/should_compile/T17787.hs b/testsuite/tests/simplCore/should_compile/T17787.hs
new file mode 100644
index 0000000000..fb6b5c1b98
--- /dev/null
+++ b/testsuite/tests/simplCore/should_compile/T17787.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE GADTs #-}
+module T17787 where
+
+data T a where
+  C :: T ()
+
+foo :: (T () -> T () -> ()) -> ()
+foo f = f C C
diff --git a/testsuite/tests/simplCore/should_compile/T17787.stderr b/testsuite/tests/simplCore/should_compile/T17787.stderr
new file mode 100644
index 0000000000..773e04795e
--- /dev/null
+++ b/testsuite/tests/simplCore/should_compile/T17787.stderr
@@ -0,0 +1,2 @@
+foo :: (T () -> T () -> ()) -> ()
+foo = \ (f :: T () -> T () -> ()) -> f T17787.$WC T17787.$WC
diff --git a/testsuite/tests/simplCore/should_compile/all.T b/testsuite/tests/simplCore/should_compile/all.T
index bd512897a7..276d8479a3 100644
--- a/testsuite/tests/simplCore/should_compile/all.T
+++ b/testsuite/tests/simplCore/should_compile/all.T
@@ -314,3 +314,4 @@ test('T17409',
 test('T17429', normal, compile, ['-dcore-lint -O2'])
 test('T17722', normal, multimod_compile, ['T17722B', '-dcore-lint -O2 -v0'])
 test('T17724', normal, compile, ['-dcore-lint -O2'])
+test('T17787',  [ grep_errmsg(r'foo') ], compile, ['-ddump-simpl -dsuppress-uniques'])