diff --git a/containers/src/Yaya/Containers/Pattern/IntMap.hs b/containers/src/Yaya/Containers/Pattern/IntMap.hs
index 6704626a..8559406a 100644
--- a/containers/src/Yaya/Containers/Pattern/IntMap.hs
+++ b/containers/src/Yaya/Containers/Pattern/IntMap.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE Safe #-}
+{-# LANGUAGE TypeFamilies #-}
 {-# OPTIONS_GHC -Wno-orphans #-}
 
 module Yaya.Containers.Pattern.IntMap
@@ -50,16 +51,26 @@ import "yaya" Yaya.Fold
     embed,
     project,
   )
+import "yaya" Yaya.Strict (Strict)
 import qualified "yaya-unsafe" Yaya.Unsafe.Fold as Unsafe
 import "base" Prelude ((+))
 #if MIN_VERSION_containers(0, 8, 0)
 import qualified "containers" Data.IntSet.Internal.IntTreeCommons as IntMap
   ( Prefix (Prefix),
   )
+#endif
+
+type instance Strict IntMap.IntMap = 'False
+
+-- |
+--
+--  __FIXME__: This is strict only if `a` is not non-strict.
+type instance Strict (IntMap.IntMap _a) = 'True
 
 data IntMapF a r
   = NilF
-  | TipF IntMap.Key a
+  | TipF IntMap.Key ~a
+#if MIN_VERSION_containers(0, 8, 0)
   | BinF IntMap.Prefix r r
   deriving stock
     ( Eq,
@@ -70,9 +81,6 @@ data IntMapF a r
       Traversable
     )
 #else
-data IntMapF a r
-  = NilF
-  | TipF IntMap.Key a
   | BinF IntMap.Prefix IntMap.Mask r r
   deriving stock
     ( Eq,
@@ -84,6 +92,18 @@ data IntMapF a r
     )
 #endif
 
+type instance Strict IntMapF = 'False
+
+-- |
+--
+--  __FIXME__: This is strict only if `a` is not non-strict.
+type instance Strict (IntMapF _a) = 'True
+
+-- |
+--
+--  __FIXME__: This is strict only if `a` is not non-strict.
+type instance Strict (IntMapF _a _r) = 'True
+
 instance Projectable (->) (IntMap.IntMap a) (IntMapF a) where
   project = \case
     IntMap.Nil -> NilF
diff --git a/containers/src/Yaya/Containers/Pattern/IntSet.hs b/containers/src/Yaya/Containers/Pattern/IntSet.hs
index 1a1b9963..87ac8489 100644
--- a/containers/src/Yaya/Containers/Pattern/IntSet.hs
+++ b/containers/src/Yaya/Containers/Pattern/IntSet.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE Safe #-}
+{-# LANGUAGE TypeFamilies #-}
 {-# OPTIONS_GHC -Wno-orphans #-}
 
 module Yaya.Containers.Pattern.IntSet
@@ -43,16 +44,21 @@ import "yaya" Yaya.Fold
     embed,
     project,
   )
+import "yaya" Yaya.Strict (Strict)
 import qualified "yaya-unsafe" Yaya.Unsafe.Fold as Unsafe
 import "base" Prelude ((+))
 #if MIN_VERSION_containers(0, 8, 0)
 import qualified "containers" Data.IntSet.Internal.IntTreeCommons as IntSet
   ( Prefix (Prefix),
   )
+#endif
+
+type instance Strict IntSet.IntSet = 'True
 
 data IntSetF r
   = NilF
   | TipF Int IntSet.BitMap
+#if MIN_VERSION_containers(0, 8, 0)
   | BinF IntSet.Prefix r r
   deriving stock
     ( Eq,
@@ -63,9 +69,6 @@ data IntSetF r
       Traversable
     )
 #else
-data IntSetF r
-  = NilF
-  | TipF Int IntSet.BitMap
   | BinF IntSet.Prefix IntSet.Mask r r
   deriving stock
     ( Eq,
@@ -77,6 +80,10 @@ data IntSetF r
     )
 #endif
 
+type instance Strict IntSetF = 'True
+
+type instance Strict (IntSetF _r) = 'True
+
 instance Projectable (->) IntSet.IntSet IntSetF where
   project = \case
     IntSet.Nil -> NilF
diff --git a/containers/src/Yaya/Containers/Pattern/Map.hs b/containers/src/Yaya/Containers/Pattern/Map.hs
index aab523fe..0739b835 100644
--- a/containers/src/Yaya/Containers/Pattern/Map.hs
+++ b/containers/src/Yaya/Containers/Pattern/Map.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE Safe #-}
+{-# LANGUAGE TypeFamilies #-}
 {-# OPTIONS_GHC -Wno-orphans #-}
 
 module Yaya.Containers.Pattern.Map
@@ -73,9 +74,19 @@ import "yaya" Yaya.Fold
     embed,
     project,
   )
+import "yaya" Yaya.Strict (Strict)
 import qualified "yaya-unsafe" Yaya.Unsafe.Fold as Unsafe
 import "base" Prelude ((+))
 
+type instance Strict Map.Map = 'False
+
+type instance Strict (Map.Map _k) = 'False
+
+-- |
+--
+--  __FIXME__: This is strict only if `v` is not non-strict.
+type instance Strict (Map.Map _k _v) = 'True
+
 data MapF k v r = TipF | BinF Map.Size k ~v r r
   deriving stock
     ( Eq,
@@ -90,6 +101,20 @@ data MapF k v r = TipF | BinF Map.Size k ~v r r
       Traversable
     )
 
+type instance Strict MapF = 'False
+
+type instance Strict (MapF _k) = 'False
+
+-- |
+--
+--  __FIXME__: This is strict only if `v` is not non-strict.
+type instance Strict (MapF _k _v) = 'True
+
+-- |
+--
+--  __FIXME__: This is strict only if `v` is not non-strict.
+type instance Strict (MapF _k _v _r) = 'True
+
 instance Projectable (->) (Map.Map k v) (MapF k v) where
   project Map.Tip = TipF
   project (Map.Bin size k v l r) = BinF size k v l r
diff --git a/containers/src/Yaya/Containers/Pattern/Set.hs b/containers/src/Yaya/Containers/Pattern/Set.hs
index 5d85eb48..e173b128 100644
--- a/containers/src/Yaya/Containers/Pattern/Set.hs
+++ b/containers/src/Yaya/Containers/Pattern/Set.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE Safe #-}
+{-# LANGUAGE TypeFamilies #-}
 {-# OPTIONS_GHC -Wno-orphans #-}
 
 module Yaya.Containers.Pattern.Set
@@ -49,9 +50,14 @@ import "yaya" Yaya.Fold
     embed,
     project,
   )
+import "yaya" Yaya.Strict (Strict)
 import qualified "yaya-unsafe" Yaya.Unsafe.Fold as Unsafe
 import "base" Prelude ((+))
 
+type instance Strict Set.Set = 'True
+
+type instance Strict (Set.Set _a) = 'True
+
 data SetF a r = TipF | BinF Set.Size a r r
   deriving stock
     ( Eq,
@@ -66,6 +72,12 @@ data SetF a r = TipF | BinF Set.Size a r r
       Traversable
     )
 
+type instance Strict SetF = 'True
+
+type instance Strict (SetF _a) = 'True
+
+type instance Strict (SetF _a _r) = 'True
+
 instance Projectable (->) (Set.Set a) (SetF a) where
   project Set.Tip = TipF
   project (Set.Bin size a l r) = BinF size a l r
diff --git a/core/src/Yaya/Applied.hs b/core/src/Yaya/Applied.hs
index aece2335..97fba5ae 100644
--- a/core/src/Yaya/Applied.hs
+++ b/core/src/Yaya/Applied.hs
@@ -2,6 +2,8 @@
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
+-- Needed by `PartialTypeError` constraints in GHC 9.4.
+{-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -Wno-orphans #-}
 {-# OPTIONS_GHC -fplugin-opt=NoRecursion:ignore-methods:sconcat #-}
 
@@ -94,7 +96,7 @@ import safe "this" Yaya.Fold.Common
     truncate',
     unarySequence,
   )
-import safe "this" Yaya.Fold.Native (Fix)
+import safe "this" Yaya.Fold.Native (Cofix, Fix)
 import safe "this" Yaya.Pattern
   ( Either (Left),
     Maybe (Just, Nothing),
@@ -102,6 +104,7 @@ import safe "this" Yaya.Pattern
     XNor (Both, Neither),
     maybe,
   )
+import safe "this" Yaya.Strict (PartialTypeError, unsatisfiable)
 import safe "base" Prelude (Integral, fromIntegral)
 
 -- See comment on @{-# LANGUAGE Safe #-}@ above.
@@ -308,8 +311,28 @@ fromListN = cata2 (embed . takeAvailable) . fromIntegral @_ @Natural
 toList :: (Projectable (->) t (XNor a)) => t -> [a]
 toList = ana project
 
+-- | This instance is safe, since both structures are lazy.
+instance IsList (Cofix (XNor a)) where
+  type Item (Cofix (XNor a)) = a
+  fromList = fromList
+  fromListN = fromListN
+  toList = toList
+
+instance (PartialTypeError Fix) => IsList (Fix (XNor a)) where
+  type Item (Fix (XNor a)) = a
+  fromList = unsatisfiable
+  fromListN = fromListN
+  toList = toList
+
+instance (PartialTypeError Mu) => IsList (Mu (XNor a)) where
+  type Item (Mu (XNor a)) = a
+  fromList = unsatisfiable
+  fromListN = fromListN
+  toList = toList
+
 -- | This instance is safe, since both structures are lazy.
 instance IsList (Nu (XNor a)) where
   type Item (Nu (XNor a)) = a
   fromList = fromList
+  fromListN = fromListN
   toList = toList
diff --git a/core/src/Yaya/Fold.hs b/core/src/Yaya/Fold.hs
index 69d300ea..f85be6e7 100644
--- a/core/src/Yaya/Fold.hs
+++ b/core/src/Yaya/Fold.hs
@@ -2,6 +2,9 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE Safe #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
 {-# LANGUAGE ViewPatterns #-}
 {-# OPTIONS_GHC -fplugin-opt=NoRecursion:ignore-decls:steppableReadPrec' #-}
 
@@ -85,7 +88,7 @@ import "base" Control.Category (id, (.))
 import "base" Control.Monad (Monad, join, (<=<), (=<<))
 import "base" Data.Bifunctor (bimap, first, second)
 import "base" Data.Bitraversable (bisequence)
-import "base" Data.Bool (Bool)
+import "base" Data.Bool (Bool (False))
 import "base" Data.Eq (Eq, (==))
 import "base" Data.Foldable (Foldable, toList)
 import "base" Data.Function (const, flip, ($))
@@ -121,9 +124,8 @@ import "base" Text.Read
 import qualified "base" Text.Read.Lex as Lex
 import "base" Text.Show (Show, ShowS, showParen, showString, showsPrec)
 import "comonad" Control.Comonad (Comonad, duplicate, extend, extract)
-import "comonad" Control.Comonad.Trans.Env (EnvT (EnvT), lowerEnvT, runEnvT)
 import "free" Control.Comonad.Cofree (Cofree ((:<)))
-import "free" Control.Monad.Trans.Free (Free, FreeF (Free, Pure), free, runFree)
+-- import "free" Control.Monad.Trans.Free (Free, free, runFree)
 import "kan-extensions" Data.Functor.Day (Day (Day))
 import "lens" Control.Lens
   ( Const (Const),
@@ -140,7 +142,6 @@ import "lens" Control.Lens
     traverse,
     view,
   )
-import "strict" Data.Strict.Classes (toStrict)
 import "this" Yaya.Fold.Common
   ( compareDay,
     diagonal,
@@ -152,24 +153,28 @@ import "this" Yaya.Functor (DFunctor, dmap)
 import "this" Yaya.Pattern
   ( AndMaybe (Indeed, Only),
     Either (Left, Right),
+    EnvT (EnvT),
+    FreeF (Free, Pure),
     Maybe (Just, Nothing),
     Pair ((:!:)),
     XNor (Both, Neither),
     fst,
+    lowerEnvT,
     maybe,
+    runEnvT,
     snd,
     uncurry,
+    unzip,
+  )
+import "this" Yaya.Strict
+  ( IsNonStrict,
+    IsStrict,
+    PartialTypeError,
+    Strict,
+    unsatisfiable,
   )
 import "base" Prelude (pred, succ)
 
--- NB: Prior to base 4.19, "Data.Functor" doesn’t export `unzip`, but starting
---     with base 4.22, the one from "Data.List.NonEmpty" is monomorphic.
-#if MIN_VERSION_base(4, 19, 0)
-import "base" Data.Functor (unzip)
-#else
-import "base" Data.List.NonEmpty (unzip)
-#endif
-
 -- $setup
 -- >>> :seti -XTypeApplications
 
@@ -246,12 +251,12 @@ class (Projectable c t f) => Steppable c t f | t -> f where
 
 -- | Inductive structures that can be reasoned about in the way we usually do –
 --   with pattern matching.
-class Recursive c t f | t -> f where
+class (IsStrict t, IsStrict f) => Recursive c t f | t -> f where
   cata :: Algebra c f a -> t `c` a
 
 -- | Coinductive (potentially-infinite) structures that guarantee _productivity_
 --   rather than termination.
-class Corecursive c t f | t -> f where
+class (IsNonStrict t) => Corecursive c t f | t -> f where
   ana :: Coalgebra c f a -> a `c` t
 
 -- | Like `recursiveEq`, but allows you to provide a custom comparator for @f@.
@@ -391,37 +396,52 @@ steppableReadPrec = steppableReadPrec' liftReadPrec
 --          @-XStrictData@ can help with this a lot.
 newtype Mu f = Mu (forall a. Algebra (->) f a -> a)
 
-instance (Functor f) => Projectable (->) (Mu f) f where
+type instance Strict (Mu f) = Strict f
+
+-- |
+--
+--  __TODO__: @`IsStrict` (`Mu` f)@ should be implied by @`IsStrict` f@.
+instance (IsStrict f, IsStrict (Mu f)) => Recursive (->) (Mu f) f where
+  cata φ (Mu f) = f φ
+
+instance (Recursive (->) (Mu f) f, Functor f) => Projectable (->) (Mu f) f where
   project = lambek
 
-instance (Functor f) => Steppable (->) (Mu f) f where
+instance (Recursive (->) (Mu f) f, Functor f) => Steppable (->) (Mu f) f where
   embed m = Mu (\f -> f (fmap (cata f) m))
 
-instance Recursive (->) (Mu f) f where
-  cata φ (Mu f) = f φ
-
 instance DFunctor Mu where
   dmap f (Mu run) = Mu (\φ -> run (φ . f))
 
-instance (Functor f, Foldable f, Eq1 f) => Eq (Mu f) where
+instance
+  (Recursive (->) (Mu f) f, Functor f, Foldable f, Eq1 f) =>
+  Eq (Mu f)
+  where
   (==) = recursiveEq
 
 -- | @since 0.6.1.0
-instance (Functor f, Foldable f, Ord1 f) => Ord (Mu f) where
+instance
+  (Recursive (->) (Mu f) f, Functor f, Foldable f, Ord1 f) =>
+  Ord (Mu f)
+  where
   compare = recursiveCompare
 
 -- | @since 0.6.1.0
-instance (Functor f, Read1 f) => Read (Mu f) where
+instance (Recursive (->) (Mu f) f, Functor f, Read1 f) => Read (Mu f) where
   readPrec = steppableReadPrec
   readListPrec = readListPrecDefault
 
-instance (Show1 f) => Show (Mu f) where
+instance (Recursive (->) (Mu f) f, Show1 f) => Show (Mu f) where
   showsPrec = recursiveShowsPrec
 
 -- | A fixed-point operator for coinductive / potentially-infinite data
 --   structures.
 data Nu f where Nu :: Coalgebra (->) f a -> a -> Nu f
 
+type instance Strict Nu = 'False
+
+type instance Strict (Nu _f) = 'False
+
 instance (Functor f) => Projectable (->) (Nu f) f where
   project (Nu f a) = Nu f <$> f a
 
@@ -477,11 +497,11 @@ instance Projectable (->) (Cofree f a) (EnvT a f) where
 instance Steppable (->) (Cofree f a) (EnvT a f) where
   embed (EnvT a ft) = a :< ft
 
-instance Projectable (->) (Free f a) (FreeF f a) where
-  project = runFree
+-- instance Projectable (->) (Free f a) (FreeF f a) where
+--   project = runFree
 
-instance Steppable (->) (Free f a) (FreeF f a) where
-  embed = free
+-- instance Steppable (->) (Free f a) (FreeF f a) where
+--   embed = free
 
 -- | Combines two `Algebra`s with different carriers into a single tupled
 --  `Algebra`.
@@ -647,7 +667,7 @@ distEnvT ::
   DistributiveLaw (->) f w ->
   f (EnvT a w c) ->
   EnvT b w (f c)
-distEnvT φ k = uncurry EnvT . bimap φ k . toStrict . unzip . fmap runEnvT
+distEnvT φ k = uncurry EnvT . bimap φ k . unzip . fmap runEnvT
 
 distCofreeT ::
   ( Corecursive (->) (t (f a)) (EnvT (f a) h),
@@ -695,7 +715,7 @@ attributeAlgebra ::
   Algebra (->) f a ->
   Algebra (->) f t
 attributeAlgebra φ ft =
-  embed $ EnvT (φ (fmap (fst . toStrict . runEnvT . project) ft)) ft
+  embed $ EnvT (φ (fmap (fst . runEnvT . project) ft)) ft
 
 -- | Converts a `Coalgebra` to one that annotates the tree with the seed that
 --   generated each node.
@@ -743,8 +763,8 @@ instance Steppable (->) (Either a b) (Const (Either a b)) where
 instance Recursive (->) (Either a b) (Const (Either a b)) where
   cata = constCata
 
-instance Corecursive (->) (Either a b) (Const (Either a b)) where
-  ana = constAna
+-- instance Corecursive (->) (Either a b) (Const (Either a b)) where
+--   ana = constAna
 
 instance Projectable (->) (Maybe a) (Const (Maybe a)) where
   project = constProject
@@ -755,8 +775,8 @@ instance Steppable (->) (Maybe a) (Const (Maybe a)) where
 instance Recursive (->) (Maybe a) (Const (Maybe a)) where
   cata = constCata
 
-instance Corecursive (->) (Maybe a) (Const (Maybe a)) where
-  ana = constAna
+-- instance Corecursive (->) (Maybe a) (Const (Maybe a)) where
+--   ana = constAna
 
 -- * Optics
 
@@ -783,3 +803,9 @@ recursivePrism alg =
   prism
     (ana (review alg))
     (\t -> first (const t) $ cata (matching alg <=< sequenceA) t)
+
+instance (PartialTypeError Nu) => Eq (Nu f) where
+  (==) = unsatisfiable
+
+instance (PartialTypeError Nu) => Show (Nu f) where
+  showsPrec = unsatisfiable
diff --git a/core/src/Yaya/Fold/Native.hs b/core/src/Yaya/Fold/Native.hs
index 69054e64..0742dfb1 100644
--- a/core/src/Yaya/Fold/Native.hs
+++ b/core/src/Yaya/Fold/Native.hs
@@ -1,5 +1,8 @@
+{-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE Safe #-}
 {-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -Wno-orphans #-}
 
 -- | Uses of recursion schemes that use Haskell’s built-in recursion in a total
@@ -11,20 +14,19 @@ module Yaya.Fold.Native
 where
 
 import "base" Control.Category ((.))
+import "base" Data.Bool (Bool (True))
 import "base" Data.Eq (Eq, (==))
 import "base" Data.Foldable (Foldable, toList)
 import "base" Data.Function (($))
-import "base" Data.Functor (Functor, fmap)
+import "base" Data.Functor (Functor, fmap, (<$>))
 import "base" Data.Functor.Classes (Eq1, Ord1, Read1, Show1)
 import "base" Data.List.NonEmpty (NonEmpty ((:|)))
 import "base" Data.Ord (Ord, compare)
 import "base" Numeric.Natural (Natural)
 import "base" Text.Read (Read, readListPrec, readListPrecDefault, readPrec)
 import "base" Text.Show (Show, showsPrec)
-import "comonad" Control.Comonad.Trans.Env (EnvT, runEnvT)
 import "free" Control.Comonad.Cofree (Cofree ((:<)))
 import "free" Control.Monad.Trans.Free (Free, FreeF (Free, Pure), free)
-import "strict" Data.Strict.Classes (toStrict)
 import "this" Yaya.Fold
   ( Corecursive,
     Projectable,
@@ -42,29 +44,52 @@ import "this" Yaya.Fold
 import "this" Yaya.Fold.Native.Internal (Cofix)
 import "this" Yaya.Pattern
   ( AndMaybe (Indeed, Only),
+    EnvT,
     Maybe,
     XNor (Both, Neither),
+    runEnvT,
     uncurry,
   )
+import "this" Yaya.Strict (IsNonStrict, IsStrict, Strict)
 
 -- | A fixed-point constructor that uses Haskell's built-in recursion. This is
 --   strict/recursive.
 newtype Fix f = Fix (f (Fix f))
 
+type instance Strict Fix = 'True
+
+type instance Strict (Fix f) = Strict f
+
 instance Projectable (->) (Fix f) f where
   project (Fix fFix) = fFix
 
 instance Steppable (->) (Fix f) f where
   embed = Fix
 
-instance (Functor f) => Recursive (->) (Fix f) f where
+-- |
+--
+--  __TODO__: @`IsStrict` (`Fix` f)@ should be implied by @`IsStrict` f@.
+instance
+  (IsStrict f, IsStrict (Fix f), Functor f) =>
+  Recursive (->) (Fix f) f
+  where
   cata ɸ = ɸ . fmap (cata ɸ) . project
 
-instance (Functor f, Foldable f, Eq1 f) => Eq (Fix f) where
+-- | When the pattern functor is not `Strict`, `Fix` may be used corecursively.
+instance (IsNonStrict (Fix f), Functor f) => Corecursive (->) (Fix f) f where
+  ana ψ = embed . fmap (ana ψ) . ψ
+
+instance
+  (Recursive (->) (Fix f) f, Functor f, Foldable f, Eq1 f) =>
+  Eq (Fix f)
+  where
   (==) = recursiveEq
 
 -- | @since 0.6.1.0
-instance (Functor f, Foldable f, Ord1 f) => Ord (Fix f) where
+instance
+  (Recursive (->) (Fix f) f, Functor f, Foldable f, Ord1 f) =>
+  Ord (Fix f)
+  where
   compare = recursiveCompare
 
 -- | @since 0.6.1.0
@@ -72,7 +97,7 @@ instance (Read1 f) => Read (Fix f) where
   readPrec = steppableReadPrec
   readListPrec = readListPrecDefault
 
-instance (Functor f, Show1 f) => Show (Fix f) where
+instance (Recursive (->) (Fix f) f, Functor f, Show1 f) => Show (Fix f) where
   showsPrec = recursiveShowsPrec
 
 instance Recursive (->) Natural Maybe where
@@ -99,9 +124,9 @@ instance (Functor f) => Corecursive (->) (Free f a) (FreeF f a) where
     free
       . ( \case
             Pure a -> Pure a
-            Free fb -> Free . fmap (ana ψ) $ fb
+            Free fb -> Free $ ana ψ <$> fb
         )
       . ψ
 
 instance (Functor f) => Corecursive (->) (Cofree f a) (EnvT a f) where
-  ana ψ = uncurry (:<) . fmap (fmap (ana ψ)) . toStrict . runEnvT . ψ
+  ana ψ = uncurry (:<) . fmap (fmap (ana ψ)) . runEnvT . ψ
diff --git a/core/src/Yaya/Fold/Native/Internal.hs b/core/src/Yaya/Fold/Native/Internal.hs
index 2f7e7882..0439145a 100644
--- a/core/src/Yaya/Fold/Native/Internal.hs
+++ b/core/src/Yaya/Fold/Native/Internal.hs
@@ -1,4 +1,6 @@
 {-# LANGUAGE Safe #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
 -- __NB__: We disable @StrictData@ here in order for `Cofix` to be lazy. I don’t
 --         think there is any way to explicitly add @~@ patterns that has the
 --         correct semantics.
@@ -13,9 +15,12 @@ module Yaya.Fold.Native.Internal
 where
 
 import "base" Control.Category ((.))
+import "base" Data.Bool (Bool (False))
+import "base" Data.Eq (Eq, (==))
 import "base" Data.Functor (Functor, fmap)
 import "base" Data.Functor.Classes (Read1)
 import "base" Text.Read (Read, readListPrec, readListPrecDefault, readPrec)
+import "base" Text.Show (Show, showsPrec)
 import "this" Yaya.Fold
   ( Corecursive,
     Projectable,
@@ -25,11 +30,16 @@ import "this" Yaya.Fold
     project,
     steppableReadPrec,
   )
+import "this" Yaya.Strict (PartialTypeError, Strict, unsatisfiable)
 
 -- | A fixed-point constructor that uses Haskell's built-in recursion. This is
 --   lazy/corecursive.
 data Cofix f = Cofix (f (Cofix f))
 
+type instance Strict Cofix = 'False
+
+type instance Strict (Cofix _f) = 'False
+
 {-# HLINT ignore Cofix "Use newtype instead of data" #-}
 
 instance Projectable (->) (Cofix f) f where
@@ -45,3 +55,9 @@ instance (Functor f) => Corecursive (->) (Cofix f) f where
 instance (Read1 f) => Read (Cofix f) where
   readPrec = steppableReadPrec
   readListPrec = readListPrecDefault
+
+instance (PartialTypeError Cofix) => Eq (Cofix f) where
+  (==) = unsatisfiable
+
+instance (PartialTypeError Cofix) => Show (Cofix f) where
+  showsPrec = unsatisfiable
diff --git a/core/src/Yaya/Functor.hs b/core/src/Yaya/Functor.hs
index 1e2fdd61..1b626a70 100644
--- a/core/src/Yaya/Functor.hs
+++ b/core/src/Yaya/Functor.hs
@@ -38,9 +38,9 @@ class DFunctor (d :: (Type -> Type) -> Type) where
 
 -- | This isn’t a Functor instance because of the position of the @a@, but you
 --   can use it like:
---   > newtype List a = List (Mu (XNor a))
---   > instance Functor List where
---   >   fmap f (List mu) = List (firstMap f mu)
+-- > newtype List a = List (Mu (XNor a))
+-- > instance Functor List where
+-- >   fmap f (List mu) = List (firstMap f mu)
 firstMap :: (DFunctor d, Bifunctor f) => (a -> b) -> d (f a) -> d (f b)
 firstMap f = dmap (first f)
 
diff --git a/core/src/Yaya/Pattern.hs b/core/src/Yaya/Pattern.hs
index 0db576ab..cd344426 100644
--- a/core/src/Yaya/Pattern.hs
+++ b/core/src/Yaya/Pattern.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE Safe #-}
+{-# LANGUAGE TypeFamilies #-}
 {-# OPTIONS_GHC -Wno-orphans #-}
 
 -- | Common pattern functors (and instances for them).
@@ -10,8 +11,14 @@ module Yaya.Pattern
     module Data.Strict.Maybe,
     module Data.Strict.Tuple,
     AndMaybe (Indeed, Only),
+    EnvT (EnvT),
+    FreeF (Pure, Free),
     XNor (Both, Neither),
     andMaybe,
+    ask,
+    lowerEnvT,
+    runEnvT,
+    unzip,
     xnor,
   )
 where
@@ -59,7 +66,7 @@ import "base" GHC.Read (expectP)
 import "base" Text.Read (Read, parens, prec, readListPrec, readPrec, step)
 import qualified "base" Text.Read.Lex as Lex
 import "base" Text.Show (Show, showList, showParen, showString, showsPrec)
-import "comonad" Control.Comonad (Comonad, duplicate, extract)
+import "comonad" Control.Comonad (Comonad, duplicate, extend, extract)
 import "strict" Data.Strict.Either
   ( Either (Left, Right),
     either,
@@ -90,10 +97,11 @@ import "strict" Data.Strict.Tuple
     snd,
     swap,
     uncurry,
-    unzip,
     zip,
     (:!:),
   )
+import "this" Yaya.Functor (HFunctor, hmap)
+import "this" Yaya.Strict (Strict)
 import "base" Prelude ((+))
 
 -- | Isomorphic to @'Maybe` (a, b)@, it’s also the pattern functor for lists.
@@ -111,6 +119,12 @@ data XNor a b = Neither | Both ~a b
       Traversable
     )
 
+type instance Strict XNor = 'False
+
+type instance Strict (XNor _a) = 'True
+
+type instance Strict (XNor _a _b) = 'True
+
 -- | Eliminator for `XNor`, akin to `Data.Either.either` or `Data.Maybe.maybe`.
 --
 --   @since 0.6.1.0
@@ -186,6 +200,12 @@ data AndMaybe a b = Only ~a | Indeed ~a b
       Traversable
     )
 
+type instance Strict AndMaybe = 'False
+
+type instance Strict (AndMaybe _a) = 'True
+
+type instance Strict (AndMaybe _a _b) = 'True
+
 -- | Eliminator for `AndMaybe`, akin to `Data.Either.either` or
 --  `Data.Maybe.maybe`.
 --
@@ -254,6 +274,108 @@ instance Show2 AndMaybe where
 instance Bifunctor AndMaybe where
   bimap f g = andMaybe (Only . f) (\a -> Indeed (f a) . g)
 
+-- | A strict environment transformer.
+data EnvT e w a = EnvT {ask :: e, lowerEnvT :: w a}
+  deriving stock
+    ( Eq,
+      Generic,
+      Ord,
+      Read,
+      Show,
+      Foldable,
+      Functor,
+      Generic1,
+      Traversable
+    )
+
+type instance Strict EnvT = 'True
+
+type instance Strict (EnvT _e) = 'True
+
+type instance Strict (EnvT _e _w) = 'True
+
+type instance Strict (EnvT _e _w _a) = 'True
+
+instance (Eq e, Eq1 f) => Eq1 (EnvT e f) where
+  liftEq eqA (EnvT e fa) (EnvT e' fa') = e == e' && liftEq eqA fa fa'
+
+instance (Ord e, Ord1 f) => Ord1 (EnvT e f) where
+  liftCompare compareA (EnvT e fa) (EnvT e' fa') =
+    compare e e' <> liftCompare compareA fa fa'
+
+instance (Read e, Read1 f) => Read1 (EnvT e f) where
+  liftReadPrec readPrecA readListA =
+    let appPrec = 10
+     in parens . prec appPrec $
+          expectP (Lex.Ident "EnvT")
+            *> ( EnvT
+                   <$> step readPrec
+                   <*> step (liftReadPrec readPrecA readListA)
+               )
+
+instance (Show e, Show1 f) => Show1 (EnvT e f) where
+  liftShowsPrec showsPrecA showListA p (EnvT e fa) =
+    let appPrec = 10
+        nextPrec = appPrec + 1
+     in showParen (nextPrec <= p) $
+          showString "EnvT "
+            . showsPrec nextPrec e
+            . showString " "
+            . liftShowsPrec showsPrecA showListA nextPrec fa
+
+instance (Comonad w) => Comonad (EnvT e w) where
+  duplicate (EnvT e wa) = EnvT e (extend (EnvT e) wa)
+  extract (EnvT _ wa) = extract wa
+
+instance HFunctor (EnvT e) where
+  hmap nat (EnvT e wa) = EnvT e $ nat wa
+
+runEnvT :: EnvT w f a -> Pair w (f a)
+runEnvT (EnvT w fa) = w :!: fa
+
+-- | A strict free applicative pattern functor.
+data FreeF f a b
+  = Pure a
+  | Free (f b)
+  deriving stock
+    ( Eq,
+      Generic,
+      Ord,
+      Read,
+      Show,
+      Foldable,
+      Functor,
+      Generic1,
+      Traversable
+    )
+
+type instance Strict FreeF = 'True
+
+type instance Strict (FreeF _f) = 'True
+
+type instance Strict (FreeF _f _a) = 'True
+
+type instance Strict (FreeF _f _a _b) = 'True
+
+instance (Eq1 f, Eq a) => Eq1 (FreeF f a) where
+  liftEq = liftEq2 (==)
+
+instance (Eq1 f) => Eq2 (FreeF f) where
+  liftEq2 eqA eqB = curry \case
+    Pure a :!: Pure a' -> eqA a a'
+    Free fb :!: Free fb' -> liftEq eqB fb fb'
+    _ :!: _ -> False
+
+instance (Ord1 f, Ord a) => Ord1 (FreeF f a) where
+  liftCompare = liftCompare2 compare
+
+instance (Ord1 f) => Ord2 (FreeF f) where
+  liftCompare2 compareA compareB = curry \case
+    Pure a :!: Pure a' -> compareA a a'
+    Pure _ :!: Free _ -> LT
+    Free _ :!: Pure _ -> GT
+    Free fb :!: Free fb' -> liftCompare compareB fb fb'
+
 -- * orphan instances for types from the strict library
 
 -- TODO: Explain why these instances are actually legit (fast & loose).
@@ -282,3 +404,7 @@ instance Monad Maybe where
 instance Comonad (Pair a) where
   extract = snd
   duplicate x@(a :!: _) = a :!: x
+
+-- | `Data.Strict.unzip` is just the wrong thing.
+unzip :: (Functor f) => f (Pair a b) -> Pair (f a) (f b)
+unzip x = fst <$> x :!: snd <$> x
diff --git a/core/src/Yaya/Retrofit.hs b/core/src/Yaya/Retrofit.hs
index f827a339..6803333a 100644
--- a/core/src/Yaya/Retrofit.hs
+++ b/core/src/Yaya/Retrofit.hs
@@ -47,7 +47,7 @@ import safe "base" Control.Category (id, (.))
 import safe "base" Control.Monad ((<=<))
 import safe "base" Control.Monad.Fail (fail)
 import safe "base" Data.Bifunctor (bimap)
-import safe "base" Data.Bool (Bool, otherwise, (&&))
+import safe "base" Data.Bool (Bool (True), otherwise, (&&))
 import safe "base" Data.Either (Either (Left), either)
 import safe "base" Data.Eq ((==))
 import safe "base" Data.Foldable (Foldable, foldl, length, null)
@@ -87,6 +87,7 @@ import safe "this" Yaya.Fold
     steppableReadPrec,
     steppableReadPrec',
   )
+import safe "this" Yaya.Strict (IsNonStrict, IsStrict, Strict)
 
 #if MIN_VERSION_template_haskell(2, 21, 0)
 type TyVarBndrUnit = TH.TyVarBndrUnit
@@ -336,16 +337,18 @@ makePrimForDI' rules safeVariant tyName vars cons = do
 
   (makeDataDefinition safeVariant tyNameF varsF consF :)
     <$> [d|
+      type instance Strict $(pure $ conAppsT tyNameF vars') = 'True
+
       instance Projectable (->) $(pure s) $(pure $ conAppsT tyNameF vars') where
         project = $(TH.LamCaseE <$> mkMorphism id (patternCon rules) cons')
 
       instance Steppable (->) $(pure s) $(pure $ conAppsT tyNameF vars') where
         embed = $(TH.LamCaseE <$> mkMorphism (patternCon rules) id cons')
 
-      instance Recursive (->) $(pure s) $(pure $ conAppsT tyNameF vars') where
+      instance (IsStrict $(pure s)) => Recursive (->) $(pure s) $(pure $ conAppsT tyNameF vars') where
         cata φ = φ . fmap (cata φ) . project
 
-      instance Corecursive (->) $(pure s) $(pure $ conAppsT tyNameF vars') where
+      instance (IsNonStrict $(pure s)) => Corecursive (->) $(pure s) $(pure $ conAppsT tyNameF vars') where
         ana ψ = embed . fmap (ana ψ) . ψ
       |]
 
diff --git a/core/src/Yaya/Strict.hs b/core/src/Yaya/Strict.hs
new file mode 100644
index 00000000..3fc49bce
--- /dev/null
+++ b/core/src/Yaya/Strict.hs
@@ -0,0 +1,178 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE Safe #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module Yaya.Strict
+  ( IsStrict,
+    IsNonStrict,
+    Strict,
+    PartialTypeError,
+    unsatisfiable,
+  )
+where
+
+import "base" Data.Bool (Bool (False, True))
+import "base" Data.Either (Either)
+import "base" Data.Functor.Const (Const)
+import "base" Data.Functor.Identity (Identity)
+import "base" Data.List.NonEmpty (NonEmpty)
+import "base" Data.Maybe (Maybe)
+import "base" Data.Type.Bool (Not)
+import "base" Data.Void (Void)
+import "base" Numeric.Natural (Natural)
+import "comonad" Control.Comonad.Trans.Env (EnvT)
+import "free" Control.Comonad.Cofree (Cofree)
+import "free" Control.Monad.Trans.Free (Free, FreeF, FreeT)
+import qualified "lens" Control.Lens as Lens
+import qualified "strict" Data.Strict as Strict
+#if MIN_VERSION_base(4, 19, 0)
+import "base" GHC.TypeError
+  ( Assert,
+    ErrorMessage (ShowType, Text, (:$$:), (:<>:)),
+    Unsatisfiable,
+    unsatisfiable
+  )
+import "base" GHC.TypeLits (Symbol)
+#else
+#if MIN_VERSION_base(4, 17, 0)
+import "base" GHC.TypeError
+  ( Assert,
+    ErrorMessage (ShowType, Text, (:$$:), (:<>:)),
+    TypeError,
+  )
+import "base" GHC.TypeLits (Symbol)
+#else
+import "base" Data.Kind (Constraint)
+import "base" GHC.TypeLits
+  ( ErrorMessage (ShowType, Text, (:$$:), (:<>:)),
+    Symbol,
+    TypeError,
+  )
+#endif
+import "base" Prelude (error)
+#endif
+
+-- | This tags types (and type constructors) with whether or not they are
+--   strict.
+--
+--   A type is only strict when all the following conditions hold:
+-- - no referenced type is non-strict
+-- - no non-phantom type parameter is applied to a non-strict type
+-- - all unapplied type parameters are strict (or phantom)
+--
+--  __FIXME__: This needs a third case (so, @`Maybe` `Bool`@) to distinguish
+--            “simple” types that can be used birecursively, because they have
+--             no recursive structure.
+type family Strict (t :: k) :: Bool
+
+type instance Strict (,) = 'False
+
+type instance Strict ((,) _a) = 'False
+
+type instance Strict (_a, _b) = 'False
+
+type instance Strict NonEmpty = 'False
+
+type instance Strict (NonEmpty _a) = 'False
+
+type instance Strict Natural = 'True
+
+type instance Strict Void = 'True
+
+type instance Strict Lens.Const = 'False
+
+-- | This is effectively `Strict` because it’s second type parameter is phantom.
+type instance Strict (Lens.Const _a) = 'True
+
+type instance Strict Lens.Identity = 'True
+
+type instance Strict [] = 'False
+
+type instance Strict [_a] = 'False
+
+type instance Strict Const = 'False
+
+-- | This is effectively `Strict` because it’s second type parameter is phantom.
+type instance Strict (Const _a) = 'True
+
+type instance Strict Identity = 'True
+
+type instance Strict Either = 'False
+
+type instance Strict (Either _a) = 'False
+
+type instance Strict (Either _a _b) = 'False
+
+type instance Strict Maybe = 'False
+
+type instance Strict (Maybe _a) = 'False
+
+type instance Strict Cofree = 'False
+
+type instance Strict (Cofree _f) = 'False
+
+type instance Strict (Cofree _f _a) = 'False
+
+type instance Strict (EnvT _a _f) = 'False
+
+type instance Strict (Free _f) = 'False
+
+type instance Strict (Free _f _a) = 'False
+
+type instance Strict (FreeF _f _a) = 'False
+
+type instance Strict FreeT = 'False
+
+type instance Strict Strict.Either = 'True
+
+type instance Strict (Strict.Either _a) = 'True
+
+type instance Strict (Strict.Either _a _b) = 'True
+
+type instance Strict Strict.Maybe = 'True
+
+type instance Strict (Strict.Maybe _a) = 'True
+
+type instance Strict Strict.Pair = 'True
+
+type instance Strict (Strict.Pair _a) = 'True
+
+type family ShowStrict (b :: Bool) :: Symbol where
+  ShowStrict 'True = "strict"
+  ShowStrict 'False = "non-strict"
+
+#if !MIN_VERSION_base(4, 19, 0)
+type Unsatisfiable msg = TypeError msg
+
+unsatisfiable :: a
+unsatisfiable = error "unsatisfiable"
+#endif
+
+#if !MIN_VERSION_base(4, 17, 0)
+type family Assert (check :: Bool) (errMsg :: Constraint) :: Constraint where
+  Assert 'True _ = ()
+  Assert _ errMsg = errMsg
+#endif
+
+-- | This `TypeError` is used to communicate why partial instances are
+--   unavailable, and what can be done instead.
+{- ORMOLU_DISABLE -}
+{- because it wants to remove the space after the tick, which triggers a GHC warning -}
+type PartialTypeError t =
+  Unsatisfiable
+    ( 'Text "‘"
+        ' :<>: 'ShowType t
+        ' :<>: 'Text "’ is "
+        ' :<>: 'Text (ShowStrict (Strict t))
+        ' :<>: 'Text ", so the instance would be partial."
+        ' :$$: 'Text
+                "See ‘yaya-unsafe:Yaya.Unsafe.Unsafe’ for the intended approach."
+    )
+{- ORMOLU_ENABLE -}
+
+type IsStrict t = Assert (Strict t) (PartialTypeError t)
+
+-- |
+--
+--  __FIXME__: This needs a different error message.
+type IsNonStrict t = Assert (Not (Strict t)) (PartialTypeError t)
diff --git a/core/src/Yaya/Zoo.hs b/core/src/Yaya/Zoo.hs
index dfc5ee3e..c0ecdb36 100644
--- a/core/src/Yaya/Zoo.hs
+++ b/core/src/Yaya/Zoo.hs
@@ -43,8 +43,6 @@ import "base" Data.Function (flip, ($))
 import "base" Data.Functor (Functor, fmap)
 import "base" Data.Traversable (Traversable, sequenceA)
 import "comonad" Control.Comonad (Comonad, duplicate, extract)
-import "comonad" Control.Comonad.Env (EnvT (EnvT))
-import "free" Control.Monad.Trans.Free (FreeF)
 import "profunctors" Data.Profunctor (Profunctor, lmap)
 import "this" Yaya.Fold
   ( Algebra,
@@ -76,6 +74,8 @@ import "this" Yaya.Fold.Common (diagonal, fromEither)
 import "this" Yaya.Pattern
   ( AndMaybe,
     Either (Left, Right),
+    EnvT (EnvT),
+    FreeF,
     Maybe,
     Pair ((:!:)),
     XNor,
diff --git a/core/yaya.cabal b/core/yaya.cabal
index 3a63aea9..3b5fc121 100644
--- a/core/yaya.cabal
+++ b/core/yaya.cabal
@@ -235,6 +235,7 @@ library
     Yaya.Functor
     Yaya.Pattern
     Yaya.Retrofit
+    Yaya.Strict
     Yaya.Zoo
   other-modules:
     Yaya.Fold.Native.Internal
diff --git a/hedgehog/src/Yaya/Hedgehog/Expr.hs b/hedgehog/src/Yaya/Hedgehog/Expr.hs
index 76ec2d2e..48ec903c 100644
--- a/hedgehog/src/Yaya/Hedgehog/Expr.hs
+++ b/hedgehog/src/Yaya/Hedgehog/Expr.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE Unsafe #-}
 
 module Yaya.Hedgehog.Expr
@@ -15,6 +16,7 @@ module Yaya.Hedgehog.Expr
 where
 
 import safe "base" Control.Applicative ((<*>))
+import safe "base" Data.Bool (Bool (True))
 import safe "base" Data.Eq (Eq)
 import safe "base" Data.Foldable (Foldable)
 import safe "base" Data.Functor (Functor, (<$>))
@@ -28,6 +30,7 @@ import safe qualified "hedgehog" Hedgehog.Gen as Gen
 import safe qualified "hedgehog" Hedgehog.Range as Range
 import safe "yaya" Yaya.Fold (Mu, Nu, Steppable)
 import safe "yaya" Yaya.Fold.Native (Cofix, Fix)
+import safe "yaya" Yaya.Strict (Strict)
 import safe "this" Yaya.Hedgehog.Fold (embeddableOfHeight)
 
 data Expr a
@@ -36,6 +39,10 @@ data Expr a
   | Mult a a
   deriving stock (Eq, Show, Functor, Foldable, Traversable)
 
+type instance Strict Expr = 'True
+
+type instance Strict (Expr _a) = 'True
+
 deriveEq1 ''Expr
 deriveShow1 ''Expr
 
diff --git a/hedgehog/src/Yaya/Hedgehog/Fold.hs b/hedgehog/src/Yaya/Hedgehog/Fold.hs
index c2572b6c..fc05927e 100644
--- a/hedgehog/src/Yaya/Hedgehog/Fold.hs
+++ b/hedgehog/src/Yaya/Hedgehog/Fold.hs
@@ -1,43 +1,29 @@
-{-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE Unsafe #-}
 {-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
 
 module Yaya.Hedgehog.Fold
-  ( corecursiveIsUnsafe,
-    embeddableOfHeight,
+  ( embeddableOfHeight,
     genAlgebra,
     genCorecursive,
     law_anaRefl,
     law_cataCancel,
     law_cataCompose,
     law_cataRefl,
-    recursiveIsUnsafe,
   )
 where
 
 import safe "base" Control.Category ((.))
 import safe "base" Data.Bifunctor (bimap, first)
 import safe "base" Data.Eq (Eq)
-import safe "base" Data.Function (($))
 import safe "base" Data.Functor (Functor, fmap)
 import safe "base" Data.Proxy (Proxy (Proxy))
-import safe qualified "base" Data.Tuple as Tuple
 import safe "base" Data.Void (Void, absurd)
 import safe "base" Numeric.Natural (Natural)
 import safe "base" Text.Show (Show)
-import "hedgehog" Hedgehog
-  ( Gen,
-    MonadTest,
-    Property,
-    Size,
-    property,
-    withTests,
-    (===),
-  )
+import "hedgehog" Hedgehog (Gen, MonadTest, Size, (===))
 import "yaya" Yaya.Fold
   ( Algebra,
     Corecursive,
-    Projectable,
     Recursive,
     Steppable,
     ana,
@@ -47,8 +33,7 @@ import "yaya" Yaya.Fold
   )
 import safe "yaya" Yaya.Fold.Common (diagonal)
 import safe "yaya" Yaya.Fold.Native ()
-import safe "yaya" Yaya.Pattern (Maybe, Pair ((:!:)), fst, maybe, uncurry)
-import "this" Yaya.Hedgehog (evalNonterminating)
+import safe "yaya" Yaya.Pattern (Maybe, maybe, uncurry)
 import safe "base" Prelude (fromIntegral)
 
 {-# HLINT ignore "Use camelCase" #-}
@@ -157,49 +142,3 @@ genAlgebra leaf branch =
 -- | Creates a generator for potentially-infinite values.
 genCorecursive :: (Corecursive (->) t f) => (a -> f a) -> Gen a -> Gen t
 genCorecursive = fmap . ana
-
--- | Show that using a `Recursive` structure corecursively can lead to
---   non-termination.
-corecursiveIsUnsafe ::
-  forall t a.
-  ( Corecursive (->) (t (Pair a)) (Pair a),
-    Projectable (->) (t (Pair a)) (Pair a),
-    Corecursive (->) (t ((,) a)) ((,) a),
-    Projectable (->) (t ((,) a)) ((,) a),
-    Eq a,
-    Show a
-  ) =>
-  Proxy t ->
-  a ->
-  Property
-corecursiveIsUnsafe Proxy x =
-  withTests 1 . property $ do
-    -- a properly-finite data structure will diverge on infinite unfolding
-    evalNonterminating . fst . project @_ @(t (Pair a)) $ ana (\y -> y :!: y) x
-    -- but using a lazy functor loses this property
-    Tuple.fst (project @_ @(t ((,) a)) $ ana (\y -> (y, y)) x) === x
-
--- | Show that using a `Corecursive` structure recursively can lead to
---   non-termination.
-recursiveIsUnsafe ::
-  forall t a.
-  ( Corecursive (->) (t (Pair a)) (Pair a),
-    Projectable (->) (t (Pair a)) (Pair a),
-    Recursive (->) (t (Pair a)) (Pair a),
-    Corecursive (->) (t ((,) a)) ((,) a),
-    Recursive (->) (t ((,) a)) ((,) a),
-    Eq a,
-    Show a
-  ) =>
-  Proxy t ->
-  a ->
-  Property
-recursiveIsUnsafe Proxy x =
-  withTests 1 . property $ do
-    -- We can easily get the first element of a corecursive infinite sequence
-    fst (project $ ana @_ @(t (Pair a)) (\y -> y :!: y) x) === x
-    -- Of course, you can’t fold it.
-    evalNonterminating . cata fst $ ana @_ @(t (Pair a)) (\y -> y :!: y) x
-    -- But again, if you use a lazy functor, you lose that property, and you can
-    -- short-circuit.
-    cata Tuple.fst (ana @_ @(t ((,) a)) (\y -> (y, y)) x) === x
diff --git a/hedgehog/tests/Test/Retrofit.hs b/hedgehog/tests/Test/Retrofit.hs
index 6d3bdd1d..f5b40fda 100644
--- a/hedgehog/tests/Test/Retrofit.hs
+++ b/hedgehog/tests/Test/Retrofit.hs
@@ -1,11 +1,13 @@
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE Unsafe #-}
 
 -- | The point of this module is that it should compile _without_ importing any
 --   other Yaya modules.
 module Test.Retrofit (tests) where
 
-import safe "base" Data.Bool (Bool)
+import safe "base" Data.Bool (Bool (True))
 import safe "base" Data.Eq (Eq, (==))
 import safe "base" Data.Int (Int)
 import safe "base" Data.Ord (Ord, compare)
@@ -30,12 +32,15 @@ import safe "yaya" Yaya.Retrofit
     recursiveShowsPrec,
     steppableReadPrec,
   )
+import safe "yaya" Yaya.Strict (Strict)
 
 data DExpr
   = Lit Int
   | Add DExpr DExpr
   | Mult DExpr DExpr
 
+type instance Strict DExpr = 'True
+
 extractPatternFunctor defaultRules ''DExpr
 
 deriving stock instance (Eq a) => Eq (DExprF a)
diff --git a/quickcheck/src/Yaya/QuickCheck/Fold.hs b/quickcheck/src/Yaya/QuickCheck/Fold.hs
index 83ce12c9..dc9e83fd 100644
--- a/quickcheck/src/Yaya/QuickCheck/Fold.hs
+++ b/quickcheck/src/Yaya/QuickCheck/Fold.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE Safe #-}
+{-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -Wno-orphans #-}
 {-# OPTIONS_GHC -fplugin-opt=NoRecursion:ignore-decls:arbitrarySteppable,shrinkSteppable #-}
 
@@ -42,7 +43,7 @@ instance (Foldable f, Functor f, QC.Arbitrary1 f) => QC.Arbitrary (Fix f) where
   arbitrary = arbitrarySteppable QC.liftArbitrary
   shrink = shrinkSteppable QC.liftShrink
 
-instance (Foldable f, Functor f, QC.Arbitrary1 f) => QC.Arbitrary (Mu f) where
+instance (Steppable (->) (Mu f) f, Foldable f, Functor f, QC.Arbitrary1 f) => QC.Arbitrary (Mu f) where
   arbitrary = arbitrarySteppable QC.liftArbitrary
   shrink = shrinkSteppable QC.liftShrink
 
diff --git a/unsafe/src/Yaya/Unsafe/Applied.hs b/unsafe/src/Yaya/Unsafe/Applied.hs
index 25407df2..f1c5f22b 100644
--- a/unsafe/src/Yaya/Unsafe/Applied.hs
+++ b/unsafe/src/Yaya/Unsafe/Applied.hs
@@ -1,15 +1,48 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# OPTIONS_GHC -Wno-orphans #-}
+
+-- __NB__: base-4.17 moves `IsList` to its own module, which avoids the unsafety
+--         of importing "GHC.Exts". With prior versions of base, we at least
+--         mark the module @Trustworthy@.
+#if MIN_VERSION_base(4, 17, 0)
 {-# LANGUAGE Safe #-}
+#else
+{-# LANGUAGE Trustworthy #-}
+#endif
 
-module Yaya.Unsafe.Applied
-  ( unsafeFromList,
-  )
-where
+module Yaya.Unsafe.Applied () where
 
-import "yaya" Yaya.Fold (Steppable, embed)
+import "yaya" Yaya.Fold (Mu)
+import "yaya" Yaya.Fold.Native (Fix)
 import "yaya" Yaya.Pattern (XNor)
-import "this" Yaya.Unsafe.Fold (unsafeCata)
+import "this" Yaya.Unsafe.Fold (Unsafe)
+
+-- See comment on @{-# LANGUAGE Safe #-}@ above.
+#if MIN_VERSION_base(4, 17, 0)
+import "base" GHC.IsList (IsList (Item, fromList, fromListN, toList))
+#else
+import "base" GHC.Exts (IsList (Item, fromList, fromListN, toList))
+#endif
+
+-- | `fromList` in this instance is unsafe, but `fromListN` is safe, because we
+--   have a finite length to fold.
+--
+--   This means that most uses of @OverloadedLists@ should be fine, but not the
+--   range (`..`) syntax.
+instance IsList (Unsafe (Fix (XNor a))) where
+  type Item (Unsafe (Fix (XNor a))) = a
+  fromList = fromList
+  fromListN = fromListN
+  toList = toList
 
--- | An unsafe implementation of `GHC.Exts.fromList` for `Steppable`
---   fixed-points of `XNor`.
-unsafeFromList :: (Steppable (->) t (XNor a)) => [a] -> t
-unsafeFromList = unsafeCata embed
+-- | `fromList` in this instance is unsafe, but `fromListN` is safe, because we
+--   have a finite length to fold.
+--
+--   This means that most uses of @OverloadedLists@ should be fine, but not the
+--   range (`..`) syntax.
+instance IsList (Unsafe (Mu (XNor a))) where
+  type Item (Unsafe (Mu (XNor a))) = a
+  fromList = fromList
+  fromListN = fromListN
+  toList = toList
diff --git a/unsafe/src/Yaya/Unsafe/Fold.hs b/unsafe/src/Yaya/Unsafe/Fold.hs
index 7a4c69e6..962cfb14 100644
--- a/unsafe/src/Yaya/Unsafe/Fold.hs
+++ b/unsafe/src/Yaya/Unsafe/Fold.hs
@@ -1,9 +1,14 @@
+{-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE Safe #-}
+{-# LANGUAGE TypeFamilies #-}
+-- For @type instance Strict (Unsafe t)@
+{-# LANGUAGE UndecidableInstances #-}
 
 -- | Definitions and instances that use direct recursion, which (because of
 --   laziness) can lead to non-termination.
 module Yaya.Unsafe.Fold
-  ( anaM,
+  ( Unsafe (..),
+    anaM,
     corecursivePrism,
     ganaM,
     ghylo,
@@ -21,11 +26,20 @@ where
 import "base" Control.Applicative (pure)
 import "base" Control.Category ((.))
 import "base" Control.Monad (Monad, (<=<))
+import "base" Data.Eq (Eq, (==))
+import "base" Data.Foldable (Foldable)
 import "base" Data.Function (flip, ($))
-import "base" Data.Functor (Functor, fmap)
+import "base" Data.Functor (Functor, fmap, (<$>))
+import "base" Data.Functor.Classes (Eq1, Ord1, Show1)
 import "base" Data.Functor.Compose (Compose (Compose), getCompose)
+import "base" Data.List.NonEmpty (NonEmpty)
+import "base" Data.Ord (Ord, compare)
 import "base" Data.Traversable (Traversable, sequenceA)
+import "base" Data.Type.Bool (Not)
+import "base" GHC.Generics (Generic, Generic1)
+import "base" Text.Show (Show, showsPrec)
 import "comonad" Control.Comonad (Comonad, extract)
+import "free" Control.Comonad.Cofree (Cofree)
 import "lens" Control.Lens (Prism', matching, prism, review)
 import "yaya" Yaya.Fold
   ( Algebra,
@@ -39,6 +53,8 @@ import "yaya" Yaya.Fold
     GAlgebraM,
     GCoalgebra,
     GCoalgebraM,
+    Mu,
+    Nu,
     Projectable,
     Recursive,
     Steppable,
@@ -50,8 +66,21 @@ import "yaya" Yaya.Fold
     lowerCoalgebra,
     lowerCoalgebraM,
     project,
+    recursiveCompare,
+    recursiveEq,
+    recursiveShowsPrec,
   )
-import "yaya" Yaya.Pattern (Maybe, Pair, maybe, uncurry)
+import "yaya" Yaya.Fold.Native (Cofix, Fix)
+import "yaya" Yaya.Pattern
+  ( AndMaybe,
+    EnvT,
+    Maybe,
+    Pair,
+    XNor,
+    maybe,
+    uncurry,
+  )
+import "yaya" Yaya.Strict (IsNonStrict, IsStrict, Strict)
 
 -- | Instances leak transitively, so while "Yaya.Unsafe.Fold.Instances" exists,
 --   it should only be used when it is unavoidable. If you are explicitly
@@ -272,3 +301,201 @@ corecursivePrism ::
   CoalgebraPrism f a ->
   Prism' a t
 corecursivePrism alg = prism (cata $ review alg) (anaM $ matching alg)
+
+-- | This is a trivial wrapper that exposes partial instances on recursive types.
+newtype Unsafe t = Unsafe t
+  deriving stock (Foldable, Functor, Generic, Generic1, Traversable)
+
+-- | The unsafe variant has the opposite strictness. Once we support “simple”
+--   types, this should probably be `Nothing`.
+type instance Strict (Unsafe t) = Not (Strict t)
+
+-- |
+--
+--  __NB__: This operation isn’t unsafe itself, it just lifts an underlying
+--         `project` to the `Unsafe` newtype.
+unsafeProject :: (Projectable (->) t f, Functor f) => Unsafe t -> f (Unsafe t)
+unsafeProject (Unsafe t) = Unsafe <$> project t
+
+-- |
+--
+--  __NB__: This operation isn’t unsafe itself, it just lifts an underlying
+--         `embed` to the `Unsafe` newtype.
+unsafeEmbed :: (Steppable (->) t f, Functor f) => f (Unsafe t) -> Unsafe t
+unsafeEmbed = Unsafe . embed . fmap (\(Unsafe t) -> t)
+
+-- instance (Projectable (->) t f) => Projectable (->) (Unsafe t) f where
+--   project = unsafeProject
+
+-- instance (Steppable (->) t f) => Steppable (->) (Unsafe t) f where
+--   embed = unsafeEmbed
+
+instance (Functor f) => Projectable (->) (Unsafe (Fix f)) f where
+  project = unsafeProject
+
+instance (Functor f) => Steppable (->) (Unsafe (Fix f)) f where
+  embed = unsafeEmbed
+
+instance
+  (IsNonStrict (Unsafe (Fix f)), Functor f) =>
+  Corecursive (->) (Unsafe (Fix f)) f
+  where
+  ana = unsafeAna
+
+instance (Functor f) => Projectable (->) (Unsafe (Cofix f)) f where
+  project = unsafeProject
+
+instance (Functor f) => Steppable (->) (Unsafe (Cofix f)) f where
+  embed = unsafeEmbed
+
+instance
+  (IsStrict f, IsStrict (Unsafe (Cofix f)), Functor f) =>
+  Recursive (->) (Unsafe (Cofix f)) f
+  where
+  cata = unsafeCata
+
+instance
+  (Recursive (->) (Unsafe (Cofix f)) f, Functor f, Foldable f, Eq1 f) =>
+  Eq (Unsafe (Cofix f))
+  where
+  (==) = recursiveEq
+
+instance
+  (Recursive (->) (Unsafe (Cofix f)) f, Functor f, Foldable f, Ord1 f) =>
+  Ord (Unsafe (Cofix f))
+  where
+  compare = recursiveCompare
+
+instance
+  (Recursive (->) (Unsafe (Cofix f)) f, Functor f, Show1 f) =>
+  Show (Unsafe (Cofix f))
+  where
+  showsPrec = recursiveShowsPrec
+
+instance
+  (Projectable (->) (Mu f) f, Functor f) =>
+  Projectable (->) (Unsafe (Mu f)) f
+  where
+  project = unsafeProject
+
+instance
+  (Steppable (->) (Mu f) f, Functor f) =>
+  Steppable (->) (Unsafe (Mu f)) f
+  where
+  embed = unsafeEmbed
+
+instance
+  (Steppable (->) (Mu f) f, IsNonStrict (Unsafe (Mu f)), Functor f) =>
+  Corecursive (->) (Unsafe (Mu f)) f
+  where
+  ana = unsafeAna
+
+instance (Functor f) => Projectable (->) (Unsafe (Nu f)) f where
+  project = unsafeProject
+
+instance (Functor f) => Steppable (->) (Unsafe (Nu f)) f where
+  embed = unsafeEmbed
+
+instance
+  (IsStrict f, IsStrict (Unsafe (Nu f)), Functor f) =>
+  Recursive (->) (Unsafe (Nu f)) f
+  where
+  cata = unsafeCata
+
+instance
+  (Recursive (->) (Nu f) f, Functor f, Foldable f, Eq1 f) =>
+  Eq (Unsafe (Nu f))
+  where
+  (==) = recursiveEq
+
+instance
+  (Recursive (->) (Nu f) f, Functor f, Foldable f, Ord1 f) =>
+  Ord (Unsafe (Nu f))
+  where
+  compare = recursiveCompare
+
+instance
+  (Recursive (->) (Nu f) f, Functor f, Show1 f) =>
+  Show (Unsafe (Nu f))
+  where
+  showsPrec = recursiveShowsPrec
+
+instance Projectable (->) (Unsafe [a]) (XNor a) where
+  project = unsafeProject
+
+instance Steppable (->) (Unsafe [a]) (XNor a) where
+  embed = unsafeEmbed
+
+instance Recursive (->) (Unsafe [a]) (XNor a) where
+  cata = unsafeCata
+
+instance (Recursive (->) (Unsafe [a]) (XNor a), Eq a) => Eq (Unsafe [a]) where
+  (==) = recursiveEq
+
+instance (Recursive (->) (Unsafe [a]) (XNor a), Ord a) => Ord (Unsafe [a]) where
+  compare = recursiveCompare
+
+instance
+  (Recursive (->) (Unsafe [a]) (XNor a), Show a) =>
+  Show (Unsafe [a])
+  where
+  showsPrec = recursiveShowsPrec
+
+instance Projectable (->) (Unsafe (NonEmpty a)) (AndMaybe a) where
+  project = unsafeProject
+
+instance Steppable (->) (Unsafe (NonEmpty a)) (AndMaybe a) where
+  embed = unsafeEmbed
+
+instance Recursive (->) (Unsafe (NonEmpty a)) (AndMaybe a) where
+  cata = unsafeCata
+
+instance
+  (Recursive (->) (Unsafe (NonEmpty a)) (AndMaybe a), Eq a) =>
+  Eq (Unsafe (NonEmpty a))
+  where
+  (==) = recursiveEq
+
+instance
+  (Recursive (->) (Unsafe (NonEmpty a)) (AndMaybe a), Ord a) =>
+  Ord (Unsafe (NonEmpty a))
+  where
+  compare = recursiveCompare
+
+instance
+  (Recursive (->) (Unsafe (NonEmpty a)) (AndMaybe a), Show a) =>
+  Show (Unsafe (NonEmpty a))
+  where
+  showsPrec = recursiveShowsPrec
+
+instance (Functor f) => Projectable (->) (Unsafe (Cofree f a)) (EnvT a f) where
+  project = unsafeProject
+
+instance (Functor f) => Steppable (->) (Unsafe (Cofree f a)) (EnvT a f) where
+  embed = unsafeEmbed
+
+instance (Functor f) => Recursive (->) (Unsafe (Cofree f a)) (EnvT a f) where
+  cata = unsafeCata
+
+instance (Foldable f, Functor f, Eq1 f, Eq a) => Eq (Unsafe (Cofree f a)) where
+  (==) = recursiveEq
+
+instance
+  (Foldable f, Functor f, Ord1 f, Ord a) =>
+  Ord (Unsafe (Cofree f a))
+  where
+  compare = recursiveCompare
+
+instance (Functor f, Show1 f, Show a) => Show (Unsafe (Cofree f a)) where
+  showsPrec = recursiveShowsPrec
+
+------ checked to here
+
+-- instance (Functor f) => Projectable (->) (Unsafe (Free f a)) (FreeF f a) where
+--   project = unsafeProject
+
+-- instance (Functor f) => Steppable (->) (Unsafe (Free f a)) (FreeF f a) where
+--   embed = unsafeEmbed
+
+-- instance (Functor f) => Recursive (->) (Unsafe (Free f a)) (FreeF f a) where
+--   cata = unsafeCata
diff --git a/unsafe/src/Yaya/Unsafe/Fold/Instances.hs b/unsafe/src/Yaya/Unsafe/Fold/Instances.hs
index 70fbcce6..bdf1ec96 100644
--- a/unsafe/src/Yaya/Unsafe/Fold/Instances.hs
+++ b/unsafe/src/Yaya/Unsafe/Fold/Instances.hs
@@ -58,68 +58,8 @@ import "base" GHC.IsList (IsList (Item, fromList, fromListN, toList))
 import "base" GHC.Exts (IsList (Item, fromList, fromListN, toList))
 #endif
 
-instance (Functor f) => Corecursive (->) (Fix f) f where
-  ana = Unsafe.hylo embed
-
-instance (Functor f) => Recursive (->) (Cofix f) f where
-  cata = flip Unsafe.hylo project
-
-instance (Functor f, Foldable f, Eq1 f) => Eq (Cofix f) where
-  (==) = recursiveEq
-
--- | @since 0.4.1.0
-instance (Functor f, Foldable f, Ord1 f) => Ord (Cofix f) where
-  compare = recursiveCompare
-
-instance (Functor f, Show1 f) => Show (Cofix f) where
-  showsPrec = recursiveShowsPrec
-
-instance (Functor f) => Corecursive (->) (Mu f) f where
-  ana = Unsafe.unsafeAna
-
-instance (Functor f) => Recursive (->) (Nu f) f where
-  cata = Unsafe.unsafeCata
-
-instance (Functor f, Foldable f, Eq1 f) => Eq (Nu f) where
-  (==) = recursiveEq
-
--- | @since 0.4.1.0
-instance (Functor f, Foldable f, Ord1 f) => Ord (Nu f) where
-  compare = recursiveCompare
-
-instance (Functor f, Show1 f) => Show (Nu f) where
-  showsPrec = recursiveShowsPrec
-
-instance Recursive (->) [a] (XNor a) where
-  cata = Unsafe.unsafeCata
-
-instance Recursive (->) (NonEmpty a) (AndMaybe a) where
-  cata = Unsafe.unsafeCata
-
 instance (Functor f) => Recursive (->) (Cofree f a) (EnvT a f) where
   cata = Unsafe.unsafeCata
 
 instance (Functor f) => Recursive (->) (Free f a) (FreeF f a) where
   cata = Unsafe.unsafeCata
-
--- | `fromList` in this instance is unsafe, but `fromListN` is safe, because we
---   have a finite length to fold.
---
---   This means that most uses of @OverloadedLists@ should be fine, but not the
---   range (`..`) syntax.
-instance IsList (Fix (XNor a)) where
-  type Item (Fix (XNor a)) = a
-  fromList = unsafeFromList
-  fromListN = fromListN
-  toList = toList
-
--- | `fromList` in this instance is unsafe, but `fromListN` is safe, because we
---   have a finite length to fold.
---
---   This means that most uses of @OverloadedLists@ should be fine, but not the
---   range (`..`) syntax.
-instance IsList (Mu (XNor a)) where
-  type Item (Mu (XNor a)) = a
-  fromList = unsafeFromList
-  fromListN = fromListN
-  toList = toList
diff --git a/unsafe/src/Yaya/Unsafe/Zoo.hs b/unsafe/src/Yaya/Unsafe/Zoo.hs
index a13292b1..a820b609 100644
--- a/unsafe/src/Yaya/Unsafe/Zoo.hs
+++ b/unsafe/src/Yaya/Unsafe/Zoo.hs
@@ -27,8 +27,6 @@ import "base" Data.Functor.Compose (Compose (Compose), getCompose)
 import "base" Data.Functor.Identity (Identity (Identity), runIdentity)
 import "base" Data.Traversable (Traversable)
 import "comonad" Control.Comonad (Comonad)
-import "comonad" Control.Comonad.Env (EnvT)
-import "free" Control.Monad.Trans.Free (FreeF)
 import "yaya" Yaya.Fold
   ( Algebra,
     Coalgebra,
@@ -55,6 +53,8 @@ import "yaya" Yaya.Fold.Common (diagonal, fromEither)
 import "yaya" Yaya.Fold.Native ()
 import "yaya" Yaya.Pattern
   ( Either,
+    EnvT,
+    FreeF,
     Maybe (Nothing),
     Pair ((:!:)),
     XNor (Both, Neither),
diff --git a/unsafe/tests/Test/Fold.hs b/unsafe/tests/Test/Fold.hs
index 19453f77..08cc7cfc 100644
--- a/unsafe/tests/Test/Fold.hs
+++ b/unsafe/tests/Test/Fold.hs
@@ -5,95 +5,160 @@
 
 module Test.Fold (tests) where
 
-import safe "base" Control.Category (id)
+import safe "base" Control.Category (id, (.))
 import safe "base" Control.Monad ((=<<))
 import safe "base" Data.Bool (Bool)
+import safe "base" Data.Eq (Eq)
 import safe "base" Data.Function (($))
+import safe "base" Data.Functor ((<$>))
 import safe "base" Data.Int (Int)
 import safe "base" Data.Proxy (Proxy (Proxy))
 import safe "base" System.IO (IO)
+import safe "base" Text.Show (Show)
 import safe "hedgehog" Hedgehog
   ( Property,
     checkParallel,
     discover,
     forAll,
     property,
+    withTests,
+    (===),
   )
 import safe qualified "hedgehog" Hedgehog.Gen as Gen
-import safe "yaya" Yaya.Fold (Mu, Nu)
+import safe "yaya" Yaya.Fold
+  ( Corecursive,
+    Mu,
+    Nu,
+    Projectable,
+    Recursive,
+    ana,
+    cata,
+    project,
+  )
 import safe "yaya" Yaya.Fold.Common (size)
-import safe "yaya" Yaya.Fold.Native (Cofix, Fix)
+import safe "yaya" Yaya.Fold.Native (Cofix)
+import safe "yaya" Yaya.Pattern (Pair ((:!:)), fst)
+import "yaya-hedgehog" Yaya.Hedgehog (evalNonterminating)
 import safe "yaya-hedgehog" Yaya.Hedgehog.Expr
   ( Expr,
     genCofixExpr,
     genExpr,
-    genFixExpr,
-    genMuExpr,
-    genNuExpr,
+    -- genFixExpr,
+    -- genMuExpr,
+    -- genNuExpr,
   )
 import safe "yaya-hedgehog" Yaya.Hedgehog.Fold
-  ( corecursiveIsUnsafe,
-    law_anaRefl,
+  ( -- law_anaRefl,
     law_cataCancel,
     law_cataCompose,
     law_cataRefl,
-    recursiveIsUnsafe,
   )
-import safe qualified "yaya-unsafe" Yaya.Unsafe.Fold.Instances ()
+import "yaya-unsafe" Yaya.Unsafe.Fold (Unsafe (Unsafe))
 
 -- TODO: For some reason HLint is complaining that TemplateHaskell is unused.
 {-# HLINT ignore "Unused LANGUAGE pragma" #-}
 
-prop_fixAnaRefl :: Property
-prop_fixAnaRefl =
-  property $ law_anaRefl =<< forAll (Gen.sized genFixExpr)
+-- prop_fixAnaRefl :: Property
+-- prop_fixAnaRefl =
+--   property $ law_anaRefl =<< forAll (fmap Unsafe . Gen.sized genFixExpr)
 
--- | NB: Only in yaya-unsafe instead of yaya because the `Eq (Cofix f)` instance
---       is needed.
-prop_cofixAnaRefl :: Property
-prop_cofixAnaRefl =
-  property $ law_anaRefl =<< forAll (Gen.sized genCofixExpr)
+-- -- | NB: Only in yaya-unsafe instead of yaya because the `Eq (Cofix f)` instance
+-- --       is needed.
+-- prop_cofixAnaRefl :: Property
+-- prop_cofixAnaRefl =
+--   property $ law_anaRefl =<< forAll (fmap Unsafe . (Gen.sized genCofixExpr))
 
 prop_cofixCataCancel :: Property
 prop_cofixCataCancel =
-  property $ law_cataCancel size =<< forAll (genExpr (Gen.sized genCofixExpr))
+  property $
+    law_cataCancel size
+      =<< forAll (genExpr (Unsafe <$> Gen.sized genCofixExpr))
 
 prop_cofixCataRefl :: Property
 prop_cofixCataRefl =
-  property $ law_cataRefl =<< forAll (Gen.sized genCofixExpr)
+  property $ law_cataRefl =<< forAll (Unsafe <$> Gen.sized genCofixExpr)
 
 prop_cofixCataCompose :: Property
 prop_cofixCataCompose =
   property $
-    law_cataCompose (Proxy :: Proxy (Fix Expr)) size id
-      =<< forAll (Gen.sized genCofixExpr)
-
--- | NB: Only in yaya-unsafe instead of yaya because the `Eq (Nu f)` instance is
---       needed.
-prop_nuAnaRefl :: Property
-prop_nuAnaRefl =
-  property $ law_anaRefl =<< forAll (Gen.sized genNuExpr)
-
-prop_nuCataCancel :: Property
-prop_nuCataCancel =
-  property $ law_cataCancel size =<< forAll (genExpr (Gen.sized genNuExpr))
-
-prop_nuCataRefl :: Property
-prop_nuCataRefl =
-  property $ law_cataRefl =<< forAll (Gen.sized genNuExpr)
-
-prop_nuCataCompose :: Property
-prop_nuCataCompose =
-  property $
-    law_cataCompose (Proxy :: Proxy (Nu Expr)) size id
-      =<< forAll (Gen.sized genNuExpr)
-
-prop_muAnaRefl :: Property
-prop_muAnaRefl =
-  property $ law_anaRefl =<< forAll (Gen.sized genMuExpr)
+    law_cataCompose (Proxy :: Proxy (Unsafe (Cofix Expr))) size id
+      =<< forAll (Unsafe <$> Gen.sized genCofixExpr)
+
+-- -- | NB: Only in yaya-unsafe instead of yaya because the `Eq (Nu f)` instance is
+-- --       needed.
+-- prop_nuAnaRefl :: Property
+-- prop_nuAnaRefl =
+--   property $ law_anaRefl =<< forAll (Gen.sized genNuExpr)
+
+-- prop_nuCataCancel :: Property
+-- prop_nuCataCancel =
+--   property $
+--     law_cataCancel size =<< forAll (genExpr (Unsafe <$> Gen.sized genNuExpr))
+
+-- prop_nuCataRefl :: Property
+-- prop_nuCataRefl =
+--   property $ law_cataRefl =<< forAll (Unsafe <$> Gen.sized genNuExpr)
+
+-- prop_nuCataCompose :: Property
+-- prop_nuCataCompose =
+--   property $
+--     law_cataCompose (Proxy :: Proxy (Unsafe (Nu Expr))) size id
+--       =<< forAll (Unsafe <$> Gen.sized genNuExpr)
+
+-- prop_muAnaRefl :: Property
+-- prop_muAnaRefl =
+--   property $ law_anaRefl =<< forAll (Gen.sized genMuExpr)
 
 -- * These tests try to verify non-termination behavior.
 
+-- | Show that using a `Recursive` structure corecursively can lead to
+--   non-termination.
+corecursiveIsUnsafe ::
+  forall t a.
+  ( Corecursive (->) (Unsafe (t (Pair a))) (Pair a),
+    Projectable (->) (Unsafe (t (Pair a))) (Pair a),
+    -- Corecursive (->) (Unsafe (t ((,) a))) ((,) a),
+    -- Projectable (->) (Unsafe (t ((,) a))) ((,) a),
+    -- Eq a,
+    Show a
+  ) =>
+  Proxy t ->
+  a ->
+  Property
+corecursiveIsUnsafe Proxy x =
+  withTests 1 . property $ do
+    -- a properly-finite data structure will diverge on infinite unfolding
+    evalNonterminating . fst . project @_ @(Unsafe (t (Pair a))) $ ana (\y -> y :!: y) x
+
+-- -- but using a lazy functor loses this property
+-- Tuple.fst (project @_ @(Unsafe (t ((,) a))) $ ana (\y -> (y, y)) x) === x
+
+-- | Show that using a `Corecursive` structure recursively can lead to
+--   non-termination.
+recursiveIsUnsafe ::
+  forall t a.
+  ( Corecursive (->) (t (Pair a)) (Pair a),
+    Projectable (->) (t (Pair a)) (Pair a),
+    Recursive (->) (Unsafe (t (Pair a))) (Pair a),
+    -- Corecursive (->) (t ((,) a)) ((,) a),
+    -- Recursive (->) (Unsafe (t ((,) a))) ((,) a),
+    Eq a,
+    Show a
+  ) =>
+  Proxy t ->
+  a ->
+  Property
+recursiveIsUnsafe Proxy x =
+  withTests 1 . property $ do
+    -- We can easily get the first element of a corecursive infinite sequence
+    fst (project $ ana @_ @(t (Pair a)) (\y -> y :!: y) x) === x
+    -- Of course, you can’t fold it.
+    evalNonterminating . cata fst . Unsafe $ ana @_ @(t (Pair a)) (\y -> y :!: y) x
+
+-- -- But again, if you use a lazy functor, you lose that property, and you can
+-- -- short-circuit.
+-- cata Tuple.fst (Unsafe $ ana @_ @(t ((,) a)) (\y -> (y, y)) x) === x
+
 prop_muIsntCorecursive :: Property
 prop_muIsntCorecursive = corecursiveIsUnsafe (Proxy :: Proxy Mu) (1 :: Int)
 
diff --git a/unsafe/yaya-unsafe.cabal b/unsafe/yaya-unsafe.cabal
index cf094db5..c02b894a 100644
--- a/unsafe/yaya-unsafe.cabal
+++ b/unsafe/yaya-unsafe.cabal
@@ -225,7 +225,6 @@ library
   exposed-modules:
     Yaya.Unsafe.Applied
     Yaya.Unsafe.Fold
-    Yaya.Unsafe.Fold.Instances
     Yaya.Unsafe.Zoo
 
 test-suite doctests