6

明らかなはずの場所で GHC に型を推論させるのに問題があります。以下は、問題を示す完全なスニペットです。

{-# 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))

では、期待どおり、明示的なタイプを指定せずにtest1印刷できます。の型は、 の明示的な署名によって推論されます。つまり、has typeの最初の要素です。cccxHListInt

ただし、ではtest2、明示的な署名cが必要です。私が単純print $ untag cにtest2

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

as in にc与えられた明示的な型からGHC が の型を推論できないのはなぜですか?xtest1

4

1 に答える 1

1

これらのエラーは let バインディングに関連していることがわかりました...正確な原因はわかりませんが、実際に GHC のバグなのかはわかりません。回避策は、代わりに case ステートメントを使用することです。

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
于 2013-09-12T18:23:30.253 に答える