<div dir="ltr">A related problem was reported in issue 2235 (<a href="https://github.com/agda/agda/issues/2235">https://github.com/agda/agda/issues/2235</a>). Both<div>problems have been fixed (as of today).</div><div><br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Oct 4, 2016 at 1:49 PM, Sergei Meshveliani <span dir="ltr">&lt;<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">I fail to link to &quot;Report a bug&quot;, so I report here.<br>
<br>
This program is not type-checked by<br>
<br>
             agda $agdaLibOpts --sharing Foo.agda<br>
<br>
(in Development Agda of September16, 2016):<br>
<br>
------------------------------<wbr>------------------------------<wbr>----------<br>
open import Relation.Binary  using (Setoid)<br>
open import Data.Maybe as Mb using (Maybe; just; nothing; Eq)<br>
<br>
module _ {α α=} {A : Setoid α α=}<br>
  where<br>
  open Setoid A using (_≈_) renaming (Carrier to C; refl to ≈refl)<br>
  open Setoid (Mb.setoid A) renaming (Carrier to C&#39;; _≈_ to _=&#39;_)<br>
<br>
  fromMb : C → Maybe C → C<br>
  fromMb _ (just x) =  x<br>
  fromMb n nothing  =  n<br>
<br>
  cong-fromMb : {n n&#39; : C} → {m m&#39; : C&#39;} → n ≈ n&#39; → m =&#39; m&#39; →<br>
                                              fromMb n m ≈ fromMb n&#39; m&#39;<br>
<br>
  cong-fromMb {n} {n&#39;} {m} {m&#39;} n=n&#39; m=m&#39;  with  m | m&#39; | m=m&#39;<br>
  ...<br>
      | just _  | just _  | Mb.Eq.just x=y =  x=y<br>
  ... | nothing | nothing | _              =  n=n&#39;<br>
  ... | nothing | just _  | ()<br>
------------------------------<wbr>------------------------------<wbr>------------<br>
<br>
<br>
Regards,<br>
<br>
------<br>
Sergei<br>
<br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
</blockquote></div><br></div>