The exhaustiveness check problem IS fundamental to GADTs. The problem is similar to one of theorem proving:given theorems t1, t2, ..., tn, all of the form forall a1, ..., an. e, where e does not contain any existential or universal quantifiers, is a quantifier free theorem Z provable using intuitionistic logic.
I believe that the problem I just stated is semi decidable: if it is provable, then you will find a proof if you search enough. If there is no proof, then you are doomed to search forever. Someone please correct me if I'm wrong.
In our case, t1, t2, ..., tn are the constructors and Z is the type of the guard. Our problem is simpler because the type of our constructors are of a simpler form: forall a1, ..., an . e -> (b1, b2, ..., bn) C where C is our type constructor and b1, ..., bn are arbitrary quantifier free formulae. If anyone knows anything about the decidability of this potentially simpler problem, I'd very much like to know.
The way O'Caml currently handles GADT exhaustiveness is like so: it searches for non exhaustive patterns in the same manner as before and whatever it finds it tries to type. However, these patterns may contain wildcards.