Ich bin in einer seltsamen Situation in GHC 8.0.1 mit gut indizierten (?) GADTs gelandet, bei denen das Einführen von Foralls in die Typ-vs-Art-Signaturen zu unterschiedlichen Typenprüfungsverhalten führt.
Betrachten Sie die folgenden Datentypen:
%Vor% Dieser Datentyp wird einfach kompiliert. Wenn wir jedoch die Art von x im Konstruktor G angeben möchten, erhalten wir einen Typfehler.
Die Fehlermeldung ist
%Vor%
Wenn wir die forall zur Art-Signatur hinzufügen (mit oder ohne forall im Konstruktor), gibt es keinen Fehler.
Was ist los?
Autor von TypeInType hier. K. A. Buhr macht es richtig oben; Das ist nur ein Fehler. Es ist in HEAD behoben.
Für die allzu neugierigen: Diese Fehlermeldung soll Definitionen wie
beseitigen %Vor%wo
%Vor% kann von Data.Proxy importiert werden. Bei der Deklaration eines Datentyps in Haskell98-artiger Syntax müssen existentiell quantifizierte Variablen explizit in den Geltungsbereich mit forall einbezogen werden. Aber k wird nie explizit in den Geltungsbereich gebracht; Es wird nur in der Art von a verwendet. Das bedeutet, dass k universell quantifizierbar sein sollte (mit anderen Worten, es sollte ein unsichtbarer Parameter für J sein, wie der Parameter k bis Proxy ) ... aber wenn wir J schreiben, Es gibt keine Möglichkeit zu bestimmen, was k sein sollte, also wäre es immer mehrdeutig. (Im Gegensatz dazu können wir die Wahl für den k -Parameter auf Proxy entdecken, indem wir uns die Art von a ansehen.)
Diese Definition für J ist in 8.0.1 und in HEAD nicht erlaubt.