如果我知道它在运行时是真的，我如何告诉 GHC 满足类型级 <= 约束？

Question

我有一个由自然数参数化的类型n：

data MyType (n :: Nat) = MyType

对这种类型的操作仅在 时才有意义n > 0，因此我将其指定为约束：

myFunction :: (KnownNat n, 1 <= n) => MyType n -> MyType n
myFunction = id

（请注意，这些功能的真正的版本做用n将其变成一个值natVal。）

我想创建一个存在类型 ( SomeMyType)，让我们n在运行时选择一个：

data SomeMyType where
  SomeMyType :: forall n. (KnownNat n, 1 <= n) => MyType n -> SomeMyType

为了产生 的值SomeMyType，我正在编写一个someMyTypeVal函数，其工作方式如下someNatVal：

someMyTypeVal :: Integer -> Maybe SomeMyType
someMyTypeVal n
  | n > 0 = case someNatVal n of
      Just (SomeNat (_ :: p n)) -> Just (SomeMyType (MyType @n))
      Nothing                   -> Nothing
  | otherwise = Nothing

这在没有1 <= n约束的情况下可以正常工作，但是在约束下我得到以下类型错误：

• Couldn't match type ‘1 <=? n’ with ‘'True’
    arising from a use of ‘SomeMyType’

我怎样才能绕过这个限制？因为我已经n > 0在运行时检查过了，所以我不介意使用像unsafeCoerce这里这样的操作来说服 GHC1 <= n是真的——但我不能只是使用，unsafeCoerce因为这会丢失n.

处理这个问题的最佳方法是什么？

Answer 1

在多摸了摸之后，我找到了Justin L 对类似问题的回答。他将他的解决方案typelits-witnesses打包到我可以用来非常干净地解决这个问题的包中：

someMyTypeVal :: Integer -> Maybe SomeMyType
someMyTypeVal n = someNatVal n >>= check
  where check :: SomeNat -> Maybe SomeMyType
        check (SomeNat (_ :: p n)) = case (SNat @1) %<=? (SNat @n) of
          LE Refl -> Just (SomeMyType (MyType @n))
          NLE _ _ -> Nothing

a %<=? b让我们比较两个类型级别的自然数，并为我们提供是否a小于b( LE) 或不小于( )的证明NLE。这在LE返回 a的情况下为我们提供了额外的约束SomeMyType，但在这种NLE情况下尝试这样做仍然会给我们带来“无法将 '1 <=? n' 与 ''True' 匹配”的错误。

注意check--没有它的显式类型签名，类型check被推断为check :: SomeNat -> Maybe a，我会得到以下类型错误：

• Couldn't match type ‘a’ with ‘SomeMyType’
   ‘a’ is untouchable
     inside the constraints: 'True ~ (1 <=? n)

使用显式类型签名，一切正常，代码甚至（合理）可读。