Re: [Agda] foo ∘ fromFoo strangeness

[Dmytro Starosud]

For type-checker it's not obvious that for all x in Foo exists y such that
x == foo y.

I think this might be because Foo is data, and data in general case can
have many constructors.
If it was a record than probably it would be type checked successfully
(since records can have only one).

Regards,
Dmytro



2014-08-31 18:00 GMT+03:00 Sergei Meshveliani <mechvel at botik.ru>:

> People,
> I observe the program
>
> ---------------------------------------------------
> open import Function using (id; _∘_)
> open import Relation.Binary.PropositionalEquality as PE using (_≗_)
>
> module _ α (A : Set α)
>   where
>   data Foo : Set α  where  foo : A → Foo
>
>   fromFoo : Foo → A
>   fromFoo (foo x) = x
>
>   fromFoo∘foo : fromFoo ∘ foo ≗ id
>   fromFoo∘foo _ = PE.refl
>
>   foo∘fromFoo : foo ∘ fromFoo ≗ id
>   foo∘fromFoo _ =  PE.refl {A = Foo}
> -----------------------------------------------------
>
> fromFoo∘foo  is type-checked (in Agda-2.4.2).
>
> For  foo∘fromFoo,
> I expected that if it is not type-checked, it would report of
> "unsolved metas".
> But it reports     " foo (fromFoo .x) != .x of type Foo  ... "
>
> Anyway, the thing can be implemented by
> foo∘fromFoo (foo _) =  PE.refl
>
> But is the above report natural?
>
> Thanks,
>
> ------
> Sergei
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140831/cce1a26a/attachment.html