Fix erroneous float in CoreOpt

The simple optimiser was making an invalid transformation
to join points -- yikes.  The fix is easy.

I also added some documentation about the fact that GHC uses
a slightly more restrictive version of join points than does
the paper.

Fix #16918

3 files changed, 66 insertions, 7 deletions

diff --git a/compiler/coreSyn/CoreLint.hs b/compiler/coreSyn/CoreLint.hs
index a84f2fe029..9247498c74 100644
--- a/compiler/coreSyn/CoreLint.hs
+++ b/compiler/coreSyn/CoreLint.hs
@@ -786,8 +786,10 @@ lintCoreExpr (Lam var expr)
 
 lintCoreExpr e@(Case scrut var alt_ty alts) =
        -- Check the scrutinee
-  do { let scrut_diverges = exprIsBottom scrut
-     ; scrut_ty <- markAllJoinsBad $ lintCoreExpr scrut
+  do { scrut_ty <- markAllJoinsBad $ lintCoreExpr scrut
+          -- See Note [Join points are less general than the paper]
+          -- in CoreSyn
+
      ; (alt_ty, _) <- lintInTy alt_ty
      ; (var_ty, _) <- lintInTy (idType var)
 
@@ -810,7 +812,7 @@ lintCoreExpr e@(Case scrut var alt_ty alts) =
               , isAlgTyCon tycon
               , not (isAbstractTyCon tycon)
               , null (tyConDataCons tycon)
-              , not scrut_diverges
+              , not (exprIsBottom scrut)
               -> pprTrace "Lint warning: case binder's type has no constructors" (ppr var <+> ppr (idType var))
                         -- This can legitimately happen for type families
                       $ return ()
@@ -880,6 +882,7 @@ lintCoreFun (Lam var body) nargs
 
 lintCoreFun expr nargs
   = markAllJoinsBadIf (nargs /= 0) $
+      -- See Note [Join points are less general than the paper]
     lintCoreExpr expr
 
 ------------------
diff --git a/compiler/coreSyn/CoreOpt.hs b/compiler/coreSyn/CoreOpt.hs
index fe9e172f38..b490e1b22b 100644
--- a/compiler/coreSyn/CoreOpt.hs
+++ b/compiler/coreSyn/CoreOpt.hs
@@ -312,11 +312,17 @@ simple_app env (Tick t e) as
 -- The let might appear there as a result of inlining
 -- e.g.   let f = let x = e in b
 --        in f a1 a2
--- (#13208)
-simple_app env (Let bind body) as
+--   (#13208)
+-- However, do /not/ do this transformation for join points
+--    See Note [simple_app and join points]
+simple_app env (Let bind body) args
   = case simple_opt_bind env bind of
-      (env', Nothing)   -> simple_app env' body as
-      (env', Just bind) -> Let bind (simple_app env' body as)
+      (env', Nothing)   -> simple_app env' body args
+      (env', Just bind')
+        | isJoinBind bind' -> finish_app env expr' args
+        | otherwise        -> Let bind' (simple_app env' body args)
+        where
+          expr' = Let bind' (simple_opt_expr env' body)
 
 simple_app env e as
   = finish_app env (simple_opt_expr env e) as
@@ -494,6 +500,34 @@ the join-point arity invariant.  #15108 was caused by simplifying
 the RHS with simple_opt_expr, which does eta-reduction.  Solution:
 simplify the RHS of a join point by simplifying under the lambdas
 (which of course should be there).
+
+Note [simple_app and join points]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In general for let-bindings we can do this:
+   (let { x = e } in b) a  ==>  let { x = e } in b a
+
+But not for join points!  For two reasons:
+
+- We would need to push the continuation into the RHS:
+   (join { j = e } in b) a  ==>  let { j' = e a } in b[j'/j] a
+                                      NB ----^^
+  and also change the type of j, hence j'.
+  That's a bit sophisticated for the very simple optimiser.
+
+- We might end up with something like
+    join { j' = e a } in
+    (case blah of        )
+    (  True  -> j' void# ) a
+    (  False -> blah     )
+  and now the call to j' doesn't look like a tail call, and
+  Lint may reject.  I say "may" because this is /explicitly/
+  allowed in the "Compiling without Continuations" paper
+  (Section 3, "Managing \Delta").  But GHC currently does not
+  allow this slightly-more-flexible form.  See CoreSyn
+  Note [Join points are less general than the paper].
+
+The simple thing to do is to disable this transformation
+for join points in the simple optimiser
 -}
 
 ----------------------
diff --git a/compiler/coreSyn/CoreSyn.hs b/compiler/coreSyn/CoreSyn.hs
index 95b05392ae..725e8da826 100644
--- a/compiler/coreSyn/CoreSyn.hs
+++ b/compiler/coreSyn/CoreSyn.hs
@@ -608,6 +608,8 @@ Join points must follow these invariants:
      same number of arguments, counting both types and values; we call this the
      "join arity" (to distinguish from regular arity, which only counts values).
 
+     See Note [Join points are less general than the paper]
+
   2. For join arity n, the right-hand side must begin with at least n lambdas.
      No ticks, no casts, just lambdas!  C.f. CoreUtils.joinRhsArity.
 
@@ -657,6 +659,26 @@ Core Lint will check these invariants, anticipating that any binder whose
 OccInfo is marked AlwaysTailCalled will become a join point as soon as the
 simplifier (or simpleOptPgm) runs.
 
+Note [Join points are less general than the paper]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In the paper "Compiling without continuations", this expression is
+perfectly valid:
+
+    join { j = \_ -> e }
+    in (case blah of       )
+       (  True  -> j void# ) arg
+       (  False -> blah    )
+
+assuming 'j' has arity 1.   Here the call to 'j' does not look like a
+tail call, but actually everything is fine. See Section 3, "Managing \Delta"
+in the paper.
+
+In GHC, however, we adopt a slightly more restrictive subset, in which
+join point calls must be tail calls.  I think we /could/ loosen it up, but
+in fact the simplifier ensures that we always get tail calls, and it makes
+the back end a bit easier I think.  Generally, just less to think about;
+nothing deeper than that.
+
 Note [The type of a join point]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 A join point has the same type it would have as a function. That is, if it takes