Core: the language

   @

   The inner case does not need a @Red@ alternative, because @x@
   can't be @Red@ at that program point.

   This is not checked by Core Lint -- it's very hard to do so.
   E.g. suppose that inner case was floated out, thus:
         let a = case x of
                   Green -> ...
                   Blue  -> ... )
         case x of
           Red   -> True
           other -> f a
   Now it's really hard to see that the Green/Blue case is
   exhaustive.  But it is.

   If you have a case-expression that really /isn't/ exhaustive,
   we may generate seg-faults.  Consider the Green/Blue case
   above.  Since there are only two branches we may generate
   code that tests for Green, and if not Green simply /assumes/
   Blue (since, if the case is exhaustive, that's all that
   remains).  Of course, if it's not Blue and we start fetching
   fields that should be in a Blue constructor, we may die
   horribly. See also Note [Core Lint guarantee] in GHC.Core.Lint.

5. Floating-point values must not be scrutinised against literals.
   See #9238 and Note [Rules for floating-point comparisons]
   in GHC.Core.Opt.ConstantFold for rationale.  Checked in lintCaseExpr;
   see the call to isFloatingPrimTy.

6. The 'ty' field of (Case scrut bndr ty alts) is the type of the
   /entire/ case expression.  Checked in lintAltExpr.
   See also Note [Why does Case have a 'Type' field?].

7. The type of the scrutinee must be the same as the type
   of the case binder, obviously.  Checked in lintCaseExpr.

8. The multiplicity of the binders in constructor patterns must be the
   multiplicity of the corresponding field /scaled by the multiplicity of the
   case binder/. Checked in lintCoreAlt.

         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.

    This contravenes I1 because x's type has kind (TYPE r), which has 'r' free.
    We thus wouldn't know how to compile this lambda abstraction.

Example of I2:

  f (undefined :: (a :: TYPE r))

    This contravenes I2: we are applying the function `f` to a value
    with an unknown runtime representation.

Note that these two invariants require us to check other types than just the
types of bound variables and types of function arguments, due to transformations
that GHC performs. For example, the definition

  myCoerce :: forall {r} (a :: TYPE r) (b :: TYPE r). Coercible a b => a -> b
  myCoerce = coerce

is invalid, because `coerce` has no binding (see GHC.Types.Id.Make.coerceId).
So, before code-generation, GHC saturates the RHS of 'myCoerce' by performing
an eta-expansion (see GHC.CoreToStg.Prep.maybeSaturate):

  myCoerce = \ (x :: TYPE r) -> coerce x

However, this transformation would be invalid, because now the binding of x
in the lambda abstraction would violate I1.

See Note [Representation-polymorphism checking built-ins] in GHC.Tc.Utils.Concrete
and Note [Linting representation-polymorphic builtins] in GHC.Core.Lint for
more details.

Note that we currently require something slightly stronger than a fixed runtime
representation: we check whether bound variables and function arguments have a
/fixed RuntimeRep/ in the sense of Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete.
See Note [Representation polymorphism checking] in GHC.Tc.Utils.Concrete
for an overview of how we enforce these invariants in the typechecker.