[Agda] Agdas constraint solver too eager?!

[James Deikun]

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.