[GHC] #10121: operational semantics is incomplete?

[GHC]

#10121: operational semantics is incomplete?
-------------------------------------+-------------------------------------
              Reporter:  javran      |             Owner:
                  Type:  bug         |            Status:  new
              Priority:  normal      |         Milestone:
             Component:              |           Version:  7.8.4
  Documentation                      |  Operating System:  Unknown/Multiple
              Keywords:              |   Type of failure:  None/Unknown
          Architecture:              |        Blocked By:
  Unknown/Multiple                   |   Related Tickets:
             Test Case:              |
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------
 I was trying to read `docs/core-spec/core-spec.pdf` to understand the
 operational semantics for core language. So I started off by playing with
 operational semantics rules manually.

 But I found the following expression gets stuck:

 {{{#!hs
 v1 = let fix = \f -> let x = f x in x
          pf = \f x -> if x == 0
                           then x
                           else f (pred x)
      in (fix pf) 2
 -- S_LETNONREC
 v2 = ((\f -> let x = f x in x)
       (\f x -> if x == 0
                    then x
                    else f (pred x)))
      2
 -- S_APP
 v3 = (let x = (\f x -> if x == 0
                            then x
                            else f (pred x)) x
       in x) 2
 -- S_APP; S_LETREC
 v4 = (let x = (\f x -> if x == 0
                            then x
                            else f (pred x)) x
       in (\f x -> if x == 0
                       then x
                       else f (pred x)) x) 2
 -- S_APP
 v5 = (let x = (\f x -> if x == 0
                            then x
                            else f (pred x)) x
       in (\x1 -> if x1 == 0
                      then x1
                      else x (pred x1))) 2

 }}}

 at this point `x` is not a free variable so `S_LETRECRETURN` cannot be
 applied.

 Did I make it wrong or some rules are missing for the operational
 semantics?

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/10121>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler