Re: Type inference of singular matches on GADTs

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)