[Agda] Agdas constraint solver too eager?!

[Ulf Norell]

On Fri, Sep 7, 2012 at 12:49 PM, Andreas Abel <andreas.abel at ifi.lmu.de>wrote:

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

This is the correct behaviour. Your assertion that 'false' would be a
solution is incorrect. If you actually try it you get

false != true of type Bool
when checking that the expression refl has type
g false y ≡ g true y

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.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20120909/4914fe63/attachment.html