[Agda] Internal error

Sergei Meshveliani mechvel at botik.ru
Thu Oct 6 20:32:15 CEST 2016


Dear Agda developers,

"Report a bug" does no connect. Neither it works
https://github.com/agda/agda/issues,

so I report a bug here.

Please, find enclosed a small Agda code.

This is on  Development Agda of October 4, 2016,  ghc-7.10.2.

        > agda $agdaLibOpt Bug-oct6-2016.agda
reports
-------------------                                                             
An internal error has occurred. Please report this as a bug.
Location of the error: src/full/Agda/TypeChecking/Substitute.hs:800
------------------                                                              

1. Development agda of September 16, 2016  produces a correct report
   (of an user error).

2. Replacing  +upGroup  with its value  (proj₁ +comG)  in the line

       +group = UpGroup.group +upGroup     -- (proj₁ +comG)     ** 


   also	leads to a correct report in both Agda versions.


Regards,

------
Sergei
-------------- next part --------------
{- This is on  Development agda of October 4, 2016,  ghc-7.10.2.

        agda $agdaLibOpt Bug-oct6-2016.agda
reports 
-------------------
An internal error has occurred. Please report this as a bug.
Location of the error: src/full/Agda/TypeChecking/Substitute.hs:800
------------------

1. Development agda of September 16, 2016  produces a correct report
   (of an user error).

2. Replacing  +upGroup  with its value  (proj₁ +comG)  in the line 

          +group = UpGroup.group +upGroup     -- (proj₁ +comG)  **

   also leads to a correct report.
-}

------------------------------------------------------------------
open import Level    using (Level; _⊔_) renaming (suc to sucL) 
open import Function using (_∘_)
open import Algebra.FunctionProperties as FP using (Op₂)
open import Relation.Nullary using (¬_) 
open import Relation.Binary  using 
            (Rel; Reflexive; Symmetric; Transitive; IsEquivalence; 
             Setoid; DecSetoid; _Preserves_⟶_; _Preserves₂_⟶_⟶_; 
             _Respects_
            )
import Relation.Binary.EqReasoning as EqR
open import Data.Product using (_×_; _,_; proj₁; proj₂; ∃; ∃₂; Σ)
open import Data.Nat     using (ℕ; suc)



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


record DSet {α α=} (decS : DecSetoid α α=) : Set (α ⊔ α=)
  where  
  decSetoid = decS
  open DecSetoid decS using (setoid; Carrier; _≈_) 

  field  dSet-foo : ℕ 
  -----

  ≈equiv : IsEquivalence _≈_
  ≈equiv = Setoid.isEquivalence setoid 

  ≈refl : Reflexive _≈_ 
  ≈refl = IsEquivalence.refl ≈equiv

  open DecSetoid decS public


record UpDSet c l : Set (sucL (c ⊔ l)) 
       where
       constructor upDSet′

       field  decSetoid : DecSetoid c l
              dSet      : DSet decSetoid
 
       open DSet dSet public hiding (decSetoid) 


--============================================================================
module _ {α α=} (A : Setoid α α=) (_∙_ : Op₂ (Setoid.Carrier A))
  where
  open Setoid A using (_≈_) renaming (Carrier to C)

  isUnity : C → Set (α ⊔ α=)    
  isUnity e =  (x : C) → ((e ∙ x) ≈ x) × ((x ∙ e) ≈ x)  

  Unity :  Set (α ⊔ α=)
  Unity =  ∃ \ (e : C) → isUnity e 


------------------------------------------------------------------------------
record Magma {α α=} (upDS : UpDSet α α=) : Set (α ⊔ α=)
       where
       upDSet     = upDS
       private dS = UpDSet.dSet upDS
          
       open DSet dS using (Carrier; _≈_; ≈refl; setoid; decSetoid) 
       infixl 7 _∙_

       field _∙_   : Op₂ Carrier
             ∙cong : _∙_ Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_  

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

       open UpDSet upDS public

record UpMagma α α= :  Set (sucL (α ⊔ α=))   
       where
       constructor upMagma′

       field  upDSet : UpDSet α α=
              magma  : Magma upDSet

       open Magma magma public hiding (upDSet)

record Semigroup {c l} (upMg : UpMagma c l) : Set (l ⊔ c) 
       where                             
       constructor semigroup′

       upMagma : UpMagma c l 
       upMagma = upMg

       open UpMagma upMg using (_≈_; _∙_)
       module FP≈ = FP _≈_ 

       field  ∙assoc : FP≈.Associative _∙_ 

       open UpMagma upMg public

record UpSemigroup c l : Set (sucL (c ⊔ l)) 
       where
       constructor upSemigroup′
       
       field upMagma   : UpMagma c l 
             semigroup : Semigroup upMagma

       open Semigroup semigroup public hiding (upMagma) 

--------------------------------------------------------------------------
record Monoid {α α=} (upSmg : UpSemigroup α α=) : Set (α ⊔ α=)
  where
  upSemigroup = upSmg
  open UpSemigroup upSmg using (setoid; semigroup; _≈_; _∙_; ∙cong₂)
                         renaming (Carrier to C) 

  open EqR setoid renaming (_≈⟨_⟩_ to _≈[_]_)

  field  unity : Unity setoid _∙_
  -----
  ε : C  
  ε = proj₁ unity 

  infixl 8 _^_

  field  _^_   : C → ℕ → C  
  -----
         ^-0   : ∀ {x}   → x ^ 0 ≈ ε
         ^-suc : ∀ x {e} → x ^ (suc e) ≈ x ∙ x ^ e

  -- add some items in-place ----------------------

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

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

  ^1 : ∀ x → x ^ 1 ≈ x  
  ^1 x = 
         begin  x ^ 1       ≈[ ^-suc x ]
                x ∙ x ^ 0   ≈[ ∙cong₂ ^-0 ]
                x ∙ ε       ≈[ ∙ε x ]
                x
         ∎

  open Semigroup   semigroup public
  open UpSemigroup upSmg     public using (semigroup)

------------------------------------------------------------------------------
record UpMonoid α α= :  Set (sucL (α ⊔ α=)) 
                        where
                        constructor upMonoid′ 
 
                        field  upSemigroup : UpSemigroup α α=
                               monoid      : Monoid upSemigroup

                        open Monoid monoid public hiding (upSemigroup)

record Group {α α=} (upMon : UpMonoid α α=) :  Set (α ⊔ α=)
  where
  upMonoid = upMon
  monoid   = UpMonoid.monoid upMon 

  open Monoid monoid using (Carrier; unity; ε) renaming (upMagma to upMg) 

  field  grFoo : ℕ 

  open Monoid monoid public 

record UpGroup α α= : Set (sucL (α ⊔ α=))  
                      where
                      field  upMonoid : UpMonoid α α=
                             group    : Group upMonoid

                      open Group group public hiding (upMonoid)

-----------------------------------------------------------
IsCommutativeGroup :  {α α= : Level} → UpGroup α α= → Set _
IsCommutativeGroup upG = 
                       Commutative _∙_
                       where
                       open UpGroup upG using (_≈_; _∙_)
                       open FP _≈_ using (Commutative)

CommutativeGroup : (α α= : Level) → Set _
CommutativeGroup α α= =  
                      Σ (UpGroup α α=) IsCommutativeGroup 


---------------------------------------------------------------------
record Ringoid {α α=} (+comG : CommutativeGroup α α=) :  Set (α ⊔ α=) 
       where
       +upGroup = proj₁ +comG 
       +group   = UpGroup.group +upGroup              -- (proj₁ +comG)  **
       open Group +group public using (upDSet; _≈_; _^_)

       field  *magma : Magma upDSet
       -----

       0# = Group.ε +group

       infixl 6 _+_ 
       infixl 7 _*_ 

       _+_ = Group._∙_ +group  
       _*_ = Magma._∙_ *magma

       *upMagma : UpMagma α α= 
       *upMagma = upMagma′ upDSet *magma

--------------------------------------------------------------------
record UpRingoid α α= :  Set (sucL (α ⊔ α=)) 
                         where
                         field  +commGroup : CommutativeGroup α α=
                                ringoid  : Ringoid +commGroup

--------------------------------------------------------------------
postulate anything : ∀ {a} {A : Set a} → A             -- 

module OverRingoid-0 {α α=} (upRd : UpRingoid α α=)
  where
  ringoid = UpRingoid.ringoid upRd
  open Ringoid ringoid using (_≈_; 0#; _*_; *upMagma; _^_)

  record R1 :  Set (α ⊔ α=)
         where
         module FP≈ = FP _≈_

         field  *assoc : FP≈.Associative _*_

         *semigroup : Semigroup *upMagma
         *semigroup = semigroup′ *assoc

         *upSemigroup = upSemigroup′ *upMagma *semigroup


  record R2 :  Set (α ⊔ α=)
         where
         field r1 : R1 

         open R1 r1 using (*upSemigroup)

         field  *monoid : Monoid *upSemigroup

         open Monoid *monoid using (^1) 
                                             -- hhere**  internal error 
         0^suc :  ∀ {n} → 0# ^ (suc n) ≈ 0#
         0^suc {0}     =  ^1 0#
         0^suc {_}     =  anything 



More information about the Agda mailing list