[Agda] Agdas constraint solver too eager?!

[Andreas Abel]

Thanks for the pointer, I will try it.

On 08.09.12 9:36 PM, James Deikun wrote:
> On Fri, 2012-09-07 at 15:13 +0200, Andreas Abel wrote:
>>     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.
>
> I feel this change would cause a lot of problems for the categories
> library, which often uses phantom or semi-phantom record type parameters
> to keep track of things like domains and codomains.  There are already
> problems coming from the way irrelevant arguments are inferred, as you
> may remember, but this sort of thing could make them much worse.
>
> I can't be sure of course; perhaps you could try testing the categories
> library ( http://github.com/copumpkin/categories/ ) against your
> prospective implementation if you have the opportunity.
>
>

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