Is that a problem of variable inference?

[ice1000]

I have a proof that type-checks:

\import Arith.Int
\import Function
\import Homotopy.Sphere.Circle
\import Paths

\func transport-ap-assoc {A :\Type} (cover : A -> \Type)
                         {a a' : A} (p : a = a')
  : transport cover p = transport id (pmap cover p) \elim p
  | idp => idp

\func transport-code-loop : transport code (path loop) = isuc =>
  transport code (path loop)                    ==< transport-ap-assoc code (path loop) >==
  transport id (pmap code (path loop))          ==< pmap (transport id) lemma >==
  transport id (path (\lam i => code (loop i))) `qed
  \where {
    \func lemma : pmap code (path loop) = path (\lam i => code (loop i)) => idp
  }

I'm using a lemma whose type is whatever but the body is idp, which means its lhs and rhs are convertible. However, when I inline lemma, say, replace it with idp directly, Arend gives me type error.

Why should this happen?

The does-not-work code:

\func transport-code-loop : transport code (path loop) = isuc =>
  transport code (path loop)                    ==< transport-ap-assoc code (path loop) >==
  transport id (pmap code (path loop))          ==< pmap (transport id) lemma >==
  transport id (path (\lam i => code (loop i))) `qed

The error message:

[ERROR] bug.ard:13:53: Type mismatch
  Expected type: transport id (pmap code (path loop)) = ?a'
    Actual type: transport id ?a = transport id ?a'

[ice1000]

I guess it tries to unify the two sides without trying to compute one of them.

[valis]

Can't you just write

\func transport-code-loop : transport code (path loop) = isuc => transport-ap-assoc code (path loop)

?

[ice1000]

That's not related to this inference problem. The proof can be simplified, and I'm aware of that

[valis]

Even \func transport-code-loop : transport code (path loop) = isuc => idp works.

[valis]

Anyway, the problem is pmap (transport id) idp. Arguments for pmap cannot be inferred from idp (since they are not specified there, but they are specified in lemma so it works with it) and they cannot be inferred from the expected type because one of them evaluates to isuc and it doesn't match the expression from the type of pmap (which is transport id ... ?a).