Gibt es eine Möglichkeit, GHC davon zu überzeugen, dass diese (injektive) Familie injektiv ist?

Ich habe mit GHC's DataKinds herumgespielt und versucht, binäre Nats vom Typ-Level zu implementieren. Sie sind einfach genug zu implementieren, aber wenn ich möchte, dass sie in häufigen Fällen nützlich sind, dann muss GHC glauben, dass die Succ -Typ-Familie injektiv ist (so dass Typ-Inferenz mindestens genauso gut funktioniert wie für unäre Typ-Level-Nats). Es fällt mir jedoch schwer, GHC davon zu überzeugen, dass dies der Fall ist. Betrachten Sie die folgende Kodierung von binären Nats:

GHC kann dies nicht akzeptieren, weil es nicht sagen kann, dass Succ1 injektiv ist:

Wir glauben, dass es injektiv ist, weil bei der Überprüfung von Succ1 , One niemals in seinem Image ist, also liefert der Bit0 (Succ1 x) -Fall niemals Bit0 One und damit Bit1 Der Fall steht niemals in Konflikt mit dem Fall One . Das gleiche Argument (" One ist nicht im Bild von Succ1 ") zeigt, dass Succ selbst ebenfalls injektiv ist. GHC ist jedoch nicht so clever genug, um dieses Argument zu finden.

Also, Frage: Gibt es in diesem Fall (und in Fällen wie diesen) eine Möglichkeit, GHC davon zu überzeugen, dass eine injizierende Familie in der Tat injektiv ist? (Vielleicht ein Typchecker-Plugin, wo ich eine Funktion bereitstellen kann, die Succ1 invertiert? Vielleicht ein Pragma, das sagt: "Versuche rückwärts von dieser Familie zu lernen, als ob es injektiv wäre; wenn du irgendwelche Unklarheiten triffst, darfst du abstürzen?") >