Type safe lookup on heterogeneous lists in Haskell

Question

I want to develop a type safe lookup function for the following data type:

data Attr (xs :: [(Symbol,*)]) where
   Nil  :: Attr '[]
   (:*) :: KnownSymbol s => (Proxy s, t) -> Attr xs -> Attr ('(s , t) ': xs)

The obvious lookup function would be like:

 lookupAttr :: (KnownSymbol s, Lookup s env ~ 'Just t) => Proxy s -> Attr env -> t
 lookupAttr s ((s',t) :* env')
       = case sameSymbol s s' of
            Just Refl -> t
            Nothing   -> lookupAttr s env'

where Lookup type family is defined in singletons library. This definition fails to type check on GHC 7.10.3 with the following error message:

 Could not deduce (Lookup s xs ~ 'Just t)
   from the context (KnownSymbol s, Lookup s env ~ 'Just t)
      bound by the type signature for
             lookupAttr :: (KnownSymbol s, Lookup s env ~ 'Just t) =>
                           Proxy s -> Attr env -> t

This message is generated for the recursive call lookupAttr s env'. This is reasonable, since we have that if

Lookup s ('(s',t') ': env) ~ 'Just t

holds, and

s :~: s'

isn't provable, then

Lookup s env ~ 'Just t

must hold. My question is, how can I convince Haskell type checker that this is indeed true?

Answer 1

Lookup is defined in terms of :== equality, which comes from here. Roughly, Lookup is implemented this way:

type family Lookup (x :: k) (xs :: [(k, v)]) :: Maybe v where
  Lookup x '[] = Nothing
  Lookup x ('(x' , v) ': xs) = If (x :== x') (Just v) (Lookup x xs)

Pattern matching on sameSymbol s s' doesn't give us any information about Lookup s env, and doesn't let GHC reduce it. We need to know about s :== s', and for that we need to use the singleton version of :==.

data Attr (xs :: [(Symbol,*)]) where
   Nil  :: Attr '[]
   (:*) :: (Sing s, t) -> Attr xs -> Attr ('(s , t) ': xs)

lookupAttr :: (Lookup s env ~ 'Just t) => Sing s -> Attr env -> t
lookupAttr s ((s', t) :* env') = case s %:== s' of
  STrue  -> t
  SFalse -> lookupAttr s env'

Generally, you shouldn't use KnownSymbol, sameSymbol, or any of the stuff in GHC.TypeLits because they're too "low-level" and don't play along with singletons by default.

Of course, you can write your own Lookup and other functions, and don't need to use the singletons imports; what matters is that you synchronize term level and type level, so that term level pattern matching produces relevant information for type level.