Jak korzystać z ograniczonych ograniczeń z GADT?

Question

Mam następujący kod, i chciałbym to nie typu sprawdzanie:

{-# 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" 

Chodzi o to, że każdy wpis w GADT jest skojarzony błąd, który ja modelowania z Prism do trochę większa struktura. Kiedy "interpretuję" ten GADT, zapewniam konkretny typ dla e, który ma instancje dla wszystkich tych Prism s. Jednak dla każdego pojedynczego przypadku nie chcę móc używać instancji, które nie zostały zadeklarowane w kontekście powiązanym z konstruktorem.

Powyższy kod powinien być błędem, ponieważ kiedy dopasowuję wzór na Two powinienem nauczyć się, że mogę używać tylko Increment e, ale używam Greet. Rozumiem, dlaczego to działa - Either String Int ma instancję dla Greet, więc wszystko się zgadza.

Nie jestem pewien, jak najlepiej to naprawić. Może mogę użyć polecenia z Data.Constraint, lub może jest sztuczka z wyższymi typami rang.

Wszelkie pomysły?

Answer 1

Problem polega na tym, że poprawiamy końcowy typ wyniku, więc instancja istnieje i narzędzie sprawdzania typu może je znaleźć.

Spróbuj czegoś takiego:

run :: GADT e a -> e 

Teraz typ wynik nie może odebrać instancję dla review i parametricity egzekwuje swoją niezmienna.