{-# LANGUAGE TypeFamilyDependencies #-}
module M where

import Data.Type.Equality

type family Bar x = y | y -> x where
  Bar String = Int
  Bar () = Bool
 
foo :: Bar s ~ Bar t => s :~: t
foo = Refl