To be ruthlessly, uselessly pedantic - after all, we're mathematicians - there's reasonable definitions of "academic" where logical unsoundness is still academic if it never interfered with the reasoning behind any proofs of interest ;)
But: so long as we're accepting that unsoundness in your checker or its underlying theory are intrinsically deal breakers, there's definitely a long history of this, perhaps somewhat more relevant than the HM example, since no proof checkers of note, AFAIK, have incorporated mutation into their type theory.
For one thing, the implementation can very easily have bugs. Coq itself certainly has had soundness bugs occasionally [0]. I'm sure Agda, Lean, Idris, etc. have too, but I've followed them less closely.
But even the underlying mathematics have been tricky. Girard's Paradox broke Martin-Löf's type theory, which is why in these dependently typed proof assistants you have to deal with the bizarre "Tower of Universes"; and Girard's Paradox is an analogue of Russell's Paradox which broke more naive set theories. And then Russell himself and his system of universal mathematics was very famously struck down by Gödel.
> there's reasonable definitions of "academic" where logical unsoundness is still academic if it never interfered with the reasoning behind any proofs of interest ;)
I wouldn't really so. If you were relying on the type system to tell you about any errors you made in your program, the revelation that your type system was unsound is not "only academic" simply because your program coincidentally didn't have errors. Just like it wouldn't be "only academic" if you discovered that your car's airbags weren't functional for the last 10 years even though you never had any accidents.
But: so long as we're accepting that unsoundness in your checker or its underlying theory are intrinsically deal breakers, there's definitely a long history of this, perhaps somewhat more relevant than the HM example, since no proof checkers of note, AFAIK, have incorporated mutation into their type theory.
For one thing, the implementation can very easily have bugs. Coq itself certainly has had soundness bugs occasionally [0]. I'm sure Agda, Lean, Idris, etc. have too, but I've followed them less closely.
But even the underlying mathematics have been tricky. Girard's Paradox broke Martin-Löf's type theory, which is why in these dependently typed proof assistants you have to deal with the bizarre "Tower of Universes"; and Girard's Paradox is an analogue of Russell's Paradox which broke more naive set theories. And then Russell himself and his system of universal mathematics was very famously struck down by Gödel.
But we've definitely gotten it right this time...
[0] https://github.com/coq/coq/issues/4294