[Agda] Type and termination checking around with clauses

[Nils Anders Danielsson]

On Wed, Apr 30, 2008 at 6:28 PM, Peter Berry <pwberry at gmail.com> wrote:
>
>  Atom : Bool -> Set
>  Atom true  = ⊤
>  Atom false = ⊥

> _<=_ : ℕ -> ℕ -> 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.

The goal types are not equal to ⊤, since the type checker is not aware
of the results of your tests. If you want the type checker to notice
the result of a pattern match, then you typically (*) need to use an
indexed type, not an unindexed type like Bool.

(*) Sometimes you can get a similar effect by using "magic with".

-- 
/NAD