[Agda] some brown for your nerves

[Conor McBride]

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