[Agda] some brown for your nerves

[Andreas Abel]

Btw, this is another instance of a non-injective family.  We have

   Lt (su m) (su n) = Lt m n

but not equality of indices, su m = m or su n = n.

Injectivity criteria for families is still an open research issue, if 
someone wants to pick it up...

Cheers,
Andreas


Conor McBride a écrit :
> 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
> 


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/