[Agda] Agdas constraint solver too eager?!

[Ulf Norell]

On Sun, Sep 9, 2012 at 7:57 AM, Ulf Norell <ulf.norell at gmail.com> wrote:

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

To drive the point home further, if you change the program so that false is
actually a solution (by replacing refl by a different proof), X is not
solved:

lem : ∀ {x₁ x₂} y → g x₁ y ≡ g x₂ y
lem true  = refl
lem false = refl

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

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