[解決済み】-XAllowAmbiguousTypesはいつが適切ですか？

質問

私は最近 質問 について 構文2.0 の定義について share . で動作させたことがあります。 GHC 7.6 :

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

のファンデプが暗示する型である。 SyntacticN . これによって、拡張子を避けることができるんだ。もちろん、これは

• すでに大きな署名に追加するための非常に長い型
• 手動で導出するのが面倒
• ファンデのため不要

質問です。

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 はこれらの正確な型名を使っているので、ここでは コミット 8cfd02^ の開発ブランチです。 この名前を使用していた最後のバージョンです。

では、なぜ GHC は fi の型署名はそうですが sugarSym ? リンク先のドキュメントでは、制約が関数従属性を使って他の曖昧でない型から曖昧な型を推論していない限り、制約の右側に表示されない型は曖昧であると説明されています。そこで、2つの関数のコンテキストを比較し、機能依存性を探してみましょう。

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 . まず最初に気がつくのは、コンパイラが ではなく は、曖昧な型についてではなく、重複するインスタンスについて文句を言っています。

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に曖昧さチェックをしないように言えば、そのような別の問題には遭遇しなかったということなのです。これが、AllowAmbiguousTypesを有効にすることであなたのコードがコンパイルできるようになる理由の説明です。

しかし、インスタンスが重複している問題は残ります。GHCがリストアップした2つのインスタンス( 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はもうオーバーラップについて文句を言いません。

私があなたなら、次のように考えます。 これらの2つの可能なインスタンスの定義 で、その2つの実装のうち1つが欲しいものであるかどうかを判断します。