Type inference of singular matches on GADTs

[Viktor Dukhovni]

On Sat, Mar 20, 2021 at 04:40:59AM -0500, Alexis King wrote:

> Today I was writing some code that uses a GADT to represent 
> heterogeneous lists:
> 
>     data HList as where
>        HNil  :: HList '[]
>        HCons :: a -> HList as -> HList (a ': as)
> 
> This type is used to provide a generic way to manipulate n-ary 
> functions. Naturally, I have some functions that accept these n-ary 
> functions as arguments, which have types like this:
> 
>     foo :: Blah as => (HList as -> Widget) -> Whatsit
> 
> The idea is that Blah does some type-level induction on as and supplies 
> the function with some appropriate values. Correspondingly, my use sites 
> look something like this:
> 
>     bar = foo (\HNil -> ...)
> 
> Much to my dismay, I quickly discovered that GHC finds these expressions 
> quite unfashionable, and it invariably insults them:
> 
>     • Ambiguous type variable ‘as0’ arising from a use of ‘foo’
>        prevents the constraint ‘(Blah as0)’ from being solved.

FWIW, the simplest possible example:

    {-# LANGUAGE DataKinds, TypeOperators, GADTs #-}

    data HList as where
      HNil  :: HList '[]
      HCons :: a -> HList as -> HList (a ': as)

    foo :: (as ~ '[]) => (HList as -> Int) -> Int
    foo f = f HNil

    bar :: Int
    bar = foo (\HNil -> 1)

compiles without error.  As soon as I try add more complex contraints, I
appear to need an explicit type signature for HNil, and then the code
again compiles:

    {-# LANGUAGE
        DataKinds
      , GADTs
      , PolyKinds
      , ScopedTypeVariables
      , TypeFamilies
      , TypeOperators
      #-}

    import GHC.Types

    data HList as where
      HNil  :: HList '[]
      HCons :: a -> HList as -> HList (a ': as)

    class Nogo a where

    type family   Blah (as :: [Type]) :: Constraint
    type instance Blah '[]        = ()
    type instance Blah (_ ': '[]) = ()
    type instance Blah (_ ': _ ': _)   = (Nogo ())

    foo :: (Blah as) => (HList as -> Int) -> Int 
    foo _ = 42

    bar :: Int
    bar = foo (\ (HNil :: HNilT) -> 1)
    type HNilT = HList '[]

    baz :: Int
    baz = foo (\ (True `HCons` HNil :: HOneT Bool) -> 2)
    type HOneT a = HList (a ': '[])

Is this at all useful?

-- 
    Viktor.