[Agda] Type and termination checking around with clauses

[Ulf Norell]

On Thu, May 1, 2008 at 1:02 AM, Ulf Norell <ulfn at cs.chalmers.se> wrote:

>
>
> On Wed, Apr 30, 2008 at 10:39 PM, Nils Anders Danielsson <
> nils.anders.danielsson at gmail.com> wrote:
>
> > 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.
>
>
> The with is supposed to make the type checker aware of the result of the
> test, that's the whole point (well, maybe not the whole point). I haven't
> tried the example yet, but just looking at it, it should work.
>

Ah, I see what the problem is. When you pattern match the types of p and q
are refined according to the matching (so p q : ⊤). The problem is that the
type checker doesn't remember the information gained by pattern matching:
when you pattern match, all occurrences of the expression you match on (in
the context) are substituted for the matches, but if you later introduce
that expression again it won't be equal to the match.

In the example trans expects arguments of type Atom (n <= m) and Atom (m <=
o) and since these types weren't sitting in the context when you did the
pattern matching they didn't get the benefit of knowing that n <= m and m <=
o turned out to be true.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080501/88648681/attachment-0001.html