从任意未知 Nats 中提取值

Question

给定类型级列表函数（来自这篇博文）

type family Length (xs :: [*]) :: Nat where
    Length '[] = 0
    Length (_ ': xs) = 1 + Length xs

“硬编码”类型列表长度的值提取按预期工作

t1 :: Integer
t1 = natVal (Proxy :: Proxy (Length '[Int]))

并且t1 = 1。但是，创建一个从任意列表中获取值的函数似乎失败了。

t2 :: forall (xs :: [*]). Proxy xs -> Integer
t2 _ = natVal (Proxy :: Proxy (Length xs))

给出错误

    • No instance for (KnownNat (Length xs))
        arising from a use of ‘natVal’

这似乎很不幸但合理，因为只有文字是“已知的”。但是，强制满足如下约束会导致对模棱两可的类型的抱怨。

unsafeKnownConstr :: c :~: (KnownNat n :: Constraint)
unsafeKnownConstr = unsafeCoerce Refl

t3 :: forall (xs :: [*]). Proxy xs -> Integer
t3 _ = case Proxy :: Proxy (Length xs) of
         p@(_ :: Proxy l) -> case unsafeKnownConstr @(KnownNat l) of
                             Refl -> natVal @l p

具体来说，

    • Could not deduce (KnownNat n0) arising from a use of ‘natVal’
      from the context: KnownNat n0 ~ KnownNat (Length xs)
        bound by a pattern with constructor:
                   Refl :: forall k (a :: k). a :~: a,
                 in a case alternative
...
      The type variable ‘n0’ is ambiguous

GHC (8.10.4) 在这里抱怨什么？或者，是否有另一种方法来提取这些未知的 Nats？