```hs {-# LANGUAGE RequiredTypeArguments, PartialTypeSignatures, DataKinds #-} import GHC.TypeLits data Foo (n :: Nat) = MkFoo mkFoo :: forall n -> Foo n mkFoo n = MkFoo blah :: forall (n :: Nat) -> _ blah n = mkFoo n ``` Here, instead of inferring `w ~ Foo n`, GHC 9.12.1 fails with: > ``` > /tmp/b.hs:11:10: error: [GHC-25897] > • Couldn't match expected type ‘w’ with actual type ‘Foo n’ > ‘w’ is a rigid type variable bound by > the inferred type of blah :: forall (n1 :: Nat) -> w > at /tmp/b.hs:11:1-16 > • In the expression: mkFoo n > In an equation for ‘blah’: blah n = mkFoo n > • Relevant bindings include > blah :: forall (n :: Nat) -> w (bound at /tmp/b.hs:11:1) > | > 11 | blah n = mkFoo n > | ^^^^^^^ > ``` If I don't use a required type argument in the definition of `blah`, it goes through: ``` {-# LANGUAGE ScopedTypeVariables #-} blah :: forall n. _ blah = MkFoo @n ``` and it gives the correct wildcard filling: > ``` > • Found type wildcard ‘_’ standing for ‘Foo n’ > Where: ‘n’ is a rigid type variable bound by > the inferred type of blah :: Foo n > at /tmp/b.hs:18:16 > • In the type signature: blah :: forall n. _ > ```