具有类型族的不明确类型

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无法产生正确结果的案例吗？

任何帮助赞赏!

注意:ScopedTypeVariables显式类型签名似乎没有帮助.添加约束a ~ Foo t并使用a替代作为gin 的类型Foobar g也不起作用.

看起来很像:使用类型系列时出现模糊类型错误,而STV没有帮助.我考虑使用a Proxy,但我觉得在这种情况下GHC应该能够弄明白.

Answer 1

据我所知,Foo不是射,而是从我的分析是GHC从来没有要求拿出t的Foo 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 twhere t与f实例的索引相同.但是,这还不足以选择一个实例g!实际上,我们可能会Foo t ~ Foo t0为其他一些人t0,因此g可能g在t0实例中引用,导致模糊错误.

请注意,即使最后一行被注释掉,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中,您需要一个代理才能明确地选择实例.