title: Infer constraints for both if and else of type equality
body: <p>I am trying to fill the hole in the following snippet</p>
  
  <pre><code>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) =&gt;
    Proxy a -&gt; Proxy b -&gt; Either (x :~: l) (x :~: r)
  ifThenElse pa pb = case sameNat pa pb of
    Just Refl -&gt; Left Refl
    Nothing -&gt; Right $ unsafeCoerce Refl -- This was the hole
  </code></pre>
  
  <p>Is it possible?</p>
  
  <p>Edit: Checked the source of <a href="https://hackage.haskell.org/package/base-4.9.1.0/docs/GHC-TypeLits.html#v:sameNat" rel="nofollow noreferrer"><code>sameNat</code></a> and it turns out they use <code>unsafeCoerce</code>. I edited the code above accordingly.</p>