[Haskell-cafe] Limitations of generalization of type constructors

Ryan Scott ryan.gl.scott at gmail.com
Mon Sep 18 13:23:19 UTC 2023

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.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20230918/23986400/attachment.html>

More information about the Haskell-Cafe mailing list