<html>
<head>
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
</head>
<body>
<p>Hi all,</p>
<p>Today I was writing some code that uses a GADT to represent
heterogeneous lists:</p>
<blockquote>
<pre>data HList as where
HNil :: HList '[]
HCons :: a -> HList as -> HList (a ': as)</pre>
</blockquote>
<p>This type is used to provide a generic way to manipulate n-ary
functions. Naturally, I have some functions that accept these
n-ary functions as arguments, which have types like this:</p>
<blockquote>
<pre>foo :: Blah as => (HList as -> Widget) -> Whatsit</pre>
</blockquote>
<p>The idea is that <tt>Blah</tt> does some type-level induction on
<tt>as</tt> and supplies the function with some appropriate
values. Correspondingly, my use sites look something like this:</p>
<blockquote>
<pre>bar = foo (\HNil -> ...)</pre>
</blockquote>
<p>Much to my dismay, I quickly discovered that GHC finds these
expressions quite unfashionable, and it invariably insults them:</p>
<blockquote>
<pre>• Ambiguous type variable ‘as0’ arising from a use of ‘foo’
prevents the constraint ‘(Blah as0)’ from being solved.</pre>
</blockquote>
<p>The miscommunication is simple enough. I expected that when given
an expression like</p>
<blockquote>
<pre>\HNil -> ...</pre>
</blockquote>
<p>GHC would see a single pattern of type <tt>HList '[]</tt> and
consequently infer a type like</p>
<blockquote>
<pre>HList '[] -> ...
</pre>
</blockquote>
<p>Alas, it was not to be. It seems GHC is reluctant to commit to
the choice of <tt>'[]</tt> for <tt>as</tt>, lest perhaps I add
another case to my function in the future. Indeed, if I were to do
that, the choice of <tt>'[]</tt> would be premature, as <tt>as ~
'[]</tt> would only be available within one branch. However, I
do not in fact have any such intention, which makes me quietly
wish GHC would get over its anxiety and learn to be a bit more of
a risk-taker.</p>
<p>I ended up taking a look at the OutsideIn(X) paper, hoping to
find some commentary on this situation, but in spite of the nice
examples toward the start about the trickiness of GADTs, I found
no discussion of this specific scenario: a function with exactly
one branch and an utterly unambiguous pattern. Most examples come
at the problem from precisely the opposite direction, trying to
tease out a principle type from a collection of branches. The case
of a function (or perhaps more accurately, a <tt>case</tt>
expression) with only a single branch does not seem to be given
any special attention.</p>
<p>Of course, fewer special cases is always nice. I have great
sympathy for generality. Still, I can’t help but feel a little
unsatisfied here. Theoretically, there is no reason GHC cannot
treat</p>
<blockquote>
<pre>\(a `HCons` b `HCons` c `HCons` HNil) -> ...
</pre>
</blockquote>
<p>and</p>
<p>
</p>
<blockquote>
<pre>\a b c -> ...</pre>
</blockquote>
<p>almost identically, with a well-defined principle type and
pleasant type inference properties, but there is no way for me to
communicate this to the typechecker! So, my questions:</p>
<ol>
<li>Have people considered this problem before? Is it discussed
anywhere already?</li>
<li>Is my desire here reasonable, or is there some deep
philosophical argument for why my program should be rejected?</li>
<li>If it <i>is</i> reasonable, are there any obvious situations
where a change targeted at what I’m describing (vague as that
is) would affect programs negatively, not positively?</li>
</ol>
<p>I realize this gets rather at the heart of the typechecker, so I
don’t intend to imply a change of this sort should be made
frivolously. Indeed, I’m not even particularly attached to the
idea that a change must be made! But I do want to understand the
tradeoffs better, so any insight would be much appreciated.<br>
</p>
<p>Thanks,<br>
Alexis<br>
</p>
</body>
</html>