Type inference of singular matches on GADTs

[Simon Peyton Jones]

What would you expect of


  1.  \x -> case x of HNil -> blah

Here the lambda and the case are separated.


  1.  \x -> (x, case x of HNil -> blah)

Here the lambda and the case are separated more, and x is used twice.

What if there are more data constructors that share a common return type?



  1.  data HL2 a where

HNil1 :: HL2 []

HNil2 :: HL2 []

HCons :: …blah…

\x -> case x of { HNil1 -> blah; HNil 2 -> blah  }

Here HNil1 and HNil2 both return HL2 [].   Is that “singular”?   What if one was a bit more general than the other?   Do we seek the least common generalisation of the alternatives given?

The water gets deep quickly here.  I don’t (yet) see an obviously-satisfying design point that isn’t massively ad-hoc.

Simon

From: ghc-devs <ghc-devs-bounces at haskell.org> On Behalf Of Alexis King
Sent: 20 March 2021 09:41
To: ghc-devs at haskell.org
Subject: Type inference of singular matches on GADTs


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/20210322/a9653efa/attachment.html>