Fix erroneous float in CoreOptwip/T16918

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

6 files changed, 100 insertions, 7 deletions

diff --git a/compiler/coreSyn/CoreLint.hs b/compiler/coreSyn/CoreLint.hs
index 91760c282b..2b8a0b37ab 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
diff --git a/testsuite/tests/simplCore/should_compile/T16918.hs b/testsuite/tests/simplCore/should_compile/T16918.hs
new file mode 100644
index 0000000000..87113b4d96
--- /dev/null
+++ b/testsuite/tests/simplCore/should_compile/T16918.hs
@@ -0,0 +1,7 @@
+module Bug where
+
+pokeArray :: () -> ()
+pokeArray = pokeArray
+
+pokeSockAddr :: String -> () -> ()
+pokeSockAddr path p = (case path of ('\0':_) -> pokeArray) p
diff --git a/testsuite/tests/simplCore/should_compile/T16918a.hs b/testsuite/tests/simplCore/should_compile/T16918a.hs
new file mode 100644
index 0000000000..8b676f83c4
--- /dev/null
+++ b/testsuite/tests/simplCore/should_compile/T16918a.hs
@@ -0,0 +1,25 @@
+{-# LANGUAGE ForeignFunctionInterface #-}
+module Bug where
+
+import Data.Word
+import Foreign
+import Foreign.C.String
+import Foreign.C.Types
+
+type CSaFamily = (Word16)
+data SockAddr = SockAddrUnix String
+
+pokeSockAddr :: Ptr a -> SockAddr -> IO ()
+pokeSockAddr p (SockAddrUnix path) = do
+    case path of
+      ('\0':_) -> zeroMemory p (110)
+      _        -> return ()
+    ((\hsc_ptr -> pokeByteOff hsc_ptr 0)) p ((1) :: CSaFamily)
+    let pathC = map castCharToCChar path
+        poker = case path of ('\0':_) -> pokeArray; _ -> pokeArray0 0
+    poker (((\hsc_ptr -> hsc_ptr `plusPtr` 2)) p) pathC
+
+foreign import ccall unsafe "string.h" memset :: Ptr a -> CInt -> CSize -> IO ()
+
+zeroMemory :: Ptr a -> CSize -> IO ()
+zeroMemory dest nbytes = memset dest 0 (fromIntegral nbytes)
diff --git a/testsuite/tests/simplCore/should_compile/all.T b/testsuite/tests/simplCore/should_compile/all.T
index 2fbe84a49e..768012d451 100644
--- a/testsuite/tests/simplCore/should_compile/all.T
+++ b/testsuite/tests/simplCore/should_compile/all.T
@@ -303,3 +303,5 @@ test('T15631',
 test('T15673', normal, compile, ['-O'])
 test('T16288', normal, multimod_compile, ['T16288B', '-O -dcore-lint -v0'])
 test('T16348', normal, compile, ['-O'])
+test('T16918', normal, compile, ['-O'])
+test('T16918a', normal, compile, ['-O'])