类型系列未评估

tjk*_*k42 6 haskell type-families

我对 haskell 中的类型级编程很陌生,并且我坚持使用以下示例。它是小型 dsl 的类型级别类型检查器的片段。我希望Find类型族返回给定元素包含在 中的证明Env,否则强制编译时错误。

{-# 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")
Run Code Online (Sandbox Code Playgroud)

然而,当我尝试Find在 ghci 中评估时,它似乎被卡住了:

kind! Find "hi" Boolean '[ '("hi", Boolean) ]
Find "hi" Boolean '[ '("hi", Boolean) ] :: Elem n a e
Run Code Online (Sandbox Code Playgroud)

我预计这会减少到DH :: Elem "hi" Boolean '[ '("hi", Boolean) ],但似乎什么也没有发生。我是否以某种方式错误地定义了我的类型系列?