小编xuh*_*xuh的帖子

(我不完全熟悉Haskell约束求解器的内部工作原理,所以这可能是一个新手问题.)

尝试在GHC 8.0.1上使用类型应用程序时,如以下示例代码所示

{-# LANGUAGE KindSignatures, RankNTypes, ConstraintKinds, ScopedTypeVariables, TypeApplications #-}
module Test where

import Data.Constraint

test0 :: forall (b :: *) . (forall a . a -> Bool) -> b -> Bool
test0 g = g @b

test1 :: forall (c :: * -> Constraint) (b :: *) . (c b) => (forall a . c a => a -> Bool) -> b -> Bool
test1 g = g @b

它给了我以下错误

• Could not deduce: c0 b
  from the …

在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 …