[Agda] Re: problem using "with"

[Wolfram Kahl]

On Sat, May 12, 2012 at 09:17:41AM +0200, Ulf Norell wrote:
> On Fri, May 11, 2012 at 9:52 PM, Guillermo Calderón <calderon at fing.edu.uy>wrote:
> > On 11/05/12 16:24, Ulf Norell wrote:
> >> On Fri, May 11, 2012 at 7:36 PM, Guillermo Calderón <calderon at fing.edu.uy> wrote:
> >> [...]
> >>     > g :  ℕ  → ℕ
> >>     > g a with  a ≤? 5
> >>     > ... |  yes _  = a
> >>     > ... |  no  _  = suc a
> >>     >
> >>     > prop-g  : ∀ n  -> (R :  ℕ  → Set)
> >>     >                -> (∀ m -> R (suc m))
> >>     >                -> (∀ n -> n ≤ 5 -> R (g n))
> >>     >                -> R (g n)
> >>     > prop-g n R f1 f2  with n ≤? 5
> >>     > ... | no  ¬p   =  f1 n
> >>     > ... | yes p    =  f2 n p- -*** ERROR here ***
> >>
> >> The problem is that the abstraction happens at the point of the
> >> with. At that point you haven't applied f2 yet, so the n in the type
> >> of f2 is a different n from the one in n ≤? 5, thus it doesn't abstract.
> >>
> > Ulf,
> > Thanks for your answer.
> > As far as i known, the same problem should happen for the case (no  ¬p).
> >
> >       > ... | no  ¬p   =  f1 n
> >
> > However,  no error is reported by agda at this level and  (f1 n)  is
> > accepted as well typed.
> > ¿what is the difference between   both cases?
> 
> In the no case you don't need the g n in f2 to reduce. The g n in the goal
> gets abstracted over
> without problems when you do the with.

Is there a way to view the generated with-function, with type declaration,
especially in cases where it fails to type-check?

That would hopefully frequently save at least some of the work
of refactoring it manually.


Wolfram