Find an element in an HList

I'm trying to write two functions to extract a value from an HList, but I can't seem to make GHC happy.

The first function would have signature extract :: HList a -> [b] which extracts all the elements of type b from the list. I only succeeded in writing it by asking the types in a to have Typeable instances.

class OfType a b where
    oftype :: a -> [Maybe b]

instance OfType (HList '[]) b where
    oftype = const []

instance (Typeable t, Typeable b, OfType (HList ts) b) => OfType (HList (t ': ts)) b where
    oftype (x :- xs) = (cast x :: Maybe b) : oftype xs

extract :: OfType a b => a -> [b]
extract = catMaybes . oftype

Which is suboptimal, as one doesn't really need the Typeable constraint to write any instance of extract.

I tried to use type equalities and inequalities in constraints, but this only gave me overlapping instances.

The second function I'm trying to write would have signature extract' :: Contains h n => HList h -> n which extracts the first element of type n in the list, and the context says that the list actually contains one element of that type.

Is it possible to write extract without Typeable constraints?

Is it possible to write extract' without Typeable constraints? How can one write Contains?

Solution

Since you want to check for type equality at compile time, I believe overlapping instances are unavoidable (and I'm not a fan of those...).

Also, I'm not 100% sure I got the overlapping pragmas right.

{-# LANGUAGE DataKinds, TypeOperators, ScopedTypeVariables,
    MultiParamTypeClasses, FlexibleInstances, FlexibleContexts #-}
{-# OPTIONS -Wall #-}
module HListFilter where

import Data.HList.HList

class OfType a b where
    oftype :: a -> [b]

instance OfType (HList '[]) b where
    oftype = const []

instance {-# OVERLAPS #-} (OfType (HList ts) t) => OfType (HList (t ': ts)) t where
    oftype (HCons x xs) = x : oftype xs

instance {-# OVERLAPPABLE #-} (OfType (HList ts) b) => OfType (HList (t ': ts)) b where
    oftype (HCons _ xs) = oftype xs

test :: HList '[Int, Char, [Char], Char, Bool]
test = HCons (1::Int) (HCons 'a' (HCons "foo" (HCons 'b' (HCons True HNil))))

test_result :: [Char]
test_result = oftype test  -- "ab"