Wie kann ich eingeschränkte Einschränkungen mit GADTs verwenden?

Question

Ich habe den folgenden Code, und ich würde das gerne Typprüfung fehlschlagen:

{-# LANGUAGE FlexibleInstances #-} 
{-# LANGUAGE GADTs #-} 
{-# LANGUAGE RankNTypes #-} 

import Control.Lens 

data GADT e a where 
    One :: Greet e => String -> GADT e String 
    Two :: Increment e => Int -> GADT e Int 

class Greet a where 
    _Greet :: Prism' a String 

class Increment a where 
    _Increment :: Prism' a Int 

instance Greet (Either String Int) where 
    _Greet = _Left 

instance Increment (Either String Int) where 
    _Increment = _Right 

run :: GADT e a -> Either String Int 
run = go 
    where 
    go (One x) = review _Greet x 
    go (Two x) = review _Greet "Hello" 

Die Idee ist, dass jeder Eintrag in der GADT einen zugehörigen Fehler hat, die ich mit einem Prism Modellierung bin in etwas größere Struktur. Wenn ich diese GADT "interpretiere", stelle ich einen konkreten Typ für e zur Verfügung, der Instanzen für alle 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 übereinstimmen auf Two 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 alles auscheckt.

Ich bin mir nicht sicher, was der beste Weg, um das zu beheben ist. Vielleicht kann ich die Entbindung von Data.Constraint verwenden, oder vielleicht gibt es einen Trick mit höheren Rangarten.

Irgendwelche Ideen?

Answer 1

Das Problem ist, dass Sie den endgültigen Ergebnistyp korrigieren, so dass die Instanz existiert und der Typprüfer sie finden kann.

Versuchen Sie so etwas wie:

run :: GADT e a -> e 

nun der Ergebnistyp der Instanz für review nicht auswählen können und Parametrizität erzwingt Ihre invariant.