类型类方法与独立函数中的范围类型变量

Question

这是一个简短的例子.我想知道为什么在TypeClass示例中我没有明确说明,forall而在函数定义中没有forall它无法编译:

Couldn't match kind ‘Nat’ with ‘*’
    When matching types
      proxy0 :: Nat -> *
      Proxy :: * -> *
    Expected type: proxy0 n0
      Actual type: Proxy p0
    In the first argument of ‘natVal’, namely ‘(Proxy :: Proxy p)’
    In the second argument of ‘($)’, namely ‘natVal (Proxy :: Proxy p)’
    In the first argument of ‘(++)’, namely
      ‘(show $ natVal (Proxy :: Proxy p))’

码:

{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE KindSignatures      #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE RoleAnnotations     #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators       #-}
{-# LANGUAGE TypeFamilies        #-}

data Container (p :: Nat) (k :: Nat) = Container { first :: [Int], second :: [Int] }

instance (KnownNat p, KnownNat k) => Show (Container p k) where
  show c  = "Container " ++ (show $ natVal (Proxy :: Proxy p)) ++ 
                     " " ++ (show $ natVal (Proxy :: Proxy k))

showMe :: forall p k . (KnownNat p, KnownNat k) => Container p k -> String
showMe c = "Container " ++ (show $ natVal (Proxy :: Proxy p)) ++ 
                    " " ++ (show $ natVal (Proxy :: Proxy k))

Answer 1

ScopedTypeVariables将实例头中的类型变量引入实例主体中的范围而不显式forall.类型签名不会发生这种情况; 相反,你必须使用forall带入p和k定义的范围showMe.