[Agda-dev] Treating variables as named types

[Nils Anders Danielsson]

Hi,

Conor uses lots of instance arguments in "How to Keep Your Neighbours in
Order". However, his code was written using the old variant of the
instance arguments, and fails to check now. I managed to make the code
work again using some small tweaks, and wonder if we could get away with
even less:

* I replaced

     record One : Set where constructor it

   with

     record One : Set where
       instance
         constructor it.

   This seems fine with me.

* I replaced

     _:-_ : forall {P T} -> <P P P> -> (P => T) -> T
     ! :- t = t

   with

     _:-_ : forall {P T} -> <P P P> -> (P => T) -> T
     ! {{prf = p}} :- t = t {{p = p}},

   because "Instance search can only be used to find elements in a named
   type". Similarly, in two cases I replaced a module parameter

     (L : REL P)

   with

     (L' : REL P) (let L = Named L'),

   where Named is a named type family:

     data Named {P : Set} (A : REL P) : REL P where
       named : forall {x} -> A x -> Named A x

   Would it be possible to treat variables as named types/named type
   families?

   Introducing special treatment for variables can be problematic, as it
   can lead to problems with subject reduction. However, in this case the
   instance resolution should happen before the variables get
   instantiated, so I don't think this will be a problem.

   Are there any other problems, related to implementation complexity or
   efficiency?

-- 
/NAD