[Agda] foo ∘ fromFoo strangeness

[Twan van Laarhoven]

fromFoo is defined as a pattern match. That means that `fromFoo x` will not 
reduce further, unless Agda can match one of the patterns. So the overall goal 
becomes `foo (fromFoo x) == x` where x is the name for the underscore.

If you also pattern match in foo∘fromFoo, then you get get that `x = foo y`, and 
hence the reduction can happen, `fromFoo x = fromFoo (foo y) = y` and so `foo 
(fromFoo x) = foo y = x`.

Twan

On 08/31/14 17:00, Sergei Meshveliani wrote:
> 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
>