# [Agda] Agdas constraint solver too eager?!

Andreas Abel andreas.abel at ifi.lmu.de
Sun Sep 9 21:39:16 CEST 2012

```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/
```