I've thought a bit about this. The main issue is that in general, we
don't know how big a value of polymorphic type is. If you don't have
this information, you have have to get it somehow. Monomorphisation
gets this information for you by specializing away the
polymorphism. Boxing gets this information for you by putting
everything into a representation of known size.
A third alternative is to keep track of this information in the
kinds. Basically, what you can do is to introduce a different kind for
each data size, and then polymorphic functions can be defined over all
types of a particular size. I'll sketch such a system below.
$$
\newcommand{\bnfalt}{\;\;|\;\;}
\newcommand{\rule}[2]{{\mathord{\array{#1}} \over {\mathord{#2}}}}
\newcommand{\judge}[3]{{#1} \vdash {#2} : {#3}}
$$
$$
\begin{array}{llcl}
\mbox{Kinds} & \kappa & ::= n \\
\mbox{Type constructors} & A & ::= & \forall a:\kappa.\; A \bnfalt \alpha \bnfalt A \times B \bnfalt A + B \bnfalt A \to B \\
& & | & \mathsf{ref}\;A \bnfalt \mathsf{Pad}(k) \bnfalt \mu \alpha:\kappa.\; A\\
\end{array}
$$
Here, the high level idea is that the kind of a type tells you how
many words it takes to lay out an object in memory. For any given
size, it's easy to be polymorphic over all types of that particular
size. Since every type -- even polymorphic ones -- still has a known
size, compilation isn't any harder than it is for C.
The kinding rules turn this English into math, and should look something like this:
$$
\rule{ \alpha:n \in \Gamma}
{ \judge{\Gamma}{\alpha}{n} }
\qquad
\rule{ \judge{\Gamma, \alpha:n}{A}{m} }
{ \judge{\Gamma}{\forall \alpha:n.\; A}{m} }
$$
$$
\rule{ \judge{\Gamma}{A}{n} &
\judge{\Gamma}{B}{m} }
{ \judge{\Gamma}{A \times B}{n + m} }
\qquad
\rule{ \judge{\Gamma}{A}{n} &
\judge{\Gamma}{B}{n} }
{ \judge{\Gamma}{A + B}{n + 1} }
$$
$$
\rule{ \judge{\Gamma}{A}{m} &
\judge{\Gamma}{B}{n} }
{ \judge{\Gamma}{A \to B}{1} }
\qquad
\rule{ \judge{\Gamma}{A}{n} }
{ \judge{\Gamma}{\mathsf{ref}\;A}{1} }
$$
$$
\rule{ }
{ \judge{\Gamma}{\mathsf{Pad}(k)}{k} }
\qquad
\rule{ \judge{\Gamma, \alpha:n}{A}{n} }
{ \judge{\Gamma}{\mu \alpha:n.\; A}{n}
}
$$
So the forall quantifier requires you to give the kind you are ranging
over. Likewise, pairing $A \times B$ is an unboxed pair type, which
just lays out an $A$ next to a $B$ in memory (like a C struct
type). Disjoint unions take two values of the same size, and then add
a word for a discriminator tag. Functions are closures, represented as
usual by a pointer to a record of the environment and the
code.
References are interesting -- pointers are always one word, but they
can point to values of any size. This lets programmers implement
polymorphism to arbitrary objects by boxing, but doesn't require
them to do so. Finally, once explicit sizes are in play, it's often
useful to introduce a padding type, which uses space but doesn't do
anything. (So if you want to take the disjoint union of an int and a
pair of ints, you'll need to add padding the first int, so that the
object layout is uniform.)
Recursive types have the standard formation rule, but note that
recursive occurences have to be the same size, which means you usually
have to stick them in a pointer to make the kinding work out. Eg, the
list datatype could be represented as
$$
\mu \alpha:1.\; \mathsf{ref}\;(\mathsf{Pad}(2) + \mathsf{int} \times \alpha)
$$
So this points to an empty list value, or a pair of an int and a pointer
to another linked list.
Type checking for systems like this is also not very hard; the
algorithm in my ICFP paper with Joshua Dunfield, Complete and Easy
Bidirectional Typechecking for Higher Rank
Polymorphism applies to this case
with almost no changes.
