Looks like backchain is forgetting the annotation on atomic goals when matching. This does not seem to be correct as the following development and "proof" shows:
Type q prop.
Define p : prop by
p := true.
Theorem cont : p -> q.
induction on 1. intros. assert p. backchain IH. backchain H2.