If the option "-c True" is used, the Haskell Substitution Stepper explains for each step, which reduction rule was chosen. This page explains what the reduction rules mean in detail.
Replace x with definition
During the reduction, the stepper always has a dictionary with bindings. Each binding entry has a named key and a Core Expression. In this reduction step, a reference to a named expression is replaced with the actual expression. This is also known as delta reduction.
Replace x with definition from class dictionary y
In an expression like True /= False, the function /= is implemented in the type class instance of Eq for the Bool type. In Haskell Core, functions defined in type class instances are passed around as a dictionary object. In this reduction step, the function or operator being used is replaced with its definition.
Lamda Application
A lamda is an anonymous function. In this reduction step, a single parameter is passed to the lamda function and the lamda is removed.
Evaluate unsteppable function/operator x
Not every function can be stepped. In this reduction step, a function and its arguments are evaluated.
Reduce Case Expression
Pattern matching with case expr of {...} is used a lot in Haskell Core code. This reduction means that the expr is not yet in head normal form and thus, pattern matching cannot be applied yet. A reduction step is applied to expr to bring it to head normal form.
Replace with matching pattern
This reduction means that a case expr of {...} is replaced with the matching pattern.
Reduce function of application
This reduction is applied to applications like expr arg when expr is not (yet) a lamda: In this case, a reduction step is applied on expr.
Strict reduce application argument
To evaluate unsteppable functions or like +, all the arguments passed to this function have to be strictly reduced. In an expression like x + y, the arguments x and y first are converted to normal form before the + operator is applied. Please note, that this is not always the same approach that GHC would choose.
Reduction complete - reduce constructor arguments for better visualization
The stepper stops the reduction if the expression is in head normal form. Often, the result is a type constructor applied to some (un-reduced) arguments, for example: Just (1 + 1). To make the output more understandable, the stepper reduces the constructor arguments to normal form. The result in this example would be Just 2.
Nested Reductions
An arrow symbol is used to show that a nested reduction was applied. A nested reduction could look like this: Reduce function of application -> Replace x with definition