[Agda] Agdas constraint solver too eager?!

[Andreas Abel]

A consequence of making Agda aware of unused arguments is that certain 
"phantom-type" tricks do not work anymore.

   data D (phantom : Nat) : Set where
     c : D phantom

If Agda may recognize 'phantom' as unused, then

   D 0 = D 1

and accordingly, D X = D 0 will not solve X to 0.  It will be necessary 
then to replace D by

   data D : Nat -> Set where
     c : {phantom : Nat} -> D phantom

to get the desired effect.  The same fix however does not work for 
records with phantom parameters (since there are no indexed records).

There is a choice to make:

   1. Go the 'semantic path' for data type parameters, allowing Agda to
      recognize them as unused.  That will make certain phantom tricks
      impossible.
      I am a bit confused, since I thought by getting rid of injective
      type constructors we had already gotten there, but it seems not.

   2. Go the 'syntactic path' for data type parameters, considering them
      never as unused, to allow phantom tricks.
      The relationship to injective type constructors should be
      clarified then.

I am tending towards 1., but people using phantoms should speak up to 
discuss whether they are essential and whether they could sustain when 
going 1.

Cheers,
Andreas

On 07.09.2012 12:49, Andreas Abel 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.
>
> I came across this example when working on making Agda aware of unused
> arguments (so as to fix issue 44).
>
> I think we should stick to the philosophy that constraint solving should
> only deliver unique solutions, and fix the issue described above.  That
> would lead to some more unsolved metas, I am afraid...
>
> 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/