-XAllowAmbiguousTypes는 언제 적절한가요?

-XAllowAmbiguousTypes는 언제 적절한가요?

---

최근 에의 정의와 관련하여 syntactic-2.0 에 대한 질문을 게시했습니다 . GHC 7.6 에서이 작업을 수행했습니다 .share

{-# LANGUAGE GADTs, TypeOperators, FlexibleContexts #-}

import Data.Syntactic
import Data.Syntactic.Sugar.BindingT

data Let a where
    Let :: Let (a :-> (a -> b) :-> Full b)

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
share = sugarSym Let

그러나 GHC 7.8은 -XAllowAmbiguousTypes해당 서명으로 컴파일 하려고 합니다. 다른 방법 fi으로

(ASTF sup (Internal a) -> AST sup ((Internal a) :-> Full (Internal b)) -> ASTF sup (Internal b))

에 Fundep이 암시하는 유형입니다 SyntacticN. 이렇게하면 확장을 피할 수 있습니다. 물론 이것은

• 이미 큰 서명에 추가 할 수있는 매우 긴 유형
• 수동으로 유도하기에 귀찮음
• Fundep로 인해 불필요

내 질문은 :

1. 이 사용이 허용 -XAllowAmbiguousTypes됩니까?
2. 일반적으로이 확장은 언제 사용해야합니까? 여기에 대한 대답 은 "거의 결코 좋은 생각이 아닙니다"를 암시합니다.

3. 문서를 읽었지만 제약 조건이 모호한 지 여부를 결정하는 데 여전히 문제가 있습니다. 특히, Data.Syntactic.Sugar에서이 기능을 고려하십시오.

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

   나에게 fi(그리고 가능하면 sup) 모호 해야하는 것처럼 보이지만 확장명없이 컴파일됩니다. 왜 sugarSym모호하지 share않은가? 이후 share의 응용 프로그램 sugarSym의 share제약 조건은 모든 직선에서 온 sugarSym.

---

서명에 sugarSym정확한 유형 이름 을 사용하는 공개 버전의 구문이 표시되지 않으므로 해당 이름을 사용한 마지막 버전 인 commit 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

So for sugarSym, the non-ambiguous types are sub, sig and f, and from those we should be able to follow functional dependencies in order to disambiguate all the other types used in the context, namely sup and fi. And indeed, the f -> internal functional dependency in SyntacticN uses our f to disambiguate our fi, and thereafter the f -> sig sym functional dependency in ApplySym uses our newly-disambiguated fi to disambiguate sup (and sig, which was already non-ambiguous). So that explains why sugarSym doesn't require the AllowAmbiguousTypes extension.

Let's now look at sugar. The first thing I notice is that the compiler is not complaining about an ambiguous type, but rather, about overlapping instances:

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

So if I'm reading this right, it's not that GHC thinks that your types are ambiguous, but rather, that while checking whether your types are ambiguous, GHC encountered a different, separate problem. It's then telling you that if you told GHC not to perform the ambiguity check, it would not have encountered that separate problem. This explains why enabling AllowAmbiguousTypes allows your code to compile.

However, the problem with the overlapping instances remain. The two instances listed by GHC (SyntacticN f fi and SyntacticN (a -> f) ...) do overlap with each other. Strangely enough, it seems like the first of these should overlap with any other instance, which is suspicious. And what does [overlap ok] mean?

I suspect that Syntactic is compiled with OverlappingInstances. And looking at the code, indeed it does.

Experimenting a bit, it seems that GHC is okay with overlapping instances when it is clear that one is strictly more general than the other:

{-# 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])

But GHC is not okay with overlapping instances when neither is clearly a better fit than the other:

{-# 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])

Your type signature uses SyntacticN (a -> (a -> b) -> b) fi, and neither SyntacticN f fi nor SyntacticN (a -> f) (AST sym (Full ia) -> fi) is a better fit than the other. If I change that part of your type signature to SyntacticN a fi or SyntacticN (a -> (a -> b) -> b) (AST sym (Full ia) -> fi), GHC no longer complains about the overlap.

If I were you, I would look at the definition of those two possible instances and determine whether one of those two implementations is the one you want.

---

I've discovered that AllowAmbiguousTypes is very convenient for use with TypeApplications. Consider the function natVal :: forall n proxy . KnownNat n => proxy n -> Integer from GHC.TypeLits.

To use this function, I could write natVal (Proxy::Proxy5). An alternate style is to use TypeApplications: natVal @5 Proxy. The type of Proxy is inferred by the type application, and it's annoying to have to write it every time you call natVal. Thus we can enable AmbiguousTypes and write:

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

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

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

However, note that once you go ambiguous, you can't go back!

참고URL : https://stackoverflow.com/questions/23684947/when-is-xallowambiguoustypes-appropriate