haskell - 非法嵌套类型族应用程序(使用 UndecidableInstances 允许这样做)

Question

在 GHC 8.0.1 中，我尝试为类型级列表实现类型级 Length 函数。它编译:

{-# LANGUAGE DataKinds, TypeOperators, TypeFamilies #-}

data Nat = Z | S Nat

type family Length (l :: [*]) :: Nat where
    Length '[] = Z
    Length (_ ': as) = S (Length as)    

但是如果我使用 TypeLits，它不会编译:

import GHC.TypeLits

type family Length (l :: [*]) :: Nat where
    Length '[] = 0
    Length (_ ': as) = 1 + Length as

编译器给出以下错误:

• Illegal nested type family application ‘1 + Length as’
  (Use UndecidableInstances to permit this)
• In the equations for closed type family ‘Length1’
  In the type family declaration for ‘Length1’

Answer 1

您需要打开 UndecideableInstances 。此扩展解除了一系列限制，这些限制的存在确保编译始终终止。其中之一与类型族有关。在第一个示例中，RHS 上的外部术语是实际类型，而不是对类型函数的另一次调用。另一方面，在第二个示例中，RHS 完全是对类型函数 (+) 的调用(不要与同名的值级别函数混淆)。

GHC 会提示，因为它无法判断您编写的内容是否会终止。事实上，它的细微变化不会:

type family Length (l :: [*]) :: Nat where
    Length '[] = 0
    Length (a ': as) = 1 + Length (a ': as)