[Agda] foo ∘ fromFoo strangeness

[Sergei Meshveliani]

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