# Agda Error after reload when successfully filling a goal

So I'm not sure what this error is and I'm not even sure how I would find out. I'm trying to code up a proof that refl is a right identity. I've gotten to this stage:

Refl∙ : {A : Type} {x y : A} (p : x ≡ y) → (compPath p refl) ≡ p
Refl∙ {x = x} {y = y} p i j  = hfill {!!} {!!} {!!}


Then, I want to fill the first hole with a partial element to lend:

Refl∙ : {A : Type} {x y : A} (p : x ≡ y) → (compPath p refl) ≡ p
Refl∙ {x = x} {y = y} p i j  = hfill ( (λ k → λ {(i = i0) → x ; (i = i1) → y ; (j = i1) → p i})) {!!} {!!}


And in fact Agda lets me enter this. I.e., Agda lets me cntrl+c cntrl+spc on the hole. But, if I then load the document, I receive the following error:

hcomp (λ { j (i = i0) → x ; j (i = i1) → refl j }) (p i) != x of
type A
when checking the definition of Refl∙


So, what is wrong with what I have entered? And why does Agda let me enter it but then throws an error when I try to re load the document?

Your code has a very simple proof using the filler of compPath, called compPath-filler:
Refl∙ {x = x} {y = y} p = sym (compPath-filler p refl)

A simple explanation of the error message: hcomp (λ { j (i = i0) → x ; j (i = i1) → refl j }) (p i) is compPath p refl, and this is what Agda expects your hfill at i = i0, but your i = i0 case is x.