Since we got the hackage version as well, would it make sense to just drop this version from nixpkgs?

As far as I can see, the tamarin-prover package adds a vim plugin and includes a tamarin plugin for something called SAPIC. So it's not exactly packaged twice.

@kmein @Mic92 No, I do not want to drop this package. The version of tamarin-prover that is exposed in all-packages.nix is the correct version for 99.99% of all users to use, because it actually exposes all the needed tooling (such as maude) in the wrappers, avoids spurious Haskell toolchain dependencies, and has multiple enhancements (like a sapic build that carefully avoids OCaml dependencies as well, for specifying alternative specs that get compiled to Tamarin.) The version on Hackage is useful for Haskell programmers and coincidentally Haskell programmers that want to install Tamarin easily. It is not a suitable replacement for the actual package for end users, who may want to run third party proofs (e.g. of the WireGuard protocol.)

Furthermore, it is not upstream that broke their package, it is the fact that the binary-orphans package which they previously depended on has changed fundamentally in its 1.0 release and no longer exposes instances. It built totally fine as of a few weeks ago until it was broken (by an automatic update, I assume). Please see #69292 for more details. In short, hackage2nix or whatever simply fixed all binary-orphans users into using 1.0+ builds. The fact that some packages were nuked by this perhaps isn't surprising; Tamarin does yearly-ish releases, so they haven't caught up with this.

The best the Tamarin authors could have done is to specify a proper upper bounds on binary-orphans, but even then the only thing that would have happened is that it would have automatically been excluded from haskellPackages anyway. The actual fix is just to write a patch that uses binary-instances instead.