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
