haskell - GHC 无法使用 GADT 和箭头确定类型相等性

Question

我无法让 GHC 注意到箭头表达式中的两种类型相等。

data PolyList a where
    Nil :: PolyList '[]
    Cons :: a -> PolyList as -> PolyList (a ': as)

class Recurse a where
    method :: PolyList a -> String

instance Recurse '[] where
    method _ = ""

instance (Show a, Recurse as) => Recurse (a ': as) where
    method = proc input -> case input of
        (Cons a as) -> do
            rest <- method -< as --Could not deduce (Recurse as)
            returnA -< show a ++ rest

    method = proc input -> case input of
        (Cons a as) -> do
            rest <- method -< as :: PolyList as --Works fine
            returnA -< show a ++ rest

    method (Cons a as) =
            let rest = method as --Also works
            in show a ++ rest

完整的错误是：

Could not deduce (Recurse as) arising from a use of `method'
from the context (Show a, Recurse as1)
  bound by the instance declaration
Possible fix:
  add (Recurse as) to the context of the instance declaration

为什么它不能告诉它as已经有类型PolyList as？

编辑：这最终还是有点没用，因为修复似乎触发了ghc #344，但仍未解决。最好知道问题出在哪里。