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 <r...@richarde.dev> wrote: > > > On Mar 26, 2021, at 8:41 PM, Alexis King <lexi.lam...@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 > _______________________________________________ > ghc-devs mailing list > ghc-devs@haskell.org > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs >
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
