我在让 GHC 在一个应该很明显的地方推断出一个类型时遇到了问题。以下是演示问题的完整片段。
{-# LANGUAGE DataKinds, ScopedTypeVariables, KindSignatures, TypeOperators, GADTs #-}
import Data.Reflection
import Data.Proxy
import Data.Tagged
-- heterogeneous list, wrapping kind [*] as *
data HList :: [*] -> * where
HNil :: HList '[]
HCons :: a -> HList as -> HList (a ': as)
main = test2
test1 = do
let x = HCons 3 HNil :: HList '[Int]
c = case x of (HCons w HNil) -> w
print c
test2 = reify True (\(_::Proxy a) -> do
let x = HCons (Tagged 3) HNil :: HList '[Tagged a Int]
c = case x of (HCons w HNil) -> w
print $ untag (c :: Tagged a Int))
在中,正如我所期望的那样,我可以在不给出明确类型的情况下进行test1
打印。的类型由 : 上的显式签名推断,即has type中的第一个元素。c
c
c
x
HList
Int
然而test2
,在 中,c
需要显式签名。如果我只是print $ untag c
在test2
,我得到
Test.hs:22:32:
Couldn't match type `s0' with `s'
`s0' is untouchable
inside the constraints (as ~ '[] *)
bound at a pattern with constructor
HNil :: HList ('[] *),
in a case alternative
`s' is a rigid type variable bound by
a type expected by the context:
Reifies * s Bool => Proxy * s -> IO ()
at Test.hs:19:9
Expected type: Tagged * s0 Int
Actual type: a
In the pattern: HNil
In the pattern: HCons w HNil
In a case alternative: (HCons w HNil) -> w
为什么 GHC 不能从给定的显式类型推断出c
类型?x
test1