Type Family Not Evaluating

Question

I am quite new to type level programming in haskell and I'm stuck with the following example. It is a fragment of a type level type checker for a small dsl. I want the Find type family to return a proof that a given element is contained in Env, or force a compile time error otherwise.

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE UndecidableInstances #-}
import GHC.TypeLits

-- atomic data types in the source language
data Atom = Boolean

-- the typechecking environment
type Env = [(Symbol, Atom)]

-- A proof that a particular pair has been declared in the Env
data Elem (n :: Symbol) (a :: Atom) (e :: Env) where
  DH :: Elem n a ('(n,a):e)
  DT :: Elem n a e -> Elem n a (t:e)

-- Compile time type env lookup
type Find :: Symbol -> Atom -> Env -> Elem n a e
type family Find n a e where
  Find n a ('(n,a): e) = DH
  Find n a ('(t,p): e) = DT (Find n a e)
  Find n a '[] = TypeError (Text "name '" :<>: Text n :<>: Text "' not found in env")

However when I try to evaluate Find in ghci it seems to be stuck:

kind! Find "hi" Boolean '[ '("hi", Boolean) ]
Find "hi" Boolean '[ '("hi", Boolean) ] :: Elem n a e

I would expect this to reduce to DH :: Elem "hi" Boolean '[ '("hi", Boolean) ], but nothing seems to have happened. Have I somehow defined my type family incorrectly?

Raeraeann

Offhand, I'm not totally sure why :kind! isn't reducing it further, but evaluating this in GHCi seems to indicate that it is working () :: Find "hi" Boolean '[ '("hi", Boolean) ] ~ DH => () – Wore

I also see that :kind! Find "hi" Boolean '[ '("hi", Boolean) ] ~ DH gives back 'DH ~ 'DH – Wore

Thank you! That was very helpful. In the end my type family was stuck because of issues with constraint resolution, and the behaviour in ghci was a misleading red herring. – Raeraeann