5

GHC 拒绝该计划

{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
import GHC.TypeLits

data Foo = Foo
data Bar = Bar

data (:::) :: * -> * -> * where
    (:=) :: sy -> t -> sy ::: t

data Rec :: [*] -> * where
    RNil :: Rec '[]
    (:&) :: (sy ::: ty) -> Rec xs ->  Rec ((sy ::: ty) ': xs)

infix 3 :=
infixr 2 :&

baz :: Num ty => Rec [Foo ::: String, Bar ::: ty]
baz = Foo := "foo" :& Bar := 1 :& RNil

--bang :: (String, Integer)
bang = case baz of
         (Foo := a :& Bar := b :& RNil) -> (a, b)

和

Rec2.hs:25:44:
    Couldn't match type ‛t’ with ‛(String, Integer)’
      ‛t’ is untouchable
        inside the constraints (xs1 ~ '[] *)
        bound by a pattern with constructor
                   RNil :: Rec ('[] *),
                 in a case alternative
        at Rec2.hs:25:35-38
      ‛t’ is a rigid type variable bound by
          the inferred type of bang :: t at Rec2.hs:24:1
    Expected type: t
      Actual type: (ty, ty1)
    Relevant bindings include bang :: t (bound at Rec2.hs:24:1)
    In the expression: (a, b)
    In a case alternative: (Foo := a :& Bar := b :& RNil) -> (a, b)
    In the expression:
      case baz of { (Foo := a :& Bar := b :& RNil) -> (a, b) }

，使用类型注释可以正常工作。我在网上找到的所有关于不可触碰的类型变量和 GADT 的答案都断言类型推断是不可能的，或者至少是难以处理的，但在这种情况下，GHC 显然掌握了类型(String, Integer)，它只是拒绝统一。

4

1 回答 1

4

也许你原来的 GADT 可能是不使用 GADT 的东西的糖，如下所示（有效）：

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
import GHC.TypeLits

data Foo = Foo
data Bar = Bar

data (:::) sy t = (:=) sy t

data RNil = RNil
data (:&) a b = a :& b

type family Rec (xs :: [*]) :: *
type instance Rec (x ': xs) = x :& Rec xs
type instance Rec '[] = RNil

infix 3 :=
infixr 2 :&

baz :: Num ty => Rec [Foo ::: String, Bar ::: ty]
baz = Foo := "foo" :& Bar := 1 :& RNil

bang = case baz of
         ( Foo := a :& Bar := b :& RNil) -> (a, b)
于 2013-09-29T14:47:40.140 回答