Type inference of singular matches on GADTs

[Viktor Dukhovni]

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