Is there any deeper type-theoretic reason GHC can't infer this type? [duplicate]

Question

This question already has an answer here:

Type inference with GADTs - a0 is untouchable (1 answer)

Closed 4 years ago.

GHC rejects the 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)

with

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

, with the type annotation it works fine. All answers regarding untouchable type variables and GADTs that I found on the net asserted that type inference would be impossible, or at least intractable but in this case it seems evident that GHC got hold of the type (String, Integer), it's just refusing to unify.

Answer 1

Maybe your original GADT could be sugar for something that doesn't use GADTs like the following (which works):

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