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.