Agda: proving that, when values are equal, their constructor arguments are equal

Question

I'm trying to write the following function:

justEq : ∀ {A} -> (x y : A) -> (just x ≡ just y) -> (x ≡ y)
justEq x y pf = {!!}

I don't know how to write this. To me, it is intuitive to the point of being axiomatic, but the compiler doesn't accept refl as a proof of it.

I'm routinely having to prove these sorts of things, for example, showing that if two non-empty lists are equal, then their heads are equal.

What is the general approach to this? Is this related to Conor McBride's "green-goo" of having functions in the return of Constructors?

Answer 1

The basis of the solution is to pattern match on pf being refl together with using a dotted pattern for y being equal to x (because of the type of refl!).

justEq : ∀ {A} -> (x y : A) -> (just x ≡ just y) -> (x ≡ y)
justEq x .x refl = {!!}

At this point, the type of the hole on the right-hand side has been unified to (x ≡ x) because of the y = .x equality from the pattern match, meaning you can use refl as a well-typed value, giving

justEq x .x refl = refl