Type checking influenced by definition

Here's a program, taken from !8820 (comment 486855)

{-# LANGUAGE DataKinds, TypeFamilies, TypeFamilyDependencies #-}
module M where

import Data.Kind
import GHC.TypeLits

data Tuple2 x y = MkTuple2 x y

type TupleArgKind :: Nat -> Type
type family TupleArgKind n = r | r -> n where
  TupleArgKind 2 = Tuple2 Type Type

type Tuple :: forall (n :: Nat). TupleArgKind n -> Type
type family Tuple ts = r | r -> ts where
  Tuple (MkTuple2 a b) = Tuple2 a b

-- works
f :: Tuple (MkTuple2 a b) -> ()
f (MkTuple2 _ _) = ()

-- fails
g :: Tuple (MkTuple2 a b) -> ()
g x = ()

-- works
h :: Tuple @2 (MkTuple2 a b) -> ()
h x = ()

f and g have the same type signature - but only g is rejected because of an error in the type. This violates the principle that a type signature should stand on its own and not be influenced by the definition (unless PartialTypeSignatures is enabled).

When typechecking the signature for f, the relevant part from -ddump-tc-trace (with wanted added) is

kindGeneralizeSome
  type: forall (a :: x_aFQ[tau:2]) (b :: y_aFR[tau:2]).
        (Tuple (MkTuple2 a b |> {co_aFS}) -> () |> (TYPE {co_aMe})_N)
  dvs: DV {dv_kvs = {x_aFQ[tau:2], y_aFR[tau:2], n_aFP[tau:2]},
           dv_tvs = {}, dv_cvs = {co_aMh}}
  wanted: WC {wc_impl =
                Implic {
                  TcLevel = 2
                  Skolems = (a_aDb[sk:2] :: k_aFL[tau:2])
                            (b_aDc[sk:2] :: k_aFM[tau:2])
                  Given-eqs = NoGivenEqs
                  Status = Unsolved
                  Given =
                  Wanted =
                    WC {wc_simple =
                          [W] hole{co_aMh} {0}:: TupleArgKind n_aFP[tau:2]
                                                 GHC.Prim.~# Tuple2
                                                               x_aFQ[tau:2] y_aFR[tau:2] (CEqCan)}
                  Binds = CoEvBindsVar<aMf>
                  the type signature for ‘f’ }}
  filtered_dvs: DV {dv_kvs = {}, dv_tvs = {}, dv_cvs = {co_aMh}}

Given a :: x, b :: y, the expression Tuple @n (MkTuple2 a b) is legal when TupleArgKind n ~ Tuple2 x y. If generalized, the full type would be

f :: forall (n :: Nat) (x :: Type) (y :: Type) (a :: x) (b :: y). TupleArgKind n ~ Tuple2 x y => Tuple (MkTuple2 a b) -> ()

but that would require coercion quantification. So we do not generalize over x, y, n. Later, in the case of f, they are inferred to be Type, Type, 2 while in the case of g, there are no further constraints and we error. Looks like we should reject f just like g.