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.