[Agda] Agdas constraint solver too eager?!

[Gabriel Scherer]

Couldn't we use an explicit polarity annotation on the "phantom"
parameter here? "unused" is the most general polarity that is sound
for this datatype, so it is desirable that the type-checker keeps it
by default, but I would expect for example (data D (=phantom : Nat) :
Set where...) to force the strictest equality. Just like I want to be
able to hide the fact that a type parameter is used covariantly, and
give it an invariant interface.

(How is invariant written in MiniAgda

On Fri, Sep 7, 2012 at 3:13 PM, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
> 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/
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda