[Agda] Agdas constraint solver too eager?!

[Andreas Abel]

On 09.09.12 6:55 AM, James Deikun wrote:
> On Fri, 2012-09-07 at 15:13 +0200, Andreas Abel 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.
>
> Is this entirely true to begin with?  What will happen if you have:
>
>    f : {phantom : Nat} -> D phantom -> Nat
>    f (c {phantom}) = phantom
>
> Do you plan to have the data constructor lose injectivity along with the
> type constructor?  I suppose it probably would not be incoherent to do
> so (treating a data constructor as a constructor, properly speaking,
> only once the parameters are saturated), but it would seem an unusual
> choice...

Mmh, good question.

But actually, it might not be an issue, since your code seems to be 
illegal already; my Agda rejects it, stating that c should have 0 
arguments but has been given 1.

Cheers,
Andresa

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