[Agda] a strange "unsolved" report

[James Wood]

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.
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

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).

Regards,
James

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
>>