fix(emacs/lean-syntax): syntax highlight, issue #306

1- FIXED     structure foo := (bar : Type) -- the name of structures is not highlighted
2- NOT FIXED check foo-- this comment is not highlighted
3- FIXED     check Type.{5} -- Type is not highlighted
4- FIXED     definition bar{thisishighlighted : Type} := foo
5- FIXED     definition bar2 {thetypeofthisvariableisnothighlighted :Type} := foo

Have no idea what is going on with 2. I'm not sure if this is our bug,
or Emacs code we depend on.
fix(kernel/error_msgs): ignore binder information when comparing type mismatches, fixes #304
fix(kernel/error_msgs): ignore binder information when comparing type mismatches, fixes #304