[Agda] Pie in the sky

[Nils Anders Danielsson]

On 2010-09-21 17:57, Samuel Gélineau wrote:
> Do the agda gatekeepers have any opposition to a new feature [...]

I would suggest that you start by researching prior work (canonical
structures, the type classes of Agda 1, etc.). You may also want to play
around with "constructor headed functions", for which Agda's unification
machinery is a bit smarter:

   http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.FindingTheValuesOfImplicitArguments

--
/NAD