Infer constraints for both if and else of type equality

I am trying to fill the hole in the following snippet

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

Is it possible?

Edit: Checked the source of sameNat and it turns out they use unsafeCoerce . I edited the code above accordingly.

---

One possible solution is to use the singletons library to get term-level functions representing the type-level ones (or vice-versa).

The gist of it is:

import Data.Singletons.Prelude

(...)

case (sing :: Sing a) %:== (sing :: Sing b) of
  STrue  -> Left Refl
  SFalse -> Right Refl

I've put up a self-contained file with all the imports and language extensions too.

链接地址: http://www.djcxy.com/p/43134.html

上一篇: 封闭式家庭的限制？

下一篇: 为类型相等的if和else推断约束