The normal form of an expression is determined by the type of the expression

Because the normal form of an expression has a constructor for a type on top, asking for the normal form of an expression without a Type is meaningless in Pie. It isn't possible to normalise anything without type information.

This is why [an expression which is not a type and is not associated with a type is ill-typed].