diff --git a/plutus-core/plutus-core/src/PlutusCore/Builtin/Polymorphism.hs b/plutus-core/plutus-core/src/PlutusCore/Builtin/Polymorphism.hs
index 19bc3481043..7a0ffc5bb82 100644
--- a/plutus-core/plutus-core/src/PlutusCore/Builtin/Polymorphism.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/Builtin/Polymorphism.hs
@@ -8,6 +8,7 @@
 {-# LANGUAGE TypeFamilies             #-}
 {-# LANGUAGE TypeOperators            #-}
 {-# LANGUAGE UndecidableInstances     #-}
+{-# LANGUAGE UndecidableSuperClasses  #-}
 
 module PlutusCore.Builtin.Polymorphism
     ( Opaque (..)
@@ -214,7 +215,8 @@ type family AllElaboratedArgs constr x where
 -- built-in type.
 type AllBuiltinArgs
         :: forall a. (GHC.Type -> GHC.Type) -> (GHC.Type -> GHC.Constraint) -> a -> GHC.Constraint
-type AllBuiltinArgs uni constr x = AllElaboratedArgs constr (ElaborateBuiltin uni x)
+class    AllElaboratedArgs constr (ElaborateBuiltin uni x) => AllBuiltinArgs uni constr x
+instance AllElaboratedArgs constr (ElaborateBuiltin uni x) => AllBuiltinArgs uni constr x
 
 -- Custom type errors to guide the programmer adding a new built-in function.
 
diff --git a/plutus-ledger-api/test-plugin/Spec/Value.hs b/plutus-ledger-api/test-plugin/Spec/Value.hs
index 87ad1c6ec24..45a66451fe9 100644
--- a/plutus-ledger-api/test-plugin/Spec/Value.hs
+++ b/plutus-ledger-api/test-plugin/Spec/Value.hs
@@ -157,7 +157,7 @@ valueToLists = ListTx.map (fmap AssocMap.toList) . AssocMap.toList . getValue
 eqValueCode :: CompiledCode Value -> CompiledCode Value -> (Bool, PLC.CountingSt)
 eqValueCode valueCode1 valueCode2 = (res, cost) where
     prog =
-        $$(compile [|| \value1 value2 -> toBuiltin ((value1 :: Value) == value2) ||])
+        $$(compile [|| \value1 value2 -> toOpaque ((value1 :: Value) == value2) ||])
             `unsafeApplyCode` valueCode1 `unsafeApplyCode` valueCode2
     (errOrRes, cost)
         = PLC.runCekNoEmit PLC.defaultCekParameters PLC.counting
diff --git a/plutus-tx-plugin/src/PlutusTx/Compiler/Builtins.hs b/plutus-tx-plugin/src/PlutusTx/Compiler/Builtins.hs
index 077f99932eb..b0d8e6b15aa 100644
--- a/plutus-tx-plugin/src/PlutusTx/Compiler/Builtins.hs
+++ b/plutus-tx-plugin/src/PlutusTx/Compiler/Builtins.hs
@@ -18,7 +18,7 @@ module PlutusTx.Compiler.Builtins (
     , lookupBuiltinType
     , errorFunc) where
 
-import PlutusTx.Builtins.Class qualified as Builtins
+import PlutusTx.Builtins.HasOpaque qualified as Builtins
 import PlutusTx.Builtins.Internal qualified as Builtins
 
 import PlutusTx.Compiler.Error
diff --git a/plutus-tx-plugin/src/PlutusTx/Compiler/Expr.hs b/plutus-tx-plugin/src/PlutusTx/Compiler/Expr.hs
index 32ab0827668..f8f4b8459ea 100644
--- a/plutus-tx-plugin/src/PlutusTx/Compiler/Expr.hs
+++ b/plutus-tx-plugin/src/PlutusTx/Compiler/Expr.hs
@@ -49,7 +49,7 @@ import PlutusTx.PIRTypes
 import PlutusTx.PLCTypes (PLCType, PLCVar)
 
 -- I feel like we shouldn't need this, we only need it to spot the special String type, which is annoying
-import PlutusTx.Builtins.Class qualified as Builtins
+import PlutusTx.Builtins.HasOpaque qualified as Builtins
 import PlutusTx.Trace
 
 import PlutusIR qualified as PIR
diff --git a/plutus-tx-plugin/test/Plugin/Primitives/9.6/deconstructorData2.pir.golden b/plutus-tx-plugin/test/Plugin/Primitives/9.6/deconstructorData2.pir.golden
index b40f8b55eb0..2919c2b1560 100644
--- a/plutus-tx-plugin/test/Plugin/Primitives/9.6/deconstructorData2.pir.golden
+++ b/plutus-tx-plugin/test/Plugin/Primitives/9.6/deconstructorData2.pir.golden
@@ -247,6 +247,14 @@
             )
           )
         )
+        (termbind
+          (nonstrict)
+          (vardecl
+            `$fHasFromOpaqueBuiltinDataBuiltinData_$cfromOpaque`
+            (fun (con data) (con data))
+          )
+          (lam eta (con data) eta)
+        )
         (termbind
           (strict)
           (vardecl
@@ -271,7 +279,7 @@
         (termbind
           (nonstrict)
           (vardecl
-            `$fFromBuiltinBuiltinListList_$cfromBuiltin`
+            `$fHasFromOpaqueBuiltinListList_$cfromOpaque`
             (all
               arep
               (type)
@@ -292,7 +300,7 @@
               a
               (type)
               (lam
-                `$dFromBuiltin`
+                `$dHasFromOpaque`
                 [ [ (lam arep (type) (lam a (type) (fun arep a))) arep ] a ]
                 (let
                   (rec)
@@ -323,7 +331,7 @@
                               [
                                 [
                                   { Cons a }
-                                  [ `$dFromBuiltin` [ { head arep } l ] ]
+                                  [ `$dHasFromOpaque` [ { head arep } l ] ]
                                 ]
                                 [ go [ { tail arep } l ] ]
                               ]
@@ -347,11 +355,6 @@
           )
           (builtin fstPair)
         )
-        (termbind
-          (nonstrict)
-          (vardecl id (all a (type) (fun a a)))
-          (abs a (type) (lam x a x))
-        )
         (termbind
           (strict)
           (vardecl
@@ -405,12 +408,12 @@
                     [
                       {
                         {
-                          `$fFromBuiltinBuiltinListList_$cfromBuiltin`
+                          `$fHasFromOpaqueBuiltinListList_$cfromOpaque`
                           (con data)
                         }
                         (con data)
                       }
-                      { id (con data) }
+                      `$fHasFromOpaqueBuiltinDataBuiltinData_$cfromOpaque`
                     ]
                     a
                   ]
diff --git a/plutus-tx/changelog.d/20240513_014001_effectfully_split_FromBuiltin_and_ToBuiltin_into_IsBuiltin_and_IsOpaque.md b/plutus-tx/changelog.d/20240513_014001_effectfully_split_FromBuiltin_and_ToBuiltin_into_IsBuiltin_and_IsOpaque.md
new file mode 100644
index 00000000000..053aa96f62a
--- /dev/null
+++ b/plutus-tx/changelog.d/20240513_014001_effectfully_split_FromBuiltin_and_ToBuiltin_into_IsBuiltin_and_IsOpaque.md
@@ -0,0 +1,5 @@
+### Changed
+
+- Split `PlutusTx.Builtins.Class` into `PlutusTx.Builtins.HasBuiltin` and `PlutusTx.Builtins.HasOpaque` in #5971:
++ Split 'FromBuiltin' into 'HasFromBuiltin' and 'HasFromOpaque'
++ Split 'ToBuiltin' into 'HasToBuiltin' and 'HasToOpaque'
diff --git a/plutus-tx/plutus-tx.cabal b/plutus-tx/plutus-tx.cabal
index 7d0786a3b58..fa3513d81f2 100644
--- a/plutus-tx/plutus-tx.cabal
+++ b/plutus-tx/plutus-tx.cabal
@@ -70,7 +70,8 @@ library
     PlutusTx.Blueprint.Write
     PlutusTx.Bool
     PlutusTx.Builtins
-    PlutusTx.Builtins.Class
+    PlutusTx.Builtins.HasBuiltin
+    PlutusTx.Builtins.HasOpaque
     PlutusTx.Builtins.Internal
     PlutusTx.Code
     PlutusTx.Coverage
@@ -108,6 +109,7 @@ library
     PlutusTx.IsData.Instances
     PlutusTx.IsData.TH
     PlutusTx.Lift.Instances
+    PlutusTx.Lift.TestInstances
     PlutusTx.Lift.TH
     PlutusTx.Lift.THUtils
 
diff --git a/plutus-tx/src/PlutusTx/Builtins.hs b/plutus-tx/src/PlutusTx/Builtins.hs
index 3f7c92e98e8..cfdd8cbe23e 100644
--- a/plutus-tx/src/PlutusTx/Builtins.hs
+++ b/plutus-tx/src/PlutusTx/Builtins.hs
@@ -103,6 +103,8 @@ module PlutusTx.Builtins (
                          , bls12_381_mulMlResult
                          , bls12_381_finalVerify
                          -- * Conversions
+                         , fromOpaque
+                         , toOpaque
                          , fromBuiltin
                          , toBuiltin
                          , integerToByteString
@@ -112,7 +114,8 @@ module PlutusTx.Builtins (
 import Data.Maybe
 import PlutusTx.Base (const, uncurry)
 import PlutusTx.Bool (Bool (..))
-import PlutusTx.Builtins.Class
+import PlutusTx.Builtins.HasBuiltin
+import PlutusTx.Builtins.HasOpaque
 import PlutusTx.Builtins.Internal (BuiltinBLS12_381_G1_Element (..),
                                    BuiltinBLS12_381_G2_Element (..), BuiltinBLS12_381_MlResult (..),
                                    BuiltinByteString (..), BuiltinData, BuiltinString)
@@ -129,12 +132,12 @@ appendByteString = BI.appendByteString
 {-# INLINABLE consByteString #-}
 -- | Adds a byte to the front of a 'ByteString'.
 consByteString :: Integer -> BuiltinByteString -> BuiltinByteString
-consByteString n bs = BI.consByteString (toBuiltin n) bs
+consByteString n bs = BI.consByteString (toOpaque n) bs
 
 {-# INLINABLE sliceByteString #-}
 -- | Returns the substring of a 'ByteString' from index 'start' of length 'n'.
 sliceByteString :: Integer -> Integer -> BuiltinByteString -> BuiltinByteString
-sliceByteString start n bs = BI.sliceByteString (toBuiltin start) (toBuiltin n) bs
+sliceByteString start n bs = BI.sliceByteString (toOpaque start) (toOpaque n) bs
 
 {-# INLINABLE lengthOfByteString #-}
 -- | Returns the length of a 'ByteString'.
@@ -144,7 +147,7 @@ lengthOfByteString = BI.lengthOfByteString
 {-# INLINABLE indexByteString #-}
 -- | Returns the byte of a 'ByteString' at index.
 indexByteString :: BuiltinByteString -> Integer -> Integer
-indexByteString b n = BI.indexByteString b (toBuiltin n)
+indexByteString b n = BI.indexByteString b (toOpaque n)
 
 {-# INLINABLE emptyByteString #-}
 -- | An empty 'ByteString'.
@@ -185,22 +188,23 @@ verifyEd25519Signature
     -> BuiltinByteString  -- ^ Message    (arbirtary length)
     -> BuiltinByteString  -- ^ Signature  (64 bytes)
     -> Bool
-verifyEd25519Signature pubKey message signature = fromBuiltin (BI.verifyEd25519Signature pubKey message signature)
+verifyEd25519Signature pubKey message signature =
+    fromOpaque (BI.verifyEd25519Signature pubKey message signature)
 
 {-# INLINABLE equalsByteString #-}
 -- | Check if two 'ByteString's are equal.
 equalsByteString :: BuiltinByteString -> BuiltinByteString -> Bool
-equalsByteString x y = fromBuiltin (BI.equalsByteString x y)
+equalsByteString x y = fromOpaque (BI.equalsByteString x y)
 
 {-# INLINABLE lessThanByteString #-}
 -- | Check if one 'ByteString' is less than another.
 lessThanByteString :: BuiltinByteString -> BuiltinByteString -> Bool
-lessThanByteString x y = fromBuiltin (BI.lessThanByteString x y)
+lessThanByteString x y = fromOpaque (BI.lessThanByteString x y)
 
 {-# INLINABLE lessThanEqualsByteString #-}
 -- | Check if one 'ByteString' is less than or equal to another.
 lessThanEqualsByteString :: BuiltinByteString -> BuiltinByteString -> Bool
-lessThanEqualsByteString x y = fromBuiltin (BI.lessThanEqualsByteString x y)
+lessThanEqualsByteString x y = fromOpaque (BI.lessThanEqualsByteString x y)
 
 {-# INLINABLE greaterThanByteString #-}
 -- | Check if one 'ByteString' is greater than another.
@@ -258,7 +262,7 @@ verifyEcdsaSecp256k1Signature
   -> BuiltinByteString -- ^ Signature (64 bytes)
   -> Bool
 verifyEcdsaSecp256k1Signature vk msg sig =
-  fromBuiltin (BI.verifyEcdsaSecp256k1Signature vk msg sig)
+  fromOpaque (BI.verifyEcdsaSecp256k1Signature vk msg sig)
 
 {-# INLINEABLE verifySchnorrSecp256k1Signature #-}
 -- | Given a Schnorr SECP256k1 verification key, a Schnorr SECP256k1 signature,
@@ -292,42 +296,42 @@ verifySchnorrSecp256k1Signature
   -> BuiltinByteString -- ^ Signature (64 bytes)
   -> Bool
 verifySchnorrSecp256k1Signature vk msg sig =
-  fromBuiltin (BI.verifySchnorrSecp256k1Signature vk msg sig)
+  fromOpaque (BI.verifySchnorrSecp256k1Signature vk msg sig)
 
 {-# INLINABLE addInteger #-}
 -- | Add two 'Integer's.
 addInteger :: Integer -> Integer -> Integer
-addInteger x y = fromBuiltin (BI.addInteger (toBuiltin x) (toBuiltin y))
+addInteger x y = fromOpaque (BI.addInteger (toOpaque x) (toOpaque y))
 
 {-# INLINABLE subtractInteger #-}
 -- | Subtract two 'Integer's.
 subtractInteger :: Integer -> Integer -> Integer
-subtractInteger x y = fromBuiltin (BI.subtractInteger (toBuiltin x) (toBuiltin y))
+subtractInteger x y = fromOpaque (BI.subtractInteger (toOpaque x) (toOpaque y))
 
 {-# INLINABLE multiplyInteger #-}
 -- | Multiply two 'Integer's.
 multiplyInteger :: Integer -> Integer -> Integer
-multiplyInteger x y = fromBuiltin (BI.multiplyInteger (toBuiltin x) (toBuiltin y))
+multiplyInteger x y = fromOpaque (BI.multiplyInteger (toOpaque x) (toOpaque y))
 
 {-# INLINABLE divideInteger #-}
 -- | Divide two integers.
 divideInteger :: Integer -> Integer -> Integer
-divideInteger x y = fromBuiltin (BI.divideInteger (toBuiltin x) (toBuiltin y))
+divideInteger x y = fromOpaque (BI.divideInteger (toOpaque x) (toOpaque y))
 
 {-# INLINABLE modInteger #-}
 -- | Integer modulo operation.
 modInteger :: Integer -> Integer -> Integer
-modInteger x y = fromBuiltin (BI.modInteger (toBuiltin x) (toBuiltin y))
+modInteger x y = fromOpaque (BI.modInteger (toOpaque x) (toOpaque y))
 
 {-# INLINABLE quotientInteger #-}
 -- | Quotient of two integers.
 quotientInteger :: Integer -> Integer -> Integer
-quotientInteger x y = fromBuiltin (BI.quotientInteger (toBuiltin x) (toBuiltin y))
+quotientInteger x y = fromOpaque (BI.quotientInteger (toOpaque x) (toOpaque y))
 
 {-# INLINABLE remainderInteger #-}
 -- | Take the remainder of dividing two 'Integer's.
 remainderInteger :: Integer -> Integer -> Integer
-remainderInteger x y = fromBuiltin (BI.remainderInteger (toBuiltin x) (toBuiltin y))
+remainderInteger x y = fromOpaque (BI.remainderInteger (toOpaque x) (toOpaque y))
 
 {-# INLINABLE greaterThanInteger #-}
 -- | Check whether one 'Integer' is greater than another.
@@ -342,22 +346,22 @@ greaterThanEqualsInteger x y = BI.ifThenElse (BI.lessThanInteger x y) False True
 {-# INLINABLE lessThanInteger #-}
 -- | Check whether one 'Integer' is less than another.
 lessThanInteger :: Integer -> Integer -> Bool
-lessThanInteger x y = fromBuiltin (BI.lessThanInteger (toBuiltin x) (toBuiltin y))
+lessThanInteger x y = fromOpaque (BI.lessThanInteger (toOpaque x) (toOpaque y))
 
 {-# INLINABLE lessThanEqualsInteger #-}
 -- | Check whether one 'Integer' is less than or equal to another.
 lessThanEqualsInteger :: Integer -> Integer -> Bool
-lessThanEqualsInteger x y = fromBuiltin (BI.lessThanEqualsInteger (toBuiltin x) (toBuiltin y))
+lessThanEqualsInteger x y = fromOpaque (BI.lessThanEqualsInteger (toOpaque x) (toOpaque y))
 
 {-# INLINABLE equalsInteger #-}
 -- | Check if two 'Integer's are equal.
 equalsInteger :: Integer -> Integer -> Bool
-equalsInteger x y = fromBuiltin (BI.equalsInteger (toBuiltin x) (toBuiltin y))
+equalsInteger x y = fromOpaque (BI.equalsInteger (toOpaque x) (toOpaque y))
 
 {-# INLINABLE error #-}
 -- | Aborts evaluation with an error.
 error :: () -> a
-error x = BI.error (toBuiltin x)
+error x = BI.error (toOpaque x)
 
 {-# INLINABLE appendString #-}
 -- | Append two 'String's.
@@ -372,7 +376,7 @@ emptyString = BI.emptyString
 {-# INLINABLE equalsString #-}
 -- | Check if two strings are equal
 equalsString :: BuiltinString -> BuiltinString -> Bool
-equalsString x y = fromBuiltin (BI.equalsString x y)
+equalsString x y = fromOpaque (BI.equalsString x y)
 
 {-# INLINABLE trace #-}
 -- | Emit the given string as a trace message before evaluating the argument.
@@ -426,17 +430,17 @@ serialiseData = BI.serialiseData
 {-# INLINABLE mkConstr #-}
 -- | Constructs a 'BuiltinData' value with the @Constr@ constructor.
 mkConstr :: Integer -> [BuiltinData] -> BuiltinData
-mkConstr i args = BI.mkConstr (toBuiltin i) (toBuiltin args)
+mkConstr i args = BI.mkConstr (toOpaque i) (toOpaque args)
 
 {-# INLINABLE mkMap #-}
 -- | Constructs a 'BuiltinData' value with the @Map@ constructor.
 mkMap :: [(BuiltinData, BuiltinData)] -> BuiltinData
-mkMap es = BI.mkMap (toBuiltin es)
+mkMap es = BI.mkMap (toOpaque es)
 
 {-# INLINABLE mkList #-}
 -- | Constructs a 'BuiltinData' value with the @List@ constructor.
 mkList :: [BuiltinData] -> BuiltinData
-mkList l = BI.mkList (toBuiltin l)
+mkList l = BI.mkList (toOpaque l)
 
 {-# INLINABLE mkI #-}
 -- | Constructs a 'BuiltinData' value with the @I@ constructor.
@@ -451,22 +455,22 @@ mkB = BI.mkB
 {-# INLINABLE unsafeDataAsConstr #-}
 -- | Deconstructs a 'BuiltinData' as a @Constr@, or fails if it is not one.
 unsafeDataAsConstr :: BuiltinData -> (Integer, [BuiltinData])
-unsafeDataAsConstr d = fromBuiltin (BI.unsafeDataAsConstr d)
+unsafeDataAsConstr d = fromOpaque (BI.unsafeDataAsConstr d)
 
 {-# INLINABLE unsafeDataAsMap #-}
 -- | Deconstructs a 'BuiltinData' as a @Map@, or fails if it is not one.
 unsafeDataAsMap :: BuiltinData -> [(BuiltinData, BuiltinData)]
-unsafeDataAsMap d = fromBuiltin (BI.unsafeDataAsMap d)
+unsafeDataAsMap d = fromOpaque (BI.unsafeDataAsMap d)
 
 {-# INLINABLE unsafeDataAsList #-}
 -- | Deconstructs a 'BuiltinData' as a @List@, or fails if it is not one.
 unsafeDataAsList :: BuiltinData -> [BuiltinData]
-unsafeDataAsList d = fromBuiltin (BI.unsafeDataAsList d)
+unsafeDataAsList d = fromOpaque (BI.unsafeDataAsList d)
 
 {-# INLINABLE unsafeDataAsI #-}
 -- | Deconstructs a 'BuiltinData' as an @I@, or fails if it is not one.
 unsafeDataAsI :: BuiltinData -> Integer
-unsafeDataAsI d = fromBuiltin (BI.unsafeDataAsI d)
+unsafeDataAsI d = fromOpaque (BI.unsafeDataAsI d)
 
 {-# INLINABLE unsafeDataAsB #-}
 -- | Deconstructs a 'BuiltinData' as a @B@, or fails if it is not one.
@@ -476,7 +480,7 @@ unsafeDataAsB = BI.unsafeDataAsB
 {-# INLINABLE equalsData #-}
 -- | Check if two 'BuiltinData's are equal.
 equalsData :: BuiltinData -> BuiltinData -> Bool
-equalsData d1 d2 = fromBuiltin (BI.equalsData d1 d2)
+equalsData d1 d2 = fromOpaque (BI.equalsData d1 d2)
 
 {-# INLINABLE matchData #-}
 -- | Given a 'BuiltinData' value and matching functions for the five constructors,
@@ -523,7 +527,7 @@ matchData' d constrCase mapCase listCase iCase bCase =
 -- G1 --
 {-# INLINABLE bls12_381_G1_equals #-}
 bls12_381_G1_equals :: BuiltinBLS12_381_G1_Element -> BuiltinBLS12_381_G1_Element -> Bool
-bls12_381_G1_equals a b = fromBuiltin (BI.bls12_381_G1_equals a b)
+bls12_381_G1_equals a b = fromOpaque (BI.bls12_381_G1_equals a b)
 
 {-# INLINABLE bls12_381_G1_add #-}
 bls12_381_G1_add :: BuiltinBLS12_381_G1_Element -> BuiltinBLS12_381_G1_Element -> BuiltinBLS12_381_G1_Element
@@ -560,7 +564,7 @@ bls12_381_G1_compressed_generator = BI.bls12_381_G1_compressed_generator
 -- G2 --
 {-# INLINABLE bls12_381_G2_equals #-}
 bls12_381_G2_equals :: BuiltinBLS12_381_G2_Element -> BuiltinBLS12_381_G2_Element -> Bool
-bls12_381_G2_equals a b = fromBuiltin (BI.bls12_381_G2_equals a b)
+bls12_381_G2_equals a b = fromOpaque (BI.bls12_381_G2_equals a b)
 
 {-# INLINABLE bls12_381_G2_add #-}
 bls12_381_G2_add :: BuiltinBLS12_381_G2_Element -> BuiltinBLS12_381_G2_Element -> BuiltinBLS12_381_G2_Element
@@ -605,7 +609,7 @@ bls12_381_mulMlResult = BI.bls12_381_mulMlResult
 
 {-# INLINABLE bls12_381_finalVerify #-}
 bls12_381_finalVerify :: BuiltinBLS12_381_MlResult -> BuiltinBLS12_381_MlResult -> Bool
-bls12_381_finalVerify a b = fromBuiltin (BI.bls12_381_finalVerify a b)
+bls12_381_finalVerify a b = fromOpaque (BI.bls12_381_finalVerify a b)
 
 -- Bitwise conversions
 
@@ -632,7 +636,7 @@ byteOrderToBool LittleEndian = False
 -- fit into a bytestring of length 8192.
 {-# INLINABLE integerToByteString #-}
 integerToByteString :: ByteOrder -> Integer -> Integer -> BuiltinByteString
-integerToByteString endianness = BI.integerToByteString (toBuiltin (byteOrderToBool endianness))
+integerToByteString endianness = BI.integerToByteString (toOpaque (byteOrderToBool endianness))
 
 -- | Convert a 'BuiltinByteString' to a 'BuiltinInteger', as described in
 -- [CIP-0087](https://github.com/mlabs-haskell/CIPs/tree/koz/to-from-bytestring/CIP-XXXX).
@@ -642,4 +646,4 @@ integerToByteString endianness = BI.integerToByteString (toBuiltin (byteOrderToB
 {-# INLINABLE byteStringToInteger #-}
 byteStringToInteger :: ByteOrder -> BuiltinByteString -> Integer
 byteStringToInteger endianness =
-  BI.byteStringToInteger (toBuiltin (byteOrderToBool endianness))
+  BI.byteStringToInteger (toOpaque (byteOrderToBool endianness))
diff --git a/plutus-tx/src/PlutusTx/Builtins/Class.hs b/plutus-tx/src/PlutusTx/Builtins/Class.hs
deleted file mode 100644
index a6de8b9223a..00000000000
--- a/plutus-tx/src/PlutusTx/Builtins/Class.hs
+++ /dev/null
@@ -1,250 +0,0 @@
--- editorconfig-checker-disable-file
-{-# LANGUAGE FlexibleInstances      #-}
-{-# LANGUAGE FunctionalDependencies #-}
-{-# LANGUAGE TypeFamilies           #-}
-{-# LANGUAGE UndecidableInstances   #-}
-
-{-# OPTIONS_GHC -Wno-orphans #-}
-{-# OPTIONS_GHC -fno-specialise #-}
-{-# OPTIONS_GHC -fno-omit-interface-pragmas #-}
-
-module PlutusTx.Builtins.Class where
-
-import Data.ByteString (ByteString)
-import PlutusTx.Builtins.Internal
-
-import Data.String (IsString (..))
-import Data.Text (Text, pack)
-
-import GHC.Magic qualified as Magic
-import PlutusCore.Crypto.BLS12_381.G1 qualified as BLS12_381.G1 (Element)
-import PlutusCore.Crypto.BLS12_381.G2 qualified as BLS12_381.G2 (Element)
-import PlutusCore.Crypto.BLS12_381.Pairing qualified as BLS12_381.Pairing (MlResult)
-import PlutusTx.Base (const, id, ($))
-import PlutusTx.Bool (Bool (..))
-import PlutusTx.Integer (Integer)
-import Prelude qualified as Haskell (String)
-
--- See Note [Builtin types and their Haskell versions]
-{-|
-A class witnessing the ability to convert from the builtin representation to the Haskell representation.
--}
-class FromBuiltin arep a | arep -> a where
-    fromBuiltin :: arep -> a
-
--- See Note [Builtin types and their Haskell versions]
-{-|
-A class witnessing the ability to convert from the Haskell representation to the builtin representation.
--}
-class ToBuiltin a arep | a -> arep where
-    toBuiltin :: a -> arep
-
-instance FromBuiltin BuiltinInteger Integer where
-    {-# INLINABLE fromBuiltin #-}
-    fromBuiltin = id
-instance ToBuiltin Integer BuiltinInteger where
-    {-# INLINABLE toBuiltin #-}
-    toBuiltin = id
-
-instance FromBuiltin BuiltinBool Bool where
-    {-# INLINABLE fromBuiltin #-}
-    fromBuiltin b = ifThenElse b True False
-instance ToBuiltin Bool BuiltinBool where
-    {-# INLINABLE toBuiltin #-}
-    toBuiltin b = if b then true else false
-
-instance FromBuiltin BuiltinUnit () where
-    -- See Note [Strict conversions to/from unit]
-    {-# INLINABLE fromBuiltin #-}
-    fromBuiltin u = chooseUnit u ()
-instance ToBuiltin () BuiltinUnit where
-    -- See Note [Strict conversions to/from unit]
-    {-# INLINABLE toBuiltin #-}
-    toBuiltin x = case x of () -> unitval
-
-instance FromBuiltin BuiltinByteString ByteString where
-    {-# INLINABLE fromBuiltin #-}
-    fromBuiltin (BuiltinByteString b) = b
-instance ToBuiltin ByteString BuiltinByteString where
-    {-# INLINABLE toBuiltin #-}
-    toBuiltin = BuiltinByteString
-
--- We can't put this in `Builtins.hs`, since that force `O0` deliberately, which prevents
--- the unfoldings from going in. So we just stick it here. Fiddly.
-instance IsString BuiltinString where
-    -- Try and make sure the dictionary selector goes away, it's simpler to match on
-    -- the application of 'stringToBuiltinString'
-    {-# INLINE fromString #-}
-    -- See Note [noinline hack]
-    fromString = Magic.noinline stringToBuiltinString
-
-{-# INLINABLE stringToBuiltinString #-}
-stringToBuiltinString :: Haskell.String -> BuiltinString
--- To explain why the obfuscatedId is here
--- See Note [noinline hack]
-stringToBuiltinString str = obfuscatedId (BuiltinString $ pack str)
-
-{-# NOINLINE obfuscatedId #-}
-obfuscatedId :: a -> a
-obfuscatedId a = a
-
-instance FromBuiltin BuiltinString Text where
-    {-# INLINABLE fromBuiltin #-}
-    fromBuiltin (BuiltinString t) = t
-instance ToBuiltin Text BuiltinString where
-    {-# INLINABLE toBuiltin #-}
-    toBuiltin = BuiltinString
-
-{- Same noinline hack as with `String` type. -}
-instance IsString BuiltinByteString where
-    -- Try and make sure the dictionary selector goes away, it's simpler to match on
-    -- the application of 'stringToBuiltinByteString'
-    {-# INLINE fromString #-}
-    -- See Note [noinline hack]
-    fromString = Magic.noinline stringToBuiltinByteString
-
-{-# INLINABLE stringToBuiltinByteString #-}
-stringToBuiltinByteString :: Haskell.String -> BuiltinByteString
-stringToBuiltinByteString str = encodeUtf8 $ stringToBuiltinString str
-
-instance (FromBuiltin arep a, FromBuiltin brep b) => FromBuiltin (BuiltinPair arep brep) (a,b) where
-    {-# INLINABLE fromBuiltin #-}
-    fromBuiltin p = (fromBuiltin $ fst p, fromBuiltin $ snd p)
-instance ToBuiltin (BuiltinData, BuiltinData) (BuiltinPair BuiltinData BuiltinData) where
-    {-# INLINABLE toBuiltin #-}
-    toBuiltin (d1, d2) = mkPairData d1 d2
-
-instance FromBuiltin arep a => FromBuiltin (BuiltinList arep) [a] where
-    {-# INLINABLE fromBuiltin #-}
-    fromBuiltin = go
-      where
-          -- The combination of both INLINABLE and a type signature seems to stop this getting lifted to the top
-          -- level, which means it gets a proper unfolding, which means that specialization can work, which can
-          -- actually help quite a bit here.
-          {-# INLINABLE go #-}
-          go :: BuiltinList arep -> [a]
-          -- Note that we are using builtin chooseList here so this is *strict* application! So we need to do
-          -- the manual laziness ourselves.
-          go l = chooseList l (const []) (\_ -> fromBuiltin (head l):go (tail l)) unitval
-
-instance ToBuiltin [BuiltinData] (BuiltinList BuiltinData) where
-    {-# INLINABLE toBuiltin #-}
-    toBuiltin []     = mkNilData unitval
-    toBuiltin (d:ds) = mkCons d (toBuiltin ds)
-
-instance ToBuiltin [(BuiltinData, BuiltinData)] (BuiltinList (BuiltinPair BuiltinData BuiltinData)) where
-    {-# INLINABLE toBuiltin #-}
-    toBuiltin []     = mkNilPairData unitval
-    toBuiltin (d:ds) = mkCons (toBuiltin d) (toBuiltin ds)
-
-instance FromBuiltin BuiltinData BuiltinData where
-    {-# INLINABLE fromBuiltin #-}
-    fromBuiltin = id
-instance ToBuiltin BuiltinData BuiltinData where
-    {-# INLINABLE toBuiltin #-}
-    toBuiltin = id
-
-instance FromBuiltin BuiltinBLS12_381_G1_Element BLS12_381.G1.Element where
-    {-# INLINABLE fromBuiltin #-}
-    fromBuiltin (BuiltinBLS12_381_G1_Element a) = a
-instance ToBuiltin BLS12_381.G1.Element BuiltinBLS12_381_G1_Element where
-    {-# INLINABLE toBuiltin #-}
-    toBuiltin = BuiltinBLS12_381_G1_Element
-
-instance FromBuiltin BuiltinBLS12_381_G2_Element BLS12_381.G2.Element where
-    {-# INLINABLE fromBuiltin #-}
-    fromBuiltin (BuiltinBLS12_381_G2_Element a) = a
-instance ToBuiltin BLS12_381.G2.Element BuiltinBLS12_381_G2_Element where
-    {-# INLINABLE toBuiltin #-}
-    toBuiltin = BuiltinBLS12_381_G2_Element
-
-instance FromBuiltin BuiltinBLS12_381_MlResult BLS12_381.Pairing.MlResult where
-    {-# INLINABLE fromBuiltin #-}
-    fromBuiltin (BuiltinBLS12_381_MlResult a) = a
-instance ToBuiltin BLS12_381.Pairing.MlResult BuiltinBLS12_381_MlResult where
-    {-# INLINABLE toBuiltin #-}
-    toBuiltin = BuiltinBLS12_381_MlResult
-
-{- Note [Builtin types and their Haskell versions]
-Consider the builtin pair type. In Plutus Tx, we have an (opaque) type for
-this. It's opaque because you can't actually pattern match on it, instead you can
-only in fact use the specific functions that are available as builtins.
-
-We _also_ have the normal Haskell pair type. This is very different: you can
-pattern match on it, and you can use whatever user-defined functions you like on it.
-
-Users would really like to use the latter, and not the former. So we often want
-to _wrap_ our builtin functions with little adapters that convert between the
-"opaque builtin" "version" of a type and the "normal Haskell" "version" of a type.
-
-This is what the ToBuiltin and FromBuiltin classes do. They let us write wrappers
-for builtins relatively consistently by just calling toBuiltin on their arguments
-and fromBuiltin on the result. They shouldn't really be used otherwise.
-
-Ideally, we would not have instances for types which don't have a different
-Haskell representation type, such as Integer. Integer in Plutus Tx user code _is_ the
-opaque builtin type, we don't expose a different one. So there's no conversion to
-do. However, this interacts badly with the instances for polymorphic builtin types, which
-also convert the type _inside_ them. (This is necessary to avoid doing multiple
-traversals of the type, e.g. we don't want to turn a builtin list into a Haskell
-list, and then traverse it again to conver the contents). Then we _need_ instances
-for all builtin types, even if they don't quite make sense.
-
-Possibly this indicates that these type classes are a bit too 'ad-hoc' and we should
-get rid of them.
--}
-
-{- Note [Fundeps versus type families in To/FromBuiltin]
-We could use a type family here to get the builtin representation of a type. After all, it's
-entirely determined by the Haskell type.
-
-However, this is harder for the plugin to deal with. It's okay to have a type variable
-for the representation type that needs to be instantiated later, but it's *not* okay to
-have an irreducible type application on a type variable. So fundeps are much nicer here.
--}
-
-{- Note [Strict conversions to/from unit]
-Converting to/from unit *should* be straightforward: just `const ()`.
-*But* GHC is very good at optimizing this, and we sometimes use unit
-where side effects matter, e.g. as the result of `trace`. So GHC will
-tend to turn `fromBuiltin (trace s)` into `()`, which is wrong.
-
-So we want our conversions to/from unit to be strict in Haskell. This
-means we need to case pointlessly on the argument, which means we need
-case on unit (`chooseUnit`) as a builtin. But then it all works okay.
--}
-
-{- Note [noinline hack]
-For some functions we have two conflicting desires:
-- We want to have the unfolding available for the plugin.
-- We don't want the function to *actually* get inlined before the plugin runs, since we rely
-on being able to see the original function for some reason.
-
-'INLINABLE' achieves the first, but may cause the function to be inlined too soon.
-
-We can solve this at specific call sites by using the 'noinline' magic function from
-GHC. This stops GHC from inlining it. As a bonus, it also won't be inlined if
-that function is compiled later into the body of another function.
-
-We do therefore need to handle 'noinline' in the plugin, as it itself does not have
-an unfolding.
-
-Another annoying quirk: even if you have 'noinline'd a function call, if the body is
-a single variable, it will still inline! This is the case for the obvious definition
-of 'stringToBuiltinString' (since the newtype constructor vanishes), so we have to add
-some obfuscation to the body to prevent it inlining.
--}
-
-{- Note [From/ToBuiltin instances for polymorphic builtin types]
-For various technical reasons
-(see Note [Representable built-in functions over polymorphic built-in types])
-it's not always easy to provide polymorphic constructors for builtin types, but
-we can usually provide destructors.
-
-What this means in practice is that we can write a generic FromBuiltin instance
-for pairs that makes use of polymorphic fst/snd builtins, but we can't write
-a polymorphic ToBuiltin instance because we'd need a polymorphic version of (,).
-
-Instead we write monomorphic instances corresponding to monomorphic constructor
-builtins that we add for specific purposes.
--}
diff --git a/plutus-tx/src/PlutusTx/Builtins/HasBuiltin.hs b/plutus-tx/src/PlutusTx/Builtins/HasBuiltin.hs
new file mode 100644
index 00000000000..85c509955fe
--- /dev/null
+++ b/plutus-tx/src/PlutusTx/Builtins/HasBuiltin.hs
@@ -0,0 +1,113 @@
+{-# LANGUAGE FlexibleContexts         #-}
+{-# LANGUAGE FlexibleInstances        #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TypeFamilies             #-}
+{-# LANGUAGE TypeOperators            #-}
+
+module PlutusTx.Builtins.HasBuiltin where
+
+import Prelude
+
+import PlutusCore.Crypto.BLS12_381.G1 qualified as BLS12_381.G1 (Element)
+import PlutusCore.Crypto.BLS12_381.G2 qualified as BLS12_381.G2 (Element)
+import PlutusCore.Crypto.BLS12_381.Pairing qualified as BLS12_381.Pairing (MlResult)
+import PlutusCore.Data (Data)
+import PlutusCore.Default qualified as PLC
+import PlutusTx.Builtins.Internal
+
+import Data.ByteString (ByteString)
+import Data.Kind qualified as GHC
+import Data.Text (Text)
+
+-- Also see Note [Built-in types and their Haskell counterparts].
+-- | A class for converting values of Haskell-defined built-in types to their Plutus Tx
+-- counterparts.
+type HasToBuiltin :: GHC.Type -> GHC.Constraint
+class PLC.DefaultUni `PLC.Contains` a => HasToBuiltin a where
+    type ToBuiltin a
+    toBuiltin :: a -> ToBuiltin a
+
+-- Also see Note [Built-in types and their Haskell counterparts].
+-- | A class for converting values of Plutus Tx built-in types to their Haskell-defined
+-- counterparts.
+type HasFromBuiltin :: GHC.Type -> GHC.Constraint
+class HasToBuiltin (FromBuiltin arep) => HasFromBuiltin arep where
+    type FromBuiltin arep
+    fromBuiltin :: arep -> FromBuiltin arep
+
+instance HasToBuiltin Integer where
+    type ToBuiltin Integer = BuiltinInteger
+    toBuiltin = id
+instance HasFromBuiltin BuiltinInteger where
+    type FromBuiltin BuiltinInteger = Integer
+    fromBuiltin = id
+
+instance HasToBuiltin ByteString where
+    type ToBuiltin ByteString = BuiltinByteString
+    toBuiltin = BuiltinByteString
+instance HasFromBuiltin BuiltinByteString where
+    type FromBuiltin BuiltinByteString = ByteString
+    fromBuiltin (BuiltinByteString b) = b
+
+instance HasToBuiltin Text where
+    type ToBuiltin Text = BuiltinString
+    toBuiltin = BuiltinString
+instance HasFromBuiltin BuiltinString where
+    type FromBuiltin BuiltinString = Text
+    fromBuiltin (BuiltinString t) = t
+
+instance HasToBuiltin () where
+    type ToBuiltin () = BuiltinUnit
+    toBuiltin = BuiltinUnit
+instance HasFromBuiltin BuiltinUnit where
+    type FromBuiltin BuiltinUnit = ()
+    fromBuiltin (BuiltinUnit u) = u
+
+instance HasToBuiltin Bool where
+    type ToBuiltin Bool = BuiltinBool
+    toBuiltin = BuiltinBool
+instance HasFromBuiltin BuiltinBool where
+    type FromBuiltin BuiltinBool = Bool
+    fromBuiltin (BuiltinBool b) = b
+
+instance HasToBuiltin a => HasToBuiltin [a] where
+    type ToBuiltin [a] = BuiltinList (ToBuiltin a)
+    toBuiltin = BuiltinList . map toBuiltin
+instance HasFromBuiltin a => HasFromBuiltin (BuiltinList a) where
+    type FromBuiltin (BuiltinList a) = [FromBuiltin a]
+    fromBuiltin (BuiltinList xs) = map fromBuiltin xs
+
+instance (HasToBuiltin a, HasToBuiltin b) => HasToBuiltin (a, b) where
+    type ToBuiltin (a, b) = BuiltinPair (ToBuiltin a) (ToBuiltin b)
+    toBuiltin (x, y) = BuiltinPair (toBuiltin x, toBuiltin y)
+instance (HasFromBuiltin a, HasFromBuiltin b) => HasFromBuiltin (BuiltinPair a b) where
+    type FromBuiltin (BuiltinPair a b) = (FromBuiltin a, FromBuiltin b)
+    fromBuiltin (BuiltinPair (x, y)) = (fromBuiltin x, fromBuiltin y)
+
+instance HasToBuiltin Data where
+    type ToBuiltin Data = BuiltinData
+    toBuiltin = BuiltinData
+instance HasFromBuiltin BuiltinData where
+    type FromBuiltin BuiltinData = Data
+    fromBuiltin (BuiltinData t) = t
+
+instance HasToBuiltin BLS12_381.G1.Element where
+    type ToBuiltin BLS12_381.G1.Element = BuiltinBLS12_381_G1_Element
+    toBuiltin = BuiltinBLS12_381_G1_Element
+instance HasFromBuiltin BuiltinBLS12_381_G1_Element where
+    type FromBuiltin BuiltinBLS12_381_G1_Element = BLS12_381.G1.Element
+    fromBuiltin (BuiltinBLS12_381_G1_Element a) = a
+
+instance HasToBuiltin BLS12_381.G2.Element where
+    type ToBuiltin BLS12_381.G2.Element = BuiltinBLS12_381_G2_Element
+    toBuiltin = BuiltinBLS12_381_G2_Element
+instance HasFromBuiltin BuiltinBLS12_381_G2_Element where
+    type FromBuiltin BuiltinBLS12_381_G2_Element = BLS12_381.G2.Element
+    fromBuiltin (BuiltinBLS12_381_G2_Element a) = a
+
+instance HasToBuiltin BLS12_381.Pairing.MlResult where
+    type ToBuiltin BLS12_381.Pairing.MlResult = BuiltinBLS12_381_MlResult
+    toBuiltin = BuiltinBLS12_381_MlResult
+instance HasFromBuiltin BuiltinBLS12_381_MlResult where
+    type FromBuiltin BuiltinBLS12_381_MlResult = BLS12_381.Pairing.MlResult
+    fromBuiltin (BuiltinBLS12_381_MlResult a) = a
diff --git a/plutus-tx/src/PlutusTx/Builtins/HasOpaque.hs b/plutus-tx/src/PlutusTx/Builtins/HasOpaque.hs
new file mode 100644
index 00000000000..dac87a968a3
--- /dev/null
+++ b/plutus-tx/src/PlutusTx/Builtins/HasOpaque.hs
@@ -0,0 +1,248 @@
+{-# LANGUAGE DefaultSignatures        #-}
+{-# LANGUAGE FlexibleInstances        #-}
+{-# LANGUAGE FunctionalDependencies   #-}
+{-# LANGUAGE MultiParamTypeClasses    #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TypeFamilies             #-}
+{-# LANGUAGE TypeOperators            #-}
+{-# LANGUAGE UndecidableInstances     #-}
+
+{-# OPTIONS_GHC -fno-specialise #-}
+{-# OPTIONS_GHC -fno-omit-interface-pragmas #-}
+{-# OPTIONS_GHC -Wno-orphans #-}
+
+module PlutusTx.Builtins.HasOpaque where
+
+import PlutusTx.Base (id, ($))
+import PlutusTx.Bool (Bool (..))
+import PlutusTx.Builtins.Internal
+
+import Data.Kind qualified as GHC
+import Data.String (IsString (..))
+import Data.Text qualified as Text
+import GHC.Magic qualified as Magic
+import Prelude qualified as Haskell (String)
+
+{- Note [noinline hack]
+For some functions we have two conflicting desires:
+- We want to have the unfolding available for the plugin.
+- We don't want the function to *actually* get inlined before the plugin runs, since we rely
+on being able to see the original function for some reason.
+
+'INLINABLE' achieves the first, but may cause the function to be inlined too soon.
+
+We can solve this at specific call sites by using the 'noinline' magic function from
+GHC. This stops GHC from inlining it. As a bonus, it also won't be inlined if
+that function is compiled later into the body of another function.
+
+We do therefore need to handle 'noinline' in the plugin, as it itself does not have
+an unfolding.
+
+Another annoying quirk: even if you have 'noinline'd a function call, if the body is
+a single variable, it will still inline! This is the case for the obvious definition
+of 'stringToBuiltinString' (since the newtype constructor vanishes), so we have to add
+some obfuscation to the body to prevent it inlining.
+-}
+
+obfuscatedId :: a -> a
+obfuscatedId a = a
+{-# NOINLINE obfuscatedId #-}
+
+stringToBuiltinByteString :: Haskell.String -> BuiltinByteString
+stringToBuiltinByteString str = encodeUtf8 $ stringToBuiltinString str
+{-# INLINABLE stringToBuiltinByteString #-}
+
+stringToBuiltinString :: Haskell.String -> BuiltinString
+-- To explain why the obfuscatedId is here
+-- See Note [noinline hack]
+stringToBuiltinString str = obfuscatedId (BuiltinString $ Text.pack str)
+{-# INLINABLE stringToBuiltinString #-}
+
+{- Same noinline hack as with `String` type. -}
+instance IsString BuiltinByteString where
+    -- Try and make sure the dictionary selector goes away, it's simpler to match on
+    -- the application of 'stringToBuiltinByteString'
+    -- See Note [noinline hack]
+    fromString = Magic.noinline stringToBuiltinByteString
+    {-# INLINE fromString #-}
+
+-- We can't put this in `Builtins.hs`, since that force `O0` deliberately, which prevents
+-- the unfoldings from going in. So we just stick it here. Fiddly.
+instance IsString BuiltinString where
+    -- Try and make sure the dictionary selector goes away, it's simpler to match on
+    -- the application of 'stringToBuiltinString'
+    -- See Note [noinline hack]
+    fromString = Magic.noinline stringToBuiltinString
+    {-# INLINE fromString #-}
+
+{- Note [Built-in types and their Haskell counterparts]
+'HasToBuiltin' allows us to convert a value of a built-in type such as 'ByteString' to its Plutus
+Tx counterpart, 'BuiltinByteString' in this case. The idea is the same for all built-in types: just
+take the Haskell version and make it the Plutus Tx one.
+
+'HasToOpaque' is different, we use it for converting values of only those built-in types that exist
+in the Plutus Tx realm, within the Plutus Tx realm. I.e. we cannot convert a 'ByteString', since
+'ByteString's don't exist in Plutus Tx, only 'BuiltinByteString's do.
+
+Consider, say, the built-in pair type. In Plutus Tx, we have an (opaque) type for this. It's opaque
+because you can't actually pattern match on it, instead you can only in fact use the specific
+functions that are available as builtins.
+
+We _also_ have the normal Haskell pair type. This is very different: you can pattern match on it,
+and you can use whatever user-defined functions you like on it.
+
+Users would really like to use the latter, and not the former. So we often want to _wrap_ our
+built-in functions with little adapters that convert between the opaque "version" of a
+type and the "normal Haskell" "version" of a type.
+
+This is what the 'HasToOpaque' and 'HasFromOpaque' classes do. They let us write wrappers for
+builtins relatively consistently by just calling 'toOpaque' on their arguments and 'fromOpaque' on
+the result. They shouldn't probably be used otherwise.
+
+Ideally, we would not have instances for types which don't have a different Haskell representation
+type, such as 'Integer'. 'Integer' in Plutus Tx user code _is_ the opaque built-in type, we don't
+expose a different one. So there's no conversion to do. However, this interacts badly with the
+instances for polymorphic built-in types, which also convert the type _inside_ them. (This is
+necessary to avoid doing multiple traversals of the type, e.g. we don't want to turn a built-in list
+into a Haskell list, and then traverse it again to conver the contents). Then we _need_ instances
+for all built-in types, so we provide a @default@ implementation for both 'toOpaque' and
+'fromOpaque' that simply returns the argument back and use it for those types that don't require any
+conversions.
+
+Summarizing, 'toBuiltin'/'fromBuiltin' should be used to cross the boundary between Plutus Tx and
+Haskell, while 'toOpaque'/'fromOpaque' should be used within Plutus Tx to convert values to/from
+their @Builtin*@ representation, which we need because neither pattern matching nor standard library
+functions are available for values of @Builtin*@ types that we get from built-in functions.
+-}
+
+{- Note [HasFromOpaque/HasToOpaque instances for polymorphic builtin types]
+For various technical reasons
+(see Note [Representable built-in functions over polymorphic built-in types])
+it's not always easy to provide polymorphic constructors for built-in types, but we can usually
+provide destructors.
+
+What this means in practice is that we can write a generic 'HasFromOpaque' instance for pairs that
+makes use of polymorphic @fst@/@snd@ builtins, but we can't write a polymorphic 'ToOpaque' instance
+because we'd need a polymorphic version of the '(,)' constructor.
+
+Instead we write monomorphic instances corresponding to monomorphic constructor builtins that we add
+for specific purposes.
+-}
+
+{- Note [Fundeps versus type families in HasFromOpaque/HasToOpaque]
+We could use a type family here to get the builtin representation of a type. After all, it's
+entirely determined by the Haskell type.
+
+However, this is harder for the plugin to deal with. It's okay to have a type variable for the
+representation type that needs to be instantiated later, but it's *not* okay to have an irreducible
+type application on a type variable. So fundeps are much nicer here.
+-}
+
+-- See Note [Built-in types and their Haskell counterparts].
+-- See Note [HasFromOpaque/HasToOpaque instances for polymorphic builtin types].
+-- See Note [Fundeps versus type families in HasFromOpaque/HasToOpaque].
+-- | A class for converting values of transparent Haskell-defined built-in types (such as '()',
+-- 'Bool', '[]' etc) to their opaque Plutus Tx counterparts. Instances for built-in types that are
+-- not transparent are provided as well, simply as identities, since those types are already opaque.
+type HasToOpaque :: GHC.Type -> GHC.Type -> GHC.Constraint
+class HasToOpaque a arep | a -> arep where
+    toOpaque :: a -> arep
+    default toOpaque :: a ~ arep => a -> arep
+    toOpaque = id
+    {-# INLINABLE toOpaque #-}
+
+-- See Note [Built-in types and their Haskell counterparts].
+-- See Note [HasFromOpaque/HasToOpaque instances for polymorphic builtin types].
+-- See Note [Fundeps versus type families in HasFromOpaque/HasToOpaque].
+-- | A class for converting values of opaque Plutus Tx types to their transparent Haskell-defined
+-- counterparts (a.k.a. pattern-matchable) built-in types (such as '()', 'Bool', '[]' etc). If no
+-- transparent counterpart exists, then the implementation is identity.
+type HasFromOpaque :: GHC.Type -> GHC.Type -> GHC.Constraint
+class HasFromOpaque arep a | arep -> a where
+    fromOpaque :: arep -> a
+    default fromOpaque :: a ~ arep => arep -> a
+    fromOpaque = id
+    {-# INLINABLE fromOpaque #-}
+
+instance HasToOpaque BuiltinInteger BuiltinInteger
+instance HasFromOpaque BuiltinInteger BuiltinInteger
+
+instance HasToOpaque BuiltinByteString BuiltinByteString
+instance HasFromOpaque BuiltinByteString BuiltinByteString
+
+instance HasToOpaque BuiltinString BuiltinString
+instance HasFromOpaque BuiltinString BuiltinString
+
+{- Note [Strict conversions to/from unit]
+Converting to/from unit *should* be straightforward: just `const ()`.
+*But* GHC is very good at optimizing this, and we sometimes use unit
+where side effects matter, e.g. as the result of `trace`. So GHC will
+tend to turn `fromOpaque (trace s)` into `()`, which is wrong.
+
+So we want our conversions to/from unit to be strict in Haskell. This
+means we need to case pointlessly on the argument, which means we need
+case on unit (`chooseUnit`) as a builtin. But then it all works okay.
+-}
+
+-- See Note [Strict conversions to/from unit].
+instance HasToOpaque () BuiltinUnit where
+    toOpaque x = case x of () -> unitval
+    {-# INLINABLE toOpaque #-}
+instance HasFromOpaque BuiltinUnit () where
+    fromOpaque u = chooseUnit u ()
+    {-# INLINABLE fromOpaque #-}
+
+instance HasToOpaque Bool BuiltinBool where
+    toOpaque b = if b then true else false
+    {-# INLINABLE toOpaque #-}
+instance HasFromOpaque BuiltinBool Bool where
+    fromOpaque b = ifThenElse b True False
+    {-# INLINABLE fromOpaque #-}
+
+instance HasToOpaque [BuiltinData] (BuiltinList BuiltinData) where
+    toOpaque = goList where
+        goList :: [BuiltinData] -> BuiltinList BuiltinData
+        goList []     = mkNilData unitval
+        goList (d:ds) = mkCons (toOpaque d) (goList ds)
+    {-# INLINABLE toOpaque #-}
+instance
+        HasToOpaque
+            [(BuiltinData, BuiltinData)]
+            (BuiltinList (BuiltinPair BuiltinData BuiltinData)) where
+    toOpaque = goList where
+        goList :: [(BuiltinData, BuiltinData)] -> BuiltinList (BuiltinPair BuiltinData BuiltinData)
+        goList []     = mkNilPairData unitval
+        goList (d:ds) = mkCons (toOpaque d) (goList ds)
+    {-# INLINABLE toOpaque #-}
+instance HasFromOpaque arep a => HasFromOpaque (BuiltinList arep) [a] where
+    fromOpaque = go
+      where
+          -- The combination of both INLINABLE and a type signature seems to stop this getting
+          -- lifted to the top level, which means it gets a proper unfolding, which means that
+          -- specialization can work, which can actually help quite a bit here.
+          go :: BuiltinList arep -> [a]
+          -- Note that we are using builtin chooseList here so this is *strict* application! So we
+          -- need to do the manual laziness ourselves.
+          go l = chooseList l (\_ -> []) (\_ -> fromOpaque (head l) : go (tail l)) unitval
+          {-# INLINABLE go #-}
+    {-# INLINABLE fromOpaque #-}
+
+instance HasToOpaque (BuiltinData, BuiltinData) (BuiltinPair BuiltinData BuiltinData) where
+    toOpaque (d1, d2) = mkPairData (toOpaque d1) (toOpaque d2)
+    {-# INLINABLE toOpaque #-}
+instance (HasFromOpaque arep a, HasFromOpaque brep b) =>
+        HasFromOpaque (BuiltinPair arep brep) (a, b) where
+    fromOpaque p = (fromOpaque $ fst p, fromOpaque $ snd p)
+    {-# INLINABLE fromOpaque #-}
+
+instance HasToOpaque BuiltinData BuiltinData
+instance HasFromOpaque BuiltinData BuiltinData
+
+instance HasToOpaque BuiltinBLS12_381_G1_Element BuiltinBLS12_381_G1_Element
+instance HasFromOpaque BuiltinBLS12_381_G1_Element BuiltinBLS12_381_G1_Element
+
+instance HasToOpaque BuiltinBLS12_381_G2_Element BuiltinBLS12_381_G2_Element
+instance HasFromOpaque BuiltinBLS12_381_G2_Element BuiltinBLS12_381_G2_Element
+
+instance HasToOpaque BuiltinBLS12_381_MlResult BuiltinBLS12_381_MlResult
+instance HasFromOpaque BuiltinBLS12_381_MlResult BuiltinBLS12_381_MlResult
diff --git a/plutus-tx/src/PlutusTx/Lift/Class.hs b/plutus-tx/src/PlutusTx/Lift/Class.hs
index 240ce9efc54..7df54048efc 100644
--- a/plutus-tx/src/PlutusTx/Lift/Class.hs
+++ b/plutus-tx/src/PlutusTx/Lift/Class.hs
@@ -30,8 +30,9 @@ import PlutusCore.Data
 import PlutusCore.Quote
 import PlutusIR.MkPir
 import PlutusTx.Builtins
-import PlutusTx.Builtins.Class (FromBuiltin)
-import PlutusTx.Builtins.Internal (BuiltinBool, BuiltinList, BuiltinPair, BuiltinUnit)
+import PlutusTx.Builtins.HasBuiltin (FromBuiltin, HasFromBuiltin)
+import PlutusTx.Builtins.Internal (BuiltinBool, BuiltinInteger, BuiltinList, BuiltinPair,
+                                   BuiltinUnit)
 
 import Language.Haskell.TH qualified as TH hiding (newName)
 
@@ -73,22 +74,21 @@ inline all the definitions so that the overall expression can have the right con
 
 type RTCompile uni fun = DefT TH.Name uni fun () Quote
 
--- TODO: try and make this work with type applications
--- | Class for types which have a corresponding Plutus IR type. Instances should always be derived, do not write
--- your own instance!
+-- | Class for types which have a corresponding Plutus IR type. Instances should always be derived,
+-- do not write your own instance!
 class Typeable uni (a :: k) where
     -- | Get the Plutus IR type corresponding to this type.
     typeRep :: Proxy a -> RTCompile uni fun (Type TyName uni ())
 
-
--- | Class for types which can be lifted into Plutus IR. Instances should be derived, do not write your
--- own instance!
+-- | Class for types which can be lifted into Plutus IR. Instances should be derived, do not write
+-- your own instance!
 class Lift uni a where
     -- | Get a Plutus IR term corresponding to the given value.
     lift :: a -> RTCompile uni fun (Term TyName Name uni fun ())
 
--- This instance ensures that we can apply typeable type constructors to typeable arguments and get a typeable
--- type. We need the kind variable, so that partial application of type constructors works.
+-- This instance ensures that we can apply typeable type constructors to typeable arguments and get
+-- a typeable type. We need the kind variable, so that partial application of type constructors
+-- works.
 instance (Typeable uni (f :: GHC.Type -> k), Typeable uni (a :: GHC.Type)) => Typeable uni (f a) where
     typeRep _ = TyApp () <$> typeRep (Proxy :: Proxy f) <*> typeRep (Proxy :: Proxy a)
 
@@ -132,28 +132,16 @@ instance (TypeError ('Text "Int is not supported, use Integer instead"))
     => Lift uni Int where
     lift = Haskell.error "unsupported"
 
-instance uni `PLC.HasTypeLevel` Integer => Typeable uni Integer where
+instance uni `PLC.HasTypeLevel` Integer => Typeable uni BuiltinInteger where
     typeRep = typeRepBuiltin
 
 -- See Note [Lift and Typeable instances for builtins]
-instance uni `PLC.HasTermLevel` Integer => Lift uni Integer where
+instance uni `PLC.HasTermLevel` Integer => Lift uni BuiltinInteger where
     lift = liftBuiltin
 
--- See Note [Lift and Typeable instances for builtins]
-instance uni `PLC.HasTypeLevel` BS.ByteString => Typeable uni BS.ByteString where
-    typeRep = typeRepBuiltin
-
--- See Note [Lift and Typeable instances for builtins]
-instance uni `PLC.HasTypeLevel` Data => Typeable uni BuiltinData where
-    typeRep _ = typeRepBuiltin (Proxy @Data)
-
--- See Note [Lift and Typeable instances for builtins]
-instance uni `PLC.HasTermLevel` Data => Lift uni BuiltinData where
-    lift = liftBuiltin . builtinDataToData
-
 -- See Note [Lift and Typeable instances for builtins]
 instance uni `PLC.HasTypeLevel` BS.ByteString => Typeable uni BuiltinByteString where
-    typeRep _proxyByteString = typeRepBuiltin (Proxy @BS.ByteString)
+    typeRep _ = typeRepBuiltin (Proxy @BS.ByteString)
 
 -- See Note [Lift and Typeable instances for builtins]
 instance uni `PLC.HasTermLevel` BS.ByteString => Lift uni BuiltinByteString where
@@ -161,7 +149,7 @@ instance uni `PLC.HasTermLevel` BS.ByteString => Lift uni BuiltinByteString wher
 
 -- See Note [Lift and Typeable instances for builtins]
 instance uni `PLC.HasTypeLevel` T.Text => Typeable uni BuiltinString where
-    typeRep _proxyByteString = typeRepBuiltin (Proxy @T.Text)
+    typeRep _ = typeRepBuiltin (Proxy @T.Text)
 
 -- See Note [Lift and Typeable instances for builtins]
 instance uni `PLC.HasTermLevel` T.Text => Lift uni BuiltinString where
@@ -169,7 +157,7 @@ instance uni `PLC.HasTermLevel` T.Text => Lift uni BuiltinString where
 
 -- See Note [Lift and Typeable instances for builtins]
 instance uni `PLC.HasTypeLevel` () => Typeable uni BuiltinUnit where
-    typeRep _proxyUnit = typeRepBuiltin (Proxy @())
+    typeRep _ = typeRepBuiltin (Proxy @())
 
 -- See Note [Lift and Typeable instances for builtins]
 instance uni `PLC.HasTermLevel` () => Lift uni BuiltinUnit where
@@ -177,7 +165,7 @@ instance uni `PLC.HasTermLevel` () => Lift uni BuiltinUnit where
 
 -- See Note [Lift and Typeable instances for builtins]
 instance uni `PLC.HasTypeLevel` Bool => Typeable uni BuiltinBool where
-    typeRep _proxyBool = typeRepBuiltin (Proxy @Bool)
+    typeRep _ = typeRepBuiltin (Proxy @Bool)
 
 -- See Note [Lift and Typeable instances for builtins]
 instance uni `PLC.HasTermLevel` Bool => Lift uni BuiltinBool where
@@ -185,17 +173,28 @@ instance uni `PLC.HasTermLevel` Bool => Lift uni BuiltinBool where
 
 -- See Note [Lift and Typeable instances for builtins]
 instance uni `PLC.HasTypeLevel` [] => Typeable uni BuiltinList where
-    typeRep _proxyBuiltinList = typeRepBuiltin (Proxy @[])
+    typeRep _ = typeRepBuiltin (Proxy @[])
 
 -- See Note [Lift and Typeable instances for builtins]
-instance (FromBuiltin arep a, uni `PLC.HasTermLevel` [a]) => Lift uni (BuiltinList arep) where
+instance (HasFromBuiltin arep, uni `PLC.HasTermLevel` [FromBuiltin arep]) =>
+        Lift uni (BuiltinList arep) where
     lift = liftBuiltin . fromBuiltin
 
 instance uni `PLC.HasTypeLevel` (,) => Typeable uni BuiltinPair where
-    typeRep _proxyBuiltinPair = typeRepBuiltin (Proxy @(,))
+    typeRep _ = typeRepBuiltin (Proxy @(,))
+
+instance
+        ( HasFromBuiltin arep, HasFromBuiltin brep
+        , uni `PLC.HasTermLevel` (FromBuiltin arep, FromBuiltin brep)
+        ) => Lift uni (BuiltinPair arep brep) where
+    lift = liftBuiltin . fromBuiltin
+
+-- See Note [Lift and Typeable instances for builtins]
+instance uni `PLC.HasTypeLevel` Data => Typeable uni BuiltinData where
+    typeRep _ = typeRepBuiltin (Proxy @Data)
 
-instance (FromBuiltin arep a, FromBuiltin brep b, uni `PLC.HasTermLevel` (a, b)) =>
-        Lift uni (BuiltinPair arep brep) where
+-- See Note [Lift and Typeable instances for builtins]
+instance uni `PLC.HasTermLevel` Data => Lift uni BuiltinData where
     lift = liftBuiltin . fromBuiltin
 
 -- See Note [Lift and Typeable instances for builtins]
@@ -235,7 +234,7 @@ trying to pattern match on them. So the types don't quite match up with what we
 to put inside the constant.
 
 Fortunately, we have To/FromBuiltin, which happen to do what we want.
-See Note [Builtin types and their Haskell versions].
+See Note [Built-in types and their Haskell counterparts].
 This is arguably slightly an abuse: the versions of the types that we want in
 Plutus Tx source code and the versions that we use as the implementations of
 the builtin types in the universe could be different. But in practice they
diff --git a/plutus-tx/src/PlutusTx/Lift/TestInstances.hs b/plutus-tx/src/PlutusTx/Lift/TestInstances.hs
new file mode 100644
index 00000000000..26fbe6c274d
--- /dev/null
+++ b/plutus-tx/src/PlutusTx/Lift/TestInstances.hs
@@ -0,0 +1,54 @@
+{-# LANGUAGE ConstraintKinds          #-}
+{-# LANGUAGE FlexibleInstances        #-}
+{-# LANGUAGE MultiParamTypeClasses    #-}
+{-# LANGUAGE QuantifiedConstraints    #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TypeFamilies             #-}
+{-# LANGUAGE TypeOperators            #-}
+{-# LANGUAGE UndecidableInstances     #-}
+{-# LANGUAGE UndecidableSuperClasses  #-}
+
+module PlutusTx.Lift.TestInstances () where
+
+import PlutusCore qualified as PLC
+import PlutusCore.Builtin qualified as PLC
+import PlutusTx.Builtins.HasBuiltin
+import PlutusTx.Lift.Class
+
+import Data.Kind qualified as GHC
+
+-- | @OnBuiltin constr a@ is the same as @constr (ToBuiltin a)@ except the latter does not work in a
+-- quantified context with GHC-8.10, hence we define this class synonym.
+type OnBuiltin :: (GHC.Type -> GHC.Constraint) -> GHC.Type -> GHC.Constraint
+class    constr (ToBuiltin a) => OnBuiltin constr a
+instance constr (ToBuiltin a) => OnBuiltin constr a
+
+-- | @BuiltinSatisfies pre post a@ holds if @pre (ToBuiltin a)@ implies @post (ToBuiltin a)@.
+type BuiltinSatisfies
+    :: (GHC.Type -> GHC.Constraint)
+    -> (GHC.Type -> GHC.Constraint)
+    -> GHC.Type
+    -> GHC.Constraint
+class    (OnBuiltin pre a => OnBuiltin post a) => BuiltinSatisfies pre post a
+instance (OnBuiltin pre a => OnBuiltin post a) => BuiltinSatisfies pre post a
+
+-- | Test that each built-in type @a@ from 'PLC.DefaultUni' satisfies @post (ToBuiltin a)@ given
+-- @pre (ToBuiltin a)@.
+type TestAllBuiltinsSatisfy
+    :: (GHC.Type -> GHC.Constraint)
+    -> (GHC.Type -> GHC.Constraint)
+    -> GHC.Constraint
+class PLC.DefaultUni `PLC.Everywhere` BuiltinSatisfies pre post => TestAllBuiltinsSatisfy pre post
+
+-- | Test that each built-in type from 'PLC.DefaultUni' has a 'Typeable' instance.
+instance TestAllBuiltinsSatisfy
+    (PLC.AllBuiltinArgs PLC.DefaultUni (Typeable PLC.DefaultUni))
+    (Typeable PLC.DefaultUni)
+
+-- | Test that each built-in type from 'PLC.DefaultUni' has a 'Lift' instance. Since the 'Lift'
+-- instances are defined in terms of 'fromBuiltin', this also tests that each built-in type has a
+-- 'FromBuiltin' instance. Which in turn requires a 'ToBuiltin' instance to exist due to the
+-- superclass constraint, so this is implicitly tested as well.
+instance TestAllBuiltinsSatisfy
+    (PLC.AllBuiltinArgs PLC.DefaultUni HasFromBuiltin)
+    (Lift PLC.DefaultUni)
diff --git a/plutus-tx/src/PlutusTx/Prelude.hs b/plutus-tx/src/PlutusTx/Prelude.hs
index 89ee23ea55d..c31ac38ce51 100644
--- a/plutus-tx/src/PlutusTx/Prelude.hs
+++ b/plutus-tx/src/PlutusTx/Prelude.hs
@@ -110,7 +110,9 @@ module PlutusTx.Prelude (
     integerToByteString,
     -- * Conversions
     fromBuiltin,
-    toBuiltin
+    toBuiltin,
+    fromOpaque,
+    toOpaque
     ) where
 
 import Data.String (IsString (..))
@@ -131,9 +133,9 @@ import PlutusTx.Builtins (BuiltinBLS12_381_G1_Element, BuiltinBLS12_381_G2_Eleme
                           bls12_381_G2_uncompress, bls12_381_finalVerify, bls12_381_millerLoop,
                           bls12_381_mulMlResult, byteStringToInteger, consByteString, decodeUtf8,
                           emptyByteString, emptyString, encodeUtf8, equalsByteString, equalsString,
-                          error, fromBuiltin, greaterThanByteString, indexByteString,
+                          error, fromBuiltin, fromOpaque, greaterThanByteString, indexByteString,
                           integerToByteString, keccak_256, lengthOfByteString, lessThanByteString,
-                          sha2_256, sha3_256, sliceByteString, toBuiltin, trace,
+                          sha2_256, sha3_256, sliceByteString, toBuiltin, toOpaque, trace,
                           verifyEcdsaSecp256k1Signature, verifyEd25519Signature,
                           verifySchnorrSecp256k1Signature)
 
@@ -227,12 +229,12 @@ odd n = if even n then False else True
 {-# INLINABLE takeByteString #-}
 -- | Returns the n length prefix of a 'ByteString'.
 takeByteString :: Integer -> BuiltinByteString -> BuiltinByteString
-takeByteString n bs = Builtins.sliceByteString 0 (toBuiltin n) bs
+takeByteString n bs = Builtins.sliceByteString 0 n bs
 
 {-# INLINABLE dropByteString #-}
 -- | Returns the suffix of a 'ByteString' after n elements.
 dropByteString :: Integer -> BuiltinByteString -> BuiltinByteString
-dropByteString n bs = Builtins.sliceByteString (toBuiltin n) (Builtins.lengthOfByteString bs - n) bs
+dropByteString n bs = Builtins.sliceByteString n (Builtins.lengthOfByteString bs - n) bs
 
 {- Note [-fno-full-laziness in Plutus Tx]
 GHC's full-laziness optimization moves computations inside a lambda that don't depend on