[Agda] Agdas constraint solver too eager?!

Andreas Abel andreas.abel at ifi.lmu.de
Fri Sep 7 12:49:57 CEST 2012

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 

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


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

More information about the Agda mailing list