제한된 제약 조건을 GADT와 함께 사용하려면 어떻게해야합니까?

Question

나는 다음과 같은 코드를 가지고 있고, 이 유형 검사를 실패에 나는 이것을 싶습니다

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

아이디어는 GADT의 각 항목은 내가 Prism로 모델링하고있어 관련 오류를 가지고 있다는 것입니다 좀 더 큰 구조. 이 GADT를 "해석"할 때 e에 대한 구체 유형을 제공하며이 유형은 모두 Prism에 대한 인스턴스를 갖습니다. 그러나 각 개별 사례에 대해 생성자의 관련 컨텍스트에서 선언되지 않은 인스턴스를 사용할 수 있기를 원하지 않습니다.

Two에서 패턴 일치가 발생하면 Increment e 만 사용할 수 있지만 Greet을 사용하고 있기 때문에 위의 코드는 오류가되어야합니다. 이유가 무엇인지 알 수 있습니다. Either String Int에 Greet에 대한 인스턴스가 있으므로 모든 것이 체크 아웃됩니다.

이 문제를 해결하는 가장 좋은 방법은 무엇인지 모르겠습니다. 어쩌면 Data.Constraint의 함부로 사용하거나 더 높은 순위 유형의 트릭이있을 수 있습니다.

아이디어가 있으십니까?

Answer 1

최종 결과 유형이 수정되어 인스턴스가 존재하고 유형 검사기가이를 찾을 수 있습니다. 이제 결과 유형은 review의 인스턴스를 선택할 수 없습니다

run :: GADT e a -> e 

및 parametricity은 불변을 적용 :

같은 것을보십시오.