[Agda] on parametric modules

[Sergei Meshveliani]

Can people, please, explain,
why the attached code produces  "unsolved metas" ?

This is 210 lines for Agda 2.4.2.3.

Unsolved metas is reported for the last line:

  fromAsd-isInj : IsInjective fromAsd
  fromAsd-isInj = fromAsd-isInjective
                                                          

Remarks
-------                                                                         
Changing  fromAsd-isInjective  to  ≈→~asd  makes it type-checked.
fromAsd-isInjective  is imported from  OfAssociated,  where it is
defined as  ≈→~asd.
And importing  ≈→~asd  from  OfAssociated  and setting it in place of
fromAsd-isInjective  makes it type-checked.

It was said that this is probably due to that
"instantiating parameterised modules changes metavariable resolution".

Can you, please, explain this on this example
(which, I think, is small enough).

Thanks,

------
Sergei

-------------- next part --------------
module ParamModQuest where
   
open import Level    using (Level; _⊔_) renaming (suc to sucL) 
open import Function using (id; _$_; _∘_; _on_)
open import Algebra.FunctionProperties as FP using (Op₂)
open import Relation.Nullary using (¬_; Dec; yes; no) 
open import Relation.Unary   using (Decidable)
open import Relation.Binary  using 
     (Rel; Reflexive; Symmetric; Transitive; module IsEquivalence; 
      IsEquivalence; Setoid; module Setoid; _Preserves_⟶_; _Preserves₂_⟶_⟶_;
      _Respects_
     )
     renaming (Decidable to Decidable₂)

open import Relation.Binary.PropositionalEquality as PE using (_≡_) 
import Relation.Binary.EqReasoning as EqR
open import Data.Product using (_×_; _,_; ∃; proj₁; proj₂; Σ; uncurry)
open PE.≡-Reasoning renaming (_≡⟨_⟩_ to _≡[_]_; begin_ to ≡begin_;
                                                                 _∎ to _≡end)



--****************************************************************************
module OfCongMap {α α= β β=} (From : Setoid α α=) (To : Setoid β β=) 
  where 
  open Setoid From using () renaming (Carrier to A; _≈_ to _=a_) 
  open Setoid To   using () renaming (Carrier to B; _≈_ to _=b_) 

  IsInjective : (A → B) → Set (β= ⊔ α= ⊔ α)
  IsInjective f =  {x x' : A} → f x =b f x' → x =a x'



--============================================================================
_Respects2_ : ∀ {a ℓ₁ ℓ₂} {A : Set a} → Rel A ℓ₁ → Rel A ℓ₂ → Set _
_Respects2_ _~_ _≈_ =
                      ∀ {x x' y y'} → x ≈ x' → y ≈ y' → x ~ y → x' ~ y'

isUnity : ∀ {α α=} (A : Setoid α α=) → let C = Setoid.Carrier A in  
                                                      Op₂ C → C → Set (α ⊔ α=)
isUnity A _∙_ e =  (x : Carrier) → ((e ∙ x) ≈ x) × ((x ∙ e) ≈ x)  where
                                                                 open Setoid A 

Unity : ∀ {α α=} (A : Setoid α α=) → Op₂ $ Setoid.Carrier A → Set (α ⊔ α=)
Unity A _∙_ =  ∃ (\ (e : Setoid.Carrier A) → isUnity A _∙_ e) 
             
RightQuotient : ∀ {α α=} (A : Setoid α α=) → 
                     let C = Setoid.Carrier A in  Op₂ C → C → C → Set (α ⊔ α=)

RightQuotient A _∙_ a b =  ∃ (\ q → (b ∙ q) ≈ a)  where _≈_ = Setoid._≈_ A


------------------------------------------------------------------------------
record CMonoid (α α= : Level) : Set (sucL (α ⊔ α=))
  where
  field  setoid : Setoid α α=
          
  open Setoid setoid using (_≈_) 
                     renaming (Carrier to C; isEquivalence to ≈equiv)

  open IsEquivalence ≈equiv using () renaming (refl to ≈refl; sym to ≈sym)  
  open module EqR≈ = EqR setoid renaming (_≈⟨_⟩_ to _≈[_]_)
  module FP≈ = FP _≈_ 

  field  _∙_    : Op₂ C
         ∙cong  : _∙_ Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_  
         ∙assoc : FP≈.Associative _∙_ 
         ∙comm  : FP≈.Commutative _∙_  
         unity  : Unity setoid _∙_

  -- some items and lemmata in-place ---------------------------------------

  ∙cong₁ : {y : C} → (\ x → x ∙ y) Preserves _≈_ ⟶ _≈_    
  ∙cong₁ x=x' =  ∙cong x=x' ≈refl

  ∙cong₂ : {x : C} → (_∙_ x) Preserves _≈_ ⟶ _≈_    
  ∙cong₂ =  ∙cong ≈refl

  _∣_ : Rel C (α ⊔ α=)                    -- `x divides y' 
  x ∣ y =  RightQuotient setoid _∙_ y x

  infix 2 _~asd_                          -- `associated'

  _~asd_ : Rel C (α ⊔ α=)
  a ~asd b =  a ∣ b  ×  b ∣ a

  ~asd→≈ :  Set _                         -- "_~asd_ is identical".
  ~asd→≈ =  ∀ {x y} → x ~asd y → x ≈ y   

  ∣cong : _∣_ Respects2 _≈_
  ∣cong {x} {x'} {y} {y'} x=x' y=y' (q , x∙q=y) =  (q , x'∙q=y')
                     where
                     x'∙q=y' :  x' ∙ q ≈ y'
                     x'∙q=y' =  begin  x' ∙ q   ≈[ ∙cong₁ $ ≈sym x=x' ]
                                       x  ∙ q   ≈[ x∙q=y ]
                                       y        ≈[ y=y' ]
                                       y'
                                ∎

  ∣cong₁ : {y : C} → (\x → x ∣ y) Respects _≈_
  ∣cong₁ x=x' =  ∣cong x=x' ≈refl

  ∣cong₂ : {x : C} → (_∣_ x) Respects _≈_
  ∣cong₂ = ∣cong ≈refl

  x∣x∙ : {x : C} → (y : C) →  x ∣ (x ∙ y)
  x∣x∙ y =  (y , ≈refl)

  ∣trans : Transitive _∣_
  ∣trans {x} {y} {z} (q , xq=y) (q' , yq'=z) =  (qq' , xqq'=z)
             where
             qq' = q ∙ q'

             xqq'=z : x ∙ qq' ≈ z
             xqq'=z = begin  x ∙ (q ∙ q')   ≈[ ≈sym $ ∙assoc x q q' ]
                             (x ∙ q) ∙ q'   ≈[ ∙cong₁ $ xq=y ]
                             y ∙ q'         ≈[ yq'=z ]
                             z
                      ∎
  ε : C  
  ε = proj₁ unity 

  ε∙ : (x : C) → (ε ∙ x) ≈ x
  ε∙ = proj₁ ∘ proj₂ unity 

  ∙ε : (x : C) → (x ∙ ε) ≈ x
  ∙ε = proj₂ ∘ proj₂ unity 

  open Setoid setoid public 





--****************************************************************************
module OfAssociated {α α=} (cMon : CMonoid α α=) 
  where
  open CMonoid cMon using (setoid; isEquivalence; _≈_; ε; _∣_; _~asd_; ∣cong;
                           ∣cong₂;∣trans; ∙ε 
                          ) 
                    renaming (Carrier to C) 

  open IsEquivalence isEquivalence using () 
                     renaming (refl to ≈refl; sym to ≈sym; trans to ≈trans)

  x∣x : (x : C) → x ∣ x
  x∣x x =  (ε , ∙ε x)

  ≈→∣ : {x y : C} → x ≈ y → x ∣ y
  ≈→∣ {x} {_} x≈y =  (ε , x∙ε≈y)  where
                                  x∙ε≈y = ≈trans (∙ε x) x≈y

 
  data Associated : Set α  where  asd : C → Associated

  fromAsd : Associated → C
  fromAsd (asd x) = x

  infixl 2 _=asd_

  _=asd_ :  Rel Associated (α ⊔ α=)
  _=asd_ =  _~asd_ on fromAsd

  ~asd-refl :  Reflexive _~asd_
  ~asd-refl {a} =  (x∣x a , x∣x a)

  ≈→~asd :  ∀ {x y} → x ≈ y → x ~asd y
  ≈→~asd {x} {y} x=y =  (x∣y , y∣x)
                                   where  x∣y = ∣cong₂ x=y $ x∣x x
                                          y∣x = ∣cong₂ (≈sym x=y) $ x∣x y
  =asdRefl : Reflexive _=asd_
  =asdRefl = ~asd-refl

  =asdSym : Symmetric _=asd_
  =asdSym (a∣b , b∣a) =  (b∣a , a∣b)

  =asdTrans : Transitive _=asd_
  =asdTrans (a∣b , b∣a) (b∣c , c∣b) =  (∣trans a∣b b∣c , ∣trans c∣b b∣a)

  asdIsEquiv : IsEquivalence _=asd_
  asdIsEquiv = record{ refl  = \{x}         → =asdRefl {x}
                     ; sym   = \{x} {y}     → =asdSym {x} {y}
                     ; trans = \{x} {y} {z} → =asdTrans {x} {y} {z} }
  
  asdSetoid : Setoid α (α ⊔ α=)
  asdSetoid = record{ Carrier       = Associated
                    ; _≈_           = _=asd_
                    ; isEquivalence = asdIsEquiv }

  open OfCongMap asdSetoid setoid using ()                              -- (1)
                                  renaming (IsInjective to IsInjective-from) 

  fromAsd-isInjective : IsInjective-from fromAsd
  fromAsd-isInjective = ≈→~asd                                          -- (2)



--****************************************************************************
module _ {α α=} (cMon : CMonoid α α=)
  where
  open CMonoid cMon using (setoid) 

  open OfAssociated {α} {α=} cMon using (asd; fromAsd; ≈→~asd; asdSetoid;
                                                          fromAsd-isInjective)
                                                                       -- (3)
  open OfCongMap {α} {α ⊔ α=} {α} {α=} asdSetoid setoid using (IsInjective)
                                                                       -- (4)
  fromAsd-isInj : IsInjective fromAsd                      
  fromAsd-isInj = fromAsd-isInjective                                  -- (5)
                  -- ≈→~asd