[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