Getting a type-level ITE to fire

IfThenElse.hs

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE KindSignatures      #-}
{-# LANGUAGE TypeOperators       #-}
{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE TypeFamilies        #-}

module Ite where

import Data.Proxy
import GHC.TypeLits
import Data.Type.Equality
import Data.Singletons.Prelude

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 (sing :: Sing a) %:== (sing :: Sing b) of
  STrue  -> Left Refl
  SFalse -> Right Refl