<div dir="ltr"><div>Hi Alexis,</div><div><br></div><div>If you really want to get by without type annotations, then Viktor's pattern synonym suggestion really is your best option! Note that</div><div><br></div><div>
pattern HNil :: HList '[];<br>
pattern HNil = HNil_</div><div><br></div><div>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 ~ '[]).</div><div>"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.)</div><div>Thus, a pattern ((a :: Int) `HCons` HNil) really has type (HList '[Int]) and is exhaustive. See also <a href="https://gitlab.haskell.org/ghc/ghc/-/wikis/pattern-synonyms#static-semantics">https://gitlab.haskell.org/ghc/ghc/-/wikis/pattern-synonyms#static-semantics</a>.</div><div>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.</div><div>You can put each of these pattern synonyms into a singleton COMPLETE pragma.</div><div><br></div><div>Hope that helps,</div><div>Sebastian<br></div><div><br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">Am Sa., 27. März 2021 um 06:27 Uhr schrieb Viktor Dukhovni <<a href="mailto:ietf-dane@dukhovni.org">ietf-dane@dukhovni.org</a>>:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">On Fri, Mar 26, 2021 at 07:41:09PM -0500, Alexis King wrote:<br>
<br>
> type applications in patterns are still not enough to satisfy me. I <br>
> provided the empty argument list example because it was simple, but I’d <br>
> also like this to typecheck:<br>
> <br>
>     baz :: Int -> String -> Widget<br>
>     baz = ....<br>
> <br>
>     bar = foo (\(a `HCons` b `HCons` HNil) -> baz a b)<br>
> <br>
<br>
Can you be a bit more specific on how the constraint `Blah` is presently<br>
defined, and how `foo` uses the HList type to execute a function of the<br>
appropriate arity and signature?<br>
<br>
The example below my signature typechecks, provided I use pattern<br>
synonyms for the GADT constructors, rather than use the constructors<br>
directly.<br>
<br>
-- <br>
    Viktor.<br>
<br>
{-# language DataKinds<br>
           , FlexibleInstances<br>
           , GADTs<br>
           , PatternSynonyms<br>
           , ScopedTypeVariables<br>
           , TypeApplications<br>
           , TypeFamilies<br>
           , TypeOperators<br>
           #-}<br>
<br>
import GHC.Types<br>
import Data.Proxy<br>
import Type.Reflection<br>
import Data.Type.Equality<br>
<br>
data HList as where<br>
  HNil_  :: HList '[]<br>
  HCons_ :: a -> HList as -> HList (a ': as)<br>
infixr 5 `HCons_`<br>
<br>
pattern HNil :: HList '[];<br>
pattern HNil = HNil_<br>
pattern (:^) :: a -> HList as -> HList (a ': as)<br>
pattern (:^) a as = HCons_ a as<br>
pattern (:$) a b = a :^ b :^ HNil<br>
infixr 5 :^<br>
infixr 5 :$<br>
<br>
class Typeable as => Blah as where<br>
    params :: HList as<br>
instance Blah '[Int,String] where<br>
    params = 39 :$ "abc"<br>
<br>
baz :: Int -> String -> Int<br>
baz i s = i + length s<br>
<br>
bar = foo (\(a :$ b) -> baz a b)<br>
<br>
foo :: Blah as => (HList as -> Int) -> Int<br>
foo f = f params<br>
_______________________________________________<br>
ghc-devs mailing list<br>
<a href="mailto:ghc-devs@haskell.org" target="_blank">ghc-devs@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br>
</blockquote></div>