Type equality in GADT/TypeFamily context

It’s failing in the case

   Nothing ->   l

and it needs to know

Pop (x : l) c ~ (x : l)

and it seems like it should be able to know that because we’ve demonstrated that x is not c, so we “should” fall through to the

  Pop m         c  = m

where m ~ (x : l). I guess you need something like a “type in equality” constraint in the Nothing branch, but I don’t think those exist!