[Agda] Agdas constraint solver too eager?!

[Andreas Abel]

On 07.09.12 5:52 PM, Gabriel Scherer wrote:
> Couldn't we use an explicit polarity annotation on the "phantom"
> parameter here?

I am for explicit polarity annotations, but Ulf is unconvinced. ;-)  The 
syntax of Agda is not easily extended (which is a good thing also, 
keeping Agda clean).

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

Yes.

> (How is invariant written in MiniAgda

In MiniAgda, it is *.

Cheers,
Andreas

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

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