1

玩弄 GHC.TypeLits 我做了这段代码

data A (a :: Symbol) = A
type B a (b :: Symbol) (c :: Symbol) = A a

class AC a where
  af :: (String, a)

-- instance SingI a => AC (A a) where
--   af = (fromSing (sing :: Sing a), A)

instance (SingI a, SingI b, SingI c) => AC (B a b c) where
  af = (fromSing (sing :: Sing c), A)

如果我尝试在某个地方调用 af 并出现此错误，则无法编译：

No instance for (SingI Symbol c) arising from a use of `af'
Possible fix: add an instance declaration for (SingI Symbol c)
In the second argument of `($)', namely
  `(af :: (String, B "a" "b" "c"))'
In the second argument of `($)', namely
  `fst $ (af :: (String, B "a" "b" "c"))'
In a stmt of a 'do' block:
  print $ fst $ (af :: (String, B "a" "b" "c"))

它仍然可以正常工作，instance SingI a => AC (A a)因为很明显它是类型同义词，但我找不到任何解释。很高兴听到它为什么会这样工作，并且有没有机会添加一些标签之王来键入同义词？

扩展，用于编译：

  DataKinds,
  KindSignatures,
  TypeSynonymInstances,
  ScopedTypeVariables,
  -- MultiParamTypeClasses,
  UndecidableInstances
4

1 回答 1

1

来自 GHC 用户指南，第7.6.3.1 节。实例头的宽松规则：

使用 -XTypeSynonymInstances 标志，实例头可以使用类型同义词。与往常一样，使用类型同义词只是编写类型同义词定义的 RHS 的简写。

将此规则应用于您的实例声明会导致：

instance (SingI a, SingI b, SingI c) => AC (A a) where
  af = (fromSing (sing :: Sing c), A)

请注意，这等于您为“A”编写的实例，但在cand上有约束b，现在甚至不会出现在实例头中。当您尝试使用该实例时：

print $ fst $ (af :: (String, B "a" "b" "c"))

这被转化为

print $ fst $ (af :: (String, A "a"))

并且编译器抱怨没有instance for SingI Symbol c，因为它不知道是什么c。要编译此代码，您必须提供一个instance SingI (c :: Symbol)适用于所有 c的代码（您可以使用 编写这样的实例FlexibleInstances，但它不会有用，因为您无法根据 做出选择c）。如果您不想要这种行为，您可以使用新类型。

于 2013-09-17T13:40:11.777 回答