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