在Haskell中，类型被擦除，它们在运行时不存在。DataKinds允许您在类型中使用数据构造函数，但它们仍然会被擦除。在forall n. Vec A n -> Nat类型的函数中，不可能返回n，因为它将被擦除。
为了使n不被擦除，您将拥有一个依赖于运行时值n的类型Vec A n，这就是依赖类型的含义。
依赖类型还不是Haskell的原生特性。但是，可以使用singletons模拟它们。length的类型将是forall n. SingI n => Vec A n -> Nat，其中SingI约束提供n的运行时反射。

在Haskell中，类型在运行时不存在。仅用于源代码中的表达式分类，不用于运行时的值分类。
当然，你可以使用data JObject (className :: Symbol) = ...，并使用它来强制一个只适用于某个特定Java类对象的函数，永远不会为另一个类名指定JObject。您甚至可以确保组合了同一类的两个Java对象的代码永远不会给JObject的不匹配类，即使在不知道实际类名是什么的多态上下文中也是如此。但所有这些都是关于你的 * 代码 *。在运行时，当内存中存在实际的JObject时，它只是不包含className。没什么可提取的。
然而，它**是可能的，使你可以访问className，就好像它是一个值而不是一个类型。您需要的是一个可以调用的函数，该函数在classNameSymbol上进行参数化，该函数将生成运行时String值。在Haskell中，创建一个对类型参数的每个可能值都有不同行为的函数的标准方法是使用类型类。你只需要一个类，它的方法给你一个String值，然后为每个可能的Symbol提供一个示例，通过返回相应的String来实现这个方法。很简单!
幸运的是，GHC实际上为每个Symbol提供了一个内置类，其中包含魔术示例，因此没有人需要手工编写所有这些示例。它被称为KnownSymbol。方法symbolSing @s实际上给出了一个SSymbol s，而不是直接给出String，但您可以通过调用fromSymbol来获得它。
KnownSymbol类除了神奇地拥有无限数量的离散示例之外，它是一个非常普通的类。这意味着，如果您所拥有的只是一个未知Symbol上的参数化类型，则无法自动获取KnownSymbol示例;您必须确保在函数上使用正确的约束，以便从实际选择Symbol的KnownSymbol示例流到您想要知道它是什么的地方。
SSymbol类型是一种称为“单例”的技术（不要与OO语言中的“单例模式”混淆）。它只意味着一个参数化的类型，其值与类型参数的选择一一对应。即SSymbol s是Symbols的每个选择的单独类型;这些类型中的每一个都只有一个值（因此称为“单例”），因此知道我们拥有哪个值可以揭示其对应的Symbol是什么，即使Symbol在技术上在运行时不存在。使用这些单例类型作为链接允许比仅仅具有直接链接类型和值的类更多的选项，即使在简单情况下不一定需要。如果您感兴趣，singletons library是一个更一般地定义和使用单例类型的框架（与base提供的极少数类型相反，因为它们需要编译器支持“魔术示例”）。

这实际上是可行的。演示：

{-# LANGUAGE DataKinds #-}
  {-# LANGUAGE GADTs #-}
    
  import GHC.Types
  import GHC.TypeLits
  import Data.Proxy

  data JavaObj :: Symbol -> * where
     JavaObj :: JavaObj a

  getJavaObjClassName :: KnownSymbol a => JavaObj a -> String
  getJavaObjClassName (_ :: JavaObj a) = symbolVal (Proxy :: Proxy a)

  mbd = JavaObj :: JavaObj "java.math.BigDecimal"

  main = do
    putStrLn (getJavaObjClassName mbd)

解释。
1.在类型上下文中，字符串字面量被提升为GHC.Types.Symbol，因此我们需要使用它作为我们的数据类型。

1. KnownSymbol a =>正是在运行时不会擦除a的对象。它拖动一个字典，可以用来恢复字符串（通过Proxy）。
   (This可能不是最惯用的方法，我不是一个Maven在野生和美妙的Haskell扩展）。