Type inference of singular matches on GADTs
carter.schonwald at gmail.com
Mon Mar 29 03:00:56 UTC 2021
i like how you've boiled down this discussion, it makes it much clearer to
me at least :)
On Sun, Mar 28, 2021 at 10:19 PM Richard Eisenberg <rae at richarde.dev> wrote:
> 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?
> ghc-devs mailing list
> ghc-devs at haskell.org
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the ghc-devs