[Agda] Agdas constraint solver too eager?!

[James Deikun]

On Sun, 2012-09-09 at 21:49 +0200, Andreas Abel wrote:
> 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.

Wow, it turns out the way Agda represents datatype constructors is
considerably different than how I thought.  In particular, a constructor
for a parametric datatype *does not have* a particular type, only a type
scheme like `c : D _1' and therefore does not need an implicit argument
to supply the type parameter; this is resolved as overloading instead.

Thanks to that it turns out we can do this amusing thing:

    Nz : Nat -> Set
    Nz zero = Bot
    Nz (suc n) = Top

    data Phin (bound : Nat) : Set where
      zero : {nz : Nz bound} -> Phin bound
      suc : {nz : Nz bound} -> Phin (pred bound) -> Phin bound

    toPhin : (n : Nat) -> Phin (suc n)
    toPhin zero = zero
    toPhin (suc n) = suc (toPhin n)

If you then normalize toPhin 20 (say) with hidden argument printing
turned on, you will observe that there are no numbers hidden into the
result, only `tt's.  This reduces the size of a normalized Phin in
memory by a logarithmic factor relative to a Fin.  (Without builtin
optimization of Nats, this would be a linear factor.)  All because a
constructor doesn't take arguments for type parameters.