To handle type lists, it's necessary to discriminate empty from nonempty lists and handle them separately. The 'Could not deduce' errors in your code occur because your instance assumes a nonempty list, when in fact the list may or may not be empty. Here is a solution using the extensions TypeFamilies
, TypeOperators
, DataKinds
, and GADTs
.
With DataKinds
, type lists are predefined. They have kind [*]
, but they'll be used in a context where kind *
is expected, so an operator is needed to cast them:
data InjList (qs :: [*])
Using type lists, FList
is defined as
data FList c q where
FNil :: FList c (InjList '[])
FCons :: c h -> FList c (InjList t) -> FList c (InjList (h ': t))
It's defined as a GADT to express how it's only possible to construct FList
s over the type InjList q'
for some type-list q'
. For instance, the term FCons [True] FNil
has type FList [] (InjList (Bool ': '[]))
. On the other hand, since Bool
isn't of the form InjList q'
, there are no terms (except ⊥) of type FList [] Bool
. By pattern matching on an FList
, a function can verify that it has been given a non-⊥ argument, and further determine whether it's been passed an empty type list.
An instance of Bar
for FList
s has to handle nil lists and cons lists separately. A nil list has an empty context.
A cons list has components for the head and tail of the list. This is expressed by pattern matching on the type-list in the associated type instance of BCtx
. The function f
examines its argument to verify that it's not ⊥ and to decide whether it's an empty list.
instance (Bar c) => Bar (FList c) where
-- Empty context for '[]
type BCtx (FList c) (InjList '[]) = ()
-- Context includes components for head and tail of list
type BCtx (FList c) (InjList (h ': t)) = (BCtx c h, BCtx (FList c) (InjList t))
f FNil FNil = FNil
f (FCons x xs) (FCons y ys) = FCons (f x y) (f xs ys)
We can load the code into GHCi to verify that it works:
instance Bar [] where
type BCtx [] q = Num q
f xs ys = zipWith (+) xs ys
instance Show (FList c (InjList '[])) where
show FNil = "FNil"
instance (Show (c h), Show (FList c (InjList t))) => Show (FList c (InjList (h ': t))) where
show (FCons h t) = "FCons (" ++ show h ++ ") (" ++ show t ++ ")"
$ ghci
> :load Test
> f (FCons [1,2] FNil) (FCons [3,4] FNil)
FCons ([4,6]) (FNil)