[Agda] Agdas constraint solver too eager?!

[James Deikun]

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