Ich habe den folgenden Code und möchte, dass fehlschlägt type checking:
%Vor% Die Idee ist, dass jeder Eintrag in der GADT einen zugehörigen Fehler hat, den ich mit einer Prism in eine größere Struktur modelliere. Wenn ich diese GADT "interpretiere", gebe ich einen konkreten Typ für e an, der Instanzen für all diese Prism s hat. Für jeden einzelnen Fall möchte ich jedoch keine Instanzen verwenden können, die nicht im zugehörigen Kontext des Konstruktors deklariert sind.
Der obige Code sollte ein Fehler sein, denn wenn ich Muster auf Two anpasse, sollte ich lernen, dass ich nur Increment e verwenden kann, aber ich verwende Greet . Ich kann sehen, warum das funktioniert - Either String Int hat eine Instanz für Greet , also wird alles ausgecheckt.
Ich bin nicht sicher, was der beste Weg ist, das zu beheben. Vielleicht kann ich die Entbindung von Data.Constraint verwenden, oder vielleicht gibt es einen Trick mit höheren Rangtypen.
Irgendwelche Ideen?
Das Problem ist, dass Sie den endgültigen Ergebnistyp korrigieren, so dass die Instanz existiert und der Typprüfer sie finden kann.
Versuchen Sie etwas wie:
%Vor% Nun kann der Ergebnistyp die Instanz für review nicht auswählen, und parametricity erzwingt Ihre Invariante.