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