[Agda] Type and termination checking around with clauses

[Peter Berry]

2008/4/30 Ulf Norell <ulfn at cs.chalmers.se>:
>
> A possible work around might be to include the recursive calls in the with
> clause (untested):
>
>  merge (x :: xs) (y :: ys) with x <= y | merge xs (y :: ys) | merge (x ::
> xs) ys
>  ... | true   | rec | _ = x :: rec
>  ... | false | _ | rec = y :: rec
>
> This isn't very nice, but at least it should make the termination checker
> happy. Of course, in this particular case an if_then_else_ would also work.

Aha, I didn't know you could do that. And yes, doh, if_then_else_
makes perfect sense.

> > Possibly related: suppose I have a 'with' clause, say
> >
> > contrived (dprod l p) with l
> > ... | [] = ?0
> > ... | x :: xs = ?1
> >
> > where p : P l for some function P : List ℕ -> Set, say a property
> > which p is a proof of, and somewhere in ?1 I need something of type P
> > (x :: xs) (like a proof of the same property). Clearly x :: xs = l so
> > p will do, but somehow the type checker misses this - it won't unify P
> > l = P (x :: xs). (If you want a concrete example I can provide one.)
>
> If p : P l then in ?1 you should have p : P (x :: xs). If you don't there's
> a bug. A concrete example might be helpful.

Heh, I just realised I prepared this earlier.

module test where

data ⊤ : Set where
  triv : ⊤
data ⊥ : Set where

data Bool : Set where
  false : Bool
  true  : Bool

Atom : Bool -> Set
Atom true  = ⊤
Atom false = ⊥

data ℕ : Set where
  Z : ℕ
  S : ℕ -> ℕ

_<=_ : ℕ -> ℕ -> Bool
Z   <= _   = true
S _ <= Z   = false
S n <= S m = n <= m

-- contrived version, I know it can be done more simply!
trans : {n m o : ℕ} -> Atom (n <= m) -> Atom (m <= o) -> Atom (n <= o)
trans {Z}               triv _ = triv
trans {S _} {Z}         () _
trans {S _} {S _} {Z}   _ ()
trans {S n} {S m} {S o} p q with n <= m
... | false with p
...     | ()
trans {S n} {S m} {S o} p q
    | true with m <= o
...     | true  = trans {n} {m} {o} {! !} {! !}
...     | false with q
...        | ()


The two holes have types Atom (n <= m) and Atom (m <= o) respectively,
which are clearly both equal to ⊤, but the type checker won't accept
'triv' there.

-- 
Peter Berry <pwberry at gmail.com>
Please avoid sending me Word or PowerPoint attachments.
See http://www.gnu.org/philosophy/no-word-attachments.html