Agda: Cannot Instantiate Metavariable

Question

I'm running into a certain error while trying to code something up in cubical Agda, but I can't understand the error. Here is my code:

liftFam' : {A : Type} {x y : A} {B : A → Type} (u : B x) (p : x ≡ y) → (x , u) ≡ (y , (transp (λ i → B (p i)) i0) u)
liftFam' u p = {!!}

But, I get the following error upon trying to load the document:

Cannot instantiate the metavariable _219 to solution B (p i1)
since it contains the variable p
which is not in scope of the metavariable
when checking that the expression transp (λ i → B (p i)) i0 u has
type _B_219 y

Can anybody give some advice on what the problem is?

Answer 1

TL; DR: Explicitly stating the type of the equality solves the problem:

_≡_ {A = Σ _ B} (x , u) (y , transp (λ i → B (p i)) i0 u)

I think the main problem is that Agda is confused about the type of the dependent pair (which should be Σ A B, but you didn't in any way indicate that). In usual cases Agda should infer that by looking at the types on both sides of the equality. The further complication of transp completely threw Agda off, so it is reporting something seemingly unrelated to the core error.

Answer 2

Apart from @Trebor's answer, there is another way to specify the implicit argument:

(x , u) ≡ (_,_ {B = B} y (transp (λ i → B (p i)) i0 u))

You may also remove the parentheses on the right hand side:

(x , u) ≡ _,_ {B = B} y (transp (λ i → B (p i)) i0 u)