I'm having problems getting GHC to infer a type in a place where it should be obvious. Below is a complete snippet demonstrating the problem.
{-# 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))
In test1
, I can print c
without giving c
and explicit type, just as I expect. The type of c
is inferred by the explicit signature on x
: namely, the first element in the HList
has type Int
.
In test2
, however, the explicit signature on c
is required. If I simply print $ untag c
in test2
, I get
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
Why can GHC not infer the type of c
from the explicit type given to x
as in test1
?
I've found these errors to be related to let-bindings... though I don't know the precise cause or if it's actually bug in GHC. The workaround is to use a case statement instead:
test4 = reify True $ \ (_::Proxy a) -> do
let x = HCons (Tagged 4) HNil :: HList '[Tagged a Int]
c = case x of (HCons w HNil) -> w
print $ untag (c :: Tagged a Int)
test5 = reify True $ \ (_::Proxy a) -> do
case HCons (Tagged 5) HNil :: HList '[Tagged a Int] of
HCons w HNil -> print $ untag w
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With