Applications: note that the argument may be a Type.

See CoreSyn#let_app_invariant for another invariant

Recursive and non recursive lets. Operationally this corresponds to allocating a thunk for the things bound and then executing the sub-expression.

The right hand sides of all top-level and recursive lets must be of lifted type (see Type#type_classification for the meaning of lifted vs. unlifted).

The right hand side of of a non-recursive Let _and_ the argument of an App, may be of unlifted type, but only if the expression is ok-for-speculation. This means that the let can be floated around without difficulty. For example, this is OK:

 y::Int# = x +# 1#

But this is not, as it may affect termination if the expression is floated out:

 y::Int# = fac 4#

In this situation you should use case rather than a let. The function CoreUtils.needsCaseBinding can help you determine which to generate, or alternatively use MkCore.mkCoreLet rather than this constructor directly, which will generate a case if necessary

We allow a non-recursive let to bind a type variable, thus:

 Let (NonRec tv (Type ty)) body

This can be very convenient for postponing type substitutions until the next run of the simplifier.

At the moment, the rest of the compiler only deals with type-let in a Let expression, rather than at top level. We may want to revist this choice.

Case split. Operationally this corresponds to evaluating the scrutinee (expression examined) to weak head normal form and then examining at most one level of resulting constructor (i.e. you cannot do nested pattern matching directly with this).

The binder gets bound to the value of the scrutinee, and the Type must be that of all the case alternatives

This is one of the more complicated elements of the Core language, and comes with a number of restrictions:

The DEFAULT case alternative must be first in the list, if it occurs at all.

The remaining cases are in order of increasing tag (for DataAlts) or lit (for LitAlts). This makes finding the relevant constructor easy, and makes comparison easier too.

The list of alternatives must be exhaustive. An exhaustive case does not necessarily mention all constructors:

      data Foo = Red | Green | Blue
 ... case x of 
      Red   -> True
      other -> f (case x of 
                      Green -> ...
                      Blue  -> ... ) ...

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

It ain't one of these constructors. OtherCon xs also indicates that something has been evaluated and hence there's no point in re-evaluating it. OtherCon [] is used even for non-data-type values to indicated evaluated-ness. Notably:

 data C = C !(Int -> Int)
 case x of { C f -> ... }

Here, f gets an OtherCon [] unfolding.

An unfolding with redundant cached information. Parameters:

1) Template used to perform unfolding; binder-info is correct

2) Is this a top level binding?

3) exprIsHNF template (cached); it is ok to discard a seq on this variable

4) Does this waste only a little work if we expand it inside an inlining? Basically this is a cached version of exprIsCheap

5) Tells us about the size of the unfolding template