시나리오는 다음과 같습니다. 유형 서명으로 일부 코드를 작성했으며 GHC는 일부 x및에 대해 x ~ y를 추론 할 수 없다고 불평 y합니다. 일반적으로 GHC에 뼈를 던지고 단순히 함수 제약 조건에 동형을 추가 할 수는 있지만 몇 가지 이유로 나쁜 생각입니다.

1. 코드 이해를 강조하지 않습니다.
2. 하나가 충분할 경우 5 개의 제약 조건으로 끝날 수 있습니다 (예 : 5가 하나 이상의 특정 제약 조건에 의해 암시되는 경우)
3. 뭔가 잘못했거나 GHC가 도움이되지 않으면 가짜 제약 조건이 생길 수 있습니다

방금 사례 3과 싸우는 데 몇 시간을 보냈습니다.에 대해 놀고 있으며 syntactic-2.0에 정의 된 버전과 share유사한 도메인 독립적 버전을 정의하려고 했습니다 NanoFeldspar.hs.

나는 이것을 가지고 있었다 :

{-# LANGUAGE GADTs, FlexibleContexts, TypeOperators #-}
import Data.Syntactic

-- Based on NanoFeldspar.hs
data Let a where
    Let :: Let (a :-> (a -> b) :-> Full b)

share :: (Let :<: sup,
          Domain a ~ sup,
          Domain b ~ sup,
          SyntacticN (a -> (a -> b) -> b) fi) 
      => a -> (a -> b) -> a
share = sugarSym Let

그리고 GHC could not deduce (Internal a) ~ (Internal b), 확실히 내가 가고있는 것이 아닙니다. 그래서 내가 의도하지 않은 코드를 작성했거나 (제약이 필요함) GHC는 내가 작성한 다른 제약으로 인해 그 제약을 원했습니다.

(Syntactic a, Syntactic b, Syntactic (a->b))제약 목록 에 추가해야한다는 것이 밝혀졌습니다 (Internal a) ~ (Internal b). 나는 기본적으로 올바른 제약 조건을 우연히 발견했습니다. 나는 여전히 체계적인 방법으로 찾을 수 없습니다.

내 질문은 :

1. GHC가 그 제약을 제안한 이유는 무엇입니까? 구문상의 어느 것도 제약 Internal a ~ Internal b이 없으므로 GHC는 어디서 그것을 끌어 냈습니까?
2. 일반적으로 GHC가 필요하다고 생각하는 제약의 기원을 추적하기 위해 어떤 기술을 사용할 수 있습니까? 내가 발견 할 수있는 제약 조건조차도 내 접근 방식은 본질적으로 재귀 제약 조건을 실제로 작성하여 문제의 경로를 강요하는 것입니다. 이 접근법은 기본적으로 무한한 토끼 구멍을 뚫고 나가는 가장 효율적인 방법에 관한 것입니다.

답변

share :: (Let :<: sup,
          Domain a ~ sup,
          Domain b ~ sup,
          SyntacticN (a -> (a -> b) -> b) fi,
          _) 
      => a -> (a -> b) -> a
share = sugarSym Let