[Agda] a strange "unsolved" report
mechvel at scico.botik.ru
mechvel at scico.botik.ru
Mon Oct 5 00:43:09 CEST 2020
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
More information about the Agda
mailing list