我对 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 …