[Agda] Agdas constraint solver too eager?!

[Andreas Abel]

I would not have expected the following program to type check:

assert : (A : Set) → A → Bool → Bool
assert _ _ true  = true
assert _ _ false = false

g : Bool -> Bool -> Bool
g x true  = true
g x false = true

unsolved : Bool -> Bool
unsolved y =
   let X : Bool
       X = _
   in  assert (g X y ≡ g true y) refl X

istrue : (unsolved false) ≡ true
istrue = refl

The meta-variable X is solved to 'true' (as witnessed by istrue), even 
though 'false' would also be a solution, semantically, because g 
actually ignores its first argument.  (It even ignores its second 
argument, but that does not matter here.)

The expected behavior would be an unsolved X, since it is not uniquely 
determined.

I came across this example when working on making Agda aware of unused 
arguments (so as to fix issue 44).

I think we should stick to the philosophy that constraint solving should 
only deliver unique solutions, and fix the issue described above.  That 
would lead to some more unsolved metas, I am afraid...

Cheers,
Andreas

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