Type inference of singular matches on GADTs

[Sebastian Graf]

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 at 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 at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20210328/e6bf438f/attachment.html>