works in the interactive prover but not in the .idr

gistfile1.idr

-- error at line 109 col 15
--     When elaborating an application of function sym:
--             Can't unify
--                     progDenote (compile e__2 ++ p) s = progDenote p (expDenote e__2 :: s)
--             with
--                     argTy -> retTy
--             
--             Specifically:
--                     Can't unify
--                             ((Maybe (List Nat)) = (Maybe (List Nat))) (progDenote (compile e__2 ++ p) s)
--                     with
--                             \{uv0} => argTy -> uv


%default total

||| This is an Idris translation of Chapter 2 of “Certified Programming with
||| Dependent Types” (http://adam.chlipala.net/cpdt/html/StackMachine.html)

-- 2.1.1

%elim
data binop : Type where
  Plus : binop
  Times : binop

%elim
data exp : Type where
  Const : Nat -> exp
  Binop : binop -> exp -> exp -> exp

binopDenote : binop -> Nat -> Nat -> Nat
binopDenote Plus = plus
binopDenote Times = mult

expDenote : exp -> Nat
expDenote (Const n) = n
expDenote (Binop b e1 e2) = (binopDenote b) (expDenote e1) (expDenote e2)

{-
> expDenote (Const 42)
42 : Nat
> expDenote (Binop Plus (Const 2) (Const 2))
4 : Nat
> expDenote (Binop Times (Binop Plus (Const 2) (Const 2)) (Const 7))
28 : Nat
-}

-- 2.1.2

data instr : Type where
  iConst : Nat -> instr
  iBinop : binop -> instr

prog : Type
prog = List instr

stack : Type
stack = List Nat

instrDenote : instr -> stack -> Maybe stack
instrDenote (iConst n) s                = Just (n :: s)
instrDenote (iBinop b) (arg1::arg2::s') = Just ((binopDenote b) arg1 arg2 :: s')
instrDenote (iBinop b) _                = Nothing

progDenote : prog -> stack -> Maybe stack
progDenote []      s = Just s
progDenote (i::p') s = case instrDenote i s of
  Nothing => Nothing
  Just s' => progDenote p' s'

-- 2.1.3

compile : exp -> prog
compile (Const n) = [iConst n]
compile (Binop b e1 e2) = compile e2 ++ compile e1 ++ [iBinop b]

{-
> compile (Const 42)
[iConst 42] : List instr
> compile (Binop Plus (Const 2) (Const 2))
[iConst 2, iConst 2, iBinop Plus] : List instr
> compile (Binop Times (Binop Plus (Const 2) (Const 2)) (Const 7))
[iConst 7, iConst 2, iConst 2, iBinop Plus, iBinop Times] : List instr
> progDenote (compile (Const 42)) []
Just [42] : Maybe (List Nat)
> progDenote (compile (Binop Plus (Const 2) (Const 2))) []
Just [4] : Maybe (List Nat)
> progDenote (compile (Binop Times (Binop Plus (Const 2) (Const 2)) (Const 7))) []
Just [28] : Maybe (List Nat)
-}

-- 2.1.4

compileCorrect : (e : exp) -> progDenote (compile e) [] = Just (expDenote e `Prelude.List.(::)` [])
compileCorrect = ?compileCorrectTheorem

compileCorrect' : (e : exp) -> (p : prog) -> (s : stack) ->
                  progDenote (compile e ++ p) s = progDenote p (expDenote e :: s)
compileCorrect' = proof
  intros
  induction e
  intros
  compute
  refine refl
  intros
  compute
  rewrite appendAssociative (compile e__2) (compile e__0 ++ [iBinop b__0]) p
  rewrite sym (ihe__2 ((compile e__0 ++ [iBinop b__0]) ++ p) s)
  rewrite appendAssociative (compile e__0) [iBinop b__0] p
  rewrite sym (ihe__0 (iBinop b__0 :: p) (expDenote e__2 :: s))
  refine refl
--   abandon
--   intro
--   induction e
--   crush

compileCorrectTheorem = proof
  intros
  rewrite (appendNilRightNeutral (compile e))
  rewrite (compileCorrect' e [] [])
  refine refl