[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