[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