Equality proofs and pattern matching in total functions

Question

I know this is a bit contrived example, but I was wondering how do I make the following function total:

total foo : (x : Int) -> {auto prf : x = 10} -> Int
foo 10 = 10

At the moment type checker complains:

Main.foo is not total as there are missing cases

Edit:

Adding impossible branch to HTNWs answer I got it to typecheck this way:

total foo : (x : Int) -> {auto prf : x = 10} -> Int
foo 10 {prf = Refl} = 10
foo x {prf = Refl} impossible

Answer 1

You have to pattern match on the equality, too

total foo : (x : Int) -> {auto prf : x = 10} -> Int
foo 10 {prf=Refl} = 10