[haskell] -XAllowAmbiguousTypes는 언제 적절한가요?

서명에 sugarSym정확한 유형 이름 을 사용하는 게시 된 구문 버전이 표시되지 않으므로 커밋 8cfd02 ^에서 개발 브랜치를 사용합니다.

그렇다면 왜 GHC가 fi타입 시그너처에 대해 불평 하지만 왜 시그니처에 대해 불평하지 sugarSym않습니까? 연결 한 문서는 제약 조건이 기능적 종속성을 사용하여 다른 모호하지 않은 유형에서 다른 모호하지 않은 유형을 유추하지 않는 한 유형이 제약 조건의 오른쪽에 나타나지 않으면 모호하다는 것을 설명합니다. 두 함수의 컨텍스트를 비교하고 함수 종속성을 찾으십시오.

class ApplySym sig f sym | sig sym -> f, f -> sig sym
class SyntacticN f internal | f -> internal

sugarSym :: ( sub :<: AST sup
            , ApplySym sig fi sup
            , SyntacticN f fi
            )
         => sub sig -> f

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

그래서 대한 sugarSym비 모호한 유형은 sub, sig와 f, 그에서 우리는 즉, 문맥에서 사용되는 모든 다른 유형을 명확하게하기 위해 함수 종속을 수행 할 수 있어야 sup하고 fi. 실제로, f -> internal기능적 의존성 SyntacticN은 우리 f를 명확하게하기 위해 사용하고 fi, 그 후에 f -> sig sym기능적으로 의존하는 것은 ApplySym명확하게 명확하게 fi하기 위해 새로 명확 하게 sup(그리고 sig이미 모호하지 않은) 사용합니다. 따라서 확장이 sugarSym필요없는 이유를 설명합니다 AllowAmbiguousTypes.

이제 보자 sugar. 가장 먼저하는 일의 I 통지 컴파일러가된다는 점이다 없는 경우 중복에 대해 다소 모호한 유형에 대해 불평하지만 :

Overlapping instances for SyntacticN b fi
  arising from the ambiguity check for ‘share’
Matching givens (or their superclasses):
  (SyntacticN (a -> (a -> b) -> b) fi1)
Matching instances:
  instance [overlap ok] (Syntactic f, Domain f ~ sym,
                         fi ~ AST sym (Full (Internal f))) =>
                        SyntacticN f fi
    -- Defined in ‘Data.Syntactic.Sugar’
  instance [overlap ok] (Syntactic a, Domain a ~ sym,
                         ia ~ Internal a, SyntacticN f fi) =>
                        SyntacticN (a -> f) (AST sym (Full ia) -> fi)
    -- Defined in ‘Data.Syntactic.Sugar’
(The choice depends on the instantiation of ‘b, fi’)
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes

따라서이 권리를 읽고 있다면 GHC가 유형이 모호하다고 생각하는 것이 아니라 유형이 모호한 지 여부를 확인하는 동안 GHC가 다른 별도의 문제를 겪었다는 것입니다. 그런 다음 GHC에 모호성 검사를 수행하지 말라고 지시하면 별도의 문제가 발생하지 않았을 것입니다. 이것은 AllowAmbiguousTypes를 활성화하면 코드를 컴파일 할 수있는 이유를 설명합니다.

그러나 겹치는 인스턴스의 문제는 남아 있습니다. GHC ( SyntacticN f fi및 SyntacticN (a -> f) ...)로 나열된 두 인스턴스 는 서로 겹칩니다. 이상하게도, 첫 번째 인스턴스는 다른 인스턴스와 겹치는 것처럼 보입니다. 그리고 무슨 [overlap ok]뜻입니까?

Syntactic이 OverlappingInstances로 컴파일 된 것 같습니다. 그리고 실제로 코드를 살펴보십시오 .

조금 실험 해보면, GHC가 하나가 다른 것보다 더 일반적이라는 것이 분명 할 때 겹치는 경우에 괜찮은 것 같습니다.

{-# LANGUAGE FlexibleInstances, OverlappingInstances #-}

class Foo a where
  whichOne :: a -> String

instance Foo a where
  whichOne _ = "a"

instance Foo [a] where
  whichOne _ = "[a]"

-- |
-- >>> main
-- [a]
main :: IO ()
main = putStrLn $ whichOne (undefined :: [Int])

그러나 GHC는 다른 인스턴스보다 명확하게 더 잘 맞지 않을 때 겹치는 인스턴스에는 적합하지 않습니다.

{-# LANGUAGE FlexibleInstances, OverlappingInstances #-}

class Foo a where
  whichOne :: a -> String

instance Foo (f Int) where  -- this is the line which changed
  whichOne _ = "f Int"

instance Foo [a] where
  whichOne _ = "[a]"

-- |
-- >>> main
-- Error: Overlapping instances for Foo [Int]
main :: IO ()
main = putStrLn $ whichOne (undefined :: [Int])

귀하의 유형 서명 사용 SyntacticN (a -> (a -> b) -> b) fi, 어느 쪽도 아니 SyntacticN f fi도는 SyntacticN (a -> f) (AST sym (Full ia) -> fi)다른 것보다 더 적합하다. 유형 서명의 해당 부분을 SyntacticN a fi또는로 변경 SyntacticN (a -> (a -> b) -> b) (AST sym (Full ia) -> fi)하면 GHC는 더 이상 중복에 대해 불평하지 않습니다.

내가 당신이라면, 가능한 두 인스턴스의 정의를 보고 그 두 구현 중 하나가 당신이 원하는 것인지 결정합니다.

답변

{-# Language AllowAmbiguousTypes, ScopedTypeVariables, TypeApplications #-}

ambiguousNatVal :: forall n . (KnownNat n) => Integer
ambiguousNatVal = natVal @n Proxy

five = ambiguousNatVal @5 -- no `Proxy ` needed!