無効なネスト型ファミリアプリケーション（これを許可するには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。この拡張機能は、コンパイルが常に終了することを保証する一連の制限を解除します。これらのうちの1つはタイプファミリーと関係しています。あなたの最初の例では、RHSの外側の項は実際の型であり、型関数への別の呼び出しではありません。一方、2番目の例では、RHSは完全に型関数(+)（同じ名前の値レベル関数と誤解されてはいけません）への呼び出しです。

GHCは、あなたが書いたことを終わらせることができないので文句を言う。実際には、それほど変わっていません。

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