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