[Agda] dangerous _$_

[Andreas Abel]

Solving meta variables is brittle.  A single use of _$_ introduces 2 
level metas and two Set metas, it makes type checking harder, and it 
might fail where ordinary application succeeds, as in your example.  If 
you want to know more, please send self-contained code.

Cheers,
Andreas

On 05.02.2013 15:56, Serge D. Mechveliani wrote:
> Who can tell, please, what is the matter with using _$_ in the
> following fragment?
>
>    ...
>    sMbFinEnum : Maybe $ DecFiniteEnumeration sSetoid
>    sMbFinEnum =
>          case  DSet.mbFiniteEnum dSet  of \
>          { nothing                 -> nothing
>          ; (just (no _))           -> nothing
>          ; (just (yes hasFinEnum)) ->
>                       just $ yes (finEnumForSubsetoid bSetoid member?
>                                                               hasFinEnum)
>
> The checker of  Agda-2.3.2 MAlonzo  (lib-0.7)  reports  "unsolved metas"
> for the line of          "just $ yes ...".
> And if I replace it with
>                           just (yes (finEnumForSubsetoid ...))
> ,
> then the code is type-checked and compiled.
> I have spent 6 hours to find who makes this "unsolved metas".
> Now, I see, who it is. But do not understand -- why;
> and also start to fear of _$_ !
>
> Thank you in advance for explanation,
>
> ------
> Sergei
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/