RE: Type inference of singular matches on GADTs

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. As I wrote in another post on this thread, it’s a bit tricky. What would you expect of (EX1) \x -> case x of HNil -> blah Here the lambda and the case are separated Now (EX2) \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? (EX3) 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? (EX4) data HL3 a where HNil1 :: HL2 [Int] HNil2 :: HL2 [a] HCons :: …blah… \x -> case x of { HNil1 -> blah; HNil 2 -> blah } What if the cases were incompatible? (EX5) data HL4 a where HNil1 :: HL2 [Int] HNil2 :: HL2 [Bool] HCons :: …blah… \x -> case x of { HNil1 -> blah; HNil 2 -> blah } Would you expect that to somehow generalise to `HL4 [a] -> blah`? What if x matched multiple times, perhaps on different constructors (EX6) \x -> (case s of HNil1 -> blah1; case x of HNil2 -> blah) 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 On Behalf Of Richard Eisenberg Sent: 29 March 2021 03:18 To: Alexis King Cc: ghc-devs@haskell.org Subject: Re: Type inference of singular matches on GADTs On Mar 26, 2021, at 8:41 PM, Alexis King mailto:lexi.lambda@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