Note [Invariants on join points]

Join points must follow these invariants:

  1. All occurrences must be tail calls. Each of these tail calls must pass the
     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. GHC.Core.Utils.joinRhsArity.

     2a. Moreover, this same constraint applies to any unfolding of
         the binder.  Reason: if we want to push a continuation into
         the RHS we must push it into the unfolding as well.

     2b. The Arity (in the IdInfo) of a join point varies independently of the
         join-arity. For example, we could have
             j x = case x of { T -> \y.y; F -> \y.3 }
         Its join-arity is 1, but its idArity is 2; and we do not eta-expand
         join points: see Note [Do not eta-expand join points] in
                          GHC.Core.Opt.Simplify.Utils.

         Allowing the idArity to be bigger than the join-arity is
         important in arityType; see GHC.Core.Opt.Arity
         Note [Arity for recursive join bindings]

         Historical note: see #17294.

  3. If the binding is recursive, then all other bindings in the recursive group
     must also be join points.

  4. The binding's type must not be polymorphic in its return type (as defined
     in Note [The polymorphism rule of join points]).

However, join points have simpler invariants in other ways

  5. A join point can have an unboxed type without the RHS being
     ok-for-speculation (i.e. drop the let-can-float invariant)
     e.g.  let j :: Int# = factorial x in ...

  6. The RHS of join point is not required to have a fixed runtime representation,
     e.g.  let j :: r :: TYPE l = fail (##) in ...
     This happened in an intermediate program #13394

Examples:

  join j1  x = 1 + x in jump j (jump j x)  -- Fails 1: non-tail call
  join j1' x = 1 + x in if even a
                          then jump j1 a
                          else jump j1 a b -- Fails 1: inconsistent calls
  join j2  x = flip (+) x in j2 1 2        -- Fails 2: not enough lambdas
  join j2' x = \y -> x + y in j3 1         -- Passes: extra lams ok
  join j @a (x :: a) = x                   -- Fails 4: polymorphic in ret type

Invariant 1 applies to left-hand sides of rewrite rules, so a rule for a join
point must have an exact call as its LHS.

Strictly speaking, invariant 3 is redundant, since a call from inside a lazy
binding isn't a tail call. Since a let-bound value can't invoke a free join
point, then, they can't be mutually recursive. (A Core binding group *can*
include spurious extra bindings if the occurrence analyser hasn't run, so
invariant 3 does still need to be checked.) For the rigorous definition of
"tail call", see Section 3 of the paper (Note [Join points]).

Invariant 4 is subtle; see Note [The polymorphism rule of join points].

Invariant 6 is to enable code like this:

  f = \(r :: RuntimeRep) (a :: TYPE r) (x :: T).
      join j :: a
           j = error @r @a "bloop"
      in case x of
           A -> j
           B -> j
           C -> error @r @a "blurp"

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.