Ich hatte Probleme mit GHC.TypeLits . Betrachten Sie die folgende GADT:
%Vor% Mein Verständnis war, dass jetzt für jeden n
der Typ Foo n
genau einen Wert enthält (entweder SmallFoo oder BigFoo, abhängig vom Wert von n
).
Aber wenn ich jetzt eine konkrete Instanz wie folgt konstruieren möchte:
%Vor%Dann spuckt GHC (7.6.2) die folgende Fehlermeldung aus:
%Vor%Das scheint seltsam - ich habe erwartet, dass es eine vordefinierte Instanz für solche Typ-Level-Nat-Vergleiche gibt. Wie kann ich diese Art von Constraints in meinem Datenkonstruktor mit Naturals auf Typenebene ausdrücken?
Solver für TypeLists ist momentan nicht in GHC, entsprechend der Statusseite sind einige Chancen, dass es in GHC 7.8 im Oktober oder etwas sein wird.
Vielleicht ist es besser, andere Pakete zu verwenden.
Dies wird auf dem aktuellen Kopf des type-nats Zweiges kompiliert, der (hoffentlich) zusammengeführt werden sollte 7.8.
%Vor% Wenn myFoo
geändert wird, um vom Typ Foo 1
zu sein, kann es nicht kompiliert werden, vermutlich weil die Klassenbedingung x <= y
auf die Gleichheitsbedingung (x <=? y) ~ 'True
erweitert wurde: