Is it possible to remove OverlappingInstances for this DataKinds-backed heterogeneous list implementation?

Question

With recent posts about HaskellDB, I've been motivated to look into HList again. As we now have -XDataKinds in GHC, which actually has an example of heterogeneous lists, I wanted to investigate how HLists look with DataKinds. So far, I have the following:

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE OverlappingInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

import Data.Tagged

data Record :: [*] -> * where
  RNil :: Record '[]
  (:*:) :: Tagged f (FieldV f) -> Record t -> Record (f ': t)

type family FieldV a :: *

emptyRecord = RNil

(=:) :: (v ~ FieldV f) => f -> v -> Tagged f v
f =: v = Tagged v

class HasField x xs where
  (=?) :: Record xs -> x -> FieldV x

instance HasField x (x ': xs) where
  (Tagged v :*: _) =? _ = v

instance HasField x xs => HasField x (a ': xs) where
  (_ :*: r) =? f = r =? f

--------------------------------------------------------------------------------
data EmployeeName = EmployeeName
type instance FieldV EmployeeName = String

data EmployeeID = EmployeeID
type instance FieldV EmployeeID = Int

employee =   (EmployeeName =: "James")
         :*: ((EmployeeID =: 5) :*: RNil)

employeeName = employee =? EmployeeName
employeeId   = employee =? EmployeeID

This works as expected, but my goal in this project was to try and do it without type classes as much as possible. So there are 2 questions here. Firstly, is it possible to write (=?) (the record field accessor function) without a type class? If not, can it be written without overlapping instances?

I imagine that it's not possible for my first question, but maybe the second may be possible. I'd love to hear what people think!

Answer 1

I think the answer to both questions is a qualified no. You simply cant have a type function of the form

type family TypeEq a b :: Bool
type instance TypeEq a a = True
type instance TypeEq a b = False

which is essentially what OverlappingInstances gives you. Oleg has suggested an alternative mechanism using type level TypeReps, but we don't have it yet. This answer is qualified, because you do have ugly "solutions" like using typeable

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

import Data.Typeable

type family FieldV a :: *

data FieldOf f where
  FieldOf :: FieldV f -> FieldOf f

(=:) :: f -> FieldV f -> FieldOf f
_ =: v = FieldOf v

fromField :: FieldOf f -> FieldV f
fromField (FieldOf v) = v

data Record :: [*] -> * where
  RNil :: Record '[]
  (:*:) :: Typeable f => FieldOf f -> Record t -> Record (f ': t)

data SameType a b where
  Refl :: SameType a a

useProof :: SameType a b -> a -> b
useProof Refl a = a 

newtype SF a b = SF (SameType (FieldOf a) (FieldOf b))
sf1 :: FieldOf f -> SF f f
sf1 _ = SF Refl

targetType :: f -> Maybe (SF g f)
targetType _ = Nothing

(?=) :: Typeable a => Record xs -> a -> Maybe (FieldV a)
RNil ?= _ = Nothing
(x :*: xs) ?= a = case (gcast (sf1 x)) `asTypeOf` (targetType a) of
                   Nothing      -> xs ?= a
                   Just (SF y)  -> Just . fromField $ useProof y x

x =? v = case x ?= v of
          Just x -> x
          Nothing -> error "this implementation under uses the type system"

data EmployeeName = EmployeeName deriving Typeable
type instance FieldV EmployeeName = String

data EmployeeID = EmployeeID deriving Typeable
type instance FieldV EmployeeID = Int

employee =   (EmployeeName =: "James")
         :*: ((EmployeeID =: 5) :*: RNil)

employeeName = employee =? EmployeeName
employeeId   = employee =? EmployeeID

this is clearly not as good as the typeclass based version. But, if you are okay with a little dynamic typing...