<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&#7481; (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&#7481; 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} &#8594; Free (Op a) A &#8594; Free (Op a) A<br>
> op {A = A} ma = impure (op&#738; A , &#955; { (inj&#8321; tt) &#8594;<br>
ma; (inj&#8322; x) &#8594; 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&#8242; : {a : Level} {A : Set (suc a)} &#8594; Free (Op a) A &#8594;<br>
Free (Op a) A<br>
> op&#8242; {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 _&#9665;_/_<br>
    field<br>
      Shape : Set a<br>
      Pos   : Shape &#8594; Set a<br>
      Ctx   : (s : Shape) &#8594; Pos s &#8594; Maybe {a = suc a} (Set a)<br>
<br>
  open Container public<br>
<br>
  &#10214;_&#10215; : Container a &#8594; (Set a &#8594; Set a) &#8594;<br>
Set a &#8594; Set a<br>
  &#10214; S &#9665; P / C &#10215; F A = &#931;[ s &#8712; S ] ((p : P s)<br>
&#8594; F (fromMaybe A (C s p)))<br>
<br>
  data Free {a : Level} (C : Container a) (A : Set a) : Set a where<br>
    pure   : A                &#8594; Free C A<br>
    impure : &#10214; C &#10215; (&#955; A &#8594; Free C A) A &#8594;<br>
Free C A<br>
<br>
  data List&#7481; (C : Container a) (A : Set a) : Set a where<br>
    nil : List&#7481; C A<br>
    cons : Free C A &#8594; Free C (List&#7481; C A) &#8594; List&#7481; C A<br>
<br>
  ROp : &#8704; a &#8594; Container (suc a)<br>
  ROp a = Set a &#9665; id / &#955; _ _ &#8594; nothing<br>
<br>
  rop : {a : Level} {A : Set a} &#8594; Free (ROp a) A<br>
  rop {_} {A} = impure (A , pure)<br>
<br>
  rop&#8242; : {a : Level} {A : Set (suc a)} &#8594; Free (ROp a) A<br>
  rop&#8242; = rop<br>
<br>
  rop&#8321; : {A : Set&#8321;} &#8594; Free (ROp 0&#8467;) A<br>
  rop&#8321; = rop&#8242;<br>
<br>
  _bind_ : {A B : Set (suc a)} &#8594; Free (ROp a) A &#8594; (A &#8594;<br>
Free (ROp a) B)<br>
    &#8594; Free (ROp a) B<br>
  pure x bind k = k x<br>
  impure (X , pf) bind k = impure (X , &#955; p &#8594; pf p bind k)<br>
<br>
  M : Set&#8321;<br>
  M = Free (ROp 0&#8467;) &#8869;<br>
<br>
  m : (I : Set&#8321;) &#8594; (I &#8594; M) &#8594; M<br>
  m I pf = rop&#8321; {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>
  _&#8712;_ : M &#8594; M &#8594; Set&#8321;<br>
  a &#8712; (impure (I , f)) = &#8707;[ i ] (a &#8801; f i)<br>
<br>
  _&#8713;_ : M &#8594; M &#8594; Set&#8321;<br>
  x &#8713; y = x &#8712; y &#8594; &#8869;<br>
<br>
  R : M<br>
  R = m (&#931; M &#955; s &#8594; s &#8713; s) proj&#8321;<br>
<br>
  lem-1 : {X : M} &#8594; X &#8712; R &#8594; X &#8713; X<br>
  lem-1 ((s , s&#8713;s) , p) = subst&#8322; _&#8713;_ p' p' s&#8713;s<br>
where p' = sym p<br>
<br>
  lem-2 : {X : M} &#8594;  X &#8713; X &#8594; X &#8712; R<br>
  lem-2 {X} X&#8713;X = ((X , X&#8713;X) , refl)<br>
<br>
  lem-3 : R &#8713; R<br>
  lem-3 R&#8712;R = lem-1 R&#8712;R R&#8712;R<br>
<br>
  contr : &#8869;<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>