Type Inference with Reflection and DataKinds

Question

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?

Joselow

for what it's worth, the older-style data HCons a b = HCons a b data HNil = HNil doesn't have this problem. – Interpolate

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: gist.github.com/NathanHowell/39748c25999548fe56ac – Musketry

@NathanHowell: Interesting, and very annoying. – Joselow

@Eric: I agree. I understand why this happens with GADTs or ExistentialQuantification when they're introducing new type variables into scope... this doesn't though and seems like it should work. Hopefully someone chimes in. – Musketry

@NathanHowell: This post isn't attracting much attention it seems. If you write your comment up and include the code in an answer, I'll accept it. – Joselow

Answer 1

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

Musketry