[Agda] a strange "unsolved" report

mechvel at scico.botik.ru mechvel at scico.botik.ru
Wed Oct 7 12:23:29 CEST 2020


On 2020-10-06 23:44, James Wood wrote:
> What happens if you replace uses of `m'mons'` by its definition? Or is
> there a way you could `let` bind it?
> [..]


If the lines
    m'mons' : List Mon
    m'mons' = m' ∷ mons'

are removed, and  m'mons'  is replaced everywhere with its definition 
(m' ∷ mons'),
then the module is checked.

To try the `let' binding for it is difficult, too much of refactoring.

--
СМ


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


More information about the Agda mailing list