haskell - 如果我知道它在运行时是真的，我如何告诉 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 这样的操作在这里说服 GHC 1 <= n是的——但我不能只使用 unsafeCoerce因为这会丢失 n 的类型级别值.
处理这个问题的最佳方法是什么？

Answer 1

再摸索了一下，我找到了Justin L's answer to a similar question .他将他的解决方案打包到 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 中的额外约束。返回 SomeMyType 的情况，但尝试在 NLE 中执行此操作case 仍然会给我们“无法将'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)

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