Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Type Inference with Reflection and DataKinds

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?

like image 971
crockeea Avatar asked Sep 10 '13 03:09

crockeea


1 Answers

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
like image 138
Nathan Howell Avatar answered Sep 23 '22 13:09

Nathan Howell