Pattern Matching on Promoted Types

Question

We can write single, comprehensive instances for parameters of kind *:

class MyClass d where
    f :: d -> Int

instance MyClass (Maybe d) where  
    f _ = 3

test1 :: Maybe d -> Int
test1 x = f x

This compiles just fine, and note that we do NOT need a (MyClass (Maybe d)) constraint on test1 because the compiler finds a matching instance for any Maybe d.

We can even write an all-encompassing instance for class parameters that are type constructors:

class MyClass2 (a :: * -> *) where
    g :: Tagged (a Int) Int

instance MyClass2 a where
    g = Tagged 3

test2 :: Int
test2 = untag (g :: Tagged (Maybe Int) Int)

This also compiles fine, and test2 does not need a (MyClass2 Maybe) constraint, because the compiler finds a matching instance.

Consider the following toy code to compute the length of a (promoted) type list:

{-# LANGUAGE TypeOperators,
DataKinds,
KindSignatures,
GADTs,
FlexibleInstances,
FlexibleContexts,
ScopedTypeVariables #-}

import Data.Tagged
import Data.Proxy

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

class ListLen a where
    len :: Tagged a Int

instance ListLen (HList '[]) where
    len = Tagged 0

instance (ListLen (HList as)) => ListLen (HList (a ': as)) where
    len = Tagged (1+(untag (len :: Tagged (HList as) Int)))

test3 :: Int
test3 = untag (len :: Tagged (HList '[Int, Double, Integer]) Int)

test4 :: (Proxy (HList qs)) -> Int
test4 (_ :: Proxy (HList qs)) = untag (len :: Tagged (HList qs) Int) -- error occurs here

This results in the error:

No instance for (ListLen (HList qs))
      arising from a use of `len'
    Possible fix: add an instance declaration for (ListLen (HList qs))
    ...

If we comment out the signature for test4, GHCi infers the type as

test4 :: (ListLen (HList qs)) => (Proxy (HList qs)) -> Int

but this shouldn't be necessary. Clearly, I've written instances for ListLen that match any conceivable type list: an 'empty list' case, and a 'cons' case. The problem remains the same if I change the kind of the ListLen parameter to have kind [*] (i.e., remove the HList wrapper in ListLen and its instances).

If we comment out test4, test3 compiles and runs fine: since I (essentially) gave it explicit syntax ('[Int,Double,Integer]) for how I constructed the type list, the compiler was able to find matching instances.

I'm attempting to write code that builds a type list for me, so I will not have to write out the explicit type list syntax. However, it seems that using explicit syntax is the only way GHC is able to match these comprehensive instances. Perhaps there's a case I'm missing? Syntax I'm not using?

What can I do to make GHC realize that I have an instance for everything of kind [*]? I'm using GHC 7.4.2. This might be related to a previous post about deconstructing non-promoted types. THE paper on type promotion can be found here.

Answer 1

This is not exactly what you want, but gets pretty close. I started out with

data Proxy a where
  Proxy :: ListLen a => Proxy

then

data Proxy a where
  Proxy :: Tagged a Int -> Proxy a

resulting in

test4 :: (Proxy (HList qs)) -> Int
test4 (Proxy len) = untag len

The problem is you either need to have the constraint, or have Proxy contain evidence of the required class (even though instances exist for all available kinds). Here, the class method is just included in Proxy.

A completely different option is to just not use a type class at all, and implement len in the usual way (transcribed from Data.List.length).

len :: HList a -> Int
len l = len' l 0
  where
    len' :: HList a -> Int -> Int
    len' HNil a = a
    len' (HCons _ xs) a = len' xs $! a + 1