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

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 <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: 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-applications-in-patterns.html (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)