Use leibniz equality

src/Type/Equality.purs

@@ -2,6 +2,8 @@ module Type.Equality
   ( class TypeEquals
   , to
   , from
+  , leibniz
+  , leibnizOp
   ) where
 
 -- | This type class asserts that types `a` and `b`
@@ -14,10 +16,26 @@ module Type.Equality
 -- | Note: any instance will necessarily overlap with
 -- | `refl` below, so instances of this class should
 -- | not be defined in libraries.
+class TypeEquals :: forall k. k -> k -> Constraint
 class TypeEquals a b | a -> b, b -> a where
-  to :: a -> b
-  from :: b -> a
+  leibniz :: forall p. p a -> p b
 
 instance refl :: TypeEquals a a where
-  to a = a
-  from a = a
+  leibniz a = a
+
+newtype Op :: forall k. k -> k -> Type
+newtype Op a b = Op (forall p. p b -> p a)
+
+leibnizOp :: forall p a b. TypeEquals a b => p b -> p a
+leibnizOp = case leibniz (Op (\pa -> pa) :: Op a a) of
+  (Op f :: Op a b) -> f
+
+newtype To a = To a
+
+to :: forall a b. TypeEquals a b => a -> b
+to a = case leibniz (To a) of
+  To b -> b
+
+from :: forall a b. TypeEquals a b => b -> a
+from b = case leibnizOp (To b) of
+  To a -> a

test/Main.purs

@@ -4,7 +4,7 @@ import Prelude
 import Effect (Effect)
 import Effect.Console (log)
 import Data.Newtype (class Newtype, unwrap)
-import Type.Equality (class TypeEquals, to, from)
+import Type.Equality (class TypeEquals, leibniz, to, from)
 
 newtype RecordNewtype = RecordNewtype
   { message :: String }
@@ -15,5 +15,8 @@ instance newtypeRecordNewtype ::
   wrap = RecordNewtype <<< to
   unwrap (RecordNewtype rec) = from rec
 
+test2 :: forall ty row. TypeEquals row ( message :: String ) => Newtype ty (Record row) => ty -> String
+test2 = unwrap >>> leibniz >>> _.message
+
 main :: Effect Unit
-main = log (unwrap (RecordNewtype { message: "Done" })).message
+main = log (test2 (RecordNewtype { message: "Done" }))