[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