fail in solving instance of `⊆-refl` in Agda 2.6.4.3

[mechvel]

This is on Agda 2.6.4.3 Built with flags (cabal -f) - optimise-heavily,
lib-2.0, ghc 9.0.2.

See the uploaded bugMay24.zip It is not large.

Installing

---

$agdaLibOpt = -i . -i .../stLib/2.0/src
$agdaFlags = --auto-inline --guardedness

agda $agdaLibOpt $agdaFlags Monomial.agda

checking Monomial (/home/mechvel/agda/tosave/bugs/may2024/Monomial.agda).
Failed to solve the following constraints:

  Vector.toList _ _ _x.exp_67 = Vector.toList _ _ (Mon.exp x)                   
    : List (Setoid.Carrier (PowerProduct.setoid-ℕ n))                           
    (blocked on _x.exp_67)                                                      
Unsolved metas at the following locations:                                      
  /home/mechvel/agda/tosave/bugs/may2024/Monomial.agda:67,11-27                 

Comments

---

Vector is a list of a given length.
PowerProduct is a vector over ℕ.
Monomial consists of a coefficient : Carrier and PowerProduct.
If the coefficients are from a Setoid, then Monomial is supplied with
monSetoid : Setoid _ _.
A monomial set is a list of monomials considered as set, the membership
is the membership of a monomial to a list of monomials.

_⊆ₘ_ is inclusion of monomial sets: _⊆_ imported from
Data.List.Relation.Binary.Subset.Setoid monSetoid
and renamed to ⊆ₘ.

The properties ⊆-refl; ⊆-trans
are imported from Data.List.Relation.Binary.Subset.Setoid.Properties
Then,

  ⊆ₘtrans :  Transitive _⊆ₘ_                                                    
  ⊆ₘtrans =  ⊆-trans monSetoid                                                  

is type-checked, and

  ⊆ₘrefl :  Reflexive _⊆ₘ_                                                      
  ⊆ₘrefl =  ⊆-refl monSetoid                                                    

is not.
The error report is difficult to understand.
There is a way out of

  ⊆ₘrefl {[]} =  λ()                                                            
  ⊆ₘrefl {m ∷ ms} {m'} (here m'=m)   =  here m'=m                               
  ⊆ₘrefl {m ∷ ms} {m'} (there m'∈ms) =  there m'∈ms                             

But this does not look nice, and if it is a bug, it still can bite in other situations.

[andreasabel]

This definition works:

⊆ₘrefl :  Reflexive _⊆ₘ_
⊆ₘrefl y = y

(NB. This is not a regression, works the same in 2.6.3 and master.)

[andreasabel]

I first tried

import Data.List.Relation.Binary.Subset.Setoid.Properties as Subset-Setoid-Properties
open Subset-Setoid-Properties monSetoid
     using ()
     renaming (⊆-refl to ⊆ₘrefl; ⊆-trans to ⊆ₘtrans)

but the ...Subset.Setoid.Properties module is not parametrized, maybe surprisingly, while the ...Subset.Setoid is:

import Data.List.Relation.Binary.Subset.Setoid as Subset-Setoid
open Subset-Setoid monSetoid public
     using ()
     renaming (_⊆_ to _⊆ₘ_)

[mechvel]

but the ...Subset.Setoid.Properties module is not parametrized, maybe surprisingly, while the ...Subset.Setoid is:

The library team has explained it long ago why had this been rearranged so, may be in CHANGELOG (personally I use it without thinking of the change reason).

[mechvel]

A.Abel wrote

This definition works:

⊆ₘrefl :  Reflexive _⊆ₘ_
⊆ₘrefl y = y

1) Of course, I tried this, and this is not type-checked. 2) Do you use exactly the unzipped code? Can you, please, set explicitly which lines have you changed? Are the options for installing Agda and applying Agda as I specified ? 3) ⊆ₘrefl needs an explicit argument monSetoid, because ...Subset.Setoid.Properties is not parameterized. 4) I tried setting there various arguments, with or without monSetoid, with explicit or implicit y, etc. And it is never type-checked. May be, you can upload here the version of Monomial.agda that is type-checked in your environment?

[andreasabel]

@mechvel: To understand when unification works in Agda and when not, I recommend this tutorial:

• https://github.com/effectfully/inference-in-agda
• Rendered: https://raw.githack.com/effectfully/inference-in-agda/master/InferenceInAgda.html

[andreasabel]

@mechvel Here is the full file:

open import Data.List using (List; []; _∷_)
import      Data.List.Relation.Binary.Subset.Setoid as Subset-Setoid
import Data.List.Relation.Binary.Subset.Setoid.Properties as Subset-Setoid-Properties
open import Data.List.Relation.Binary.Subset.Setoid.Properties using
                                             (⊆-refl; ⊆-trans)  -- ** I
open import Data.Nat using (ℕ)
open import Data.Product using (_×_; _,_)
open import Level using (_⊔_)
open import Relation.Binary using
     (Rel; Reflexive; Symmetric; Transitive; IsEquivalence; Setoid; _⇒_
     )
open import Relation.Binary.PropositionalEquality as PE using (_≡_)

import PowerProduct  -- of Application

-- ***************************************************************************
module Monomial {α α≈} (S : Setoid α α≈) (0# : Setoid.Carrier S) (n : ℕ) where

open Setoid S using (_≈_; refl; sym; trans) renaming (Carrier to C)

open PowerProduct n  using (PowerProduct; _=ₑ_; =ₑrefl; =ₑsym; =ₑtrans;
                            setoidₑ
                           )

record Mon : Set α where constructor mkMon           -- Monomial
                         field coef : C
                               exp  : PowerProduct

_=ₘ_ : Rel Mon α≈
(mkMon c e) =ₘ (mkMon c' e') =  c ≈ c' × e =ₑ e'

=ₘrefl : Reflexive _=ₘ_
=ₘrefl {mkMon c e} =  refl {c} , =ₑrefl {e}

=ₘreflexive :  (_≡_ {A = Mon}) ⇒ _=ₘ_
=ₘreflexive {m} {_} PE.refl =  =ₘrefl {m}

=ₘsym : Symmetric _=ₘ_
=ₘsym {mkMon c e} {mkMon c' e'} (c≈c' , e=e') =
                                              (sym c≈c' , =ₑsym {e}{e'} e=e')

=ₘtrans : Transitive _=ₘ_
=ₘtrans {mkMon _ e} {mkMon _ e'} {mkMon _ e''}
                                 (c≈c' , e=e') (c'≈c'' , e'=e'') =
                       (trans c≈c' c'≈c'' , =ₑtrans {e}{e'}{e''} e=e' e'=e'')

=ₘisEquivalence : IsEquivalence _=ₘ_
=ₘisEquivalence = record{ refl  = \{f}     → =ₘrefl {f}
                        ; sym   = \{f g}   → =ₘsym {f} {g}
                        ; trans = \{f g h} → =ₘtrans {f} {g} {h}
                        }

monSetoid : Setoid α α≈
monSetoid = record{ Carrier       = Mon
                  ; _≈_           = _=ₘ_
                  ; isEquivalence = =ₘisEquivalence
                  }

open Subset-Setoid monSetoid public
     using ()
     renaming (_⊆_ to _⊆ₘ_)  -- inclusion of monomial sets

⊆ₘtrans :  Transitive _⊆ₘ_
⊆ₘtrans =  ⊆-trans monSetoid

-- ** II
⊆ₘrefl :  Reflexive _⊆ₘ_
⊆ₘrefl y = y

The last line is the proof that you complained about.

[andreasabel]

• ⊆ₘrefl needs an explicit argument monSetoid, because ...Subset.Setoid.Properties is not parameterized.

Not if you do not even use ⊆-refl.

[mechvel]

-- ** II                                                                        
⊆ₘrefl :  Reflexive _⊆ₘ_                                                        
⊆ₘrefl y = y                                                                    

1. You added

   import Data.List.Relation.Binary.Subset.Setoid.Properties as  Subset-Setoid-Properties         

   which is not used in the further code. So, let us remove it. Do you agree?

2. I doubt about the whole approach.
   Your code

   ⊆ₘrefl :  Reflexive _⊆ₘ_                                                        
   ⊆ₘrefl y = y                                                                    

   implements ⊆ₘrefl without using the library function ⊆-refl,
   that is by programming this by new instead of substituting the parameter
   value monSetoid to the library module.
   The monSetoid argument is not needed here because the module of ⊆-refl
   is not applied. It is equivalent to

   ⊆ₘrefl {mons} {m'} m'∈mons =  m'∈mons                                           

   , where m'∈mons is called y.

But this approach is not universal.
Suppose that foo-refl : Reflexive
is implemented in a library module parameterized by arbitrary
S : Setoid _ _, and the user has fooₘ under monSetoid,
and needs to prove fooₘrefl : Reflexive.
But in some cases foo-refl : Reflexive may be difficult to prove
and may take a large proof code. In such cases one needs to apply

fooₘrefl = foo-refl monSetoid                                                   

may be, with some arguments added to help the inference.
This means: "use the library module by substituting the parameter value".

Because programming it by hand would add a large piece of code,
probably similar to the one in the foo-refl implementation.
Right?

3. Therefore a regular universal implementation here has to be of kind

   ⊆ₘrefl = ⊆-refl monSetoid                                                       

   Otherwise, it will occur that generally,
   the parametric modules tool does not support proofs for Reflexive
   (?)

What one needs to add there to help Agda to solve the types?

4. For ⊆ₘtrans, this regular approach works, the libary proof is used.
   Why the programmer cannot use the libary proof for ⊆ₘrefl?
   (may be, with adding some arguments).

You refer to a manual on the type inference. But it is large.
Can you point at a concrete place?
I do not know, we could move the question to Zulip.

5. Your ⊆ₘrefl y = y works on an older Debian Linux + ghc-9.2.7, but did not work on Debian Linux 12 + ghc-9.0.2. This is not for sure, I shall get to the responsible machine and make sure.

[andreasabel]

If you do not like my cheat, then here is the generic solution:

⊆ₘrefl {xs} {x} = ⊆-refl monSetoid {xs} {x}

The problem with ⊆ₘrefl = ⊆-refl monSetoid is a recurring one: Agda inserts hidden arguments eagerly, so you get ⊆ₘrefl {xs} {x} = ⊆-refl monSetoid {_} {_}, but then Agda does not know how to solve the underscores. The solution I applied here is manual "eta-expansion".

[mechvel]

On 2024-05-29 16:03, Andreas Abel wrote:

If you do not like my cheat, then here is the generic solution:

⊆ₘrefl {xs} {x} = ⊆-refl monSetoid {xs} {x}

Yes, this uses the library module all right, in an universal way. I thought that you were forced to avoid this approach. I withdraw my suspicion about the parametric modules tool.

It remains for me to find out of why did not this work in a bit different system environment (because initially I tried "everything"). Maybe I missed something.

The problem why ⊆ₘrefl = ⊆-refl monSetoid is a recurring one: Agda inserts hidden arguments eagerly, so you get ⊆ₘrefl {xs} {x} = ⊆-refl monSetoid {} {}, but then it does not know how to solve the underscores. The solution I applied here is manual "eta-expansion".

Thank you very much.

[mechvel]

I wrote

It remains for me to find out of why did not this work in a bit different system environment (because initially I tried "everything").

Now, in both environments all the versions (A), (B), (C) work :

⊆ₘrefl :  Reflexive _⊆ₘ_
⊆ₘrefl y = y                                                                 -- (A)

-- ⊆ₘrefl {mons} {m'} m'∈mons =   m'∈mons                   (B)

--⊆ₘrefl {mons} {m} =  ⊆-refl monSetoid {mons} {m}          (C)

I have started the issue because the versions with ⊆-refl in the right hand side did not work. Probably I missed the version of (C). So, I am sorry for noise.

[andreasabel]

Similar:

• 6559