[Agda] a strange "unsolved" report

[James Wood]

Is `mmons` used somewhere, maybe giving a hint as to what type to check
it at?

James

On 04/10/2020 23:43, mechvel at scico.botik.ru wrote:
> On 2020-10-04 23:30, James Wood wrote:
>> Hi Sergei,
>>
>> Quick questions first: is `_∷_` overloaded at all in this context?
>> That'd be my guess for why Agda has no clue what the type is supposed
>> to be.
>>
> 
> It is overloaded.
> But there are other similar assignments before and around (like the one
> marked with *),
> and Agda does resolve them without providing a signature.
> 
> -- 
> SM
> 
> 
> 
>> On 04/10/2020 18:19, mechvel at scico.botik.ru wrote:
>>> Dear Agda developers,
>>>
>>> There is a question about the following code fragment:
>>>
>>> -----------------------------------------------------
>>> +ms-assoc-aux {monᶜ a e ∷ mons} {monᶜ b e' ∷ mons'} {monᶜ c e'' ∷
>>> mons''} ... =
>>>
>>>     aux (<-cmp e e') (<-cmp e' e'') (<-cmp e e'')
>>>     where
>>>     m = monᶜ a e;  m' = monᶜ b e';   m'' = monᶜ c e''
>>>
>>>     mmons = m ∷ mons                 -- *
>>>
>>>     -- m'mons' : List Mon            -- (I-s)
>>>     m'mons' = m' ∷ mons'             -- (I)
>>>
>>>     m''mons'' = m'' ∷ mons''
>>>     ...
>>> -----------------------------------------------------
>>>
>>> Agda 2.6.1 reports
>>> "
>>> Sort _1156  [ at ...Over-abelianGroup.agda:414,5-12 ]
>>> _1157 : _1156  [ at ...Over-abelianGroup.agda:414,5-12 ]
>>> _1159 : _1157  [ at ...Over-abelianGroup.agda:414,15-25 ]
>>> "
>>>
>>> I guess this is the kind of "unsolved metas".
>>> And the first "unsolved" is about the line marked (I).
>>>
>>> The previous line (marked *) is solved - while it is not any more clear
>>> than (I).
>>>
>>> Then, after adding the signature (I-s), everything is type-checked.
>>> 1) This necessity to add signature in the middle of an array of short
>>> assignments of the same
>>>    type looks strange.
>>> 2) There are many similar fragments in the program, and I never observed
>>> such an effect.
>>>
>>> What might this mean?
>>>
>>> -- 
>>> SM
>>> _______________________________________________
>>> Agda mailing list
>>> Agda at lists.chalmers.se
>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>
>>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>