Re: Type inference of singular matches on GADTs

27 Mar 2021

      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

Re: Type inference of singular matches on GADTs

Viktor Dukhovni