I've used equality witnesses in F# before, they kinda work but can't match proper GADTs. First you'll need identity conversion methods on the witness, because patterns can't introduce type equalities, then you'll realise you can't refute unreachable branches for the same reason, so you still need to use exceptions.