6

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?

5
  • for what it's worth, the older-style data HCons a b = HCons a b data HNil = HNil doesn't have this problem.
    – aavogt
    Sep 10, 2013 at 6:37
  • 3
    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 Sep 10, 2013 at 6:38
  • @NathanHowell: Interesting, and very annoying.
    – crockeea
    Sep 10, 2013 at 13:43
  • @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. Sep 10, 2013 at 15:14
  • @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.
    – crockeea
    Sep 12, 2013 at 17:08

1 Answer 1

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.