Can't infer explicit argument to tryGenOp, Can't infer explicit argument to S, Can't infer explicit argument to doAdd

ex_13_1_2.idr

mutual 
  
  tryGenOp : StackCmd () pre (S _) -> StackIO h
  tryGenOp x {pre} {h} = case decEq pre h of
                              (Yes Refl) => do x
                                               res <- Top
                                               PutStr (show res ++ "\n")
                                               stackCalc
                              (No contra) => do PutStr $ "not enough item on the stack, expected " ++
                                                  (show pre) ++
                                                  ", got " ++ 
                                                  (show h) ++ "\n"
                                                stackCalc


  stackCalc : StackIO height
  stackCalc = do PutStr "> "
                 input <- GetStr
                 case strToInput input of
                      Nothing => do PutStr "Invalid Input\n"
                                    stackCalc
                      Just (Number x) => do Push x
                                            stackCalc
                      Just (Add) => tryGenOp doAdd 
                      Just (Sub) => tryGenOp doSubtract
                      Just (Neg) => ?negation

ex_13_1_2.idr:112:28:
Can't infer explicit argument to tryGenOp,
Can't infer explicit argument to S,
Can't infer explicit argument to doAdd