使用 GADT 进行类型推断

Question

在下面的代码中，我试图匹配 GADT 构造函数 Cons 以让编译器看到 xs 是非空的：

{-# LANGUAGE DataKinds           #-} 
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE KindSignatures      #-} 
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators       #-}

import Data.Typeable

data Foo (ts :: [*]) where
  Nil :: Foo '[]
  Cons :: (Typeable t) => Foo ts -> Foo ( t ': ts)

foo :: Foo xs -> IO ()
foo Nil = print "done"
foo (Cons rest :: Foo (y ': ys)) = do
  print $ show $ typeRep (Proxy::Proxy y)
  foo rest

很遗憾，这个简单的示例无法使用 GHC 8 进行编译：

• Couldn't match type ‘xs’ with ‘y : ys’
  ‘xs’ is a rigid type variable bound by
    the type signature for:
      foo :: forall (xs :: [*]). Foo xs -> IO ()
  Expected type: Foo (y : ys)
    Actual type: Foo xs
• When checking that the pattern signature: Foo (y : ys)
    fits the type of its context: Foo xs
  In the pattern: Cons rest :: Foo (y : ys)
  In an equation for ‘foo’:
      foo (Cons rest :: Foo (y : ys))
        = print $ (show $ typeRep (Proxy :: Proxy y))

我知道使用 GADT 进行类型推断可能会很棘手（例如，#9695、#10195、#10338），但这如此很简单...

我需要做些什么来让 GHC 相信，当我在 Cons 上匹配时，GADT 参数至少有一个元素？

Answer 1

您只需要一个从Foo (t ': ts) 中提取Proxy t 的函数：

fooFstType :: Foo (t ': ts) -> Proxy t 
fooFstType _ = Proxy 

请注意，由于Foo 的类型参数是t ': ts，而不仅仅是ts，您可以引用表示类型签名中第一个元素的类型变量（而不是在正文中，不知何故， ScopedTypeVariables)。

你的函数变成了

foo :: Foo xs -> IO ()
foo Nil = print "done"
foo f@(Cons rest) = do
  print $ show $ typeRep (fooFstType f)
  foo rest

另一种可能性是将作品移到类型级别：

type family First (xs :: [k]) :: k where 
  First (x ': xs) = x 

foo :: forall xs . Foo xs -> IO ()
foo Nil = print "done"
foo (Cons rest) = do
  print $ show $ typeRep (Proxy :: Proxy (First xs))
  foo rest