Agda Error after reload when successfully filling a goal

Question

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?

Answer 1

This is a problem of the implementation of Cubical Agda. The cubical equations are thrown to the constraint solver, and probably (I guess) the goal-filling mechanism only checks the type, not the constraints. When you recheck the file, it realizes that some constraints cannot be solved, so it marks you code as yellow.

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.