Czy istnieje jakiś głębszy teoretyczny powód, dla którego GHC nie może wywnioskować tego typu?

Question

GHC odrzuca program

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

z

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) } 

, z dopiskiem typu działa dobrze. Wszystkie odpowiedzi dotyczące niedotykalnych zmiennych typu i GADT, które znalazłem w sieci, zapewniły, że wnioskowanie typu byłoby niemożliwe lub co najmniej nie do rozwiązania, ale w tym przypadku wydaje się oczywiste, że GHC uzyskało typ (String, Integer), po prostu odmawia ujednolicenia.

Answer 1

Może oryginalny GADT może być cukier za coś, co nie korzysta GADTs jak poniżej (które działa):

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