[Agda] _$_

[Serge D. Mechveliani]

To my

>> For  Agda-2.3.0.1 + lib-0.6,  
>>      _$_  imported from  Function,  
>> [..]
>> each of the following 4 declarations causes "unsolved metas":
>> 
>>   n : Nat
>>   n = suc $ suc 0
>>
>> [..]

Nils Anders Danielsson wrote	

> I suspect that suc is overloaded. Is your code accepted if you write
> ???.suc instead of suc?


Thank you.
Indeed,
           n : Nat
           n = Nat.suc $ Nat.suc 0
does work.
In my module,  suc  is imported from  Data.Nat  and from  Data.Fin.

But it is strange that Agda reports  "unsolved metas"  for  `suc $ suc 0'.
I have got used that rather it reports of an overlapping import,
like this:

  suc  is visible at the following locations:
    Data/Fin/Fin.agda
    Data/Nat/Nat.agda
    ...

So, I do not fear to write  suc, +,  and such. Because, if an overlapping
import happens, the compiler reports adequately, and it is easy to
understand and to fix -- by adding  `<module-name>.'  or `hiding' or
`using' or `renaming'.

Now, this has bitten me for the first time. Is this a specific of `$' ?

Regards,

------
Sergei