All geek questions in one place

Type inference with reflection and DataKinds

I'm having trouble getting GHC to type in the place where this should be obvious. The following 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 specifying c and an explicit type, as I expected. Type c is inferred by an explicit signature on x , namely, the first element in the HList is of type Int .

In test2 , however, explicit signature on c is required. If I just 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't GHC deduce type c from an explicit type specified in x , like in test1 ?

+6
source share
1 answer

I found that these errors are related to let-bindings ... although I don’t know the exact cause or if it really is a bug in the GHC. The workaround is to use the 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
+1
source

Source: https://habr.com/ru/post/953530/

More articles:


All Articles