diff --git a/libraries/base/Unsafe/Coerce.hs b/libraries/base/Unsafe/Coerce.hs
index 0b35eeca1b761c9a4907ad553bcc6670e083e174..3b70450b9c426afdb66a10014b57f6b3b4de21d1 100644
--- a/libraries/base/Unsafe/Coerce.hs
+++ b/libraries/base/Unsafe/Coerce.hs
@@ -8,6 +8,7 @@
 {-# LANGUAGE MagicHash #-}
 {-# LANGUAGE NoImplicitPrelude #-}
 {-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE Unsafe #-}
@@ -16,6 +17,16 @@ module Unsafe.Coerce
   ( unsafeCoerce, unsafeCoerceUnlifted, unsafeCoerceAddr
   , unsafeEqualityProof
   , UnsafeEquality (..)
+  , symUnsafe
+  , transUnsafe
+  , castWithUnsafe
+  , gcastWithUnsafe
+  , applyUnsafe
+  , congUnsafe
+  , cong2Unsafe
+  , congAppUnsafe
+  , innerUnsafe
+  , outerUnsafe
   , unsafeCoerce#
   ) where
 
@@ -278,6 +289,64 @@ unsafeCoerceAddr :: forall (a :: TYPE 'AddrRep) (b :: TYPE 'AddrRep) . a -> b
 -- Kind-homogeneous, but representation-monomorphic (TYPE AddrRep)
 unsafeCoerceAddr x = case unsafeEqualityProof @a @b of UnsafeRefl -> x
 
+-- Unsafe equality utilities
+
+-- | Symmetry of unsafe equality
+symUnsafe :: UnsafeEquality a b -> UnsafeEquality b a
+symUnsafe UnsafeRefl = UnsafeRefl
+
+-- | Transitivity of unsafe equality
+transUnsafe :: UnsafeEquality a b -> UnsafeEquality b c -> UnsafeEquality a c
+transUnsafe UnsafeRefl bc = bc
+
+-- | Unsafe cast, using unsafe equality proof
+castWithUnsafe :: UnsafeEquality a b -> a -> b
+castWithUnsafe UnsafeRefl x = x
+
+-- | Generalized form of unsafe cast using unsafe equality proof
+--
+-- === Caution
+--
+-- This function is more limited than one might initially expect. In
+-- particular, GHC eagerly rejects constraints it sees as obviously
+-- unsatisfiable, so you cannot construct a function of type @Int ~ Char => r@
+-- to pass to @gcastWithUnsafe@.
+gcastWithUnsafe :: forall {rep} a b (r :: TYPE rep).
+  UnsafeEquality a b -> (a ~ b => r) -> r
+gcastWithUnsafe UnsafeRefl x = x
+
+-- | Apply one unsafe equality proof to another
+applyUnsafe :: UnsafeEquality f g -> UnsafeEquality a b -> UnsafeEquality (f a) (g b)
+applyUnsafe UnsafeRefl UnsafeRefl = UnsafeRefl
+
+-- | Apply an unsafe equality proof to a type argument
+--
+-- @ congUnsafe ab = 'applyUnsafe' 'UnsafeRefl' ab @
+congUnsafe :: UnsafeEquality a b -> UnsafeEquality (f a) (f b)
+congUnsafe UnsafeRefl = UnsafeRefl
+
+-- | Apply unsafe equality proofs to two type arguments
+--
+-- @ cong2Unsafe aa' bb' = 'applyUnsafe' ('congUnsafe' aa') bb' @
+cong2Unsafe :: UnsafeEquality a a' -> UnsafeEquality b b' -> UnsafeEquality (f a b) (f a' b')
+cong2Unsafe UnsafeRefl UnsafeRefl = UnsafeRefl
+
+-- | Apply an unsafe equality proof to an applied type
+--
+-- @ congAppUnsafe fg = 'applyUnsafe' fg 'UnsafeRefl' @
+congAppUnsafe :: UnsafeEquality f g -> UnsafeEquality (f a) (g a)
+congAppUnsafe UnsafeRefl = UnsafeRefl
+
+-- | Extract unsafe equality of the arguments from an unsafe equality of
+-- applied types
+innerUnsafe :: UnsafeEquality (f a) (g b) -> UnsafeEquality a b
+innerUnsafe UnsafeRefl = UnsafeRefl
+
+-- | Extract unsafe equality of type constructors from an unsafe equality of
+-- applied types
+outerUnsafe :: UnsafeEquality (f a) (g b) -> UnsafeEquality f g
+outerUnsafe UnsafeRefl = UnsafeRefl
+
 -- | Highly, terribly dangerous coercion from one representation type
 -- to another. Misuse of this function can invite the garbage collector
 -- to trounce upon your data and then laugh in your face. You don't want