[Agda] stuck with "unsolved metas"

[Sergei Meshveliani]

On Thu, 2016-05-19 at 09:44 +0200, Andreas Abel wrote:
> I see, you are referring to
> 
>    https://github.com/agda/agda/issues/1079
> 
> In this instance, Agda inserts _too many_ hidden arguments, which it 
> cannot solve then.  Sergei has run into this problem before, see
> 
>    https://github.com/agda/agda/issues/1092
> 
> This issue can only be finally settled by drastically restricting the 
> use of hidden quantification, which would rule out many Agda programs 
> which are legal at this point.  So we don't.
> [..]

The fragments like  "(\ {x y z} -> foo {x} {y} {z})"  instead of  "foo"
look ugly.

With these restrictions applied, will Agda programs look nicer?

My observation about breaking the application code is as follows.

1) The Agda team warns about the language being not stable, so far.
2) I write in Haskell during many years, and write in Agda during 4
years. My Haskell code for DoCon needs change after each 3 GHC versions
(on average). And my Agda code for DoCon-A needs change after each 1-2
Agda versions. 
3) It is natural for each version of application to announce:  which
tool versions is required. For example, DoCon runs on GHC-7.8.3, needs
an effort to port it higher (mainly due to the problem of overlapping
instances). 

This is only an observation. I have not a definite idea about usefulness
of this change, even for myself.

Regards,

------
Sergei