Short answer: This is expected behavior, and it's unlikely that behavior will change any time soon. Long answer: The key phrase in your original post is "the quantifier moved". That is, in this definition:

fc3 :: Int fc3 = f (const 0)

GHC will turn it into something like this behind the scenes when compiling it to Core:

fc3 :: Int fc3 = f (\ (@z). const @Int @(Maybe z) 0 :: forall (z :: Type). Maybe z -> Int)

Note the presence of `\ (@z)`, which binds a type variable with a lambda. This process of moving quantifiers by using type variables in lambdas is called *regeneralization*. A somewhat surprising fact is that GHC can only perform regeneralization some of the time. GHC can regeneralize type-level `forall`s—that is, `forall`s in the types of terms, as is the case in the example above—but it cannot regeneralize *kind*-level `forall`s. In your post, the `forall`s in the kinds of C2 and Const are kind-level `forall`s. This restriction is documented here [1] in the GHC User's Guide. I've also written a slightly longer blog post [2] about the topic. The reason why this restriction exists is because there is no type-level counterpart to `\ (@z)` in Core, which would be required for regeneralization at the kind level. Adding type-level lambdas to Core would likely be a non-trivial effort. The UnsaturatedTypeFamilies proposal [3], which proposes to relax some restrictions about when types can appear partially applied, is the closest thing that I can think of, but it stops short of proposing full type-level lambdas. Best, Ryan ----- [1] https://downloads.haskell.org/ghc/9.6.2/docs/users_guide/exts/poly_kinds.htm... [2] https://ryanglscott.github.io/2019/07/10/the-surprising-rigidness-of-higher-... [3] https://github.com/ghc-proposals/ghc-proposals/blob/7e380dcc4494de30f95bd15d...