タイプファミリを持つあいまいなタイプ

Question

GHCがFoo tとFoo t0と一致することができない問題に遭遇しています。それは間違いなくt ~ t0のように見えます。ここでは、最小限の例です：最後の行をコメントアウトすると

{-# LANGUAGE GADTs   #-} 
{-# LANGUAGE KindSignatures #-} 
{-# LANGUAGE TypeFamilies #-} 

data Foobar :: * -> * where 
    Foobar :: Foo t -> Foobar t 

type family Foo a :: * 

class Bar t where 
    f :: Foobar t 
    g :: Foo t 
-- f = Foobar g 

、GHCは文句：

Couldn't match expected type ‘Foo t’ with actual type ‘Foo t0’ 
NB: ‘Foo’ is a type function, and may not be injective 
The type variable ‘t0’ is ambiguous 
Relevant bindings include f :: Foobar t (bound at test.hs:13:3) 
In the first argument of ‘Foobar’, namely ‘g’ 
In the expression: Foobar g 

私はFooが単射ではないことを理解し、私の分析からGHCからtを思い付くように頼まれることはありませんFoo t。タイプtはFoobar gで失われているため、本来のFoo tと新しいFoo t0には一致しません。ここでのコンテキストは十分ではないのですか？ f = Foobar gが正しい結果を得られない場合がありますか？

N.B .: ScopedTypeVariablesと明示的なタイプシグネチャは役立たないようです。 a ~ Foo tという制約を追加し、代わりにgのタイプとしてaを使用すると、Foobar gにも機能しません。

多くのように見えます。ambiguous type error when using type families, and STV is not helping。私はProxyを使うと考えましたが、この場合、GHCはそれを理解できるはずです。

Answer 1

私はFooが単射ではないことを理解し、私の分析からGHCがFoo tからtを思い付くように頼まれることはありません。

したがって、あなたはあいまいさを認識します。さんが作ろうと、明示的である：f = Foobar gで

type instance Foo() = Bool 
type instance Foo Char = Bool 

instance Bar() where 
    -- I omit the declaration for f 
    g = True 
instance Bar Char where 
    g = False 

main = print (g :: Bool) 

あなたの問題を曖昧に関連しています。

要点：f = Foobar gの定義は、gがfと同じインスタンスで選択されることを意味しません。それは別のインスタンスを参照することができます！

が上記

show (x,y) = "(" ++ show x ++ ", " ++ show y ++ ")" 

を考慮し、RHSはshowの使用は、LHS showがあるものとは異なるインスタンスからです。

f = Foobar g行では、g :: Foo tとなります。ここで、tはfインスタンスと同じインデックスです。ただし、gのインスタンスを選択するだけでは不十分です。実際には、t0にはFoo t ~ Foo t0がある可能性があります。したがって、gは、t0インスタンス内のgを参照する可能性があり、あいまいなエラーが発生します。

あなたのコードがgのタイプは本質的に曖昧であるため、最後の行は、コメントアウトされている場合でもGHC 8によってを拒否されることに注意してください：

• Couldn't match expected type ‘Foo t’ with actual type ‘Foo t0’ 
    NB: ‘Foo’ is a type function, and may not be injective 
    The type variable ‘t0’ is ambiguous 
• In the ambiguity check for ‘g’ 
    To defer the ambiguity check to use sites, enable AllowAmbiguousTypes 
    When checking the class method: g :: forall t. Bar t => Foo t 
    In the class declaration for ‘Bar’ 

我々はGHC 8以上を作るための提案に従うことができますGHC 7のように寛大ではありません。これにより、最後の行のコメントを解除するまで、コードタイプのチェックが行われます。

• Couldn't match expected type ‘Foo t’ with actual type ‘Foo t0’ 
     NB: ‘Foo’ is a type function, and may not be injective 
     The type variable ‘t0’ is ambiguous 

これは、あなたがGHC 8でGHC 7 で見た同じエラーがあり、我々は別の贅沢を持って次のように私たちは明示的がgためtを選択することができます。

class Bar t where 
    f :: Foobar t 
    f = Foobar (g @ t) 
    g :: Foo t 

はこれが必要ですもちろん、いくつかの拡張機能をオンにする必要があります。 GHC 7では、インスタンスを明白に選択できるようにプロキシが必要です。