曖昧類型與家族類型

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，所以它不能匹配inital Foo t和新的Foo t0。這裏的背景是不夠的嗎？我是否錯過f = Foobar g無法產生正確結果的情況？

任何幫助表示讚賞！

N.B .: ScopedTypeVariables和顯式類型簽名似乎沒有幫助。添加約束條件a ~ Foo t並使用a而不是Foobar g中的g類型也不起作用。

看起來很像：ambiguous type error when using type families, and STV is not helping。我考慮使用Proxy，但我覺得在這種情況下，GHC應該能夠弄清楚。

Answer 1

我明白Foo不射，但是從我的分析是GHC從來沒有要求從Foo t拿出t。

因此，你意識到模糊性。讓我們爲明確：

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問題與不確定性。

關鍵是：定義f = Foobar g並不意味着g在f相同的實例中被挑選出來。它可以指代一個不同的實例！

考慮

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

上面，RHS的show使用是從一個在LHS show是不同的實例。

在您的f = Foobar g一行中，GHC推斷g :: Foo t其中t與f實例的索引相同。但是，這不足以爲g選擇一個實例！的確，我們可能有Foo t ~ Foo t0對於其他一些t0，因此g可能引用t0實例中的g，從而導致模糊性錯誤。

請注意，你的代碼是由GHC 8，即使最後一行被註釋掉拒絕，因爲g類型本質上是不明確的：

• 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 7 看到GHC 8相同的錯誤，我們有另一種奢侈的：我們可以明確地選擇的t爲g如下：

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

這需要當然，還有幾個擴展需要打開。在GHC 7中，您需要一個代理才能夠明確地選擇一個實例。