[Agda] a strange "unsolved" report

James Wood james.wood.100 at strath.ac.uk
Tue Oct 6 22:44:37 CEST 2020


What happens if you replace uses of `m'mons'` by its definition? Or is
there a way you could `let` bind it?

(More reply below)

On 06/10/2020 19:25, mechvel at scico.botik.ru wrote:
> 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.
> - ?

The point of this example is that, as far as I'm aware, `where`
declarations are not inlined for type checking, but nonetheless Agda has
managed to check the definition of `foo` based on the context in which
it is used. This behaviour is slightly different to that of top-level
definitions, as the non-workingness of this example shows:

  module _ (A : Set) (x : A) (xs : List A) where

    foo = x ∷ xs

    test : List A
    test = foo

> 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