GHC有沒有更深的類型 - 理論原因不能推斷這種類型？

Question

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)，它只是拒絕統一。

Answer 1

也許你原來GADT可能是糖的東西，不使用GADTs像下面的（工作）：

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