[Haskell-cafe] Limitations of generalization of type constructors

[Ryan Scott]

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.html#higher-rank-kinds
[2]
https://ryanglscott.github.io/2019/07/10/the-surprising-rigidness-of-higher-rank-kinds/
[3]
https://github.com/ghc-proposals/ghc-proposals/blob/7e380dcc4494de30f95bd15d18342eb2302430c4/proposals/0242-unsaturated-type-families.rst
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20230918/23986400/attachment.html>