Type inference of singular matches on GADTs

[Richard Eisenberg]

> On Mar 26, 2021, at 8:41 PM, Alexis King <lexi.lambda at gmail.com> wrote:
> 
> If there’s a single principal type that makes my function well-typed and exhaustive, I’d really like GHC to pick it.

I think this is the key part of Alexis's plea: that the type checker take into account exhaustivity in choosing how to proceed.

Another way to think about this:

> f1 :: HList '[] -> ()
> f1 HNil = ()
> 
> f2 :: HList as -> ()
> f2 HNil = ()

Both f1 and f2 are well typed definitions. In any usage site where both are well-typed, they will behave the same. Yet f1 is exhaustive while f2 is not. This isn't really about an open-world assumption or the possibility of extra cases -- it has to do with what the runtime behaviors of the two functions are. f1 never fails, while f2 must check a constructor tag and perhaps throw an exception.

If we just see \HNil -> (), Alexis seems to be suggesting we prefer the f1 interpretation over the f2 interpretation. Why? Because f1 is exhaustive, and when we can choose an exhaustive interpretation, that's probably a good idea to pursue.

I haven't thought about how to implement such a thing. At the least, it would probably require some annotation saying that we expect `\HNil -> ()` to be exhaustive (as GHC won't, in general, make that assumption). Even with that, could we get type inference to behave? Possibly.

But first: does this match your understanding?

Richard
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20210329/63c9f84e/attachment.html>