Hi Alexis, The following works and will have inferred type `Int`:

bar = foo (\(HNil :: HList '[]) -> 42)

I'd really like it if we could write

bar2 = foo (\(HNil @'[]) -> 42)

though, even if you write out the constructor type with explicit constraints and forall's. E.g. by using a -XTypeApplications here, I specify the universal type var of the type constructor `HList`. I think that is a semantics that is in line with Type Variables in Patterns, Section 4 https://dl.acm.org/doi/10.1145/3242744.3242753: The only way to satisfy the `as ~ '[]` constraint in the HNil pattern is to refine the type of the pattern match to `HList '[]`. Consequently, the local `Blah '[]` can be discharged and bar2 will have inferred `Int`. But that's simply not implemented at the moment, I think. I recall there's some work that has to happen before. The corresponding proposal seems to be https://ghc-proposals.readthedocs.io/en/latest/proposals/0126-type-applicati... (or https://github.com/ghc-proposals/ghc-proposals/pull/238? I'm confused) and your example should probably be added there as motivation. If `'[]` is never mentioned anywhere in the pattern like in the original example, I wouldn't expect it to type-check (or at least emit a pattern-match warning): First off, the type is ambiguous. It's a similar situation as in https://stackoverflow.com/questions/50159349/type-abstraction-in-ghc-haskell. If it was accepted and got type `Blah as => Int`, then you'd get a pattern-match warning, because depending on how `as` is instantiated, your pattern-match is incomplete. E.g., `bar3 @[Int]` would crash. Complete example code: {-# LANGUAGE DataKinds #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE RankNTypes #-} module Lib where data HList as where HNil :: forall as. (as ~ '[]) => HList as HCons :: forall as a as'. (as ~ (a ': as')) => a -> HList as' -> HList as class Blah as where blah :: HList as instance Blah '[] where blah = HNil foo :: Blah as => (HList as -> Int) -> Int foo f = f blah bar = foo (\(HNil :: HList '[]) -> 42) -- compiles bar2 = foo (\(HNil @'[]) -> 42) -- errors Cheers, Sebastian Am Sa., 20. März 2021 um 13:57 Uhr schrieb Viktor Dukhovni < ietf-dane@dukhovni.org>:

On Sat, Mar 20, 2021 at 08:13:18AM -0400, Viktor Dukhovni wrote:

...

As soon as I try add more complex contraints, I appear to need an explicit type signature for HNil, and then the code again compiles:

But aliasing the promoted constructors via pattern synonyms, and using those instead, appears to resolve the ambiguity.

-- Viktor.

{-# LANGUAGE DataKinds , GADTs , PatternSynonyms , PolyKinds , ScopedTypeVariables , TypeFamilies , TypeOperators #-}

import GHC.Types

infixr 1 `HC`

data HList as where HNil :: HList '[] HCons :: a -> HList as -> HList (a ': as)

pattern HN :: HList '[]; pattern HN = HNil pattern HC :: a -> HList as -> HList (a ': as) pattern HC a as = HCons a as

class Nogo a where

type family Blah (as :: [Type]) :: Constraint type instance Blah '[] = () type instance Blah (_ ': '[]) = () type instance Blah (_ ': _ ': '[]) = () type instance Blah (_ ': _ ': _ ': _) = (Nogo ())

foo :: (Blah as) => (HList as -> Int) -> Int foo _ = 42

bar :: Int bar = foo (\ HN -> 1)

baz :: Int baz = foo (\ (True `HC` HN) -> 2)

pattern One :: Int pattern One = 1 bam :: Int bam = foo (\ (True `HC` One `HC` HN) -> 2) _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

I appreciate your point Sebastian, but I think in this particular case, type applications in patterns are still not enough to satisfy me. I provided the empty argument list example because it was simple, but I’d also like this to typecheck: baz :: Int -> String -> Widget baz = .... bar = foo (\(a `HCons` b `HCons` HNil) -> baz a b) I don’t want to have to annotate the types of a and b because they’re both eminently inferrable. I’d like to get type inference properties comparable to an ordinary two-argument lambda expression, since that’s how I’m trying to use this, after all. Really what I’m complaining about here is type inference of GADT patterns. For comparison, suppose I had these definitions: class Blah a where foo :: (a -> Widget) -> Whatsit instance Blah (Int, String) where foo = .... baz :: Int -> String -> Widget baz = .... bar = foo (\(a, b) -> baz a b) This compiles without any issues. The pattern (a, b) is inferred to have type (t1, t2), where both t1 and t2 are metavariables. These are unified to particular types in the body, and everything is fine. But type inference for GADT patterns works differently. In fact, even this simple definition fails to compile: bar = \(a `HCons` HNil) -> not a GHC rejects it with the following error: error: • Could not deduce: a ~ Bool from the context: as ~ (a : as1) This seems to arise from GHC’s strong reluctance to pick any particular type for a match on a GADT constructor. One way to explain this is as a sort of “open world assumption” as it applies to case expressions: we always /could/ add more cases, and if we did, specializing the type based on the existing cases might be premature. Furthermore, non-exhaustive pattern-matching is not a type error in Haskell, only a warning, so perhaps we /wanted/ to write a non-exhaustive function on an arbitrary HList. Of course, I think that’s somewhat silly. If there’s a single principal type that makes my function well-typed /and exhaustive/, I’d really like GHC to pick it. Alexis On 3/22/21 1:28 PM, Sebastian Graf wrote:

Cale made me aware of the fact that the "Type applications in patterns" proposal had already been implemented. See https://gitlab.haskell.org/ghc/ghc/-/issues/19577 where I adapt Alexis' use case into a test case that I'd like to see compiling.

Am Sa., 20. März 2021 um 15:45 Uhr schrieb Sebastian Graf mailto:sgraf1337@gmail.com>:

Hi Alexis,

The following works and will have inferred type `Int`:

> bar = foo (\(HNil :: HList '[]) -> 42)

I'd really like it if we could write

> bar2 = foo (\(HNil @'[]) -> 42)

though, even if you write out the constructor type with explicit constraints and forall's. E.g. by using a -XTypeApplications here, I specify the universal type var of the type constructor `HList`. I think that is a semantics that is in line with Type Variables in Patterns, Section 4 https://dl.acm.org/doi/10.1145/3242744.3242753: The only way to satisfy the `as ~ '[]` constraint in the HNil pattern is to refine the type of the pattern match to `HList '[]`. Consequently, the local `Blah '[]` can be discharged and bar2 will have inferred `Int`.

But that's simply not implemented at the moment, I think. I recall there's some work that has to happen before. The corresponding proposal seems to be https://ghc-proposals.readthedocs.io/en/latest/proposals/0126-type-applicati... (or https://github.com/ghc-proposals/ghc-proposals/pull/238? I'm confused) and your example should probably be added there as motivation.

If `'[]` is never mentioned anywhere in the pattern like in the original example, I wouldn't expect it to type-check (or at least emit a pattern-match warning): First off, the type is ambiguous. It's a similar situation as in https://stackoverflow.com/questions/50159349/type-abstraction-in-ghc-haskell. If it was accepted and got type `Blah as => Int`, then you'd get a pattern-match warning, because depending on how `as` is instantiated, your pattern-match is incomplete. E.g., `bar3 @[Int]` would crash.

Complete example code:

{-# LANGUAGE DataKinds #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE RankNTypes #-}

module Lib where

data HList as where   HNil  :: forall as. (as ~ '[]) => HList as   HCons :: forall as a as'. (as ~ (a ': as')) => a -> HList as' -> HList as

class Blah as where   blah :: HList as

instance Blah '[] where   blah = HNil

foo :: Blah as => (HList as -> Int) -> Int foo f = f blah

bar = foo (\(HNil :: HList '[]) -> 42) -- compiles bar2 = foo (\(HNil @'[]) -> 42) -- errors

Cheers, Sebastian

Am Sa., 20. März 2021 um 13:57 Uhr schrieb Viktor Dukhovni mailto:ietf-dane@dukhovni.org>:

On Sat, Mar 20, 2021 at 08:13:18AM -0400, Viktor Dukhovni wrote:

> As soon as I try add more complex contraints, I appear to need an > explicit type signature for HNil, and then the code again compiles:

But aliasing the promoted constructors via pattern synonyms, and using those instead, appears to resolve the ambiguity.

--     Viktor.

{-# LANGUAGE     DataKinds   , GADTs   , PatternSynonyms   , PolyKinds   , ScopedTypeVariables   , TypeFamilies   , TypeOperators   #-}

import GHC.Types

infixr 1 `HC`

data HList as where   HNil  :: HList '[]   HCons :: a -> HList as -> HList (a ': as)

pattern HN :: HList '[]; pattern HN = HNil pattern HC :: a -> HList as -> HList (a ': as) pattern HC a as = HCons a as

class Nogo a where

type family   Blah (as :: [Type]) :: Constraint type instance Blah '[]        = () type instance Blah (_ ': '[]) = () type instance Blah (_ ': _ ': '[]) = () type instance Blah (_ ': _ ': _ ': _) = (Nogo ())

foo :: (Blah as) => (HList as -> Int) -> Int foo _ = 42

bar :: Int bar = foo (\ HN -> 1)

baz :: Int baz = foo (\ (True `HC` HN) -> 2)

pattern One :: Int pattern One = 1 bam :: Int bam = foo (\ (True `HC` One `HC` HN) -> 2)

Hi Alexis, If you really want to get by without type annotations, then Viktor's pattern synonym suggestion really is your best option! Note that pattern HNil :: HList '[]; pattern HNil = HNil_ Does not actually declare an HNil that is completely synonymous with HNil_, but it changes the *provided* GADT constraint (as ~ '[]) into a *required* constraint (as ~ '[]). "Provided" as in "a pattern match on the synonym provides this constraint as a new Given", "required" as in "... requires this constraint as a new Wanted". (I hope I used the terminology correctly here.) Thus, a pattern ((a :: Int) `HCons` HNil) really has type (HList '[Int]) and is exhaustive. See also https://gitlab.haskell.org/ghc/ghc/-/wikis/pattern-synonyms#static-semantics . At the moment, I don't think it's possible to declare a GADT constructor with required constraints, so a pattern synonym seems like your best bet and fits your use case exactly. You can put each of these pattern synonyms into a singleton COMPLETE pragma. Hope that helps, Sebastian Am Sa., 27. März 2021 um 06:27 Uhr schrieb Viktor Dukhovni < ietf-dane@dukhovni.org>:

On Fri, Mar 26, 2021 at 07:41:09PM -0500, Alexis King wrote:

...

type applications in patterns are still not enough to satisfy me. I provided the empty argument list example because it was simple, but I’d also like this to typecheck:

baz :: Int -> String -> Widget baz = ....

bar = foo (\(a `HCons` b `HCons` HNil) -> baz a b)

Can you be a bit more specific on how the constraint `Blah` is presently defined, and how `foo` uses the HList type to execute a function of the appropriate arity and signature?

The example below my signature typechecks, provided I use pattern synonyms for the GADT constructors, rather than use the constructors directly.

-- Viktor.

{-# language DataKinds , FlexibleInstances , GADTs , PatternSynonyms , ScopedTypeVariables , TypeApplications , TypeFamilies , TypeOperators #-}

import GHC.Types import Data.Proxy import Type.Reflection import Data.Type.Equality

data HList as where HNil_ :: HList '[] HCons_ :: a -> HList as -> HList (a ': as) infixr 5 `HCons_`

pattern HNil :: HList '[]; pattern HNil = HNil_ pattern (:^) :: a -> HList as -> HList (a ': as) pattern (:^) a as = HCons_ a as pattern (:$) a b = a :^ b :^ HNil infixr 5 :^ infixr 5 :$

class Typeable as => Blah as where params :: HList as instance Blah '[Int,String] where params = 39 :$ "abc"

baz :: Int -> String -> Int baz i s = i + length s

bar = foo (\(a :$ b) -> baz a b)

foo :: Blah as => (HList as -> Int) -> Int foo f = f params _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

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 wrote:

On Mar 26, 2021, at 8:41 PM, Alexis King 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

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

I'm not saying this is a good idea for GHC or that it's implementable. But the idea of having type inference account for exhaustivity in this way does not seem, a priori, unspecified. No, but I’m pointing out that specifying it might be tricky, involving some highly non-local reasoning. I can’t yet see how to write a formal specification. Note “yet” -- growth mindset! Simon From: Richard Eisenberg Sent: 30 March 2021 04:58 To: Simon Peyton Jones Cc: Alexis King ; ghc-devs@haskell.org Subject: Re: Type inference of singular matches on GADTs As usual, I want to separate out the specification of a feature from the implementation. So let's just focus on specification for now -- with the caveat that there might be no possible implementation of these ideas. The key innovation I see lurking here is the idea of an *exhaustive* function, where we know that any pattern-match on an argument is always exhaustive. I will write such a thing with @->, in both the type and in the arrow that appears after the lambda. The @-> type is a subtype of -> (and perhaps does not need to be written differently from ->). EX1: \x @-> case x of HNil -> blah This is easy: we can infer HList '[] @-> blah's type, because the pattern match is declared to be exhaustive, and no other type grants that property. EX2: \x @-> (x, case x of HNit -> blah) Same as EX1. EX3: \x @-> case x of { HNil1 -> blah; HNil2 -> blah } Same as EX1. There is still a unique type for which the patten-match is exhaustive. EX4: Reject. There are multiple valid types, and we don't know which one to pick. This is like classic untouchable-variables territory. EX5: This is hard. A declarative spec would probably choose HL2 [a] -> ... as you suggest, but there may be no implementation of such an idea. EX6: Reject. No type leads to exhaustive matches. I'm not saying this is a good idea for GHC or that it's implementable. But the idea of having type inference account for exhaustivity in this way does not seem, a priori, unspecified. Richard On Mar 29, 2021, at 5:00 AM, Simon Peyton Jones mailto:simonpj@microsoft.com> wrote: 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 mailto:ghc-devs-bounces@haskell.org> On Behalf Of Richard Eisenberg Sent: 29 March 2021 03:18 To: Alexis King mailto:lexi.lambda@gmail.com> Cc: ghc-devs@haskell.orgmailto: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