<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"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></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 "Report a bug", 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'; _≈_ to _='_)<br>
<br>
fromMb : C → Maybe C → C<br>
fromMb _ (just x) = x<br>
fromMb n nothing = n<br>
<br>
cong-fromMb : {n n' : C} → {m m' : C'} → n ≈ n' → m =' m' →<br>
fromMb n m ≈ fromMb n' m'<br>
<br>
cong-fromMb {n} {n'} {m} {m'} n=n' m=m' with m | m' | m=m'<br>
...<br>
| just _ | just _ | Mb.Eq.just x=y = x=y<br>
... | nothing | nothing | _ = n=n'<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>