[Agda] Agdas constraint solver too eager?!

[Andreas Abel]

On 09.09.12 7:57 AM, Ulf Norell wrote:
>
> On Fri, Sep 7, 2012 at 12:49 PM, Andreas Abel <andreas.abel at ifi.lmu.de
> <mailto: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.

Yes, I remember the discussion.  It is recorded on the bug tracker under 
issue 423.

For the current intensional equality, true is the only solution for X. 
However, I consider intensionality as something evolving as we research 
Dependent Type Theory, with the goal to become more and more 
extensional.  An example are eta-laws, which are not part of the 
intensional equality of some type theories (prominently the original CIC 
and some versions of Martin-Loef Type Theory), but which are being added 
as our understanding has evolved (Coq got first class eta for functions 
in 8.3 or 8.4, and Mathieu Sozeau is working on that for records).

As we make intensional equality stronger, naturally, unification, as its 
inverse gets weaker, since there are more things that can be equal, 
hence more possible solutions may exist.  Currently, I am experimenting 
with a 'Nonvariant' polarity which labels unused arguments of functions. 
  In this case, g's first argument is constant, so intensional equality 
will now accept

   g false y = g true y

without requiring false = true.  Under this change of intensional 
equality, X no longer has a unique solution.

That X has a unique solution in current Agda, is merely "by chance", by 
the choice of intensional equality.  I myself get puzzled by it, because 
the intuitive thinking uses the "semantic", the extensional equality.

Anyway, the task at hand is to research whether incorporating 
non-variance into the system is feasible.  If it breaks a lot of things 
by generating a lot of unsolved metas, I will abstain from it.  My 
original motivation for non-variance was that it solves issue 44 (and 
the positivity checker uses non-variance already).

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/