<div dir="ltr"><div>For type-checker it's not obvious that for all x in Foo exists y such that x == foo y.<br></div><div><br></div><div>I think this might be because Foo is data, and data in general case can have many constructors.<br>
If it was a record than probably it would be type checked successfully (since records can have only one).<br><br></div><div>Regards,<br></div><div>Dmytro <br><br></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">
2014-08-31 18:00 GMT+03:00 Sergei Meshveliani <span dir="ltr"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
People,<br>
I observe the program<br>
<br>
---------------------------------------------------<br>
open import Function using (id; _∘_)<br>
open import Relation.Binary.PropositionalEquality as PE using (_≗_)<br>
<br>
module _ α (A : Set α)<br>
where<br>
data Foo : Set α where foo : A → Foo<br>
<br>
fromFoo : Foo → A<br>
fromFoo (foo x) = x<br>
<br>
fromFoo∘foo : fromFoo ∘ foo ≗ id<br>
fromFoo∘foo _ = PE.refl<br>
<br>
foo∘fromFoo : foo ∘ fromFoo ≗ id<br>
foo∘fromFoo _ = PE.refl {A = Foo}<br>
-----------------------------------------------------<br>
<br>
fromFoo∘foo is type-checked (in Agda-2.4.2).<br>
<br>
For foo∘fromFoo,<br>
I expected that if it is not type-checked, it would report of<br>
"unsolved metas".<br>
But it reports " foo (fromFoo .x) != .x of type Foo ... "<br>
<br>
Anyway, the thing can be implemented by<br>
foo∘fromFoo (foo _) = PE.refl<br>
<br>
But is the above report natural?<br>
<br>
Thanks,<br>
<br>
------<br>
Sergei<br>
<br>
_______________________________________________<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" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div><br></div>