[Agda] Not understanding some goal solving stuff

[Chris Moline]

Hi, I'm trying to do an exercise from "Dependent Types at Work". The
exercise is from section 4.4 and asks to prove eq-succ and eq-mult-rec. My
problem is I don't understand some of the typing issues.

Here's what I have so far:

>>>
module exercises where

--

data Nat : Set where
  zero : Nat
  succ : Nat -> Nat

_+_ : Nat -> Nat -> Nat
zero + m = m
succ n + m = succ (n + m)

natrec : {C : Nat -> Set} -> (C zero) ->
         ((m : Nat) -> C m -> C (succ m)) -> (n : Nat) -> C n
natrec p h zero = p
natrec p h (succ n) = h n (natrec p h n)

plus : Nat -> Nat -> Nat
plus n m = natrec m (λ x y -> succ y) n

--

data _==_ {A : Set} : A -> A -> Set where
  refl : (a : A) -> a == a

subst : {A : Set} -> {C : A -> Set} -> {a' a'' : A} ->
        a' == a'' -> C a' -> C a''
subst (refl a) c = c

--

eq-succ : {n m : Nat} -> n == m -> succ n == succ m
eq-succ (refl m) = refl (succ m)

eq-plus-rec : (n m : Nat) -> (n + m) == (plus n m)
eq-plus-rec n m = natrec (refl m) (λ j ih -> {! !}) n

<<<

When I replace the hole with 'eq-succ ih', like it is in the pdf, agda
gives an error:

>>>
Refuse to construct infinite term by instantiating _47 to succ
(_n_47 n m k)
when checking that the expression eq-succ ih has type
_n_47 n m (succ k) == _m_48 n m (succ k)
<<<

Sticking a hole in there to try and typing 'c-c c-,' to try and understand
what's happening agda tells me:

>>>
ih : _C_41 n m k'
k' : Nat
m : Nat
n : Nat
<<<

Typing 'c-c c-l' to see what _C_41 is tells me that it has type 'Nat ->
Set'. So is ih a parameterized type? Or is it just a list of types?

If I put 'eq-succ ih' in the hole and type 'c-c c-.' agda tells me

>>>
Goal: _n_50 n m (succ k') == _m_51 n m (succ k')
Have: succ (_n_50 n m k') == succ (_m_51 n m k')
----
ih : _n_50 n m k' == _m_51 n m k'
...
<<<

So I see that to make the definition work I somehow have to move the succ
from the outside to the k' but I don't know what _n_50 n m k' is.

So three questions; how is it I'm constructing an infinite type when I
replace the hole with 'eq-succ ih'? What is '_C_41 n m k'' and '_n_50 n m
k'' and what do I do with them? It's probably a stupid question but I'm
stumped.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140108/12084669/attachment.html