[Agda] a strange "unsolved" report

[mechvel at scico.botik.ru]

On 2020-10-05 01:47, James Wood wrote:
> Is `mmons` used somewhere, maybe giving a hint as to what type to check
> it at?
> 

It has
    m   = monᶜ a e;     m'    = monᶜ b e'
    m'' = monᶜ c e'';   mmons = m ∷ mons

    m'mons' : List Mon     -- Agda forces me to set this signature
    m'mons' = m' ∷ mons'

m m' m'' : Mon,     monᶜ a constructor for the record Mon.
and
mons mons' mons'' : List Mon   are derived from the head function 
pattern:

   m = monᶜ a e;  m' = monᶜ b e';   m'' = monᶜ c e''

mmons m'mons m''mons :  List Mon   are computed by the assignments

   mmons = m ∷ mons                 -- *

   m'mons' : List Mon
   m'mons' = m' ∷ mons'

   m''mons'' = m'' ∷ mons''

_∷_  is overloaded by

   open import Data.List using (List; []; _∷_ ...),
   open import Data.List.Relation.Unary.All as AllM using (All; []; _∷_)


It does work. But it looks new and a bit strange that it chooses one 
assignment in the middle
of an array of similar assignments, and requires a signature for it:

-----------------------------------------------------------------------------
+ms-assoc-aux {monᶜ a e ∷ mons} {monᶜ b e' ∷ mons'} {monᶜ c e'' ∷ 
mons''}
               ord-ees ord-e'es' ord-e''es'' (suc l) l₁'+[l₂'+l₃']≤l' =

               aux (<-cmp e e') (<-cmp e' e'') (<-cmp e e'')
     where
     a+b = a + b;       b+c = b + c
     m   = monᶜ a e;    m'  = monᶜ b e'
     m'' = monᶜ c e''

     mmons = m ∷ mons

     m'mons' : List Mon      -- (I)  forced
     m'mons' = m' ∷ mons'

     m''mons'' = m'' ∷ mons''
     es = map Mon.exp mons;  es' = map Mon.exp mons';  es'' = map Mon.exp 
mons''

     mons'+mons'' = mons' +ms mons''
     ...

     aux : Tri (e < e')   (e ≡ e')   (e > e')   →
           Tri (e' < e'') (e' ≡ e'') (e' > e'') →
           Tri (e < e'')  (e ≡ e'')  (e > e'')  →

           ((m ∷ mons) +ms (m' ∷ mons')) +ms (m'' ∷ mons'')  =ms
           (m ∷ mons) +ms ((m' ∷ mons') +ms (m'' ∷ mons''))

     -- many patterns for  aux :

     aux (tri> _ _ e>e') (tri< e'<e'' _ _) (tri> _ _ e>e'') =  ...

     ...
------------------------------------------------------------------------------

The effect is only in the assigments before `aux'.

--
SM




> 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
>>> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda