Perhaps slightly off-topic. I have looked at the core-spec document, and had a question regarding the operational semantics part.
Given the Core expressions:
case (let r = 1 : r in r) of (x:xs) -> x
An interpreter following the semantics would loop on the above expression, as the S_LetRecReturn rule, the one that throws away let-expressions, never applies.
case (let r = 1 : r in r) of (x:xs) -> x => S_Case + S_LetRec + S_Var case (let r = 1 : r in 1:r) of (x:xs) -> x => S_Case + S_LetRec + S_Var case (let r = 1 : r in 1:1:r) of (x:xs) -> x etc.
Actually, I don't think it would loop, it would just get stuck:
case (let r = 1 : r in r) of (x:xs) -> x => S_Case + S_LetRec + S_Var case (let r = 1 : r in 1:r) of (x:xs) -> x => no more rules step apply
The body of the let-expression can not be reduced any further since it is a constructor application. I assume it should not get stuck, right? So we would need extra step-reduction rules. -- Christiaan