[Agda] some brown for your nerves

[Conor McBride]

On 2 May 2010, at 22:47, James Chapman wrote:

> I wonder if this is related to this bug:
>
> http://code.google.com/p/agda/issues/detail?id=246

Had a quick look. Seems highly likely. It's not a 118.

Cheers

Conor


>
> 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
>>