Определить ограничения для обоих, если и остальное типа равенства

Я пытаюсь заполнить дыру в следующем фрагменте

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

Возможно ли это?

Edit: проверил источник sameNat и получается, что они используют unsafeCoerce. Я соответствующим образом отредактировал приведенный выше код.

1 2
haskell type-families

1 ответ:

Одним из возможных решений является использование библиотеки синглетов для получения функций уровня термов, представляющих функции уровня типов (или наоборот).

Суть его такова: 

import Data.Singletons.Prelude

(...) 

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

Я создал автономный файл со всеми импортами и языковыми расширениями.

2