From aa5f290df2ea12a4cae04d8445f821d40ec64e76 Mon Sep 17 00:00:00 2001
From: Brent Yorgey <byorgey@gmail.com>
Date: Sun, 2 Jun 2024 13:35:35 -0500
Subject: [PATCH 1/8] equirecursive types

---
 src/swarm-lang/Swarm/Language/Capability.hs  |  2 ++
 src/swarm-lang/Swarm/Language/Kindcheck.hs   | 21 +++++++------
 src/swarm-lang/Swarm/Language/Parser/Lex.hs  |  2 +-
 src/swarm-lang/Swarm/Language/Parser/Type.hs | 27 +++++++++++++++++
 src/swarm-lang/Swarm/Language/Pretty.hs      |  6 ++++
 src/swarm-lang/Swarm/Language/Types.hs       | 32 ++++++++++++++++++++
 6 files changed, 80 insertions(+), 10 deletions(-)

diff --git a/src/swarm-lang/Swarm/Language/Capability.hs b/src/swarm-lang/Swarm/Language/Capability.hs
index 101055eb3..8600911f3 100644
--- a/src/swarm-lang/Swarm/Language/Capability.hs
+++ b/src/swarm-lang/Swarm/Language/Capability.hs
@@ -185,6 +185,8 @@ data Capability
     CHandleinput
   | -- | Capability to make other robots halt.
     CHalt
+  | -- | Capability to handle recursive types.
+    CRectype
   | -- | God-like capabilities.  For e.g. commands intended only for
     --   checking challenge mode win conditions, and not for use by
     --   players.
diff --git a/src/swarm-lang/Swarm/Language/Kindcheck.hs b/src/swarm-lang/Swarm/Language/Kindcheck.hs
index 9105cdc4c..3978736f9 100644
--- a/src/swarm-lang/Swarm/Language/Kindcheck.hs
+++ b/src/swarm-lang/Swarm/Language/Kindcheck.hs
@@ -35,12 +35,15 @@ checkPolytypeKind pty@(Forall xs t) = TydefInfo pty (Arity $ length xs) <$ check
 --   Type) -> Type@ etc.) which would require generalizing this
 --   checking code a bit.
 checkKind :: (Has (Reader TDCtx) sig m, Has (Throw KindError) sig m) => Type -> m ()
-checkKind ty@(Fix (TyConF c tys)) = do
-  tdCtx <- ask
-  case getArity <$> tcArity tdCtx c of
-    Nothing -> throwError $ UndefinedTyCon c ty
-    Just a -> case compare (length tys) a of
-      EQ -> mapM_ checkKind tys
-      _ -> throwError $ ArityMismatch c a tys
-checkKind (Fix (TyVarF _)) = return ()
-checkKind (Fix (TyRcdF m)) = mapM_ checkKind m
+checkKind ty@(Fix tyF) = case tyF of
+  TyConF c tys -> do
+    tdCtx <- ask
+    case getArity <$> tcArity tdCtx c of
+      Nothing -> throwError $ UndefinedTyCon c ty
+      Just a -> case compare (length tys) a of
+        EQ -> mapM_ checkKind tys
+        _ -> throwError $ ArityMismatch c a tys
+  TyVarF _ -> return ()
+  TyRcdF m -> mapM_ checkKind m
+  TyRecF _ t -> checkKind t
+  TyRecVarF _ -> return ()
diff --git a/src/swarm-lang/Swarm/Language/Parser/Lex.hs b/src/swarm-lang/Swarm/Language/Parser/Lex.hs
index ffec58f0f..3972f58f3 100644
--- a/src/swarm-lang/Swarm/Language/Parser/Lex.hs
+++ b/src/swarm-lang/Swarm/Language/Parser/Lex.hs
@@ -164,7 +164,7 @@ primitiveTypeNames = "Cmd" : baseTypeNames
 
 -- | List of keywords built into the language.
 keywords :: [Text]
-keywords = T.words "let in def tydef end true false forall require requirements"
+keywords = T.words "let in def tydef end true false forall require requirements rec"
 
 -- | List of reserved words that cannot be used as variable names.
 reservedWords :: Set Text
diff --git a/src/swarm-lang/Swarm/Language/Parser/Type.hs b/src/swarm-lang/Swarm/Language/Parser/Type.hs
index 2798e2f80..c4705ffa4 100644
--- a/src/swarm-lang/Swarm/Language/Parser/Type.hs
+++ b/src/swarm-lang/Swarm/Language/Parser/Type.hs
@@ -16,6 +16,7 @@ import Control.Lens (view)
 import Control.Monad (join)
 import Control.Monad.Combinators (many)
 import Control.Monad.Combinators.Expr (Operator (..), makeExprParser)
+import Data.Fix (Fix (..), foldFix)
 import Data.Maybe (fromMaybe)
 import Data.Set qualified as S
 import Swarm.Language.Parser.Core (LanguageVersion (..), Parser, languageVersion)
@@ -90,6 +91,7 @@ parseTypeAtom =
     <|> TyConApp <$> parseTyCon <*> pure []
     <|> TyDelay <$> braces parseType
     <|> TyRcd <$> brackets (parseRecord (symbol ":" *> parseType))
+    <|> tyRec <$> (reserved "rec" *> tyVar) <*> (symbol "." *> parseType)
     <|> parens parseType
 
 -- | A type constructor.
@@ -104,3 +106,28 @@ parseTyCon = do
   choice (map (\b -> TCBase b <$ reservedCase (baseTyName b)) listEnums)
     <|> TCCmd <$ reservedCase "Cmd"
     <|> TCUser <$> tyName
+
+-- | Close over a recursive type, replacing any bound occurrences
+--   of its variable in the body with de Bruijn indices.  Note that
+--   (1) we don't have to worry about conflicts with type variables
+--   bound by a top-level @forall@; since @forall@ must always be at
+--   the top level, any @rec@ will necessarily be lexically within the
+--   scope of any @forall@ and hence variables bound by @rec@ will
+--   shadow any variables bound by a @forall@.  For example, @forall
+--   a. a -> (rec a. unit + a)@ is a function from an arbitrary type
+--   to a recursive natural number. (2) Any @rec@ contained inside
+--   this one will have already been closed over when it was parsed,
+--   and its bound variables thus replaced by de Bruijn indices, so
+--   neither do we have to worry about being shadowed --- any
+--   remaining free occurrences of the variable name in question are
+--   indeed references to this @rec@ binder.
+tyRec :: Var -> Type -> Type
+tyRec x = TyRec x . ($ NZ) . foldFix s
+ where
+  s :: TypeF (Nat -> Type) -> Nat -> Type
+  s = \case
+    TyRecF y ty -> Fix . TyRecF y . ty . NS
+    TyVarF y
+      | x == y -> Fix . TyRecVarF
+      | otherwise -> const (Fix (TyVarF y))
+    fty -> \i -> Fix (fmap ($ i) fty)
diff --git a/src/swarm-lang/Swarm/Language/Pretty.hs b/src/swarm-lang/Swarm/Language/Pretty.hs
index 8d11deace..1e8607d95 100644
--- a/src/swarm-lang/Swarm/Language/Pretty.hs
+++ b/src/swarm-lang/Swarm/Language/Pretty.hs
@@ -154,6 +154,7 @@ instance (PrettyPrec (t (Free t v)), PrettyPrec v) => PrettyPrec (Free t v) wher
   prettyPrec p (Free t) = prettyPrec p t
   prettyPrec p (Pure v) = prettyPrec p v
 
+-- XXX use case!
 instance ((UnchainableFun t), (PrettyPrec t)) => PrettyPrec (TypeF t) where
   prettyPrec _ (TyVarF v) = pretty v
   prettyPrec _ (TyRcdF m) = brackets $ hsep (punctuate "," (map prettyBinding (M.assocs m)))
@@ -173,6 +174,9 @@ instance ((UnchainableFun t), (PrettyPrec t)) => PrettyPrec (TypeF t) where
         multiLine l r = l <+> "->" <> hardline <> r
      in pparens (p > 1) . align $
           flatAlt (concatWith multiLine funs) (concatWith inLine funs)
+  -- Recursive types XXX
+  prettyPrec _ (TyRecVarF i) = pretty (show (natToInt i))
+  prettyPrec p (TyRecF _ ty) = pparens (p > 0) $ "rec." <+> prettyPrec 0 ty
   -- Fallthrough cases for type constructor application.  Handles base
   -- types, Cmd, user-defined types, or ill-kinded things like 'Int
   -- Bool'.
@@ -474,6 +478,8 @@ tyNounPhrase = \case
   TyConF c _ -> tyConNounPhrase c
   TyVarF {} -> "a type variable"
   TyRcdF {} -> "a record"
+  TyRecF {} -> "a recursive type"
+  TyRecVarF {} -> "a recursive type variable"
 
 tyConNounPhrase :: TyCon -> Doc a
 tyConNounPhrase = \case
diff --git a/src/swarm-lang/Swarm/Language/Types.hs b/src/swarm-lang/Swarm/Language/Types.hs
index 0bdab7c14..660795cbf 100644
--- a/src/swarm-lang/Swarm/Language/Types.hs
+++ b/src/swarm-lang/Swarm/Language/Types.hs
@@ -21,6 +21,10 @@ module Swarm.Language.Types (
   -- ** Type structure functor
   TypeF (..),
 
+  -- ** Recursive types
+  Nat (..),
+  natToInt,
+
   -- * @Type@
   Type,
   tyVars,
@@ -42,6 +46,7 @@ module Swarm.Language.Types (
   pattern TyCmd,
   pattern TyDelay,
   pattern TyUser,
+  pattern TyRec,
 
   -- * @UType@
   IntVar (..),
@@ -64,6 +69,7 @@ module Swarm.Language.Types (
   pattern UTyCmd,
   pattern UTyDelay,
   pattern UTyUser,
+  pattern UTyRec,
 
   -- ** Utilities
   ucata,
@@ -149,6 +155,19 @@ data BaseTy
 baseTyName :: BaseTy -> Text
 baseTyName = into @Text . drop 1 . show
 
+------------------------------------------------------------
+-- Recursive type utilities
+------------------------------------------------------------
+
+data Nat where
+  NZ :: Nat
+  NS :: Nat -> Nat
+  deriving (Eq, Ord, Show, Data, Generic, FromJSON, ToJSON)
+
+natToInt :: Nat -> Int
+natToInt NZ = 0
+natToInt (NS n) = 1 + natToInt n
+
 ------------------------------------------------------------
 -- Type constructors
 ------------------------------------------------------------
@@ -202,6 +221,13 @@ data TypeF t
     TyVarF Var
   | -- | Record type.
     TyRcdF (Map Var t)
+  | -- | A recursive type variable bound by an enclosing Rec,
+    --   represented by a de Bruijn index.
+    TyRecVarF Nat
+  | -- | Recursive type.  The variable is just a suggestion for a name to use
+    --   when pretty-printing; the actual bound variables are represented
+    --   via de Bruijn indices.
+    TyRecF Var t
   deriving (Show, Eq, Functor, Foldable, Traversable, Generic, Generic1, Data, FromJSON, ToJSON)
 
 deriveEq1 ''TypeF
@@ -380,6 +406,9 @@ pattern TyDelay ty = TyConApp TCDelay [ty]
 pattern TyUser :: Var -> [Type] -> Type
 pattern TyUser v tys = TyConApp (TCUser v) tys
 
+pattern TyRec :: Var -> Type -> Type
+pattern TyRec x ty = Fix (TyRecF x ty)
+
 --------------------------------------------------
 -- UType
 
@@ -437,6 +466,9 @@ pattern UTyDelay ty = UTyConApp TCDelay [ty]
 pattern UTyUser :: Var -> [UType] -> UType
 pattern UTyUser v tys = UTyConApp (TCUser v) tys
 
+pattern UTyRec :: Var -> UType -> UType
+pattern UTyRec x ty = Free (TyRecF x ty)
+
 pattern PolyUnit :: Polytype
 pattern PolyUnit = Forall [] (TyCmd TyUnit)
 

From 2e799b0112bfee4cdf5bb53fb407aa3ad9a01bf9 Mon Sep 17 00:00:00 2001
From: Brent Yorgey <byorgey@gmail.com>
Date: Mon, 3 Jun 2024 05:41:43 -0500
Subject: [PATCH 2/8] typechecking for equirecursive types

---
 src/swarm-lang/Swarm/Effect/Unify.hs       |  3 +
 src/swarm-lang/Swarm/Effect/Unify/Fast.hs  | 94 ++++++++++++++++++----
 src/swarm-lang/Swarm/Effect/Unify/Naive.hs |  5 +-
 src/swarm-lang/Swarm/Language/Pretty.hs    | 62 +++++++-------
 src/swarm-lang/Swarm/Language/Types.hs     | 61 ++++++++++----
 5 files changed, 166 insertions(+), 59 deletions(-)

diff --git a/src/swarm-lang/Swarm/Effect/Unify.hs b/src/swarm-lang/Swarm/Effect/Unify.hs
index 364eb078e..595dc05df 100644
--- a/src/swarm-lang/Swarm/Effect/Unify.hs
+++ b/src/swarm-lang/Swarm/Effect/Unify.hs
@@ -52,4 +52,7 @@ data UnificationError where
   UnifyErr :: TypeF UType -> TypeF UType -> UnificationError
   -- | Encountered an undefined/unknown type constructor.
   UndefinedUserType :: UType -> UnificationError
+  -- | Encountered an unexpanded recursive type in unifyF.  This
+  --   should never happen.
+  UnexpandedRecTy :: TypeF UType -> UnificationError
   deriving (Show)
diff --git a/src/swarm-lang/Swarm/Effect/Unify/Fast.hs b/src/swarm-lang/Swarm/Effect/Unify/Fast.hs
index b34940f65..a04c8466c 100644
--- a/src/swarm-lang/Swarm/Effect/Unify/Fast.hs
+++ b/src/swarm-lang/Swarm/Effect/Unify/Fast.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE DerivingStrategies #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE UndecidableInstances #-}
 
 -- |
@@ -32,6 +33,7 @@ import Control.Monad.Trans (MonadIO)
 import Data.Function (on)
 import Data.Map qualified as M
 import Data.Map.Merge.Lazy qualified as M
+import Data.Set (Set)
 import Data.Set qualified as S
 import Swarm.Effect.Unify
 import Swarm.Effect.Unify.Common
@@ -83,6 +85,8 @@ instance Substitutes IntVar UType UType where
     goF seen (TyConF c ts) = TyConF c <$> mapM (go seen) ts
     goF _ t@(TyVarF {}) = pure t
     goF seen (TyRcdF m) = TyRcdF <$> mapM (go seen) m
+    goF seen (TyRecF x t) = TyRecF x <$> go seen t
+    goF _ t@(TyRecVarF _) = pure t
 
 ------------------------------------------------------------
 -- Carrier type
@@ -92,7 +96,17 @@ instance Substitutes IntVar UType UType where
 --   throw unification errors.
 newtype UnificationC m a = UnificationC
   { unUnificationC ::
-      StateC (Subst IntVar UType) (StateC FreshVarCounter (ThrowC UnificationError m)) a
+      StateC
+        (Set (UType, UType))
+        ( StateC
+            (Subst IntVar UType)
+            ( StateC
+                FreshVarCounter
+                ( ThrowC UnificationError m
+                )
+            )
+        )
+        a
   }
   deriving newtype (Functor, Applicative, Alternative, Monad, MonadIO)
 
@@ -108,7 +122,11 @@ runUnification ::
   UnificationC m a ->
   m (Either UnificationError a)
 runUnification =
-  unUnificationC >>> evalState idS >>> evalState (FreshVarCounter 0) >>> runThrow
+  unUnificationC
+    >>> evalState S.empty
+    >>> evalState idS
+    >>> evalState (FreshVarCounter 0)
+    >>> runThrow
 
 ------------------------------------------------------------
 -- Unification
@@ -149,32 +167,68 @@ instance
     L (FreeUVars t) -> do
       s <- get @(Subst IntVar UType)
       (<$ ctx) . fuvs <$> subst s t
-    R other -> alg (unUnificationC . hdl) (R (R (R other))) ctx
+    R other -> alg (unUnificationC . hdl) (R (R (R (R other)))) ctx
 
 -- | Unify two types, returning a unified type equal to both.  Note
 --   that for efficiency we /don't/ do an occurs check here, but
 --   instead lazily during substitution.
+--
+--   We keep track of a set of pairs of types we have seen; if we ever
+--   see a pair a second time we simply assume they are equal without
+--   recursing further.  This constitutes a finite (coinductive)
+--   algorithm for doing unification on recursive types.
+--
+--   For example, suppose we wanted to unify @rec s. Unit + Unit + s@
+--   and @rec t. Unit + t@.  These types are actually equal since
+--   their infinite unfoldings are both @Unit + Unit + Unit + ...@ In
+--   practice we would proceed through the following recursive calls
+--   to unify:
+--
+--   @
+--     (rec s. Unit + Unit + s)                 =:= (rec t. Unit + t)
+--         { unfold the LHS }
+--     (Unit + Unit + (rec s. Unit + Unit + s)) =:= (rec t. Unit + t)
+--         { unfold the RHS }
+--     (Unit + Unit + (rec s. Unit + Unit + s)) =:= (Unit + (rec t. Unit + t)
+--         { unifyF matches the + and makes two calls to unify }
+--     Unit =:= Unit   { trivial}
+--     (Unit + (rec s. Unit + Unit + s))        =:= (rec t. Unit + t)
+--         { unfold the RHS }
+--     (Unit + (rec s. Unit + Unit + s))        =:= (Unit + (rec t. Unit + t))
+--         { unifyF on + }
+--     (rec s. Unit + Unit + s)                 =:= (rec t. Unit + t)
+--         { back to the starting pair, return success }
+--   @
 unify ::
   ( Has (Throw UnificationError) sig m
   , Has (Reader TDCtx) sig m
   , Has (State (Subst IntVar UType)) sig m
+  , Has (State (Set (UType, UType))) sig m
   ) =>
   UType ->
   UType ->
   m UType
-unify ty1 ty2 = case (ty1, ty2) of
-  (Pure x, Pure y) | x == y -> pure (Pure x)
-  (Pure x, y) -> do
-    mxv <- lookupS x
-    case mxv of
-      Nothing -> unifyVar x y
-      Just xv -> unify xv y
-  (x, Pure y) -> unify (Pure y) x
-  (UTyUser x1 tys, _) -> do
-    ty1' <- expandTydef x1 tys
-    unify ty1' ty2
-  (_, UTyUser {}) -> unify ty2 ty1
-  (Free t1, Free t2) -> Free <$> unifyF t1 t2
+unify ty1 ty2 = do
+  seen <- get @(Set (UType, UType))
+  case S.member (ty1, ty2) seen of
+    True -> return ty1
+    False -> do
+      modify (S.insert (ty1, ty2))
+      case (ty1, ty2) of
+        (Pure x, Pure y) | x == y -> pure (Pure x)
+        (Pure x, y) -> do
+          mxv <- lookupS x
+          case mxv of
+            Nothing -> unifyVar x y
+            Just xv -> unify xv y
+        (x, Pure y) -> unify (Pure y) x
+        (UTyRec x ty, _) -> unify (unfoldRec x ty) ty2
+        (_, UTyRec x ty) -> unify ty1 (unfoldRec x ty)
+        (UTyUser x1 tys, _) -> do
+          ty1' <- expandTydef x1 tys
+          unify ty1' ty2
+        (_, UTyUser {}) -> unify ty2 ty1
+        (Free t1, Free t2) -> Free <$> unifyF t1 t2
 
 -- | Unify a unification variable which /is not/ bound by the current
 --   substitution with another term.  If the other term is also a
@@ -183,6 +237,7 @@ unifyVar ::
   ( Has (Throw UnificationError) sig m
   , Has (Reader TDCtx) sig m
   , Has (State (Subst IntVar UType)) sig m
+  , Has (State (Set (UType, UType))) sig m
   ) =>
   IntVar ->
   UType ->
@@ -211,11 +266,18 @@ unifyF ::
   ( Has (Throw UnificationError) sig m
   , Has (Reader TDCtx) sig m
   , Has (State (Subst IntVar UType)) sig m
+  , Has (State (Set (UType, UType))) sig m
   ) =>
   TypeF UType ->
   TypeF UType ->
   m (TypeF UType)
 unifyF t1 t2 = case (t1, t2) of
+  -- Recursive types are always expanded in 'unify', these first four cases
+  -- should never happen.
+  (TyRecF {}, _) -> throwError $ UnexpandedRecTy t1
+  (_, TyRecF {}) -> throwError $ UnexpandedRecTy t2
+  (TyRecVarF {}, _) -> throwError $ UnexpandedRecTy t1
+  (_, TyRecVarF {}) -> throwError $ UnexpandedRecTy t2
   (TyConF c1 ts1, TyConF c2 ts2) -> case c1 == c2 of
     True -> TyConF c1 <$> zipWithM unify ts1 ts2
     False -> unifyErr
diff --git a/src/swarm-lang/Swarm/Effect/Unify/Naive.hs b/src/swarm-lang/Swarm/Effect/Unify/Naive.hs
index 6612f7df3..6501ead60 100644
--- a/src/swarm-lang/Swarm/Effect/Unify/Naive.hs
+++ b/src/swarm-lang/Swarm/Effect/Unify/Naive.hs
@@ -13,7 +13,7 @@
 --
 -- Not used in Swarm, and also unmaintained
 -- (e.g. "Swarm.Effect.Unify.Fast" now supports expanding type
--- aliases; this module does not). It's still here just for
+-- aliases + recursive types; this module does not). It's still here just for
 -- testing/comparison.
 module Swarm.Effect.Unify.Naive where
 
@@ -164,5 +164,8 @@ unifyF t1 t2 = case (t1, t2) of
       False -> unifyErr
       _ -> (fmap compose . sequence) (M.merge M.dropMissing M.dropMissing (M.zipWithMatched (const unify)) m1 m2)
   (TyRcdF {}, _) -> unifyErr
+  -- Don't support any extra features (e.g. recursive types), so just
+  -- add a catch-all failure case
+  (_, _) -> unifyErr
  where
   unifyErr = throwError $ UnifyErr t1 t2
diff --git a/src/swarm-lang/Swarm/Language/Pretty.hs b/src/swarm-lang/Swarm/Language/Pretty.hs
index 1e8607d95..2529732ba 100644
--- a/src/swarm-lang/Swarm/Language/Pretty.hs
+++ b/src/swarm-lang/Swarm/Language/Pretty.hs
@@ -154,34 +154,38 @@ instance (PrettyPrec (t (Free t v)), PrettyPrec v) => PrettyPrec (Free t v) wher
   prettyPrec p (Free t) = prettyPrec p t
   prettyPrec p (Pure v) = prettyPrec p v
 
--- XXX use case!
-instance ((UnchainableFun t), (PrettyPrec t)) => PrettyPrec (TypeF t) where
-  prettyPrec _ (TyVarF v) = pretty v
-  prettyPrec _ (TyRcdF m) = brackets $ hsep (punctuate "," (map prettyBinding (M.assocs m)))
-  -- Special cases for type constructors with special syntax.
-  -- Always use parentheses around sum and product types, see #1625
-  prettyPrec p (TyConF TCSum [ty1, ty2]) =
-    pparens (p > 0) $
-      prettyPrec 2 ty1 <+> "+" <+> prettyPrec 2 ty2
-  prettyPrec p (TyConF TCProd [ty1, ty2]) =
-    pparens (p > 0) $
-      prettyPrec 2 ty1 <+> "*" <+> prettyPrec 2 ty2
-  prettyPrec _ (TyConF TCDelay [ty]) = braces $ ppr ty
-  prettyPrec p (TyConF TCFun [ty1, ty2]) =
-    let (iniF, lastF) = unsnocNE $ ty1 <| unchainFun ty2
-        funs = (prettyPrec 2 <$> iniF) <> [prettyPrec 1 lastF]
-        inLine l r = l <+> "->" <+> r
-        multiLine l r = l <+> "->" <> hardline <> r
-     in pparens (p > 1) . align $
-          flatAlt (concatWith multiLine funs) (concatWith inLine funs)
-  -- Recursive types XXX
-  prettyPrec _ (TyRecVarF i) = pretty (show (natToInt i))
-  prettyPrec p (TyRecF _ ty) = pparens (p > 0) $ "rec." <+> prettyPrec 0 ty
-  -- Fallthrough cases for type constructor application.  Handles base
-  -- types, Cmd, user-defined types, or ill-kinded things like 'Int
-  -- Bool'.
-  prettyPrec _ (TyConF c []) = ppr c
-  prettyPrec p (TyConF c tys) = pparens (p > 9) $ ppr c <+> hsep (map (prettyPrec 10) tys)
+instance (UnchainableFun t, PrettyPrec t, SubstRec t) => PrettyPrec (TypeF t) where
+  prettyPrec p = \case
+    TyVarF v -> pretty v
+    TyRcdF m -> brackets $ hsep (punctuate "," (map prettyBinding (M.assocs m)))
+    -- Special cases for type constructors with special syntax.
+    -- Always use parentheses around sum and product types, see #1625
+    TyConF TCSum [ty1, ty2] ->
+      pparens (p > 0) $
+        prettyPrec 2 ty1 <+> "+" <+> prettyPrec 2 ty2
+    TyConF TCProd [ty1, ty2] ->
+      pparens (p > 0) $
+        prettyPrec 2 ty1 <+> "*" <+> prettyPrec 2 ty2
+    TyConF TCDelay [ty] -> braces $ ppr ty
+    TyConF TCFun [ty1, ty2] ->
+      let (iniF, lastF) = unsnocNE $ ty1 <| unchainFun ty2
+          funs = (prettyPrec 2 <$> iniF) <> [prettyPrec 1 lastF]
+          inLine l r = l <+> "->" <+> r
+          multiLine l r = l <+> "->" <> hardline <> r
+       in pparens (p > 1) . align $
+            flatAlt (concatWith multiLine funs) (concatWith inLine funs)
+    TyRecF x ty ->
+      pparens (p > 0) $
+        "rec" <+> pretty x <> "." <+> prettyPrec 0 (substRec (TyVarF x) ty NZ)
+    -- This case shouldn't be possible, since TyRecVar should only occur inside a TyRec,
+    -- and pretty-printing the TyRec (above) will substitute a variable name for
+    -- any bound TyRecVars before recursing.
+    TyRecVarF i -> pretty (show (natToInt i))
+    -- Fallthrough cases for type constructor application.  Handles base
+    -- types, Cmd, user-defined types, or ill-kinded things like 'Int
+    -- Bool'.
+    TyConF c [] -> ppr c
+    TyConF c tys -> pparens (p > 9) $ ppr c <+> hsep (map (prettyPrec 10) tys)
 
 instance PrettyPrec Polytype where
   prettyPrec _ (Forall [] t) = ppr t
@@ -422,6 +426,8 @@ instance PrettyPrec UnificationError where
       "Can't unify" <+> ppr ty1 <+> "and" <+> ppr ty2
     UndefinedUserType ty ->
       "Undefined user type" <+> ppr ty
+    UnexpandedRecTy ty ->
+      "Unexpanded recursive type" <+> ppr ty <+> "encountered in unifyF.  This should never happen, please report this as a bug."
 
 instance PrettyPrec Arity where
   prettyPrec _ (Arity a) = pretty a
diff --git a/src/swarm-lang/Swarm/Language/Types.hs b/src/swarm-lang/Swarm/Language/Types.hs
index 660795cbf..32cbf25b3 100644
--- a/src/swarm-lang/Swarm/Language/Types.hs
+++ b/src/swarm-lang/Swarm/Language/Types.hs
@@ -24,6 +24,8 @@ module Swarm.Language.Types (
   -- ** Recursive types
   Nat (..),
   natToInt,
+  unfoldRec,
+  SubstRec (..),
 
   -- * @Type@
   Type,
@@ -112,6 +114,7 @@ import Data.Kind qualified
 import Data.Map.Strict (Map)
 import Data.Map.Strict qualified as M
 import Data.Maybe (fromMaybe)
+import Data.Ord.Deriving (deriveOrd1)
 import Data.Set (Set)
 import Data.Set qualified as S
 import Data.String (IsString (..))
@@ -155,19 +158,6 @@ data BaseTy
 baseTyName :: BaseTy -> Text
 baseTyName = into @Text . drop 1 . show
 
-------------------------------------------------------------
--- Recursive type utilities
-------------------------------------------------------------
-
-data Nat where
-  NZ :: Nat
-  NS :: Nat -> Nat
-  deriving (Eq, Ord, Show, Data, Generic, FromJSON, ToJSON)
-
-natToInt :: Nat -> Int
-natToInt NZ = 0
-natToInt (NS n) = 1 + natToInt n
-
 ------------------------------------------------------------
 -- Type constructors
 ------------------------------------------------------------
@@ -205,6 +195,16 @@ instance FromJSON Arity where
 -- Types
 ------------------------------------------------------------
 
+-- | Peano naturals, for use as de Bruijn indices in recursive types.
+data Nat where
+  NZ :: Nat
+  NS :: Nat -> Nat
+  deriving (Eq, Ord, Show, Data, Generic, FromJSON, ToJSON)
+
+natToInt :: Nat -> Int
+natToInt NZ = 0
+natToInt (NS n) = 1 + natToInt n
+
 -- | A "structure functor" encoding the shape of type expressions.
 --   Actual types are then represented by taking a fixed point of this
 --   functor.  We represent types in this way, via a "two-level type",
@@ -228,9 +228,10 @@ data TypeF t
     --   when pretty-printing; the actual bound variables are represented
     --   via de Bruijn indices.
     TyRecF Var t
-  deriving (Show, Eq, Functor, Foldable, Traversable, Generic, Generic1, Data, FromJSON, ToJSON)
+  deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Generic, Generic1, Data, FromJSON, ToJSON)
 
 deriveEq1 ''TypeF
+deriveOrd1 ''TypeF
 deriveShow1 ''TypeF
 deriveFromJSON1 defaultOptions ''TypeF
 deriveToJSON1 defaultOptions ''TypeF
@@ -555,3 +556,35 @@ tcArity tydefs =
     TCProd -> Just 2
     TCFun -> Just 2
     TCUser t -> getArity . view tydefArity <$> Ctx.lookup t tydefs
+
+------------------------------------------------------------
+-- Recursive type utilities
+------------------------------------------------------------
+
+-- | @unfoldRec x t@ unfolds the recursive type @rec x. t@ one step,
+--   to @t [(rec x. t) / x]@.
+unfoldRec :: Var -> UType -> UType
+unfoldRec x ty = substRec (TyRecF x ty) ty NZ
+
+-- | Class of type-like things where we can substitute for a bound de
+--   Bruijn variable.
+class SubstRec t where
+  -- | @substRec s t n@ substitutes @s@ for the bound de Bruijn variable
+  --   @n@ everywhere in @t@.
+  substRec :: TypeF t -> t -> Nat -> t
+
+instance SubstRec (Free TypeF v) where
+  substRec s = ucata (\i _ -> Pure i) $ \f i -> case f of
+    TyRecVarF j
+      | i == j -> Free s
+      | otherwise -> Free (TyRecVarF j)
+    TyRecF x g -> Free (TyRecF x (g (NS i)))
+    _ -> Free (fmap ($ i) f)
+
+instance SubstRec Type where
+  substRec s = foldFix $ \f i -> case f of
+    TyRecVarF j
+      | i == j -> Fix s
+      | otherwise -> Fix (TyRecVarF j)
+    TyRecF x g -> Fix (TyRecF x (g (NS i)))
+    _ -> Fix (fmap ($ i) f)

From e65d86d45ad9303a728121b061b7f3de480016b9 Mon Sep 17 00:00:00 2001
From: Brent Yorgey <byorgey@gmail.com>
Date: Mon, 3 Jun 2024 11:31:40 -0500
Subject: [PATCH 3/8] better error messages for infinite type errors

---
 src/swarm-lang/Swarm/Effect/Unify/Fast.hs | 54 +++++++++++++++++------
 src/swarm-lang/Swarm/Language/Pretty.hs   |  5 ++-
 2 files changed, 45 insertions(+), 14 deletions(-)

diff --git a/src/swarm-lang/Swarm/Effect/Unify/Fast.hs b/src/swarm-lang/Swarm/Effect/Unify/Fast.hs
index a04c8466c..801e3df9c 100644
--- a/src/swarm-lang/Swarm/Effect/Unify/Fast.hs
+++ b/src/swarm-lang/Swarm/Effect/Unify/Fast.hs
@@ -1,7 +1,6 @@
 {-# LANGUAGE DerivingStrategies #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE UndecidableInstances #-}
 
 -- |
@@ -21,18 +20,23 @@ module Swarm.Effect.Unify.Fast where
 
 import Control.Algebra
 import Control.Applicative (Alternative)
+import Control.Carrier.Accum.FixedStrict (AccumC, runAccum)
+import Control.Carrier.Reader (ReaderC, runReader)
 import Control.Carrier.State.Strict (StateC, evalState)
 import Control.Carrier.Throw.Either (ThrowC, runThrow)
 import Control.Category ((>>>))
-import Control.Effect.Reader (Reader)
+import Control.Effect.Accum (Accum, add)
+import Control.Effect.Reader (Reader, ask, local)
 import Control.Effect.State (State, get, gets, modify)
 import Control.Effect.Throw (Throw, throwError)
 import Control.Monad (zipWithM)
 import Control.Monad.Free
 import Control.Monad.Trans (MonadIO)
 import Data.Function (on)
+import Data.Functor.Identity
 import Data.Map qualified as M
 import Data.Map.Merge.Lazy qualified as M
+import Data.Monoid (First (..))
 import Data.Set (Set)
 import Data.Set qualified as S
 import Swarm.Effect.Unify
@@ -73,20 +77,44 @@ class Substitutes n b a where
 -- | We can perform substitution on terms built up as the free monad
 --   over a structure functor @f@.
 instance Substitutes IntVar UType UType where
-  subst s = go S.empty
+  subst s u = case runSubst (go u) of
+    -- If the substitution completed without encountering a repeated
+    -- variable, just return the result.
+    (First Nothing, u') -> return u'
+    -- Otherwise, throw an error, but re-run substitution starting at
+    -- the repeated variable to generate an expanded cyclic equality
+    -- constraint of the form x = ... x ... .
+    (First (Just x), _) ->
+      throwError $
+        Infinite x (snd (runSubst (go $ Pure x)))
    where
-    go seen (Pure x) = case lookup x s of
+    runSubst :: ReaderC (Set IntVar) (AccumC (First IntVar) Identity) a -> (First IntVar, a)
+    runSubst = run . runAccum (First Nothing) . runReader S.empty
+
+    -- A version of substitution that recurses through the term,
+    -- keeping track of unification variables seen along the current
+    -- path.  When it encounters a previously-seen variable, it simply
+    -- returns it unchanged but notes the first such variable that was
+    -- encountered.
+    go ::
+      (Has (Reader (Set IntVar)) sig m, Has (Accum (First IntVar)) sig m) =>
+      UType ->
+      m UType
+    go (Pure x) = case lookup x s of
       Nothing -> pure $ Pure x
-      Just t
-        | S.member x seen -> throwError $ Infinite x t
-        | otherwise -> go (S.insert x seen) t
-    go seen (Free t) = Free <$> goF seen t
+      Just t -> do
+        seen <- ask
+        case S.member x seen of
+          True -> add (First (Just x)) >> pure (Pure x)
+          False -> local (S.insert x) $ go t
+    go (Free t) = Free <$> goF t
 
-    goF seen (TyConF c ts) = TyConF c <$> mapM (go seen) ts
-    goF _ t@(TyVarF {}) = pure t
-    goF seen (TyRcdF m) = TyRcdF <$> mapM (go seen) m
-    goF seen (TyRecF x t) = TyRecF x <$> go seen t
-    goF _ t@(TyRecVarF _) = pure t
+    goF :: (Has (Reader (Set IntVar)) sig m, Has (Accum (First IntVar)) sig m) => TypeF UType -> m (TypeF UType)
+    goF (TyConF c ts) = TyConF c <$> mapM go ts
+    goF t@(TyVarF {}) = pure t
+    goF (TyRcdF m) = TyRcdF <$> mapM go m
+    goF (TyRecF x t) = TyRecF x <$> go t
+    goF t@(TyRecVarF _) = pure t
 
 ------------------------------------------------------------
 -- Carrier type
diff --git a/src/swarm-lang/Swarm/Language/Pretty.hs b/src/swarm-lang/Swarm/Language/Pretty.hs
index 2529732ba..42c7646ce 100644
--- a/src/swarm-lang/Swarm/Language/Pretty.hs
+++ b/src/swarm-lang/Swarm/Language/Pretty.hs
@@ -421,7 +421,10 @@ instance PrettyPrec TypeErr where
 instance PrettyPrec UnificationError where
   prettyPrec _ = \case
     Infinite x uty ->
-      "Infinite type:" <+> ppr x <+> "=" <+> ppr uty
+      vsep
+        [ "Encountered infinite type" <+> ppr x <+> "=" <+> ppr uty <> "."
+        , "Swarm will not infer recursive types; if you want a recursive type, add an explicit type annotation."
+        ]
     UnifyErr ty1 ty2 ->
       "Can't unify" <+> ppr ty1 <+> "and" <+> ppr ty2
     UndefinedUserType ty ->

From fb97acb36ddb01b6702fa5de2f2011b2fabde708 Mon Sep 17 00:00:00 2001
From: Brent Yorgey <byorgey@gmail.com>
Date: Mon, 3 Jun 2024 11:31:40 -0500
Subject: [PATCH 4/8] Recursive types example

---
 example/rectypes.sw | 107 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 107 insertions(+)
 create mode 100644 example/rectypes.sw

diff --git a/example/rectypes.sw b/example/rectypes.sw
new file mode 100644
index 000000000..adfe645e4
--- /dev/null
+++ b/example/rectypes.sw
@@ -0,0 +1,107 @@
+// 'rec t. F(t)' creates a recursive type which is the solution of t = F(t).
+// For example 'rec l. Unit + Int * l' is the type l such that l = Unit + Int * l,
+// that is, arbitrary-length finite lists of Int.
+//
+// Recursive types are equal up to alpha-renaming, so e.g.
+// (rec l. Unit + Int * l) = (rec q. Unit + Int * q)
+
+////////////////////////////////////////////////////////////
+// Lists
+////////////////////////////////////////////////////////////
+
+tydef List a = rec l. Unit + a * l end
+
+def nil : List a = inl () end
+def cons : a -> List a -> List a = \x. \l. inr (x, l) end
+
+def foldr : (a -> b -> b) -> b -> List a -> b = \f. \z. \xs.
+  case xs
+    (\_. z)
+    (\c. f (fst c) (foldr f z (snd c)))
+end
+
+def map : (a -> b) -> List a -> List b = \f.
+  foldr (\y. cons (f y)) nil
+end
+
+def append : List a -> List a -> List a = \xs. \ys.
+  foldr cons ys xs
+end
+
+def concat : List (List a) -> List a = foldr append nil end
+
+def sum : List Int -> Int =
+  foldr (\x. \y. x + y) 0
+end
+
+def twentySeven = sum (cons 12 (cons 5 (cons 3 (cons 7 nil)))) end
+
+// Note that if a function returns e.g. (rec t. Unit + (Int * Int) * t),
+// that is the *same type* as List (Int * Int), so we can use any List
+// functions on the output.
+
+def someFun : Int -> (rec t. Unit + (Int * Int) * t) = \x. inr ((x, x), inl ()) end
+
+def doSomethingWithSomeFun : List (Int * Int) =
+  (cons (2,3) (cons (4,7) (someFun 5)))
+end
+
+////////////////////////////////////////////////////////////
+// Binary trees with a at internal nodes and b at leaves
+////////////////////////////////////////////////////////////
+
+tydef BTree a b = rec bt. b + bt * a * bt end
+
+def leaf : b -> BTree a b = inl end
+
+def branch : BTree a b -> a -> BTree a b -> BTree a b =
+  \l. \a. \r. inr (l, a, r)
+end
+
+def foldBTree : (b -> c) -> (c -> a -> c -> c) -> BTree a b -> c =
+  \lf. \br. \t.
+    case t
+      lf
+      // fst p, fst (snd p), snd (snd p) is annoying; see #1893
+      (\p. br (foldBTree lf br (fst p)) (fst (snd p)) (foldBTree lf br (snd (snd p))))
+end
+
+def max : Int -> Int -> Int = \a. \b. if (a > b) {a} {b} end
+
+def height : BTree a b -> Int =
+  foldBTree (\_. 0) (\l. \_. \r. 1 + max l r)
+end
+
+////////////////////////////////////////////////////////////
+// Rose trees
+////////////////////////////////////////////////////////////
+
+// It would be better to reuse the definition of List
+// and define Rose a = rec r. a * List r,
+// but we do it this way just to show off nested rec
+tydef Rose a = rec r. a * (rec l. Unit + r * l) end
+
+def foldRose : (a -> List b -> b) -> Rose a -> b = \f. \r.
+  f (fst r) (map (foldRose f) (snd r))
+end
+
+def flatten : Rose a -> List a =
+  foldRose (\a. \ts. cons a (concat ts))
+end
+
+////////////////////////////////////////////////////////////
+// Equirecursive types
+////////////////////////////////////////////////////////////
+
+// Swarm has equirecursive types, which means a recursive type is
+// *equal to* its unfolding.  This has some interesting consequences
+// including the fact that types are equal if their infinite unfoldings
+// would be equal.
+
+// For example, U1 and U2 below are the same, and the Swarm
+// typechecker can tell:
+
+tydef U1 = rec u1. Unit + u1 end
+tydef U2 = rec u2. Unit + Unit + u2 end
+
+def u : U1 -> U2 = \u. u end

From 9aef5019a9c596316c329c82f37ae68a2b969569 Mon Sep 17 00:00:00 2001
From: Brent Yorgey <byorgey@gmail.com>
Date: Mon, 3 Jun 2024 15:36:17 -0500
Subject: [PATCH 5/8] another recursive types example

---
 example/omega.sw | 5 +++++
 1 file changed, 5 insertions(+)
 create mode 100644 example/omega.sw

diff --git a/example/omega.sw b/example/omega.sw
new file mode 100644
index 000000000..0d053a103
--- /dev/null
+++ b/example/omega.sw
@@ -0,0 +1,5 @@
+tydef D = rec d. d -> d end
+
+def selfApp : D -> D = \x. x x end
+
+def omega : D = selfApp selfApp end

From 6456a855158b486fc517d58a210628e84b3666fb Mon Sep 17 00:00:00 2001
From: Brent Yorgey <byorgey@gmail.com>
Date: Mon, 3 Jun 2024 20:49:49 -0500
Subject: [PATCH 6/8] recursive type unit tests

---
 swarm.cabal                       |  1 +
 test/unit/TestLanguagePipeline.hs | 12 ++++++++++++
 test/unit/TestPretty.hs           | 13 +++++++++++++
 3 files changed, 26 insertions(+)

diff --git a/swarm.cabal b/swarm.cabal
index f8c5435f4..411cfcea6 100644
--- a/swarm.cabal
+++ b/swarm.cabal
@@ -856,6 +856,7 @@ test-suite swarm-unit
     base,
     boolexpr,
     containers,
+    data-fix,
     filepath,
     hashable,
     lens,
diff --git a/test/unit/TestLanguagePipeline.hs b/test/unit/TestLanguagePipeline.hs
index 9749bae8b..f4bf9701c 100644
--- a/test/unit/TestLanguagePipeline.hs
+++ b/test/unit/TestLanguagePipeline.hs
@@ -588,6 +588,18 @@ testLanguagePipeline =
                 "1:34:\n  |\n1 | tydef Unbound a b = a + b + c end\n  |                                  ^\nUndefined type variable(s) on right-hand side of tydef: c\n"
             )
         ]
+    , testGroup
+        "recursive types"
+        [ testCase
+            "occurs check"
+            ( process
+                "def sum = \\l. case l (\\_. 0) (\\c. fst c + sum (snd c)) end"
+                "Encountered infinite type u5 = Int * (u4 + u5).\nSwarm will not infer recursive types; if you want a recursive type, add an explicit type annotation."
+            )
+        , testCase
+            "no occurs check with type annotation"
+            (valid "def sum : (rec l. Unit + Int * l) -> Int = \\l. case l (\\_. 0) (\\c. fst c + sum (snd c)) end")
+        ]
     ]
  where
   valid = flip process ""
diff --git a/test/unit/TestPretty.hs b/test/unit/TestPretty.hs
index 85b60dc44..519b48af5 100644
--- a/test/unit/TestPretty.hs
+++ b/test/unit/TestPretty.hs
@@ -6,6 +6,7 @@
 -- Swarm unit tests
 module TestPretty where
 
+import Data.Fix (Fix (..))
 import Swarm.Language.Pretty
 import Swarm.Language.Syntax hiding (mkOp)
 import Swarm.Language.Types
@@ -197,6 +198,18 @@ testPrettyConst =
                     (TyUnit :+: (TyVar "a" :*: TyVar "b") :+: ((TyVar "c" :->: TyVar "d") :*: TyVar "a"))
                 )
         ]
+    , testGroup
+        "recursive types"
+        [ testCase "nat" $
+            equalPretty "rec n. Unit + n" $
+              TyRec "n" (TyUnit :+: Fix (TyRecVarF NZ))
+        , testCase "list" $
+            equalPretty "rec list. Unit + (a * list)" $
+              TyRec "list" (TyUnit :+: (TyVar "a" :*: Fix (TyRecVarF NZ)))
+        , testCase "rose" $
+            equalPretty "rec r. a * (rec l. Unit + (r * l))" $
+              TyRec "r" (TyVar "a" :*: TyRec "l" (TyUnit :+: (Fix (TyRecVarF (NS NZ)) :*: Fix (TyRecVarF NZ))))
+        ]
     ]
  where
   equalPretty :: PrettyPrec a => String -> a -> Assertion

From b023c5c758bfcb3bfadd1a602de646bfbf0b78fb Mon Sep 17 00:00:00 2001
From: Brent Yorgey <byorgey@gmail.com>
Date: Mon, 3 Jun 2024 22:06:58 -0500
Subject: [PATCH 7/8] check for vacuous recursive types

---
 src/swarm-lang/Swarm/Language/Kindcheck.hs | 93 ++++++++++++++++++++--
 src/swarm-lang/Swarm/Language/Pretty.hs    | 41 ++++++----
 src/swarm-lang/Swarm/Language/Types.hs     | 41 +++++++---
 test/unit/TestLanguagePipeline.hs          | 30 +++++++
 4 files changed, 174 insertions(+), 31 deletions(-)

diff --git a/src/swarm-lang/Swarm/Language/Kindcheck.hs b/src/swarm-lang/Swarm/Language/Kindcheck.hs
index 3978736f9..4a28d33e0 100644
--- a/src/swarm-lang/Swarm/Language/Kindcheck.hs
+++ b/src/swarm-lang/Swarm/Language/Kindcheck.hs
@@ -11,14 +11,23 @@ module Swarm.Language.Kindcheck (
 import Control.Algebra (Has)
 import Control.Effect.Reader (Reader, ask)
 import Control.Effect.Throw (Throw, throwError)
+import Control.Monad.Extra (unlessM)
 import Data.Fix (Fix (..))
 import Swarm.Language.Types
 
--- | Kind checking errors that can occur.  For now, the only possible
---   error is an arity mismatch error.
+-- | Kind checking errors that can occur.
 data KindError
-  = ArityMismatch TyCon Int [Type]
-  | UndefinedTyCon TyCon Type
+  = -- | A type constructor expects n arguments, but was given these
+    --   arguments instead.
+    ArityMismatch TyCon Int [Type]
+  | -- | An undefined type constructor was encountered in the given type.
+    UndefinedTyCon TyCon Type
+  | -- | A trivial recursive type (one that does not use its bound
+    --   variable) was encountered.
+    TrivialRecTy Var Type
+  | -- | A vacuous recursive type (one that expands immediately to
+    --   itself) was encountered.
+    VacuousRecTy Var Type
   deriving (Eq, Show)
 
 -- | Check that a polytype is well-kinded.
@@ -34,6 +43,11 @@ checkPolytypeKind pty@(Forall xs t) = TydefInfo pty (Arity $ length xs) <$ check
 --   well want to generalize to arbitrary higher kinds (e.g. @(Type ->
 --   Type) -> Type@ etc.) which would require generalizing this
 --   checking code a bit.
+--
+--   Here we also check that any recursive types are non-vacuous,
+--   /i.e./ not of the form @rec t. t@, and non-trivial, /i.e./ the
+--   variable bound by the @rec@ actually occurs somewhere in the
+--   body.
 checkKind :: (Has (Reader TDCtx) sig m, Has (Throw KindError) sig m) => Type -> m ()
 checkKind ty@(Fix tyF) = case tyF of
   TyConF c tys -> do
@@ -45,5 +59,74 @@ checkKind ty@(Fix tyF) = case tyF of
         _ -> throwError $ ArityMismatch c a tys
   TyVarF _ -> return ()
   TyRcdF m -> mapM_ checkKind m
-  TyRecF _ t -> checkKind t
+  TyRecF x t -> do
+    -- It's important to call checkKind first, to rule out undefined
+    -- type constructors. Within the recursive kind check, we
+    -- substitute the given variable name for the bound de Bruijn
+    -- index 0 in the body.  This doesn't affect the checking but it
+    -- does ensure that error messages will use the variable name and
+    -- not de Bruijn indices.
+    checkKind (substRec (TyVarF x) t NZ)
+    -- Now check that the recursive type is well-formed.  We call this
+    -- with the *unsubstituted* t because the check will be looking
+    -- for de Bruijn variables specifically.
+    checkRecTy x t
   TyRecVarF _ -> return ()
+
+-- | Check that the body of a recursive type actually contains the
+--   bound variable at least once (otherwise there's no point in using
+--   @rec@) and does not consist solely of that variable.
+checkRecTy :: (Has (Reader TDCtx) sig m, Has (Throw KindError) sig m) => Var -> Type -> m ()
+checkRecTy x ty = do
+  unlessM (containsVar NZ ty) $ throwError (TrivialRecTy x ty)
+  unlessM (nonVacuous NZ ty) $ throwError (VacuousRecTy x ty)
+
+-- Note, in theory it would be more efficient to combine containsVar
+-- and nonVacuous into a single check that walks over the type only
+-- once, but we keep them separate just to simplify things.  This
+-- won't make much difference in the grand scheme of things since
+-- types are small.
+
+-- | Check whether a type contains a specific bound recursive type
+--   variable.
+containsVar :: Has (Reader TDCtx) sig m => Nat -> Type -> m Bool
+containsVar i (Fix tyF) = case tyF of
+  TyRecVarF j -> pure (i == j)
+  TyVarF {} -> pure False
+  TyConF (TCUser u) tys -> do
+    ty' <- expandTydef u tys
+    containsVar i ty'
+  TyConF _ tys -> or <$> mapM (containsVar i) tys
+  TyRcdF m -> or <$> mapM (containsVar i) m
+  TyRecF _ ty -> containsVar (NS i) ty
+
+-- | @nonVacuous ty@ checks that the recursive type @rec x. ty@ is
+--   non-vacuous, /i.e./ that it doesn't look like @rec x. x@.  Put
+--   another way, we make sure the recursive type is "productive" in
+--   the sense that unfolding it will result in a well-defined
+--   infinite type (as opposed to @rec x. x@ which just unfolds to
+--   itself).  However, we can't just check whether it literally looks
+--   like @rec x. x@ since we must also (1) expand type aliases and
+--   (2) ignore additional intervening @rec@s.  For example, given
+--   @tydef Id a = a@, the type @rec x. rec y. Id x@ is also vacuous.
+nonVacuous :: (Has (Reader TDCtx) sig m) => Nat -> Type -> m Bool
+nonVacuous i (Fix tyF) = case tyF of
+  -- The type simply consists of a variable bound by some @rec@.
+  -- Check if it's the variable we're currently looking for.
+  TyRecVarF j -> pure (i /= j)
+  -- Expand a user-defined type and keep looking.
+  TyConF (TCUser u) tys -> do
+    ty' <- expandTydef u tys
+    nonVacuous i ty'
+  -- Increment the variable we're looking for when going under a @rec@
+  -- binder.
+  TyRecF _ ty -> nonVacuous (NS i) ty
+  -- If we encounter any other kind of type constructor or record
+  -- type, rejoice!
+  TyConF {} -> pure True
+  TyRcdF {} -> pure True
+  -- This last case can't actully happen if we already checked that
+  -- the recursive type actually contains its bound variable (with
+  -- 'containsVar'), since it would correspond to something like @rec
+  -- x. y@.  However, it's still correct to return True.
+  TyVarF {} -> pure True
diff --git a/src/swarm-lang/Swarm/Language/Pretty.hs b/src/swarm-lang/Swarm/Language/Pretty.hs
index 42c7646ce..c5efd7a99 100644
--- a/src/swarm-lang/Swarm/Language/Pretty.hs
+++ b/src/swarm-lang/Swarm/Language/Pretty.hs
@@ -436,21 +436,32 @@ instance PrettyPrec Arity where
   prettyPrec _ (Arity a) = pretty a
 
 instance PrettyPrec KindError where
-  prettyPrec _ (ArityMismatch c a tys) =
-    nest 2 . vsep $
-      [ "Kind error:"
-      , hsep
-          [ ppr c
-          , "requires"
-          , pretty a
-          , "type"
-          , pretty (number a "argument" <> ",")
-          , "but was given"
-          , pretty (length tys)
-          ]
-      ]
-        ++ ["in the type:" <+> ppr (TyConApp c tys) | not (null tys)]
-  prettyPrec _ (UndefinedTyCon tc _ty) = "Undefined type" <+> ppr tc
+  prettyPrec _ = \case
+    ArityMismatch c a tys ->
+      nest 2 . vsep $
+        [ "Kind error:"
+        , hsep
+            [ ppr c
+            , "requires"
+            , pretty a
+            , "type"
+            , pretty (number a "argument" <> ",")
+            , "but was given"
+            , pretty (length tys)
+            ]
+        ]
+          ++ ["in the type:" <+> ppr (TyConApp c tys) | not (null tys)]
+    UndefinedTyCon tc _ty -> "Undefined type" <+> ppr tc
+    TrivialRecTy x ty ->
+      nest 2 . vsep $
+        [ "Encountered trivial recursive type" <+> ppr (TyRec x ty)
+        , "Did you forget to use" <+> pretty x <+> "in the body of the type?"
+        ]
+    VacuousRecTy x ty ->
+      nest 2 . vsep $
+        [ "Encountered vacuous recursive type" <+> ppr (TyRec x ty)
+        , "Recursive types must be productive, i.e. must not expand to themselves."
+        ]
 
 -- | Given a type and its source, construct an appropriate description
 --   of it to go in a type mismatch error message.
diff --git a/src/swarm-lang/Swarm/Language/Types.hs b/src/swarm-lang/Swarm/Language/Types.hs
index 32cbf25b3..7aa36e549 100644
--- a/src/swarm-lang/Swarm/Language/Types.hs
+++ b/src/swarm-lang/Swarm/Language/Types.hs
@@ -281,6 +281,25 @@ instance IsString Type where
 instance IsString UType where
   fromString x = UTyVar (from @String x)
 
+------------------------------------------------------------
+-- Generic folding over type representations
+------------------------------------------------------------
+
+class Typical t where
+  foldT :: (TypeF t -> t) -> t -> t
+  rollT :: TypeF t -> t
+  fromType :: Type -> t
+
+instance Typical Type where
+  foldT = foldFix
+  rollT = Fix
+  fromType = id
+
+instance Typical UType where
+  foldT = ucata Pure
+  rollT = Free
+  fromType = toU
+
 ------------------------------------------------------------
 -- Polytypes
 ------------------------------------------------------------
@@ -509,7 +528,7 @@ type TDCtx = Ctx TydefInfo
 --   number of arguments must match up; we don't worry about what
 --   happens if the lists have different lengths since in theory that
 --   can never happen.
-expandTydef :: Has (Reader TDCtx) sig m => Var -> [UType] -> m UType
+expandTydef :: (Has (Reader TDCtx) sig m, Typical t) => Var -> [t] -> m t
 expandTydef userTyCon tys = do
   mtydefInfo <- Ctx.lookupR userTyCon
   tdCtx <- ask @TDCtx
@@ -526,17 +545,17 @@ expandTydef userTyCon tys = do
       tydefInfo = fromMaybe (error errMsg) mtydefInfo
   return $ substTydef tydefInfo tys
 
--- | Substitute the given types into the body of the given type
---   synonym definition.
-substTydef :: TydefInfo -> [UType] -> UType
-substTydef (TydefInfo (Forall as ty) _) tys = ucata Pure substF (toU ty)
+-- | Given the definition of a type alias, substitute the given
+--   arguments into its body and return the resulting type.
+substTydef :: forall t. Typical t => TydefInfo -> [t] -> t
+substTydef (TydefInfo (Forall as ty) _) tys = foldT @t substF (fromType ty)
  where
-  tyMap = M.fromList $ zip as tys
+  argMap = M.fromList $ zip as tys
 
-  substF tyF@(TyVarF x) = case M.lookup x tyMap of
-    Nothing -> Free tyF
-    Just uty -> uty
-  substF tyF = Free tyF
+  substF tyF@(TyVarF x) = case M.lookup x argMap of
+    Nothing -> rollT tyF
+    Just ty' -> ty'
+  substF tyF = rollT tyF
 
 ------------------------------------------------------------
 -- Arity
@@ -563,7 +582,7 @@ tcArity tydefs =
 
 -- | @unfoldRec x t@ unfolds the recursive type @rec x. t@ one step,
 --   to @t [(rec x. t) / x]@.
-unfoldRec :: Var -> UType -> UType
+unfoldRec :: SubstRec t => Var -> t -> t
 unfoldRec x ty = substRec (TyRecF x ty) ty NZ
 
 -- | Class of type-like things where we can substitute for a bound de
diff --git a/test/unit/TestLanguagePipeline.hs b/test/unit/TestLanguagePipeline.hs
index f4bf9701c..7cf476bf4 100644
--- a/test/unit/TestLanguagePipeline.hs
+++ b/test/unit/TestLanguagePipeline.hs
@@ -599,6 +599,36 @@ testLanguagePipeline =
         , testCase
             "no occurs check with type annotation"
             (valid "def sum : (rec l. Unit + Int * l) -> Int = \\l. case l (\\_. 0) (\\c. fst c + sum (snd c)) end")
+        , testCase
+            "vacuous"
+            ( process
+                "tydef X = rec x. x end"
+                "1:1: Encountered vacuous recursive type rec x. x"
+            )
+        , testCase
+            "nonobviously vacuous"
+            ( process
+                "tydef I a = a end; tydef M a b c = b end; tydef X = rec y. rec x. M x (I x) Int end"
+                "1:43: Encountered vacuous recursive type rec x. M x (I x) Int"
+            )
+        , testCase
+            "trivial"
+            ( process
+                "tydef X = rec x. Int end"
+                "1:1: Encountered trivial recursive type rec x. Int"
+            )
+        , testCase
+            "free rec vars"
+            ( process
+                "tydef X = rec y. rec x. y end"
+                "1:1: Encountered trivial recursive type rec x. y"
+            )
+        , testCase
+            "rec type with undefined tycon"
+            ( process
+                "tydef X = rec x. U + x end"
+                "1:1: Undefined type U"
+            )
         ]
     ]
  where

From faeb898ded78cdd382168c30d44f0133b15de622 Mon Sep 17 00:00:00 2001
From: Brent Yorgey <byorgey@gmail.com>
Date: Thu, 6 Jun 2024 09:18:06 -0500
Subject: [PATCH 8/8] update editor configs for `rec` keyword

---
 editors/emacs/swarm-mode.el | 2 +-
 editors/vim/swarm.vim       | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/editors/emacs/swarm-mode.el b/editors/emacs/swarm-mode.el
index 469f617d1..d331e58f3 100644
--- a/editors/emacs/swarm-mode.el
+++ b/editors/emacs/swarm-mode.el
@@ -154,7 +154,7 @@
   "Regexp that recognizes types (all uppercase strings are supposed to be types) in swarm language.")
 
 (defvar swarm-mode-keywords-regexp
-  (concat "\\b" (regexp-opt '("def" "tydef" "end" "let" "in" "require") t) "\\b")
+  (concat "\\b" (regexp-opt '("def" "tydef" "rec" "end" "let" "in" "require") t) "\\b")
   "Regexp that recognizes keywords in swarm language.")
 
 (defvar swarm-font-lock-keywords
diff --git a/editors/vim/swarm.vim b/editors/vim/swarm.vim
index 13e1ec818..f4b009306 100644
--- a/editors/vim/swarm.vim
+++ b/editors/vim/swarm.vim
@@ -1,4 +1,4 @@
-syn keyword Keyword def tydef end let in require
+syn keyword Keyword def tydef rec end let in require
 syn keyword Builtins self parent base if inl inr case fst snd force undefined fail not format chars split charat tochar key
 syn keyword Command noop wait selfdestruct move backup volume path push stride turn grab harvest sow ignite place ping give equip unequip make has equipped count drill use build salvage reprogram say listen log view appear create halt time scout whereami waypoint structure floorplan hastag tagmembers detect resonate density sniff chirp watch surveil heading blocked scan upload ishere isempty meet meetall whoami setname random run return try swap atomic instant installkeyhandler teleport as robotnamed robotnumbered knows
 syn keyword Direction east north west south down forward left back right