为类型相等的if和else推断约束
我正试图填补下面的代码片段中的漏洞
import Data.Proxy
import GHC.TypeLits
import Data.Type.Equality
import Data.Type.Bool
import Unsafe.Coerce
ifThenElse :: forall (a :: Nat) (b :: Nat) x l r.
(KnownNat a, KnownNat b, x ~ If (a==b) l r) =>
Proxy a -> Proxy b -> Either (x :~: l) (x :~: r)
ifThenElse pa pb = case sameNat pa pb of
Just Refl -> Left Refl
Nothing -> Right $ unsafeCoerce Refl -- This was the hole
可能吗？
编辑：检查sameNat的来源，结果他们使用unsafeCoerce 。 我相应地编辑了上面的代码。
一种可能的解决方案是使用singletons库来获取表示类型级别的term-level函数（反之亦然）。
其要点是：
import Data.Singletons.Prelude
（......）
case (sing :: Sing a) %:== (sing :: Sing b) of
STrue -> Left Refl
SFalse -> Right Refl
我已经创建了一个包含所有导入和语言扩展的自包含文件。
链接地址: http://www.djcxy.com/p/43133.html上一篇: Infer constraints for both if and else of type equality