[Agda] Termination proof in partiality monad

[Dan Doel]

Well, I've completed proving fac-↓, sort of. Here are the proofs (hopefully 
it's still properly formatted; I had to modify for 80-columns a bit):

fix-fac-↓₁ : {g : Nat -> D Nat} {n k : Nat}
           -> fix-aux g fac-aux n ↓ k
           -> fix-aux (fac-aux g) fac-aux (suc n) ↓ suc n * k
fix-fac-↓₁ {g} {n} pf with fac-aux g n
fix-fac-↓₁ {g} {n} {k} (converge-now   .k) | now   .k
        = converge-now (suc n * k)
fix-fac-↓₁ {g} {n} {k} (converge-later pf) | later dx
        = converge-later (fix-fac-↓₁ pf) -- problem 1

fac-↓ : forall {n} -> fac n ↓
fac-↓ {0}     = (1 , converge-now 1)
fac-↓ {suc n} with fac-↓ {n}
fac-↓ {suc n} | n! , pf-n!-↓
        = (suc n * n! , converge-later (fix-fac-↓₁ pf-n!-↓)) -- problem 2

Now, here's the rub: both of these don't pass type checking. However, when 
using Agda mode, with, say:

    ... converge-later {fix-fac-↓₁ pf-n!-↓ }0 ...

it *does* pass type checking, and allows insertion. However, upon reloading 
the buffer, Agda complains:

    fix-aux (fac-aux (\x -> fac-aux g x)) fac-aux (suc n)
    | map-D (_*_ (suc n)) (fac-aux (\x -> fac-aux g x) n)
    != fix-aux (fac-aux (fac-aux g)) fac-aux (suc n) of type D Nat

in the first problem area, and:

    (fix-aux (fac-aux (\x -> never)) fac-aux (suc n)
     | map-D (_*_ (suc n)) (fac-aux (\x -> never) n))
    != fix-aux (fac-aux (\_ -> never)) fac-aux (suc n) of type D Nat

in the second. Now, there are two differences I see in those types. First is 
that "\x -> fac-aux g x" is different from "fac-aux g", and "\x -> never" is 
different from "\_ -> never" purely syntactically. However, that can't be the 
problem can it? The other difference is that the former types have the with 
annotations on them. However, when the subgoal is displayed, those aren't 
present, which, I assume, is why the mode lets me put in my expressions, since 
they match the subgoal type.

So, I'm at a bit of a loss as to what's going on here. Is there a way I can 
restructure my proofs to eliminate this problem? Is it possibly a bug of some 
sort?

Thanks for your help.
-- Dan