[Agda] some brown for your nerves

[James Chapman]

I wonder if this is related to this bug:

http://code.google.com/p/agda/issues/detail?id=246

James

On Sun, May 2, 2010 at 11:49 PM, Conor McBride
<conor at strictlypositive.org> wrote:
> Folks
>
> I was in the middle of something else when I tripped over this
> little infelicity. The following code-with-shed refines, but the
> resulting code will not reload. I can guess why, but I wonder
> what will come of it. Here's the stuff.
>
> ---------------------------------------------------------------
> module PushyU where
>
> data Nat : Set where
>  ze : Nat
>  su : Nat -> Nat
>
> data Bool : Set where
>  tt ff : Bool
>
> record One : Set where
> data Zero : Set where
>
> So : Bool -> Set
> So tt = One
> So ff = Zero
>
> _<_ : Nat -> Nat -> Bool
> _ < ze = ff
> ze < su n = tt
> su m < su n = m < n
>
> data Lt (m n : Nat) : Set where
>  lt : So (m < n) -> Lt m n
>
> boo : {m n : Nat} -> So (m < n) -> Lt (su m) (su n)
> boo p = lt {!p!}
> ---------------------------------------------------------------
>
> Interactively, I suppose it's rightly happy to
> accept p : So (m < n) when it wants a (So (su m < su n)) as
> these types are definitionally equal.
>
> On reload, I fear it foolishly jumps to the conclusion that
> when I write
>  lt p
> I mean
>  lt {m} {n} p : Lt m n
> because
>  p : So (m < n)
> and unification is happy to choose the solution which presents
> itself, even if it's not unique.
>
> Am I right? Is it choosing a non-unique unifier over the more
> reliable information coming from the type pushed in? Is this a
> bug or a feature?
>
> I've noticed in the past that Agda's implicit syntax machinery
> commits hastily, but less often that doing so produces incorrect
> results. It may very well be the case that making unification
> less aggressive will break a lot of existing code which relies
> on correct guesswork rather than forced moves.
>
> It may be that, pragmatically, just tweaking the order in which
> constraints are attacked to make better use of types pushed in
> will result in better guesswork. Of course, it might just result
> in different guesswork. That's the trouble with guesswork.
>
> As ever, unvoodoo overdue
>
> Cheers
>
> Conor
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>