Type inference of singular matches on GADTs
lexi.lambda at gmail.com
Sat Mar 20 09:40:59 UTC 2021
Today I was writing some code that uses a GADT to represent
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
\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) -> ...
\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
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.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the ghc-devs