Leibniz equality as a quantified constraint with safe reification and reflection

LeibnizC.hs

{-# LANGUAGE QuantifiedConstraints
           , UndecidableInstances
           , AllowAmbiguousTypes
#-}
{-# OPTIONS_GHC -Wno-simplifiable-class-constraints #-}

module LeibnizC where

import Leibniz

class    (forall c. c a => c b) => a <~> b
instance (forall c. c a => c b) => a <~> b

reify :: a <~> b => a := b
reify = refl

data Dict c a = c a => Dict

reflect :: forall a b r. a := b -> (a <~> b => r) -> r
reflect aforb r = case substitute aforb (Dict @((<~>) a)) of
  Dict -> r

toLeibnizC :: a ~ b => (a <~> b => r) -> r
toLeibnizC r = r

fromLeibnizC :: a <~> b => (a ~ b => r) -> r
fromLeibnizC r = r

reflC :: (a <~> a => r) -> r
reflC r = r

transC :: forall a b c r. (a <~> b, b <~> c) => (a <~> c => r) -> r
transC r = r

castC :: a <~> b => a -> b
castC x = x