In particular, instead of
   Cannot match 'a' with 'b'
we get
   Could not deduce (a~b) from context (F a ~ b)
or whatever