<br><div class="gmail_quote">On Fri, Sep 7, 2012 at 12:49 PM, Andreas Abel <span dir="ltr"><<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
I would not have expected the following program to type check:<br>
<br>
assert : (A : Set) → A → Bool → Bool<br>
assert _ _ true = true<br>
assert _ _ false = false<br>
<br>
g : Bool -> Bool -> Bool<br>
g x true = true<br>
g x false = true<br>
<br>
unsolved : Bool -> Bool<br>
unsolved y =<br>
let X : Bool<br>
X = _<br>
in assert (g X y ≡ g true y) refl X<br>
<br>
istrue : (unsolved false) ≡ true<br>
istrue = refl<br>
<br>
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.)<br>
<br>
The expected behavior would be an unsolved X, since it is not uniquely determined.<br></blockquote><div><br></div><div>This is the correct behaviour. Your assertion that 'false' would be a solution is incorrect. If you actually try it you get</div>
<div><br></div><div><div>false != true of type Bool</div><div>when checking that the expression refl has type</div><div>g false y ≡ g true y</div></div><div><br></div><div>We've had this discussion before. Metavariables are solved with unique solutions that make the intensional equality hold, not the extensional equality. This is why solving true for X is fine in g X y ≡ g true y, even though, for all closed y, g false y ≡ g true y.</div>
<div><br></div><div>/ Ulf</div></div>