[Agda] Pie in the sky (was: Again, a question on records)

[Samuel Gélineau]

On 2010-09-20 04:34, Benja Fallenstein wrote:
> Pie-in-the-sky idea: I've thought for a while that it might be nice
> solution to a number of things if we could have implicit arguments
> that are named by types, and that are used to fill in blanks of that
> type when type inference fails:
>
>    _$_ : {T} -> T.carrier t -> T.carrier t
>    x $ y = T.op _ x y

Wow. What a great idea! If Agda were to have this feature, it would
become my all-time favorite language instead of... well, instead of
current Agda.

I must insist. I am really enthusiastic about this feature. Like, if
the Agda developers refuse to put it in, I'll just have to fork and
attempt to add it in myself. In other words, if you need help
implementing it, I volunteer. I might ask lots of questions, though,
because last time I opened Agda's internals to add something, I got
stuck rather early in the process. But this time, I'll try harder,
because the feature is definitely worth it!

please don't have an obvious and true reason why something like this
could never work,
– Samuel