非法嵌套类型系列应用程序(使用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)