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