<div dir="ltr"><div>Hi Jonas,</div><div><br></div><div>If you can prove false, then it is reasonable to assume that you indeed found a bug in the current version of Agda. Could you please report this issue on the bug tracker at <a href="http://github.com/agda/agda/issues">github.com/agda/agda/issues</a>? Somehow the unicode did not come through correctly which makes the code hard to read.</div><div><br></div><div>-- Jesper<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, Sep 15, 2020 at 10:10 AM <<a href="mailto:jonas.hoefer@stud.htwk-leipzig.de">jonas.hoefer@stud.htwk-leipzig.de</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Hello<br>
<br>
> Note that the last example works fine:<br>
<br>
Your code only seems works with the current Agda version from the Master<br>
branch<br>
not Agda version 2.6.1 (or 2.6.1.1). I don't think the last example should<br>
work.<br>
It fails in version 2.6.1 with the error message "Set (suc a) is not less or<br>
equal than Set a".<br>
<br>
> foo bar : Free (Op a) (Listᴹ (Op a) Bool)<br>
> foo = pure nil<br>
> bar = op foo<br>
<br>
Op a produces a container of level suc a. Free and Listᴹ both use<br>
the level of<br>
their container i.e. suc a. op expects an argument of level a (not suc a,<br>
because the stored type is smaller), but passing foo seems to work.<br>
<br>
> op : {A : Set a} → Free (Op a) A → Free (Op a) A<br>
> op {A = A} ma = impure (opˢ A , λ { (inj₁ tt) →<br>
ma; (inj₂ x) → pure x })<br>
<br>
Replacing Set a with Set (suc a) in the definition of op fails with the same<br>
error, but the following works.<br>
<br>
> op′ : {a : Level} {A : Set (suc a)} → Free (Op a) A →<br>
Free (Op a) A<br>
> op′ {a} {A} ma = op {a} ma<br>
<br>
Passing {A} directly as an argument to op also yields the error, but omitting<br>
it works. I think this behavior is a bug in the current version, because the<br>
following implementation of Russel's paradox type checks with my build of the<br>
latest version (commit 832057961873856915c41745c37e055ff4b2c583).<br>
<br>
{-# OPTIONS --cumulativity #-}<br>
<br>
open import Data.Bool<br>
open import Data.Empty<br>
open import Data.Product<br>
open import Data.Sum<br>
open import Data.Unit<br>
open import Data.Maybe<br>
<br>
open import Function<br>
open import Level<br>
<br>
open import Relation.Binary.PropositionalEquality<br>
<br>
private<br>
variable<br>
a : Level<br>
<br>
record Container a : Set (suc a) where<br>
constructor _◁_/_<br>
field<br>
Shape : Set a<br>
Pos : Shape → Set a<br>
Ctx : (s : Shape) → Pos s → Maybe {a = suc a} (Set a)<br>
<br>
open Container public<br>
<br>
⟦_⟧ : Container a → (Set a → Set a) →<br>
Set a → Set a<br>
⟦ S ◁ P / C ⟧ F A = Σ[ s ∈ S ] ((p : P s)<br>
→ F (fromMaybe A (C s p)))<br>
<br>
data Free {a : Level} (C : Container a) (A : Set a) : Set a where<br>
pure : A → Free C A<br>
impure : ⟦ C ⟧ (λ A → Free C A) A →<br>
Free C A<br>
<br>
data Listᴹ (C : Container a) (A : Set a) : Set a where<br>
nil : Listᴹ C A<br>
cons : Free C A → Free C (Listᴹ C A) → Listᴹ C A<br>
<br>
ROp : ∀ a → Container (suc a)<br>
ROp a = Set a ◁ id / λ _ _ → nothing<br>
<br>
rop : {a : Level} {A : Set a} → Free (ROp a) A<br>
rop {_} {A} = impure (A , pure)<br>
<br>
rop′ : {a : Level} {A : Set (suc a)} → Free (ROp a) A<br>
rop′ = rop<br>
<br>
rop₁ : {A : Set₁} → Free (ROp 0ℓ) A<br>
rop₁ = rop′<br>
<br>
_bind_ : {A B : Set (suc a)} → Free (ROp a) A → (A →<br>
Free (ROp a) B)<br>
→ Free (ROp a) B<br>
pure x bind k = k x<br>
impure (X , pf) bind k = impure (X , λ p → pf p bind k)<br>
<br>
M : Set₁<br>
M = Free (ROp 0ℓ) ⊥<br>
<br>
m : (I : Set₁) → (I → M) → M<br>
m I pf = rop₁ {I} bind pf<br>
<br>
-- Now we can follow some implementation of Russell's Paradox<br>
-- <a href="http://www.cs.nott.ac.uk/~psztxa/g53cfr/l20.html/l20.html" rel="noreferrer" target="_blank">http://www.cs.nott.ac.uk/~psztxa/g53cfr/l20.html/l20.html</a><br>
<br>
_∈_ : M → M → Set₁<br>
a ∈ (impure (I , f)) = ∃[ i ] (a ≡ f i)<br>
<br>
_∉_ : M → M → Set₁<br>
x ∉ y = x ∈ y → ⊥<br>
<br>
R : M<br>
R = m (Σ M λ s → s ∉ s) proj₁<br>
<br>
lem-1 : {X : M} → X ∈ R → X ∉ X<br>
lem-1 ((s , s∉s) , p) = subst₂ _∉_ p' p' s∉s<br>
where p' = sym p<br>
<br>
lem-2 : {X : M} → X ∉ X → X ∈ R<br>
lem-2 {X} X∉X = ((X , X∉X) , refl)<br>
<br>
lem-3 : R ∉ R<br>
lem-3 R∈R = lem-1 R∈R R∈R<br>
<br>
contr : ⊥<br>
contr = lem-3 (lem-2 {R} lem-3)<br>
<br>
Jonas<br>
<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>