`linarith` `splitNe` option fails too easily

[hrmacbeth]

The following example should be solved by the linarith call:

import Mathlib.Tactic.Linarith

example {V : Type*} [AddCommGroup V] {x : V} (hx : x ≠ 0) {a b : ℚ} (hab : a ≠ b) (hab' : a = b) :
    False := by
  linarith (config := { splitNe := true })

but instead we get the error "failed to synthesize LinearOrder V". I assume that what's happening is an issue in the linarith splitNe option: that it assumes all ≠ hypotheses are relevant to linarith. The tactic should be fixed by having linarith ignore ≠ hypotheses if no LinearOrderedField instance can be found on the type.