[Agda] a strange "unsolved" report

mechvel at scico.botik.ru mechvel at scico.botik.ru
Tue Oct 6 20:25:57 CEST 2020


On 2020-10-05 22:13, James Wood wrote:
> I don't see any uses of `mmons` in the code you've posted so far. I'm
> more surprised that that definition checks than that the others don't.

Each of mmons, m'mons', m''mons'' is used below in the function aux, 
like this:

  begin⟨ monsSetoid ⟩
    ...
    (m ∷ mons) +ms (m' ∷ (mons' +ms m''mons''))
                         ≈⟨ =ms-reflexive $ cong (mmons +ms_) $ sym $
                                                  -----
                            +ms-step> {b} {e'} {c} {e''} {mons'} {mons''} 
e'>e''
                          ⟩
    ...
  ∎



> Notice that, for example, the following definition does not check.
> 
>   open import Data.List
>   open import Data.List.Relation.Unary.All
> 
>   test : (A : Set) (x : A) (xs : List A) → _
>   test A x xs = x ∷ xs
> 
> Sort _3  [ at 
> /sharedhome/home/james/Documents/agda/Scratch.agda:6,42-43 ]
> _4 : _3  [ at 
> /sharedhome/home/james/Documents/agda/Scratch.agda:6,42-43 ]
> _6 : _4 (A = A) (x = x) (xs = xs)  [ at
> /sharedhome/home/james/Documents/agda/Scratch.agda:7,15-21 ]
> 
> ———— Errors ————————————————————————————————————————————————
> Unsolved constraints
> 
> Meanwhile, the following checks because `foo` is used somewhere which
> makes its type obvious.
> 
>   open import Data.List
>   open import Data.List.Relation.Unary.All
> 
>   test : (A : Set) (x : A) (xs : List A) → List A
>   test A x xs = foo
>     where
>     foo = x ∷ xs

It is checked not because foo is used below, but because the result type 
is set
List A,  while in the first your example it is "_".
I discover this by setting  "... → _"  to your second example.
- ?

I am sorry, my main example is not reduced, this "aux" is the most 
lengthy proofs in the project.
Anyway it is checked when the signature for m'mons' is provided.


> So I think `mmons` must be being used, and the others not (or not in a
> context which gives enough of a hint as to their types).

All the three are used in aux in similar way, but may be  m'mons'  is 
used in a slightly
different way. So that you guess may occur true.

Thank you.

--
SM



> On 05/10/2020 17:37, mechvel at scico.botik.ru wrote:
>> 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
>>> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda


More information about the Agda mailing list