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-d...@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 >
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs