Type inference of singular matches on GADTs

[Alexis King]

Hi all,

Today I was writing some code that uses a GADT to represent 
heterogeneous lists:

    data HList as where
       HNil  :: HList '[]
       HCons :: a -> HList as -> HList (a ': as)

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:

    foo :: Blah as => (HList as -> Widget) -> Whatsit

The idea is that Blah does some type-level induction on as and supplies 
the function with some appropriate values. Correspondingly, my use sites 
look something like this:

    bar = foo (\HNil -> ...)

Much to my dismay, I quickly discovered that GHC finds these expressions 
quite unfashionable, and it invariably insults them:

    • Ambiguous type variable ‘as0’ arising from a use of ‘foo’
       prevents the constraint ‘(Blah as0)’ from being solved.

The miscommunication is simple enough. I expected that when given an 
expression like

    \HNil -> ...

GHC would see a single pattern of type HList '[] and consequently infer 
a type like

    HList '[] -> ...

Alas, it was not to be. It seems GHC is reluctant to commit to the 
choice of '[] for as, lest perhaps I add another case to my function in 
the future. Indeed, if I were to do that, the choice of '[] would be 
premature, as as ~ '[] 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.

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 case expression) with only a single branch does not seem 
to be given any special attention.

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

    \(a `HCons` b `HCons` c `HCons` HNil) -> ...

and

    \a b c -> ...

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:

 1. Have people considered this problem before? Is it discussed anywhere
    already?
 2. Is my desire here reasonable, or is there some deep philosophical
    argument for why my program should be rejected?
 3. If it /is/ 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?

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.

Thanks,
Alexis

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20210320/a7d92bac/attachment.html>