diff --git a/primer/gen/Primer/Gen/Core/Raw.hs b/primer/gen/Primer/Gen/Core/Raw.hs
index dda15ead5..e01930e00 100644
--- a/primer/gen/Primer/Gen/Core/Raw.hs
+++ b/primer/gen/Primer/Gen/Core/Raw.hs
@@ -105,10 +105,10 @@ genCon :: ExprGen Expr
 genCon =
   Gen.recursive
     Gen.choice
-    [genCon' (pure []) (pure [])]
-    [genCon' (Gen.list (Range.linear 0 3) genType) (Gen.list (Range.linear 0 5) genExpr)]
+    [genCon' (pure [])]
+    [genCon' (Gen.list (Range.linear 0 5) genExpr)]
   where
-    genCon' tys tms = Con <$> genMeta <*> genValConName <*> tys <*> tms
+    genCon' tms = Con <$> genMeta <*> genValConName <*> tms
 
 genLam :: ExprGen Expr
 genLam = Lam <$> genMeta <*> genLVarName <*> genExpr
diff --git a/primer/gen/Primer/Gen/Core/Typed.hs b/primer/gen/Primer/Gen/Core/Typed.hs
index 8c0912355..e71a1fc19 100644
--- a/primer/gen/Primer/Gen/Core/Typed.hs
+++ b/primer/gen/Primer/Gen/Core/Typed.hs
@@ -87,7 +87,6 @@ import Primer.Typecheck (
   buildTypingContextFromModules',
   consistentKinds,
   consistentTypes,
-  decomposeTAppCon,
   extendLocalCxt,
   extendLocalCxtTy,
   extendLocalCxtTys,
@@ -387,7 +386,6 @@ genChk ty = do
               let cons' =
                     M.toList cons <&> \(c, (params, fldsTys0)) -> do
                       indicesMap <- for params $ \(p, k) -> (p,) <$> genWTType k
-                      let indices = snd <$> indicesMap
                       -- NB: it is vital to use simultaneous substitution here.
                       -- Consider the case where we have a local type variable @a@
                       -- in scope, say because we have already generated a
@@ -402,23 +400,16 @@ genChk ty = do
                       -- @Bool@.
                       fldsTys <- traverse (substTySimul $ M.fromList indicesMap) fldsTys0
                       flds <- traverse (Gen.small . genChk) fldsTys
-                      pure $ Con () c indices flds
+                      pure $ Con () c flds
               Gen.choice cons'
         Left _ -> pure Nothing -- not an ADT
         Right (_, _, []) -> pure Nothing -- is an empty ADT
-        -- TODO (saturated constructors) eventually (constructors are
-        -- saturated & checkable, and thus don't store their indices),
-        -- we will not need to record @params@ in the @Con@, and thus
-        -- the guard (and the panic) will be removed.
-        Right (tc, _, vcs)
-          | Just (tc', params) <- decomposeTAppCon ty
-          , tc == tc' ->
-              pure $
-                Just $
-                  Gen.choice $
-                    vcs <&> \(vc, tmArgTypes) ->
-                      Con () vc params <$> traverse genChk tmArgTypes
-          | otherwise -> panic "genCon invariants failed"
+        Right (_, _, vcs) ->
+          pure $
+            Just $
+              Gen.choice $
+                vcs <&> \(vc, tmArgTypes) ->
+                  Con () vc <$> traverse genChk tmArgTypes
     lambda =
       matchArrowType ty <&> \(sTy, tTy) -> do
         n <- genLVarNameAvoiding [tTy, sTy]
diff --git a/primer/src/Primer/API.hs b/primer/src/Primer/API.hs
index fa4deea38..75342e7df 100644
--- a/primer/src/Primer/API.hs
+++ b/primer/src/Primer/API.hs
@@ -720,11 +720,11 @@ viewTreeExpr e0 = case e0 of
       , childTrees = [viewTreeExpr e, viewTreeType t]
       , rightChild = Nothing
       }
-  Con _ c tyApps tmApps ->
+  Con _ c tmApps ->
     Tree
       { nodeId
       , body = TextBody $ RecordPair Flavor.Con $ globalName c
-      , childTrees = map viewTreeType tyApps ++ map viewTreeExpr tmApps
+      , childTrees = map viewTreeExpr tmApps
       , rightChild = Nothing
       }
   Lam _ s e ->
diff --git a/primer/src/Primer/Action.hs b/primer/src/Primer/Action.hs
index ae60837fe..9073854c7 100644
--- a/primer/src/Primer/Action.hs
+++ b/primer/src/Primer/Action.hs
@@ -22,7 +22,6 @@ import Data.Aeson (Value)
 import Data.Bifunctor.Swap qualified as Swap
 import Data.Generics.Product (typed)
 import Data.List (findIndex)
-import Data.List.Extra ((!?))
 import Data.List.NonEmpty qualified as NE
 import Data.Map.Strict qualified as Map
 import Data.Set qualified as Set
@@ -130,7 +129,6 @@ import Primer.Zipper (
   findNodeWithParent,
   findType,
   focus,
-  focusConTypes,
   focusLoc,
   focusOn,
   focusType,
@@ -351,7 +349,6 @@ applyAction' a = case a of
   ConstructLAM x -> termAction (constructLAM x) "cannot construct function in type"
   ConstructPrim p -> termAction (constructPrim p) "cannot construct primitive literal in type"
   ConstructSaturatedCon c -> termAction (constructSatCon c) "cannot construct con in type"
-  ConstructRefinedCon c -> termAction (constructRefinedCon c) "cannot construct con in type"
   ConstructLet x -> termAction (constructLet x) "cannot construct let in type"
   ConstructLetrec x -> termAction (constructLetrec x) "cannot construct letrec in type"
   ConvertLetToLetrec -> termAction convertLetToLetrec "cannot convert type to letrec"
@@ -365,12 +362,6 @@ applyAction' a = case a of
   ExitType -> \case
     InType zt -> pure $ InExpr $ unfocusType zt
     _ -> throwError $ CustomFailure ExitType "cannot exit type - not in type"
-  EnterConTypeArgument n -> \case
-    InExpr ze -> case (!? n) <$> focusConTypes ze of
-      Nothing -> throwError $ CustomFailure (EnterConTypeArgument n) "Move-to-constructor-argument failed: this is not a constructor"
-      Just Nothing -> throwError $ CustomFailure (EnterConTypeArgument n) "Move-to-constructor-argument failed: no such argument"
-      Just (Just z') -> pure $ InType z'
-    _ -> throwError $ CustomFailure (EnterConTypeArgument n) "cannot enter value constructors argument - not in expr"
   ConstructArrowL -> typeAction constructArrowL "cannot construct arrow - not in type"
   ConstructArrowR -> typeAction constructArrowR "cannot construct arrow - not in type"
   ConstructTCon c -> typeAction (constructTCon c) "cannot construct tcon in expr"
@@ -621,11 +612,11 @@ constructSatCon :: ActionM m => QualifiedText -> ExprZ -> m ExprZ
 constructSatCon c ze = case target ze of
   -- Similar comments re smartholes apply as to insertSatVar
   EmptyHole{} -> do
-    (_, nTyArgs, nTmArgs) <-
+    (_, nTmArgs) <-
       conInfo n >>= \case
         Left err -> throwError $ SaturatedApplicationError $ Left err
         Right t -> pure t
-    flip replace ze <$> con n (replicate nTyArgs tEmptyHole) (replicate nTmArgs emptyHole)
+    flip replace ze <$> con n (replicate nTmArgs emptyHole)
   e -> throwError $ NeedEmptyHole (ConstructSaturatedCon c) e
   where
     n = unsafeMkGlobalName c
@@ -633,58 +624,22 @@ constructSatCon c ze = case target ze of
 -- returns
 -- - "type" of ctor: the type an eta-expanded version of this constructor would check against
 --   e.g. @Cons@'s "type" is @∀a. a -> List a -> List a@.
--- - its arity (number of type args and number of term args required for full saturation)
+-- - its arity (number of args required for full saturation)
 conInfo ::
   MonadReader TC.Cxt m =>
   ValConName ->
-  m (Either Text (TC.Type, Int, Int))
+  m (Either Text (TC.Type, Int))
 conInfo c =
   asks (flip lookupConstructor c . TC.typeDefs) <&> \case
-    Just (vc, tc, td) -> Right (valConType tc td vc, length $ td.astTypeDefParameters, length $ vc.valConArgs)
+    Just (vc, tc, td) -> Right (valConType tc td vc, length $ vc.valConArgs)
     Nothing -> Left $ "Could not find constructor " <> show c
 
-constructRefinedCon :: ActionM m => QualifiedText -> ExprZ -> m ExprZ
-constructRefinedCon c ze = do
-  let n = unsafeMkGlobalName c
-  (cTy, numTyArgs, numTmArgs) <-
-    conInfo n >>= \case
-      Left err -> throwError $ RefineError $ Left err
-      Right t -> pure t
-  -- our Cxt in the monad does not care about the local context, we have to extract it from the zipper.
-  -- See https://github.com/hackworthltd/primer/issues/11
-  -- We only care about the type context for refine
-  let (tycxt, _) = localVariablesInScopeExpr (Left ze)
-  cxt <- asks $ TC.extendLocalCxtTys tycxt
-  tgtTy <- getTypeCache $ target ze
-  case target ze of
-    EmptyHole{} ->
-      breakLR <<$>> getRefinedApplications cxt cTy tgtTy >>= \case
-        Just (Just (tys, tms))
-          | length tys == numTyArgs && length tms == numTmArgs ->
-              flip replace ze <$> con n (pure <$> tys) (pure <$> tms)
-          -- If the refinement is not saturated, just give a saturated constructor
-          -- This could happen when refining @Cons@ to fit in a hole of type @List Nat -> List Nat@
-          -- as we get the "type" of @Cons@ being @∀a. a -> List a -> List a@
-          -- and thus a refinement of @Nat, _@.
-          | otherwise -> flip replace ze <$> hole (con n (replicate numTyArgs tEmptyHole) (replicate numTmArgs emptyHole) `ann` tEmptyHole)
-        -- See Note [No valid refinement]
-        -- NB: the inside of a hole must be synthesisable (see Note [Holes and bidirectionality])
-        Nothing -> flip replace ze <$> hole (con n (replicate numTyArgs tEmptyHole) (replicate numTmArgs emptyHole) `ann` tEmptyHole)
-        Just Nothing -> throwError $ InternalFailure "Types of constructors always have type abstractions before term abstractions"
-    e -> throwError $ NeedEmptyHole (ConstructRefinedCon c) e
-
 getTypeCache :: MonadError ActionError m => Expr -> m TypeCache
 getTypeCache =
   maybeTypeOf <&> \case
     Nothing -> throwError $ RefineError $ Left "Don't have a cached type"
     Just ty -> pure ty
 
--- | A view for lists where all 'Left' come before all 'Right'
-breakLR :: [Either a b] -> Maybe ([a], [b])
-breakLR =
-  spanMaybe leftToMaybe <&> \case
-    (ls, rest) -> (ls,) <$> traverse rightToMaybe rest
-
 constructLet :: ActionM m => Maybe Text -> ExprZ -> m ExprZ
 constructLet mx ze = case target ze of
   EmptyHole{} -> do
@@ -968,9 +923,8 @@ toProgActionInput ::
   Either ActionError [ProgAction]
 toProgActionInput def defName mNodeSel opt0 = \case
   Available.MakeConSat -> do
-    ref <- offerRefined
     opt <- optGlobal
-    toProg [if ref then ConstructRefinedCon opt else ConstructSaturatedCon opt]
+    toProg [ConstructSaturatedCon opt]
   Available.MakeInt -> do
     opt <- optNoCxt
     n <- maybeToEither (NeedInt opt0) $ readMaybe opt
diff --git a/primer/src/Primer/Action/Actions.hs b/primer/src/Primer/Action/Actions.hs
index 902de34fc..344d3e055 100644
--- a/primer/src/Primer/Action/Actions.hs
+++ b/primer/src/Primer/Action/Actions.hs
@@ -62,8 +62,6 @@ data Action
     ConstructPrim PrimCon
   | -- | Put a constructor applied to a saturated spine in an empty hole
     ConstructSaturatedCon QualifiedText
-  | -- | Put a constructor in an empty hole, and infer what it should be applied to
-    ConstructRefinedCon QualifiedText
   | -- | Put a let expression in an empty hole
     ConstructLet (Maybe Text)
   | -- | Put a letrec expression in an empty hole
@@ -80,17 +78,8 @@ data Action
     RenameLet Text
   | -- | Move from an annotation to its type
     EnterType
-  | -- TODO (saturated constructors) this includes moving from one of a
-    -- constructor's type arguments back to the constructor itself. This
-    -- will be removed when constructors no longer store their indices
-
-    -- | Move from a type up into the surrounding annotation
+  | -- | Move from a type up into the surrounding annotation
     ExitType
-  | -- TODO (saturated constructors) this is a temporary situation, and will be
-    -- removed once constructors no longer store their indices
-
-    -- | Move from a constructor into one if its type arguments (zero-indexed)
-    EnterConTypeArgument Int
   | -- | Construct a function type around the type under the cursor.
     -- The type under the cursor is placed in the domain (left) position.
     ConstructArrowL
diff --git a/primer/src/Primer/Action/Movement.hs b/primer/src/Primer/Action/Movement.hs
index d127cf6d1..b05d83ef2 100644
--- a/primer/src/Primer/Action/Movement.hs
+++ b/primer/src/Primer/Action/Movement.hs
@@ -12,12 +12,6 @@ data Movement
   | Parent
   | Branch ValConName
   | -- | Move into a term argument of a saturated constructor (zero-indexed)
-    -- TODO (saturated constructors) the current, temporary, situation is that
-    -- constructors have both type arguments (indices) and term arguments. To move
-    -- into a term argument, one uses this @Movement@ type. To move into a *type*
-    -- argument, use the special 'EnterConTypeArgument' action (it cannot be a
-    -- movement because it changes from focusing on an expression to focusing on a
-    -- type).
     ConChild Int
   deriving stock (Eq, Show, Read, Generic)
   deriving (FromJSON, ToJSON) via PrimerJSON Movement
diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs
index 3454e99da..64ca49404 100644
--- a/primer/src/Primer/App.hs
+++ b/primer/src/Primer/App.hs
@@ -799,9 +799,9 @@ applyProgAction prog mdefName = \case
               -- This last case means that the input program had no (useful) metadata
               (_, Nothing, Nothing) -> hole $ pure x `ann` tEmptyHole
          in transformM $ \case
-              Con m con' tys tms | con' == con -> do
+              Con m con' tms | con' == con -> do
                 adjustAtA index enhole tms >>= \case
-                  Just args' -> pure $ Con m con' tys args'
+                  Just args' -> pure $ Con m con' args'
                   Nothing -> throwError $ ConNotSaturated con
               e -> pure e
       updateDecons = transformCaseBranches prog type_ $
@@ -846,10 +846,10 @@ applyProgAction prog mdefName = \case
       -- not update the scrutinee before this happens.
       updateDefs = traverseOf (traversed % #_DefAST % #astDefExpr) (updateCons <=< updateDecons)
       updateCons = transformM $ \case
-        Con m con' tys tms | con' == con -> do
+        Con m con' tms | con' == con -> do
           m' <- DSL.meta
           case insertAt index (EmptyHole m') tms of
-            Just args' -> pure $ Con m con' tys args'
+            Just args' -> pure $ Con m con' args'
             Nothing -> throwError $ ConNotSaturated con
         e -> pure e
       updateDecons = transformCaseBranches prog type_ $
diff --git a/primer/src/Primer/Builtins/DSL.hs b/primer/src/Primer/Builtins/DSL.hs
index 487bc419b..d610c6a04 100644
--- a/primer/src/Primer/Builtins/DSL.hs
+++ b/primer/src/Primer/Builtins/DSL.hs
@@ -29,7 +29,6 @@ import Primer.Builtins (
 import Primer.Core (
   Expr,
   ID,
-  TyConName,
   Type,
  )
 import Primer.Core.DSL (
@@ -53,21 +52,21 @@ nat = \case
   0 -> con0 cZero
   n -> con1 cSucc $ nat (n - 1)
 
-maybe_ :: MonadFresh ID m => m Type -> (a -> m Expr) -> Maybe a -> m Expr
-maybe_ t f = \case
-  Nothing -> con cNothing [t] []
-  Just x -> con cJust [t] [f x]
+maybe_ :: MonadFresh ID m => (a -> m Expr) -> Maybe a -> m Expr
+maybe_ f = \case
+  Nothing -> con cNothing []
+  Just x -> con cJust [f x]
 
 maybeAnn :: MonadFresh ID m => m Type -> (a -> m Expr) -> Maybe a -> m Expr
-maybeAnn t f x = maybe_ t f x `ann` (tcon tMaybe `tapp` t)
+maybeAnn t f x = maybe_ f x `ann` (tcon tMaybe `tapp` t)
 
-list_ :: MonadFresh ID m => TyConName -> [m Expr] -> m Expr
-list_ t =
+list_ :: MonadFresh ID m => [m Expr] -> m Expr
+list_ =
   foldr
     ( \a b ->
-        con cCons [tcon t] [a, b]
+        con cCons [a, b]
     )
-    (con cNil [tcon t] [])
+    (con cNil [])
 
 listOf :: MonadFresh ID m => m Type -> m Type
 listOf = tapp (tcon tList)
diff --git a/primer/src/Primer/Core.hs b/primer/src/Primer/Core.hs
index 9c61b7d79..866f2d47c 100644
--- a/primer/src/Primer/Core.hs
+++ b/primer/src/Primer/Core.hs
@@ -34,12 +34,12 @@ import Data.Generics.Product
 import Data.Generics.Uniplate.Data ()
 import Optics (
   AffineFold,
+  AffineTraversal',
   Lens,
   Lens',
   Traversal,
-  Traversal',
   afailing,
-  traversalVL,
+  atraversalVL,
   (%),
  )
 import Primer.Core.Meta (
@@ -145,7 +145,7 @@ data Expr' a b
   | Ann a (Expr' a b) (Type' b)
   | App a (Expr' a b) (Expr' a b)
   | APP a (Expr' a b) (Type' b)
-  | Con a ValConName [Type' b] [Expr' a b] -- See Note [Checkable constructors]
+  | Con a ValConName [Expr' a b] -- See Note [Checkable constructors]
   | Lam a LVarName (Expr' a b)
   | LAM a TyVarName (Expr' a b)
   | Var a TmVarRef
@@ -232,23 +232,15 @@ data Expr' a b
 -- We represent a constructor-applied-to-a-spine as a thing (and can
 -- only check its type), where we insist that it is fully saturated.
 -- Thus whilst `Cons` is a term, it is ill-typed. The only well-formed
--- `Cons` usages are `Cons @A x xs`, which checks against `List A`
+-- `Cons` usages are `Cons x xs`, which checks against `List A`
 -- when `A ∋ x` and `List A ∋ xs`.
---
--- TODO (saturated constructors): the occurence of `@A` above is a temporary
--- wart here, and will be removed in due course. (It was needed when
--- constructors were still synthesisable, but is now a needless
--- complication. It also leads to some inaccuracies in this
--- description of the typing rule.)
+-- (Note that there are no type arguments here!)
 --
 -- Whilst this may be a bit inconsistent with the treatment of
 -- functions, it has the advantage of symmetry with construction and
 -- matching. (I.e. every time one sees a particular constructor, it
 -- has the same form: a head of that constructor, and the same number
 -- of (term) fields.)
--- TODO (saturated constructors): technically, a construction will
--- have type arguments/indices and a match will not, but this is
--- temporary, as we will soon remove indices.
 --
 -- As an example, `List Int ∋ Cons 2 Nil`, but `Cons` and `Cons 2` are ill-typed.
 -- Thus one needs to be aware of the difference between, say,
@@ -261,10 +253,6 @@ data Expr' a b
 -- corresponding to the parameters of its datatype.)
 -- Clearly one could eta-expand, (and if necessary add an annotation) to
 -- use as constructor non-saturatedly: e.g. write `map (λn . Succ n) [2,3]`.
---
--- TODO (saturated constructors): the above parenthetical about not
--- needing type applications is not currently true, but will be
--- shortly.
 
 -- Note [Case]
 -- We use a list for compatibility and ease of JSON
@@ -326,16 +314,13 @@ _bindMeta :: forall a b. Lens (Bind' a) (Bind' b) a b
 _bindMeta = position @1
 
 -- | Note that this does not recurse in to sub-expressions or sub-types.
-typesInExpr :: Traversal' (Expr' a b) (Type' b)
--- TODO (saturated constructors): if constructors did not store their indices,
--- then this could be an affine traversal
-typesInExpr = traversalVL $ \f -> \case
+typesInExpr :: AffineTraversal' (Expr' a b) (Type' b)
+typesInExpr = atraversalVL $ \point f -> \case
   Ann m e ty -> Ann m e <$> f ty
   APP m e ty -> APP m e <$> f ty
-  Con m c tys tms -> Con m c <$> traverse f tys <*> pure tms
   LetType m x ty e -> (\ty' -> LetType m x ty' e) <$> f ty
   Letrec m x b ty e -> (\ty' -> Letrec m x b ty' e) <$> f ty
-  e -> pure e
+  e -> point e
 
 instance HasID a => HasID (Expr' a b) where
   _id = position @1 % _id
diff --git a/primer/src/Primer/Core/DSL.hs b/primer/src/Primer/Core/DSL.hs
index e16e4a088..fc06dddb9 100644
--- a/primer/src/Primer/Core/DSL.hs
+++ b/primer/src/Primer/Core/DSL.hs
@@ -113,22 +113,22 @@ emptyHole = EmptyHole <$> meta
 ann :: MonadFresh ID m => m Expr -> m Type -> m Expr
 ann e t = Ann <$> meta <*> e <*> t
 
-con :: MonadFresh ID m => ValConName -> [m Type] -> [m Expr] -> m Expr
-con c tys tms = Con <$> meta <*> pure c <*> sequence tys <*> sequence tms
+con :: MonadFresh ID m => ValConName -> [m Expr] -> m Expr
+con c tms = Con <$> meta <*> pure c <*> sequence tms
 
 -- | Create a constructor of arity zero.
 -- (This condition is not checked here.
 --  If used with a constructor which has fields,
 --  then the typechecker will complain, when run.)
 con0 :: MonadFresh ID m => ValConName -> m Expr
-con0 c = con c [] []
+con0 c = con c []
 
 -- | Create a constructor of arity one.
 -- (This condition is not checked here.
 --  If used with a constructor which has fields,
 --  then the typechecker will complain, when run.)
 con1 :: MonadFresh ID m => ValConName -> m Expr -> m Expr
-con1 c t = con c [] [t]
+con1 c t = con c [t]
 
 lvar :: MonadFresh ID m => LVarName -> m Expr
 lvar v = Var <$> meta <*> pure (LocalVarRef v)
@@ -177,7 +177,7 @@ con0' m n = con0 $ qualifyName (ModuleName m) n
 con1' :: MonadFresh ID m => NonEmpty Name -> Name -> m Expr -> m Expr
 con1' m n = con1 $ qualifyName (ModuleName m) n
 
-con' :: MonadFresh ID m => NonEmpty Name -> Name -> [m Type] -> [m Expr] -> m Expr
+con' :: MonadFresh ID m => NonEmpty Name -> Name -> [m Expr] -> m Expr
 con' m n = con $ qualifyName (ModuleName m) n
 
 gvar' :: MonadFresh ID m => NonEmpty Name -> Name -> m Expr
diff --git a/primer/src/Primer/Core/Utils.hs b/primer/src/Primer/Core/Utils.hs
index b8c6a4fc4..514d37a30 100644
--- a/primer/src/Primer/Core/Utils.hs
+++ b/primer/src/Primer/Core/Utils.hs
@@ -119,7 +119,7 @@ _freeTmVars = traversalVL $ go mempty
       Ann m e ty -> Ann m <$> go bound f e <*> pure ty
       App m e s -> App m <$> go bound f e <*> go bound f s
       APP m e ty -> APP m <$> go bound f e <*> pure ty
-      Con m c tys tms -> Con m c tys <$> traverse (go bound f) tms
+      Con m c tms -> Con m c <$> traverse (go bound f) tms
       Lam m v e -> Lam m v <$> go (S.insert v bound) f e
       LAM m tv e ->
         -- A well scoped term will not refer to tv as a term
@@ -151,7 +151,7 @@ _freeTyVars = traversalVL $ go mempty
       Ann m e ty -> Ann m <$> go bound f e <*> traverseFreeVarsTy bound f ty
       App m e s -> App m <$> go bound f e <*> go bound f s
       APP m e ty -> APP m <$> go bound f e <*> traverseFreeVarsTy bound f ty
-      Con m c tys tms -> Con m c <$> traverse (traverseFreeVarsTy bound f) tys <*> traverse (go bound f) tms
+      Con m c tms -> Con m c <$> traverse (go bound f) tms
       Lam m v e ->
         -- A well scoped term will not refer to v as a type
         -- variable, so we do not need to add it to the bound set
diff --git a/primer/src/Primer/Eval/NormalOrder.hs b/primer/src/Primer/Eval/NormalOrder.hs
index e402bf2ec..2666b9765 100644
--- a/primer/src/Primer/Eval/NormalOrder.hs
+++ b/primer/src/Primer/Eval/NormalOrder.hs
@@ -108,7 +108,6 @@ import Primer.Zipper (
   TypeZ,
   down,
   focus,
-  focusConTypes,
   focusType,
   getBoundHere,
   getBoundHere',
@@ -165,8 +164,7 @@ foldMapExpr extract topDir = flip evalAccumT mempty . go . (topDir,) . focus
           _ ->
             msum $
               (goType =<< focusType' ez)
-                : ((goType =<<) <$> focusConTypes' ez)
-                  <> map (go <=< hoistAccum) (exprChildren dez)
+                : map (go <=< hoistAccum) (exprChildren dez)
     goType :: TypeZ -> AccumT Cxt f a
     goType tz =
       readerToAccumT (ReaderT $ extract.ty tz)
@@ -187,11 +185,6 @@ focusType' :: MonadPlus m => ExprZ -> AccumT Cxt m TypeZ
 -- so we don't need to 'add' anything
 focusType' = maybe empty pure . focusType
 
-focusConTypes' :: Monad m => ExprZ -> [AccumT Cxt m TypeZ]
--- Note that nothing in Expr binds a variable which scopes over a type child
--- so we don't need to 'add' anything
-focusConTypes' = maybe empty (fmap pure) . focusConTypes
-
 hoistAccum :: Monad m => Accum Cxt b -> AccumT Cxt m b
 hoistAccum = Foreword.hoistAccum generalize
 
@@ -262,8 +255,7 @@ findRedex tydefs globals =
                   _ -> mzero
              in msum @[] $
                   Foreword.hoistAccum hoistMaybe (substTyChild =<< focusType' ez)
-                    : (Foreword.hoistAccum hoistMaybe . (substTyChild =<<) <$> focusConTypes' ez)
-                      <> map (substChild <=< hoistAccum) (exprChildren (d, ez))
+                    : map (substChild <=< hoistAccum) (exprChildren (d, ez))
        in here <|> innerLet <|> dive
     goSubstTy :: TyVarName -> Type -> TypeZ -> AccumT Cxt Maybe RedexWithContext
     goSubstTy v t tz =
diff --git a/primer/src/Primer/Eval/Redex.hs b/primer/src/Primer/Eval/Redex.hs
index d66051d3e..f27b3e31c 100644
--- a/primer/src/Primer/Eval/Redex.hs
+++ b/primer/src/Primer/Eval/Redex.hs
@@ -24,7 +24,6 @@ import Control.Monad.Fresh (MonadFresh)
 import Control.Monad.Log (MonadLog, WithSeverity)
 import Control.Monad.Trans.Maybe (MaybeT (runMaybeT))
 import Data.Data (Data)
-import Data.Functor.Classes (liftEq)
 import Data.List (zip3)
 import Data.Map qualified as M
 import Data.Set qualified as S
@@ -92,7 +91,6 @@ import Primer.Core (
 import Primer.Core.DSL (ann, letType, let_, letrec, lvar, tlet, tvar)
 import Primer.Core.Transform (decomposeTAppCon)
 import Primer.Core.Utils (
-  alphaEqTy,
   concreteTy,
   forgetTypeMetadata,
   freeVars,
@@ -139,7 +137,7 @@ import Primer.Eval.Detail (
 import Primer.Eval.Detail qualified
 import Primer.Eval.Prim (tryPrimFun)
 import Primer.JSON (CustomJSON (CustomJSON), FromJSON, PrimerJSON, ToJSON)
-import Primer.Log (ConvertLogMessage (convert), logInfo, logWarning)
+import Primer.Log (ConvertLogMessage (convert), logWarning)
 import Primer.Name (Name, NameCounter)
 import Primer.TypeDef (
   TypeDefMap,
@@ -188,16 +186,6 @@ data EvalLog
     -- (Or the number of arguments expected from the scrutinee's type differs from either of these.)
     -- This should not happen if the expression is type correct.
     CaseRedexWrongArgNum ValConName [Expr] [Type' ()] [LVarName]
-  | -- | Found something that may have been a case redex,
-    -- but the number of type arguments in the scrutinee differs from the number in its annotation,
-    -- or the number of type arguments expected from the scrutinee's type differs from either of these.
-    -- This should not happen if the expression is type correct.
-    CaseRedexWrongTyArgNum ValConName [Type' ()] [Expr] [Type' ()] [TyVarName]
-  | -- | A case redex required a double annotation on (some of) its resultant let binding(s)
-    -- This is expected to happen for e.g. @case Just \@? True : Maybe Int of ...@, and
-    -- does not represent any problem. We log it to obtain insight about how common this
-    -- is in practice.
-    CaseRedexDoubleAnn ValConName [Expr] [Type' ()] [(TyVarName, Type' (), Type' ())] [LVarName]
   | InvariantFailure Text
   deriving stock (Show, Eq, Data, Generic)
   deriving anyclass (NFData)
@@ -285,18 +273,6 @@ data Redex
       -- ^ Where was @var@ bound (used for details)
       }
   | -- case C as : T A of ... ; C xs -> e ; ...   ~>  let xs=as:(lettype p=A in S) in e for data T p = C S
-    -- [However, for technical reasons (a hole type can act as a type-changing cast)
-    -- we need to annotate the let bindings with *both* the type arising from the constructor,
-    -- and that arising from the annotation, since these may differ in the presence of holes.
-    -- An also worry about variable capture.
-    -- In particular,
-    --  case C @A a : T B of C x -> e
-    -- should reduce to
-    --  let x=a:(lettype p=A in S):(lettype p=B in S) in e
-    -- when we have
-    --  data T p = C S[p].
-    -- If the two annotations happen to be the same, then we only need one copy.
-    -- ]
     -- Since constructors are checkable and scrutinees must be synthesisable,
     -- there must be an annotation if the term is well-typed
     -- (i.e. we do not need to consider @case C as of ...@).
@@ -308,10 +284,9 @@ data Redex
       , argTys :: [Type' ()]
       -- ^ The type of each scrutinee's argument, directly from the constructor's definition
       -- (thus is not well formed in the current scope)
-      , params :: [(TyVarName, Type' (), Type' ())]
+      , params :: [(TyVarName, Type' ())]
       -- ^ The parameters of the constructor's datatype, and their
-      -- instantiations from inspecting the constructor's type applications and
-      -- the type annotation on the scrutinee.
+      -- instantiations from inspecting the type annotation on the scrutinee.
       , binders :: [Bind]
       -- ^ The binders of the matching branch
       , rhs :: Expr
@@ -518,8 +493,7 @@ viewCaseRedex tydefs = \case
   -- variables. This is especially important, as we do not (yet?) take care of
   -- metadata correctly in this evaluator (for instance, substituting when we
   -- do a BETA reduction)!
-  orig@(Case mCase scrut@(Ann _ (Con mCon c tyargsFromCon' args) annotation) brs) -> do
-    let tyargsFromCon = forgetTypeMetadata <$> tyargsFromCon'
+  orig@(Case mCase scrut@(Ann _ (Con mCon c args) annotation) brs) -> do
     (abstractArgTys, params) <- case lookupConstructor tydefs c of
       Nothing -> do
         logWarning $ CaseRedexUnknownCtor c
@@ -535,10 +509,11 @@ viewCaseRedex tydefs = \case
       Nothing -> mzero
       Just tyargsFromAnn -> do
         tyargs <- do
-          unless (length params == length tyargsFromCon && length params == length tyargsFromAnn) $
+          unless (length params == length tyargsFromAnn) $
             logWarning $
-              CaseRedexWrongTyArgNum c tyargsFromCon args tyargsFromAnn params
-          pure $ zip3 params tyargsFromCon tyargsFromAnn
+              CaseRedexNotSaturated $
+                forgetTypeMetadata annotation
+          pure $ zip params tyargsFromAnn
         (patterns, br) <- extractBranch c brs
         renameBindings mCase scrut brs patterns orig
           <|> pure (formCaseRedex c abstractArgTys tyargs args patterns br (orig, scrut, getID mCon))
@@ -554,26 +529,22 @@ viewCaseRedex tydefs = \case
     {- Note [Case reduction and variable capture]
        There is a subtlety here around variable capture.
        Consider
-         case C @A' @B' s t : R A B of C a b -> e
+         case C s t : R A B of C a b -> e
        We would like to reduce this to
-         let a = s : (lettype p1=A',p2=B' in S) : (lettype p1=A,p2=B in S); let b = t : (lettype p1=A',p2=B' in T) : (lettype p1=A,p2=B in T) in e
-       where we have annotated `s` and `t` with their two types
-       (one from the arguments `A'` `B'` to the constructor,
-        one from the arguments `A` `B` to the annotation), which will be
-       built from `A` and `B` according to the definition of the type `data R p1 p2 = ... | C S T`
-       (for reasons of bidirectionality).
+         let a = s : (lettype p1=A,p2=B in S); let b = t : (lettype p1=A,p2=B in T) in e
+       where we have annotated `s` and `t` with their types, which will be
+       built from `A` and `B` according to the definition of the type `data R p1 p2 = ... | C S T`.
        Note that the binding of `a` may capture a reference in `t`
-       or (assuming type and term variables can shadow) in `A'`,`B'`, `A` or `B`.
+       or (assuming type and term variables can shadow) in `A` or `B`.
        (NB: the free variables in `S` and `T` are a subset of `p1,p2`.)
        We must catch this case and rename the case binders as a first step.
        Note that the free vars in
-       `t : (lettype p1=A',p2=B' in T) : (lettype p1=A,p2=B in T)`
-       are a subset of the free vars in the
-       arguments of the constructor (A', B', s, t) plus the arguments to its type
+       `t : (lettype p1=A,p2=B in T)` are a subset of the free vars in the
+       arguments of the constructor (s, t) plus the arguments to its type
        annotation (A, B).
        We shall be conservative and rename all binders in every branch apart
        from these free vars, i.e. from any free var in the scrutinee
-       `C @A' @B' s t : R A B`.
+       `C s t : R A B`.
        (We could get away with only renaming within the matching branch, only
        avoiding those FVs that actually occur, and in a "telescope" fashion:
        the first binder needs to avoid the FVs of all except the first
@@ -590,7 +561,7 @@ viewCaseRedex tydefs = \case
     formCaseRedex ::
       ValConName ->
       [Type' ()] ->
-      [(TyVarName, Type' (), Type' ())] ->
+      [(TyVarName, Type' ())] ->
       [Expr] ->
       [Bind] ->
       Expr ->
@@ -911,30 +882,19 @@ runRedex = \case
                     ps
             foldr (\(_, a', tA) -> tlet a' $ pure tA) renamed ps
       let subAnns ps' ty = do
-            let ps'' = (\(a, b, c) -> (a, (b, c))) <$> ps'
             let fvs = freeVarsTy ty
-            let ps = filter (flip elem fvs . fst) ps''
-            let psC = second fst <$> ps
-            aC <- subAnn psC ty
-            let psA = second snd <$> ps
-            -- If all relevant parameters are the same in both instantiations, then we only need one annotation
-            aA <- if liftEq (liftEq alphaEqTy) psA psC then pure Nothing else Just <$> subAnn psA ty
-            pure (aC, aA)
+            let ps = filter (flip elem fvs . fst) ps'
+            subAnn ps ty
       let ann' x t = x `ann` pure t
-      let mkAnn (tyC, tyA') = case tyA' of
-            Nothing -> (False, (`ann'` tyC))
-            Just tyA -> (True, \x -> x `ann'` tyC `ann'` tyA)
-      (diffAnn, letIDs, expr') <-
+      (letIDs, expr') <-
         foldrM
-          ( \(x, arg, argTy) (diffAnn, is, tm) -> do
-              (aC, aA) <- subAnns params argTy
-              let (d, putAnn) = mkAnn (aC, aA)
-              tm' <- let_ x (putAnn $ pure arg) (pure tm)
-              pure (diffAnn || d, getID tm' : is, tm')
+          ( \(x, arg, argTy) (is, tm) -> do
+              aA <- subAnns params argTy
+              tm' <- let_ x (pure arg `ann'` aA) (pure tm)
+              pure (getID tm' : is, tm')
           )
-          (False, [], rhs)
+          ([], rhs)
           $ zip3 binderNames args argTys
-      when diffAnn $ logInfo $ CaseRedexDoubleAnn con args argTys params binderNames
       let details =
             CaseReductionDetail
               { before = orig
diff --git a/primer/src/Primer/Examples.hs b/primer/src/Primer/Examples.hs
index c37a80e2a..dfb3a8026 100644
--- a/primer/src/Primer/Examples.hs
+++ b/primer/src/Primer/Examples.hs
@@ -97,7 +97,6 @@ import Primer.Core.DSL (
   tforall,
   tfun,
   thole,
-  tlet,
   tvar,
  )
 import Primer.Def (
@@ -147,9 +146,9 @@ map modName =
                   case_
                     (lvar "xs")
                     [ branch B.cNil [] $
-                        con B.cNil [tvar "b"] []
+                        con B.cNil []
                     , branch B.cCons [("y", Nothing), ("ys", Nothing)] $
-                        con B.cCons [tvar "b"] [lvar "f" `app` lvar "y", gvar this `aPP` tvar "a" `aPP` tvar "b" `app` lvar "f" `app` lvar "ys"]
+                        con B.cCons [lvar "f" `app` lvar "y", gvar this `aPP` tvar "a" `aPP` tvar "b" `app` lvar "f" `app` lvar "ys"]
                     ]
         pure (this, DefAST $ ASTDef term type_)
 
@@ -162,9 +161,9 @@ map' modName = do
         lam "xs" $
           case_
             (lvar "xs")
-            [ branch B.cNil [] $ con B.cNil [tvar "b"] []
+            [ branch B.cNil [] $ con B.cNil []
             , branch B.cCons [("y", Nothing), ("ys", Nothing)] $
-                con B.cCons [tvar "b"] [lvar "f" `app` lvar "y", lvar "go" `app` lvar "ys"]
+                con B.cCons [lvar "f" `app` lvar "y", lvar "go" `app` lvar "ys"]
             ]
   term <-
     lAM "a" $
@@ -254,7 +253,7 @@ comprehensive' typeable modName = do
           "y"
           ( app
               ( hole
-                  (con B.cJust [tEmptyHole] [emptyHole] `ann` (tcon B.tMaybe `tapp` tEmptyHole))
+                  (con B.cJust [emptyHole] `ann` (tcon B.tMaybe `tapp` tEmptyHole))
               )
               ( if typeable then emptyHole else hole $ gvar' (unModuleName modName) "unboundName"
               )
@@ -271,7 +270,7 @@ comprehensive' typeable modName = do
                           ( aPP
                               ( if typeable
                                   then
-                                    lAM "b" (lam "x" $ con B.cLeft [tcon B.tBool, tvar "b"] [lvar "x"])
+                                    lAM "b" (lam "x" $ con B.cLeft [lvar "x"])
                                       `ann` tforall
                                         "b"
                                         KType
@@ -282,8 +281,7 @@ comprehensive' typeable modName = do
                                     letType
                                       "b"
                                       (tcon B.tBool)
-                                      ( con B.cLeft [tlet "c" (tvar "b") $ tvar "c"] []
-                                      )
+                                      (con B.cLeft [])
                               )
                               (tvar "β")
                           )
@@ -394,9 +392,9 @@ mapOddProg len =
         (oddName, oddDef) <- odd modName
         (mapName, mapDef) <- map modName
         mapOddDef <- do
-          type_ <- tcon B.tList `tapp` tcon B.tBool
-          let lst = list_ B.tNat $ take len $ nat <$> [0 ..]
+          let lst = list_ $ take len $ nat <$> [0 ..]
           term <- gvar mapName `aPP` tcon B.tNat `aPP` tcon B.tBool `app` gvar oddName `app` lst
+          type_ <- tcon B.tList `tapp` tcon B.tBool
           pure $ DefAST $ ASTDef term type_
         let globs = [("even", evenDef), ("odd", oddDef), ("map", mapDef), ("mapOdd", mapOddDef)]
         pure (builtinModule', globs)
@@ -436,7 +434,7 @@ mapOddPrimProg len =
         (mapName, mapDef) <- map modName
         mapOddDef <- do
           type_ <- tcon B.tList `tapp` tcon B.tBool
-          let lst = list_ P.tInt $ take len $ int <$> [0 ..]
+          let lst = list_ $ take len $ int <$> [0 ..]
           term <- gvar mapName `aPP` tcon P.tInt `aPP` tcon B.tBool `app` gvar oddName `app` lst
           pure $ DefAST $ ASTDef term type_
         let globs = [("odd", oddDef), ("map", mapDef), ("mapOdd", mapOddDef)]
diff --git a/primer/src/Primer/Prelude/Polymorphism.hs b/primer/src/Primer/Prelude/Polymorphism.hs
index 9741fac6b..46094a7ea 100644
--- a/primer/src/Primer/Prelude/Polymorphism.hs
+++ b/primer/src/Primer/Prelude/Polymorphism.hs
@@ -74,11 +74,11 @@ mapDef = do
           lam "xs" $
             case_
               (lvar "xs")
-              [ branch cNil [] (con cNil [tvar "b"] [])
+              [ branch cNil [] (con cNil [])
               , branch cCons [("y", Nothing), ("ys", Nothing)] $
                   let fy = app (lvar "f") (lvar "y")
                       fys = apps' (gvar map) [Right $ tvar "a", Right $ tvar "b", Left $ lvar "f", Left $ lvar "ys"]
-                   in con cCons [tvar "b"] [fy, fys]
+                   in con cCons [fy, fys]
               ]
   pure $ DefAST $ ASTDef term type_
 
diff --git a/primer/src/Primer/Pretty.hs b/primer/src/Primer/Pretty.hs
index fc4c0dd5b..62b8473f0 100644
--- a/primer/src/Primer/Pretty.hs
+++ b/primer/src/Primer/Pretty.hs
@@ -19,7 +19,6 @@ import Prettyprinter (
   flatAlt,
   group,
   hardline,
-  hsep,
   indent,
   line,
   line',
@@ -88,10 +87,9 @@ prettyExpr :: PrettyOptions -> Expr' a b -> Doc AnsiStyle
 prettyExpr opts = \case
   Hole _ e -> (if inlineHoles opts then group else identity) (brac Curly Red (pE e))
   EmptyHole _ -> col Red "?"
-  Con _ n tys tms ->
-    let prettyTys = (col Yellow "@" <>) . pT <$> tys
-        prettyTms = brac Round White . pE <$> tms
-     in vsep $ hsep (col Green (gname opts n) : prettyTys) : prettyTms
+  Con _ n tms ->
+    let prettyTms = brac Round White . pE <$> tms
+     in vsep $ col Green (gname opts n) : prettyTms
   Var _ v -> case v of
     GlobalVarRef n -> col Blue (gname opts n)
     LocalVarRef n -> lname n
diff --git a/primer/src/Primer/Primitives.hs b/primer/src/Primer/Primitives.hs
index 52a22971a..a0e8f0aee 100644
--- a/primer/src/Primer/Primitives.hs
+++ b/primer/src/Primer/Primitives.hs
@@ -272,7 +272,7 @@ primFunDef def args = case def of
     _ -> err
   where
     exprToNat = \case
-      Con _ c [] [] | c == cZero -> Just 0
-      Con _ c [] [x] | c == cSucc -> succ <$> exprToNat x
+      Con _ c [] | c == cZero -> Just 0
+      Con _ c [x] | c == cSucc -> succ <$> exprToNat x
       _ -> Nothing
     err = Left $ PrimFunError def args
diff --git a/primer/src/Primer/Typecheck.hs b/primer/src/Primer/Typecheck.hs
index 8261403f2..5526355c4 100644
--- a/primer/src/Primer/Typecheck.hs
+++ b/primer/src/Primer/Typecheck.hs
@@ -590,7 +590,7 @@ check :: TypeM e m => Type -> Expr -> m ExprT
 check t = \case
   -- We assume that constructor names are unique
   -- See Note [Checkable constructors] in Core.hs
-  con@(Con i c tys tms) -> do
+  con@(Con i c tms) -> do
     -- If the input type @t@ is a hole-applied-to-some-arguments,
     -- then refine it to the parent type of @c@ applied to some holes plus those original arguments
     (cParent, parentParams) <-
@@ -627,62 +627,15 @@ check t = \case
       -- And 'C' is a constructor of 'T' (writing 'T's parameters as 'ps' with kinds 'ks')
       -- with arguments 'Rs[ps]',
       -- then this particular instantiation should have arguments 'Rs[As]'
-      Right (tc, td, instVCs) -> case lookup c instVCs of
+      Right (tc, _td, instVCs) -> case lookup c instVCs of
         Nothing -> recoverSH $ ConstructorWrongADT tc c
-        Just _argTys -> do
-          -- TODO (saturated constructors) unfortunately, due to constructors
-          -- currently having type arguments, this is not quite true. We instead
-          -- - check the kinding of @tys@ to ensure the third point is sane
-          -- - check consistency of @tys@ and 'As' (we do this before the next
-          --   point as SmartHoles may kick in in *both* the previous point and
-          --   this point, for example eliding a hole above and then re-inserting
-          --   it here. We need to check the arguments at the consistent type!)
-          -- - instantiate 'T' at @tys@ to find the required types of the term arguments
-          tys' <- ensureJust ConstructorTypeArgsKinding $ zipWithExactM checkKind' (snd <$> astTypeDefParameters td) tys
-          tAs <-
-            ensureJust (InternalError "instantiateValCons succeeded, but decomposeTAppCon did not") $
-              pure . snd <$> decomposeTAppCon t'
-          -- See comments on UnsaturatedConstructor error below about the fatal 'ensureJust' error
-          --
-          -- If a type argument is inconsistent between the type and the
-          -- constructor, then wrap that of the constructor in a hole.
-          -- Arguably we should be finer-grained here, say changing
-          -- @Maybe (List Bool) ∋ Just (List Int) t@ into @Just (List {?
-          -- Int ?}) t@, but we do not have the infrastructure to do that,
-          -- and it is only temporary that constructors have type
-          -- arguments, so it does not seem worthwhile. (Note that
-          -- normally when we do a consistency check, neither side is
-          -- verbatim from the AST, and thus it normally does not make
-          -- sense to do smartholes on that problem.)
-          tys'' <-
-            ensureJust ConstructorTypeArgsInconsistentNumber $
-              zipWithExactM
-                ( \(tFromConOrig, tFromCon) tFromType ->
-                    if consistentTypes (forgetTypeMetadata tFromCon) tFromType
-                      then pure tFromCon
-                      else
-                        asks smartHoles >>= \case
-                          NoSmartHoles -> throwError' ConstructorTypeArgsInconsistentTypes
-                          -- We are careful to not remove an outer hole when kind checking, only
-                          -- to re-add it here with a different ID.
-                          SmartHoles -> case tFromConOrig of
-                            THole (Meta id _ m) _ -> pure $ THole (Meta id KHole m) tFromCon
-                            _ -> THole <$> meta' KHole <*> pure tFromCon
-                )
-                (zip tys tys')
-                tAs
-          let tys''NoMeta = forgetTypeMetadata <$> tys''
-          instantiateValCons (foldl' (TApp ()) (TCon () tc) tys''NoMeta) >>= \case
-            Left _ -> throwError' $ InternalError "instantiateValCons succeeded, but changing type args to others of same kind made it fail"
-            Right (_, _, instVCs') -> case lookup c instVCs' of
-              Nothing -> throwError' $ InternalError "same ADT now does not contain the constructor"
-              Just argTys -> do
-                -- Check that the arguments have the correct type
-                -- Note that being unsaturated is a fatal error and SmartHoles will not try to recover
-                -- (this is a design decision -- we put the burden onto code that builds ASTs,
-                -- e.g. the action code is responsible for only creating saturated constructors)
-                tms' <- ensureJust (UnsaturatedConstructor c) $ zipWithExactM check argTys tms
-                pure $ Con (annotate (TCChkedAt t') i) c tys'' tms'
+        Just argTys -> do
+          -- Check that the arguments have the correct type
+          -- Note that being unsaturated is a fatal error and SmartHoles will not try to recover
+          -- (this is a design decision -- we put the burden onto code that builds ASTs,
+          -- e.g. the action code is responsible for only creating saturated constructors)
+          tms' <- ensureJust (UnsaturatedConstructor c) $ zipWithExactM check argTys tms
+          pure $ Con (annotate (TCChkedAt t') i) c tms'
   lam@(Lam i x e) -> do
     case matchArrowType t of
       Just (t1, t2) -> do
diff --git a/primer/src/Primer/Typecheck/TypeError.hs b/primer/src/Primer/Typecheck/TypeError.hs
index c50ba21bf..a35ebef17 100644
--- a/primer/src/Primer/Typecheck/TypeError.hs
+++ b/primer/src/Primer/Typecheck/TypeError.hs
@@ -18,27 +18,9 @@ data TypeError
     ConstructorNotFullAppADT (Type' ()) ValConName
   | -- | This ADT does not have a constructor of that name
     ConstructorWrongADT TyConName ValConName
-  | -- TODO (saturated constructors) this is a temporary situation, and this
-    -- error will be removed once constructors do not store their indices
-
-    -- | A constructor has inconsistently-kinded type arguments
-    -- (wrt the ADT containing the constructor)
-    ConstructorTypeArgsKinding
-  | -- TODO (saturated constructors) this is a temporary situation, and this
-    -- error will be removed once constructors do not store their indices
-
-    -- | A constructor has the wrong number of type arguments
-    -- (wrt the type we are checking it at)
-    ConstructorTypeArgsInconsistentNumber
-  | -- TODO (saturated constructors) this is a temporary situation, and this
-    -- error will be removed once constructors do not store their indices
-
-    -- | A constructor has the inconsistent type arguments
-    -- (wrt the type we are checking it at)
-    ConstructorTypeArgsInconsistentTypes
   | UnknownConstructor ValConName
   | -- | Constructors (term-level) must be saturated.
-    -- This error catches both under- and over-saturation (of term arguments).
+    -- This error catches both under- and over-saturation.
     UnsaturatedConstructor ValConName
   | -- | Cannot use a PrimCon when either no type of the appropriate name is
     -- in scope, or it is a user-defined type
diff --git a/primer/src/Primer/Zipper.hs b/primer/src/Primer/Zipper.hs
index 6c82ab1b5..a55f246fc 100644
--- a/primer/src/Primer/Zipper.hs
+++ b/primer/src/Primer/Zipper.hs
@@ -16,7 +16,6 @@ module Primer.Zipper (
   BindLoc,
   BindLoc' (..),
   focusType,
-  focusConTypes,
   focusLoc,
   unfocusType,
   focusOnlyType,
@@ -67,7 +66,6 @@ import Foreword
 
 import Data.Data (Data)
 import Data.Generics.Product (position)
-import Data.Generics.Uniplate.Data (holesBi)
 import Data.Generics.Uniplate.Zipper (
   Zipper,
   fromZipper,
@@ -251,15 +249,6 @@ instance HasID a => HasID (BindLoc' a b) where
 -- @Letrec@ or @LetType@ node (as those are the only ones that contain a
 -- @Type@).
 focusType :: (Data a, Data b) => ExprZ' a b -> Maybe (TypeZ' a b)
--- TODO (saturated constructors): This is incomplete, since currently Con
--- have type arguments. However, this is only a temporary situation, and
--- handling them is difficult, since they have multiple type children we
--- cannot focus on just one! We will put up with this (will need a small
--- workaround in Eval and in focusOn: we can focus on these by ID, just
--- not via focusType!) until constructors no longer store their indices.
--- Whilst we could use 'singular' to focus on the first index of a constructor,
--- we prefer to focus on *no* type children of constructors, rather than
--- arbitrarily choosing the first one.
 focusType z = case target z of
   Con{} -> Nothing
   _ -> do
@@ -268,14 +257,6 @@ focusType z = case target z of
   where
     l = _target % typesInExpr
 
--- TODO (saturated constructors): This is part of the temporary workaround for
--- @focusType@ (see comments there for details)
--- The outer 'Maybe' says whether the 'ExprZ'' was a 'Con' or not.
-focusConTypes :: (Data a, Data b) => ExprZ' a b -> Maybe [TypeZ' a b]
-focusConTypes ez = case target ez of
-  Con m c tys tms -> Just $ holesBi tys <&> \(t, cxt) -> TypeZ (zipper t) $ \t' -> replace (Con m c (cxt t') tms) ez
-  _ -> Nothing
-
 -- | If the currently focused expression is a case expression, search the bindings of its branches
 -- to find one matching the given ID, and return the 'Loc' for that binding.
 -- If no match is found, return @Nothing@.
@@ -362,10 +343,9 @@ focusOn' i = fmap snd . search matchesID
       -- If the target has an embedded type, search the type for a match.
       -- If the target is a case expression with bindings, search each binding for a match.
       | otherwise =
-          let inCtorIndices = focusConTypes z >>= getFirst . foldMap' (First . fmap fst . search (guarded (== i) . getID . target)) <&> InType
-              inType = focusType z >>= search (guarded (== i) . getID . target) <&> fst <&> InType
+          let inType = focusType z >>= search (guarded (== i) . getID . target) <&> fst <&> InType
               inCaseBinds = findInCaseBinds i z
-           in inCtorIndices <|> inType <|> inCaseBinds
+           in inType <|> inCaseBinds
 
 -- Gets all binders that scope over the focussed subtree
 bindersAbove :: ExprZ -> S.Set Name
diff --git a/primer/test/Tests/Action.hs b/primer/test/Tests/Action.hs
index b4c0835d8..57be3d11b 100644
--- a/primer/test/Tests/Action.hs
+++ b/primer/test/Tests/Action.hs
@@ -13,7 +13,7 @@ import Hedgehog hiding (
  )
 import Primer.Action (
   Action (..),
-  ActionError (CaseBindsClash, NameCapture, RefineError),
+  ActionError (CaseBindsClash, NameCapture),
   Movement (..),
   applyActionsToExpr,
  )
@@ -39,7 +39,6 @@ import Primer.Primitives (tChar, tInt)
 import Primer.Test.TestM (evalTestM)
 import Primer.Test.Util (
   clearMeta,
-  constructRefinedCon,
   constructSaturatedCon,
   constructTCon,
  )
@@ -352,16 +351,16 @@ unit_rename_LAM :: Assertion
 unit_rename_LAM =
   actionTest
     NoSmartHoles
-    (ann (lAM "a" (con cNil [tvar "a"] [])) (tforall "b" KType $ listOf (tvar "b")))
+    (ann (lAM "a" (emptyHole `aPP` tvar "a")) (tforall "b" KType $ listOf (tvar "b")))
     [Move Child1, RenameLAM "b"]
-    (ann (lAM "b" (con cNil [tvar "b"] [])) (tforall "b" KType $ listOf (tvar "b")))
+    (ann (lAM "b" (emptyHole `aPP` tvar "b")) (tforall "b" KType $ listOf (tvar "b")))
 
 unit_rename_LAM_2 :: Assertion
 unit_rename_LAM_2 =
   actionTestExpectFail
     (const True)
     NoSmartHoles
-    (ann (lAM "b" (lAM "a" (con cNil [tvar "b"] []))) tEmptyHole)
+    (ann (lAM "b" (lAM "a" (emptyHole `aPP` tvar "b"))) tEmptyHole)
     [Move Child1, Move Child1, RenameLAM "b"]
 
 unit_rename_LAM_3 :: Assertion
@@ -1024,54 +1023,21 @@ unit_smart_type_2 =
     [EnterType, ConstructTApp]
     (emptyHole `ann` (tcon tList `tapp` tEmptyHole))
 
-unit_refine_1 :: Assertion
-unit_refine_1 =
-  actionTestExpectFail
-    (\case RefineError _ -> True; _ -> False)
-    NoSmartHoles
-    emptyHole
-    [constructRefinedCon cNil]
-
-unit_refine_2 :: Assertion
-unit_refine_2 =
-  actionTest
-    NoSmartHoles
-    (emptyHole `ann` (tcon tList `tapp` tcon tNat))
-    [Move Child1, constructRefinedCon cNil]
-    (con cNil [tcon tNat] [] `ann` (tcon tList `tapp` tcon tNat))
-
-unit_refine_3 :: Assertion
-unit_refine_3 =
-  actionTest
-    NoSmartHoles
-    (emptyHole `ann` (tcon tList `tapp` tEmptyHole))
-    [Move Child1, constructRefinedCon cNil]
-    (con cNil [tEmptyHole] [] `ann` (tcon tList `tapp` tEmptyHole))
-
 unit_refine_4 :: Assertion
 unit_refine_4 =
   actionTest
     NoSmartHoles
-    (let_ "nil" (lAM "a" (con cNil [tvar "a"] []) `ann` tforall "a" KType (tcon tList `tapp` tvar "a")) $ emptyHole `ann` (tcon tList `tapp` tcon tNat))
+    (let_ "nil" (lAM "a" (con cNil []) `ann` tforall "a" KType (tcon tList `tapp` tvar "a")) $ emptyHole `ann` (tcon tList `tapp` tcon tNat))
     [Move Child2, Move Child1, InsertRefinedVar $ LocalVarRef "nil"]
-    (let_ "nil" (lAM "a" (con cNil [tvar "a"] []) `ann` tforall "a" KType (tcon tList `tapp` tvar "a")) $ (lvar "nil" `aPP` tcon tNat) `ann` (tcon tList `tapp` tcon tNat))
+    (let_ "nil" (lAM "a" (con cNil []) `ann` tforall "a" KType (tcon tList `tapp` tvar "a")) $ (lvar "nil" `aPP` tcon tNat) `ann` (tcon tList `tapp` tcon tNat))
 
 unit_refine_5 :: Assertion
 unit_refine_5 =
   actionTest
     NoSmartHoles
-    (let_ "nil" (lAM "a" (con cNil [tvar "a"] []) `ann` tforall "a" KType (tcon tList `tapp` tvar "a")) $ emptyHole `ann` (tcon tList `tapp` tEmptyHole))
+    (let_ "nil" (lAM "a" (con cNil []) `ann` tforall "a" KType (tcon tList `tapp` tvar "a")) $ emptyHole `ann` (tcon tList `tapp` tEmptyHole))
     [Move Child2, Move Child1, InsertRefinedVar $ LocalVarRef "nil"]
-    (let_ "nil" (lAM "a" (con cNil [tvar "a"] []) `ann` tforall "a" KType (tcon tList `tapp` tvar "a")) $ (lvar "nil" `aPP` tEmptyHole) `ann` (tcon tList `tapp` tEmptyHole))
-
--- If there is no valid refinement, insert saturated constructor into a non-empty hole
-unit_refine_mismatch_con :: Assertion
-unit_refine_mismatch_con =
-  actionTest
-    NoSmartHoles
-    (emptyHole `ann` tcon tNat)
-    [Move Child1, constructRefinedCon cCons]
-    (hole (con cCons [tEmptyHole] [emptyHole, emptyHole] `ann` tEmptyHole) `ann` tcon tNat)
+    (let_ "nil" (lAM "a" (con cNil []) `ann` tforall "a" KType (tcon tList `tapp` tvar "a")) $ (lvar "nil" `aPP` tEmptyHole) `ann` (tcon tList `tapp` tEmptyHole))
 
 -- If there is no valid refinement, insert saturated variable into a non-empty hole
 unit_refine_mismatch_var :: Assertion
@@ -1108,30 +1074,6 @@ unit_refine_mismatch_var =
         $ hole (lvar "cons" `aPP` tEmptyHole `app` emptyHole `app` emptyHole) `ann` tcon tBool
     )
 
--- Constructors are saturated, so if the hole has an arrow type, when we insert
--- a constructor it cannot match the arrow, so it is inserted into a hole
-unit_refine_arr_1 :: Assertion
-unit_refine_arr_1 =
-  actionTest
-    NoSmartHoles
-    (emptyHole `ann` (tEmptyHole `tfun` tEmptyHole))
-    [Move Child1, constructRefinedCon cCons]
-    (hole (con cCons [tEmptyHole] [emptyHole, emptyHole] `ann` tEmptyHole) `ann` (tEmptyHole `tfun` tEmptyHole))
-
--- TODO (saturated constructors) update this comment for ctors-dont-store-indices ('Cons Nat')
---
--- Constructors are checkable and fully saturated, so even if the hole has type
--- @List Nat -> List Nat@, when we insert a @Cons@ constructor, we end up with
--- @{? Cons @? ? ? :: ? ?}@
--- (the inside of a hole is synthesisable position: see Note [Holes and bidirectionality])
-unit_refine_arr_2 :: Assertion
-unit_refine_arr_2 =
-  actionTest
-    NoSmartHoles
-    (emptyHole `ann` ((tcon tList `tapp` tcon tNat) `tfun` (tcon tList `tapp` tcon tNat)))
-    [Move Child1, constructRefinedCon cCons]
-    (hole (con cCons [tEmptyHole] [emptyHole, emptyHole] `ann` tEmptyHole) `ann` ((tcon tList `tapp` tcon tNat) `tfun` (tcon tList `tapp` tcon tNat)))
-
 unit_primitive_1 :: Assertion
 unit_primitive_1 =
   actionTest
@@ -1158,12 +1100,6 @@ unit_move_ctor =
     (emptyHole `ann` tEmptyHole)
     [ Move Child1
     , constructSaturatedCon cMakePair
-    , EnterConTypeArgument 0
-    , constructTCon tNat
-    , ExitType
-    , EnterConTypeArgument 1
-    , constructTCon tBool
-    , ExitType
     , Move $ ConChild 0
     , constructSaturatedCon cZero
     , Move Parent
@@ -1171,7 +1107,7 @@ unit_move_ctor =
     , constructSaturatedCon cFalse
     , Move Parent
     ]
-    (con cMakePair [tcon tNat, tcon tBool] [con0 cZero, con0 cFalse] `ann` tEmptyHole)
+    (con cMakePair [con0 cZero, con0 cFalse] `ann` tEmptyHole)
 
 -- * Helpers
 
diff --git a/primer/test/Tests/Action/Available.hs b/primer/test/Tests/Action/Available.hs
index 03fb3d4b8..4f57e4007 100644
--- a/primer/test/Tests/Action/Available.hs
+++ b/primer/test/Tests/Action/Available.hs
@@ -369,7 +369,7 @@ unit_sat_con_1 =
     (emptyHole `ann` (tEmptyHole `tfun` tEmptyHole))
     [Child1]
     (Right (MakeConSat, Option "Cons" $ Just $ unName <$> unModuleName builtinModuleName))
-    (hole (con cCons [tEmptyHole] [emptyHole, emptyHole] `ann` tEmptyHole) `ann` (tEmptyHole `tfun` tEmptyHole))
+    (hole (con cCons [emptyHole, emptyHole] `ann` tEmptyHole) `ann` (tEmptyHole `tfun` tEmptyHole))
 
 unit_sat_con_2 :: Assertion
 unit_sat_con_2 =
@@ -379,7 +379,7 @@ unit_sat_con_2 =
     (emptyHole `ann` ((tcon tList `tapp` tcon tNat) `tfun` (tcon tList `tapp` tcon tNat)))
     [Child1]
     (Right (MakeConSat, Option "Cons" $ Just $ unName <$> unModuleName builtinModuleName))
-    (hole (con cCons [tEmptyHole] [emptyHole, emptyHole] `ann` tEmptyHole) `ann` ((tcon tList `tapp` tcon tNat) `tfun` (tcon tList `tapp` tcon tNat)))
+    (hole (con cCons [emptyHole, emptyHole] `ann` tEmptyHole) `ann` ((tcon tList `tapp` tcon tNat) `tfun` (tcon tList `tapp` tcon tNat)))
 
 -- | Apply the action to the node in the input expression pointed to by the
 -- 'Movement' (starting from the root), checking that it would actually be offered
diff --git a/primer/test/Tests/Action/Capture.hs b/primer/test/Tests/Action/Capture.hs
index 53fc774e3..3d6398a19 100644
--- a/primer/test/Tests/Action/Capture.hs
+++ b/primer/test/Tests/Action/Capture.hs
@@ -8,7 +8,6 @@ import Primer.Action (
   ActionError (NameCapture, NeedEmptyHole),
   Movement (..),
  )
-import Primer.Builtins
 import Primer.Core (
   Kind (KType),
  )
@@ -160,7 +159,7 @@ unit_ty_tm_same_namespace =
   actionTestExpectFail
     isNameCapture
     NoSmartHoles
-    (ann (lAM "a" $ con cNil [tvar "a"] []) tEmptyHole)
+    (ann (lAM "a" $ emptyHole `ann` tvar "a") tEmptyHole)
     [Move Child1, Move Child1, ConstructLam (Just "a")]
 
 -- * Helpers
diff --git a/primer/test/Tests/Action/Prog.hs b/primer/test/Tests/Action/Prog.hs
index fead3341c..295b39ff6 100644
--- a/primer/test/Tests/Action/Prog.hs
+++ b/primer/test/Tests/Action/Prog.hs
@@ -537,7 +537,7 @@ unit_copy_paste_duplicate = do
       toDef = gvn "blank"
       ((p, fromType, fromExpr, _toType, _toExpr), maxID) = create $ do
         mainType <- tforall "a" KType (tvar "a" `tfun` (tcon tMaybe `tapp` tEmptyHole))
-        mainExpr <- lAM "b" $ lam "x" $ con cJust [tvar "b"] [lvar "x"]
+        mainExpr <- lAM "b" $ lam "x" $ con cJust [lvar "x"]
         let mainDef = ASTDef mainExpr mainType
         blankDef <- ASTDef <$> emptyHole <*> tEmptyHole
         pure
@@ -635,16 +635,16 @@ unit_raise = do
         clearDefMapIDs (foldMap' moduleDefsQualified $ progModules r) @?= clearDefMapIDs (foldMap' moduleDefsQualified $ progModules tcpExpected)
 
 -- ∀a. List a -> ∀b. b -> Pair a b
--- /\a . λ x . case x of Nil -> ? ; Cons y ys -> /\b . λz . MakePair @a @b y z
+-- /\a . λ x . case x of Nil -> ? ; Cons y ys -> /\b . λz . MakePair (y : a) (z : b)
 -- copy the MakePair @a @b y z into the hole to get
--- /\a . λ x . case x of Nil -> MakePair @a @? ? ? ; Cons y ys -> /\b . λz . MakePair @a @b y z
+-- /\a . λ x . case x of Nil -> MakePair (? : a) (? : ?) ; Cons y ys -> /\b . λz . MakePair (y : a) (z : b)
 unit_copy_paste_expr_1 :: Assertion
 unit_copy_paste_expr_1 = do
   let mainName' = "main"
       mainName = gvn mainName'
       ((pInitial, srcID, pExpected), maxID) = create $ do
         ty <- tforall "a" KType $ (tcon tList `tapp` tvar "a") `tfun` tforall "b" KType (tvar "b" `tfun` (tcon tPair `tapp` tvar "a" `tapp` tvar "b"))
-        let toCopy' = con cMakePair [tvar "a", tvar "b"] [lvar "y", lvar "z"] -- want different IDs for the two occurences in expected
+        let toCopy' = con cMakePair [lvar "y" `ann` tvar "a", lvar "z" `ann` tvar "b"] -- want different IDs for the two occurences in expected
         toCopy <- toCopy'
         let skel r =
               lAM "a" $
@@ -654,7 +654,7 @@ unit_copy_paste_expr_1 = do
                     [ branch cNil [] r
                     , branch cCons [("y", Nothing), ("ys", Nothing)] $ lAM "b" $ lam "z" $ pure toCopy
                     ]
-        expectPasted <- con cMakePair [tvar "a", tEmptyHole] [emptyHole, emptyHole]
+        expectPasted <- con cMakePair [emptyHole `ann` tvar "a", emptyHole `ann` tEmptyHole]
         -- TODO: in the future we may want to insert let bindings for variables
         -- which are out of scope in the target, and produce something like
         -- expectPasted <- letType "b" tEmptyHole $ let_ "y" (emptyHole `ann` tvar "a") $ let_ "z" (emptyHole `ann` tvar "b") toCopy'
@@ -900,9 +900,6 @@ unit_RenameCon =
                       case_
                         ( con
                             cA
-                            [ tEmptyHole
-                            , tEmptyHole
-                            ]
                             [ con0 (vcn "True")
                             , con0 (vcn "True")
                             , con0 (vcn "True")
@@ -934,9 +931,6 @@ unit_RenameCon =
                     case_
                       ( con
                           (vcn "A'")
-                          [ tEmptyHole
-                          , tEmptyHole
-                          ]
                           [ con0 (vcn "True")
                           , con0 (vcn "True")
                           , con0 (vcn "True")
@@ -961,9 +955,6 @@ unit_RenameCon_clash =
                   ( hole
                       ( con
                           cA
-                          [ tEmptyHole
-                          , tEmptyHole
-                          ]
                           [ emptyHole
                           , emptyHole
                           , emptyHole
@@ -1042,9 +1033,6 @@ unit_SetConFieldType_con =
         x <-
           con
             cA
-            [ tEmptyHole
-            , tEmptyHole
-            ]
             [ con0 (vcn "True")
             , con0 (vcn "True")
             , con0 (vcn "True")
@@ -1065,9 +1053,6 @@ unit_SetConFieldType_con =
           ( create' $
               con
                 cA
-                [ tEmptyHole
-                , tEmptyHole
-                ]
                 [ con0 (vcn "True")
                 , hole (con0 (vcn "True") `ann` tcon (tcn "Bool"))
                 , con0 (vcn "True")
@@ -1082,8 +1067,8 @@ setConFieldTypeHelper ty1 tmInput ty2' tmExpected =
    in progActionTest
         ( defaultProgEditableTypeDefs . sequence . pure $ do
             x <-
-              con cB [tEmptyHole, ty1] [emptyHole, tmInput]
-            astDef "def" x <$> tEmptyHole
+              con cB [emptyHole, tmInput]
+            astDef "def" x <$> ((tcon tT `tapp` tEmptyHole) `tapp` ty1)
         )
         [SetConFieldType tT cB 1 ty2]
         $ expectSuccess
@@ -1097,7 +1082,7 @@ setConFieldTypeHelper ty1 tmInput ty2' tmExpected =
           forgetMetadata (astDefExpr def)
             @?= forgetMetadata
               ( create' $
-                  con cB [tEmptyHole, ty1] [emptyHole, tmExpected]
+                  con cB [emptyHole, tmExpected]
               )
 
 -- change the type of a field which currently wraps a checkable term
@@ -1235,9 +1220,6 @@ unit_AddConField =
           case_
             ( con
                 cA
-                [ tEmptyHole
-                , tEmptyHole
-                ]
                 [ con0 (vcn "True")
                 , con0 (vcn "True")
                 , con0 (vcn "True")
@@ -1266,9 +1248,6 @@ unit_AddConField =
               case_
                 ( con
                     cA
-                    [ tEmptyHole
-                    , tEmptyHole
-                    ]
                     [ con0 (vcn "True")
                     , emptyHole
                     , con0 (vcn "True")
@@ -1276,7 +1255,7 @@ unit_AddConField =
                     ]
                     `ann` (tcon tT `tapp` tEmptyHole `tapp` tEmptyHole)
                 )
-                [ branch cA [("p", Nothing), ("a46", Nothing), ("q", Nothing), ("p1", Nothing)] emptyHole
+                [ branch cA [("p", Nothing), ("a44", Nothing), ("q", Nothing), ("p1", Nothing)] emptyHole
                 , branch cB [("r", Nothing), ("x", Nothing)] emptyHole
                 ]
           )
diff --git a/primer/test/Tests/Eval.hs b/primer/test/Tests/Eval.hs
index ad62c8f91..1830c3066 100644
--- a/primer/test/Tests/Eval.hs
+++ b/primer/test/Tests/Eval.hs
@@ -175,7 +175,7 @@ unit_tryReduce_BETA :: Assertion
 unit_tryReduce_BETA = do
   let ((body, lambda, arg, input, expectedResult, k, ty), maxid) =
         create $ do
-          b <- con cNil [tvar "x"] []
+          b <- con cNil []
           l <- lAM "x" (pure b)
           a <- tcon tBool
           let k_ = KFun KType KType
@@ -397,7 +397,7 @@ unit_tryReduce_case_2 = do
   let (expr, i) =
         create $
           case_
-            (con' ["M"] "C" [] [lam "x" (lvar "x"), lvar "y", lvar "z"] `ann` tcon' ["M"] "T")
+            (con' ["M"] "C" [lam "x" (lvar "x"), lvar "y", lvar "z"] `ann` tcon' ["M"] "T")
             [ branch' (["M"], "B") [("b", Nothing)] (con0' ["M"] "D")
             , branch' (["M"], "C") [("c", Nothing), ("d", Nothing), ("e", Nothing)] (con0' ["M"] "E")
             ]
@@ -450,7 +450,7 @@ unit_tryReduce_case_3 = do
   let (expr, i) =
         create $
           case_
-            ( con' ["M"] "C" [tcon' ["M"] "D"] [con0' ["M"] "E"]
+            ( con' ["M"] "C" [con0' ["M"] "E"]
                 `ann` (tcon' ["M"] "T" `tapp` tcon' ["M"] "D")
             )
             [ branch' (["M"], "B") [("b", Nothing)] (con0' ["M"] "D")
@@ -478,10 +478,10 @@ unit_tryReduce_case_3 = do
       detail.targetID @?= 1
       detail.targetCtorID @?= 2
       detail.ctorName @?= vcn ["M"] "C"
-      detail.targetArgIDs @?= [4]
-      detail.branchBindingIDs @?= [10]
-      detail.branchRhsID @?= 11
-      detail.letIDs @?= [17]
+      detail.targetArgIDs @?= [3]
+      detail.branchBindingIDs @?= [9]
+      detail.branchRhsID @?= 10
+      detail.letIDs @?= [16]
     _ -> assertFailure $ show result
 
 unit_tryReduce_case_name_clash :: Assertion
@@ -489,7 +489,7 @@ unit_tryReduce_case_name_clash = do
   let (expr, i) =
         create $
           case_
-            (con' ["M"] "C" [] [emptyHole, lvar "x"] `ann` tcon' ["M"] "T")
+            (con' ["M"] "C" [emptyHole, lvar "x"] `ann` tcon' ["M"] "T")
             [branch' (["M"], "C") [("x", Nothing), ("y", Nothing)] emptyHole]
       tydef =
         Map.singleton (unsafeMkGlobalName (["M"], "T")) $
@@ -502,7 +502,7 @@ unit_tryReduce_case_name_clash = do
       expectedResult =
         create' $
           case_
-            (con' ["M"] "C" [] [emptyHole, lvar "x"] `ann` tcon' ["M"] "T")
+            (con' ["M"] "C" [emptyHole, lvar "x"] `ann` tcon' ["M"] "T")
             [branch' (["M"], "C") [("a9", Nothing), ("y", Nothing)] $ let_ "x" (lvar "a9") emptyHole]
   result <- runTryReduce tydef mempty mempty (expr, i)
   case result of
@@ -1039,7 +1039,7 @@ unit_redexes_lettype_1 =
 
 unit_redexes_lettype_2 :: Assertion
 unit_redexes_lettype_2 =
-  redexesOf (letType "x" (tcon' ["M"] "T") (con' ["M"] "C" [tvar "x"] [])) <@?=> Set.fromList [3]
+  redexesOf (letType "x" (tcon' ["M"] "T") (con0' ["M"] "C" `ann` tvar "x")) <@?=> Set.fromList [4]
 
 unit_redexes_lettype_3 :: Assertion
 unit_redexes_lettype_3 =
diff --git a/primer/test/Tests/EvalFull.hs b/primer/test/Tests/EvalFull.hs
index 9023c95de..5c16f8681 100644
--- a/primer/test/Tests/EvalFull.hs
+++ b/primer/test/Tests/EvalFull.hs
@@ -57,7 +57,6 @@ import Primer.Module (
   builtinModule,
   builtinTypes,
   moduleDefsQualified,
-  moduleTypesQualified,
   primitiveModule,
  )
 import Primer.Primitives (
@@ -119,8 +118,7 @@ import Test.Tasty.HUnit (Assertion, assertBool, assertFailure, (@?=))
 import Tests.Action.Prog (runAppTestM)
 import Tests.Eval.Utils (genDirTm, hasTypeLets, testModules, (~=))
 import Tests.Gen.Core.Typed (checkTest)
-import Tests.Typecheck (expectTypedWithPrims, runTypecheckTestM, runTypecheckTestMWithPrims)
-import Prelude (error)
+import Tests.Typecheck (runTypecheckTestM, runTypecheckTestMWithPrims)
 
 unit_1 :: Assertion
 unit_1 =
@@ -152,9 +150,9 @@ unit_3 =
 unit_4 :: Assertion
 unit_4 =
   let ((expr, expected), maxID) = create $ do
-        e <- let_ "a" (lvar "b") $ con' ["M"] "C" [] [lvar "a", lam "a" (lvar "a"), lam "b" (con' ["M"] "D" [] [lvar "a", lvar "b"])]
+        e <- let_ "a" (lvar "b") $ con' ["M"] "C" [lvar "a", lam "a" (lvar "a"), lam "b" (con' ["M"] "D" [lvar "a", lvar "b"])]
         let b' = "a19" -- NB: fragile name
-        expect <- con' ["M"] "C" [] [lvar "b", lam "a" (lvar "a"), lam b' (con' ["M"] "D" [] [lvar "b", lvar b'])]
+        expect <- con' ["M"] "C" [lvar "b", lam "a" (lvar "a"), lam b' (con' ["M"] "D" [lvar "b", lvar b'])]
         pure (e, expect)
    in do
         s <- evalFullTest maxID mempty mempty 7 Syn expr
@@ -225,10 +223,10 @@ unit_9 =
         (mapName, mapDef) <- Examples.map' modName
         (evenName, evenDef) <- Examples.even modName
         (oddName, oddDef) <- Examples.odd modName
-        let lst = list_ tNat $ take n $ iterate (con1 cSucc) (con0 cZero)
+        let lst = list_ $ take n $ iterate (con1 cSucc) (con0 cZero)
         expr <- gvar mapName `aPP` tcon tNat `aPP` tcon tBool `app` gvar evenName `app` lst
         let globs = [(mapName, mapDef), (evenName, evenDef), (oddName, oddDef)]
-        expect <- list_ tBool (take n $ cycle [con0 cTrue, con0 cFalse]) `ann` (tcon tList `tapp` tcon tBool)
+        expect <- list_ (take n $ cycle [con0 cTrue, con0 cFalse]) `ann` (tcon tList `tapp` tcon tBool)
         pure (globs, expr, expect)
    in do
         evalFullTest maxID builtinTypes (M.fromList globals) 500 Syn e >>= \case
@@ -274,12 +272,12 @@ unit_11 =
         let ty = tcon tNat `tfun` (tcon tPair `tapp` tcon tBool `tapp` tcon tNat)
         let expr1 =
               let_ "x" (con0 cZero) $
-                lam "n" (con cMakePair [tcon tBool, tcon tNat] [gvar evenName `app` lvar "n", lvar "x"])
+                lam "n" (con cMakePair [gvar evenName `app` lvar "n", lvar "x"])
                   `ann` ty
         expr <- expr1 `app` con0 cZero
         let globs = [(evenName, evenDef), (oddName, oddDef)]
         expect <-
-          con cMakePair [tcon tBool, tcon tNat] [con0 cTrue, con0 cZero]
+          con cMakePair [con0 cTrue, con0 cZero]
             `ann` (tcon tPair `tapp` tcon tBool `tapp` tcon tNat)
         pure (globs, expr, expect)
    in do
@@ -313,8 +311,8 @@ unit_12 =
 unit_13 :: Assertion
 unit_13 =
   let ((e, expected), maxID) = create $ do
-        expr <- (lam "x" (con' ["M"] "C" [] [lvar "x", let_ "x" (con0 cTrue) (lvar "x"), lvar "x"]) `ann` (tcon tNat `tfun` tcon tBool)) `app` con0 cZero
-        expect <- con' ["M"] "C" [] [con0 cZero, con0 cTrue, con0 cZero] `ann` tcon tBool
+        expr <- (lam "x" (con' ["M"] "C" [lvar "x", let_ "x" (con0 cTrue) (lvar "x"), lvar "x"]) `ann` (tcon tNat `tfun` tcon tBool)) `app` con0 cZero
+        expect <- con' ["M"] "C" [con0 cZero, con0 cTrue, con0 cZero] `ann` tcon tBool
         pure (expr, expect)
    in do
         s <- evalFullTest maxID builtinTypes mempty 15 Syn e
@@ -343,7 +341,7 @@ unit_15 :: Assertion
 unit_15 =
   let ((expr, steps, expected), maxID) = create $ do
         let l = let_ "x" (lvar "y")
-        let c a b = con' ["M"] "C" [] [lvar a, lvar b]
+        let c a b = con' ["M"] "C" [lvar a, lvar b]
         e0 <- l $ lam "y" $ c "x" "y"
         let y' = "a38"
         e1 <- l $ lam y' $ let_ "y" (lvar y') $ c "x" "y"
@@ -502,15 +500,15 @@ unit_type_preservation_case_regression_tm =
         e <-
           lam "x" $
             case_
-              ( con cMakePair [tcon tNat, tcon tBool] [emptyHole, lvar "x"]
+              ( con cMakePair [emptyHole, lvar "x"]
                   `ann` ((tcon tPair `tapp` tcon tNat) `tapp` tcon tBool)
               )
               [branch cMakePair [("x", Nothing), ("y", Nothing)] emptyHole]
-        let x' = "a50" -- NB fragile name
+        let x' = "a46" -- NB fragile name
         expect1 <-
           lam "x" $
             case_
-              ( con cMakePair [tcon tNat, tcon tBool] [emptyHole, lvar "x"]
+              ( con cMakePair [emptyHole, lvar "x"]
                   `ann` ((tcon tPair `tapp` tcon tNat) `tapp` tcon tBool)
               )
               [branch cMakePair [(x', Nothing), ("y", Nothing)] $ let_ "x" (lvar x') emptyHole]
@@ -540,15 +538,15 @@ unit_type_preservation_case_regression_ty =
         e <-
           lAM "x" $
             case_
-              ( con cMakePair [tEmptyHole, tvar "x"] [emptyHole, emptyHole]
+              ( con cMakePair [emptyHole, emptyHole]
                   `ann` (tcon tPair `tapp` tEmptyHole `tapp` tvar "x")
               )
               [branch cMakePair [("x", Nothing), ("y", Nothing)] emptyHole]
-        let x' = "a50" -- NB fragile name
+        let x' = "a46" -- NB fragile name
         expect1 <-
           lAM "x" $
             case_
-              ( con cMakePair [tEmptyHole, tvar "x"] [emptyHole, emptyHole]
+              ( con cMakePair [emptyHole, emptyHole]
                   `ann` (tcon tPair `tapp` tEmptyHole `tapp` tvar "x")
               )
               [branch cMakePair [(x', Nothing), ("y", Nothing)] $ let_ "x" (lvar x') emptyHole]
@@ -564,43 +562,6 @@ unit_type_preservation_case_regression_ty =
         s2 <- evalFullTest maxID builtinTypes mempty 2 Chk expr
         s2 <~==> Left (TimedOut expected2)
 
--- Consider
---   case Just @? False : Maybe Nat of Just x -> Succ x ; Nothing -> ?
--- In the past we would reduce this to
---   let x = False : Nat in Succ x
--- which is ill-typed (we ignored the hole in the type-application,
--- which acts as a type-changing cast).
--- We simply test that the first "nice" reduction of this expression is well-typed,
--- without mandating what the result should be.
--- Here, "nice" means "without LetType or TLet", since these are
--- currently unsupported in the typechecker.
-unit_type_preservation_case_hole_regression :: Assertion
-unit_type_preservation_case_hole_regression = evalTestM 0 $ do
-  t <-
-    case_
-      (con cJust [tEmptyHole] [con0 cFalse] `ann` (tcon tMaybe `tapp` tcon tNat))
-      [ branch cNothing [] emptyHole
-      , branch cJust [("x", Nothing)] $ con1 cSucc $ lvar "x"
-      ]
-  let tds = foldMap' moduleTypesQualified $ create' $ sequence testModules
-  let globs = foldMap' moduleDefsQualified $ create' $ sequence testModules
-  let reducts = (\n -> runPureLogT $ evalFullStepCount tds globs n Syn t) <$> [1 ..]
-  let go = \case
-        [] -> error "impossible, reducts is an infinite list"
-        (x : xs) -> do
-          x'@((_, s), _) <- x
-          if any hasTypeLets $ s ^.. evalResultExpr
-            then go xs
-            else pure x'
-  ((_steps, s), logs) <- go reducts
-  let s' = case s of
-        Left (TimedOut e) -> e
-        Right e -> e
-  pure $ do
-    expectTypedWithPrims $ pure t `ann` tEmptyHole
-    assertNoSevereLogs @EvalLog logs
-    expectTypedWithPrims $ pure s' `ann` tEmptyHole
-
 -- Previously EvalFull reducing a BETA expression could result in variable
 -- capture. We would reduce (Λa.t : ∀b.T) S to
 -- let b = S in (let a = S in t) : T
@@ -913,7 +874,7 @@ tasty_prim_hex_nat = withTests 20 . property $ do
                   [ branch
                       cNothing
                       []
-                      (con cNothing [tcon tChar] [])
+                      (con cNothing [])
                   , branch
                       cJust
                       [("x", Nothing)]
@@ -921,13 +882,13 @@ tasty_prim_hex_nat = withTests 20 . property $ do
                           `app` lvar "x"
                       )
                   ]
-                <*> con cJust [tcon tNat] [ne]
+                <*> con cJust [ne]
                 `ann` (tcon tMaybe `tapp` tcon tNat)
             else
               (,)
                 <$> pfun NatToHex
                 `app` ne
-                <*> con cNothing [tcon tChar] []
+                <*> con cNothing []
                 `ann` (tcon tMaybe `tapp` tcon tChar)
   s <- evalFullTasty maxID builtinTypes primDefs 7 Syn e
   over evalResultExpr zeroIDs s === Right (zeroIDs r)
@@ -1006,7 +967,7 @@ unit_prim_int_quotient =
     IntQuotient
     (int 7)
     (int 3)
-    (con cJust [tcon tInt] [int 2] `ann` (tcon tMaybe `tapp` tcon tInt))
+    (con cJust [int 2] `ann` (tcon tMaybe `tapp` tcon tInt))
 
 unit_prim_int_quotient_negative :: Assertion
 unit_prim_int_quotient_negative =
@@ -1014,7 +975,7 @@ unit_prim_int_quotient_negative =
     IntQuotient
     (int (-7))
     (int 3)
-    (con cJust [tcon tInt] [int (-3)] `ann` (tcon tMaybe `tapp` tcon tInt))
+    (con cJust [int (-3)] `ann` (tcon tMaybe `tapp` tcon tInt))
 
 unit_prim_int_quotient_zero :: Assertion
 unit_prim_int_quotient_zero =
@@ -1022,7 +983,7 @@ unit_prim_int_quotient_zero =
     IntQuotient
     (int (-7))
     (int 0)
-    (con cNothing [tcon tInt] [] `ann` (tcon tMaybe `tapp` tcon tInt))
+    (con cNothing [] `ann` (tcon tMaybe `tapp` tcon tInt))
 
 unit_prim_int_remainder :: Assertion
 unit_prim_int_remainder =
@@ -1030,7 +991,7 @@ unit_prim_int_remainder =
     IntRemainder
     (int 7)
     (int 3)
-    (con cJust [tcon tInt] [int 1] `ann` (tcon tMaybe `tapp` tcon tInt))
+    (con cJust [int 1] `ann` (tcon tMaybe `tapp` tcon tInt))
 
 unit_prim_int_remainder_negative_1 :: Assertion
 unit_prim_int_remainder_negative_1 =
@@ -1038,7 +999,7 @@ unit_prim_int_remainder_negative_1 =
     IntRemainder
     (int (-7))
     (int (-3))
-    (con cJust [tcon tInt] [int (-1)] `ann` (tcon tMaybe `tapp` tcon tInt))
+    (con cJust [int (-1)] `ann` (tcon tMaybe `tapp` tcon tInt))
 
 unit_prim_int_remainder_negative_2 :: Assertion
 unit_prim_int_remainder_negative_2 =
@@ -1046,7 +1007,7 @@ unit_prim_int_remainder_negative_2 =
     IntRemainder
     (int (-7))
     (int 3)
-    (con cJust [tcon tInt] [int 2] `ann` (tcon tMaybe `tapp` tcon tInt))
+    (con cJust [int 2] `ann` (tcon tMaybe `tapp` tcon tInt))
 
 unit_prim_int_remainder_negative_3 :: Assertion
 unit_prim_int_remainder_negative_3 =
@@ -1054,7 +1015,7 @@ unit_prim_int_remainder_negative_3 =
     IntRemainder
     (int 7)
     (int (-3))
-    (con cJust [tcon tInt] [int (-2)] `ann` (tcon tMaybe `tapp` tcon tInt))
+    (con cJust [int (-2)] `ann` (tcon tMaybe `tapp` tcon tInt))
 
 unit_prim_int_remainder_zero :: Assertion
 unit_prim_int_remainder_zero =
@@ -1062,7 +1023,7 @@ unit_prim_int_remainder_zero =
     IntRemainder
     (int 7)
     (int 0)
-    (con cNothing [tcon tInt] [] `ann` (tcon tMaybe `tapp` tcon tInt))
+    (con cNothing [] `ann` (tcon tMaybe `tapp` tcon tInt))
 
 unit_prim_int_quot :: Assertion
 unit_prim_int_quot =
@@ -1245,14 +1206,14 @@ unit_prim_int_toNat =
   unaryPrimTest
     IntToNat
     (int 0)
-    (con cJust [tcon tNat] [nat 0] `ann` (tcon tMaybe `tapp` tcon tNat))
+    (con cJust [nat 0] `ann` (tcon tMaybe `tapp` tcon tNat))
 
 unit_prim_int_toNat_negative :: Assertion
 unit_prim_int_toNat_negative =
   unaryPrimTest
     IntToNat
     (int (-1))
-    (con cNothing [tcon tNat] [] `ann` (tcon tMaybe `tapp` tcon tNat))
+    (con cNothing [] `ann` (tcon tMaybe `tapp` tcon tNat))
 
 unit_prim_int_fromNat :: Assertion
 unit_prim_int_fromNat =
@@ -1287,13 +1248,11 @@ unit_prim_partial_map =
             `aPP` tcon tChar
             `app` pfun ToUpper
             `app` list_
-              tChar
               [ char 'a'
               , char 'b'
               , char 'c'
               ]
             <*> list_
-              tChar
               [ char 'A'
               , char 'B'
               , char 'C'
diff --git a/primer/test/Tests/Prelude/Integer.hs b/primer/test/Tests/Prelude/Integer.hs
index 6a5808319..bdffa9c0d 100644
--- a/primer/test/Tests/Prelude/Integer.hs
+++ b/primer/test/Tests/Prelude/Integer.hs
@@ -14,9 +14,6 @@ import Primer.Core.DSL (
   int,
  )
 import Primer.Prelude.Integer qualified as P
-import Primer.Primitives (
-  tInt,
- )
 import Tasty (Property, property, withTests)
 import Tests.Prelude.Utils (functionOutput, (<===>))
 
@@ -69,9 +66,9 @@ tasty_odd_prop = property $ do
 tasty_sum_prop :: Property
 tasty_sum_prop = property $ do
   ns <- forAll $ G.list (Range.linear 0 10) (G.integral_ (Range.constant (-10) 10))
-  functionOutput P.sum [list_ tInt $ map int ns] 2000 <===> Right (create' $ int $ sum ns)
+  functionOutput P.sum [list_ $ map int ns] 2000 <===> Right (create' $ int $ sum ns)
 
 tasty_product_prop :: Property
 tasty_product_prop = property $ do
   ns <- forAll $ G.list (Range.linear 0 10) (G.integral_ (Range.constant 1 10))
-  functionOutput P.product [list_ tInt $ map int ns] 2000 <===> Right (create' $ int $ product ns)
+  functionOutput P.product [list_ $ map int ns] 2000 <===> Right (create' $ int $ product ns)
diff --git a/primer/test/Tests/Prelude/Polymorphism.hs b/primer/test/Tests/Prelude/Polymorphism.hs
index 9148f55e7..bf444e1c1 100644
--- a/primer/test/Tests/Prelude/Polymorphism.hs
+++ b/primer/test/Tests/Prelude/Polymorphism.hs
@@ -49,7 +49,7 @@ tasty_id_prop = property $ do
   ns <- forAll $ G.list (Range.constant 0 10) (G.integral_ (Range.constant (-10) 10))
   functionOutput' P.id [Right $ tcon tInt, Left $ int n] 20 <===> Right (create' $ int n) -- Integer Test
   functionOutput' P.id [Right $ tcon tBool, Left $ bool_ b] 20 <===> Right (create' $ bool_ b) -- Bool Test
-  functionOutput' P.id [Right $ tcon tList `tapp` tcon tInt, Left $ list_ tInt $ map int ns] 20 <===> Right (create' $ list_ tInt $ map int ns) -- List of Int Test
+  functionOutput' P.id [Right $ tcon tList `tapp` tcon tInt, Left $ list_ $ map int ns] 20 <===> Right (create' $ list_ $ map int ns) -- List of Int Test
 
 tasty_const_prop :: Property
 tasty_const_prop = property $ do
@@ -77,12 +77,12 @@ tasty_const_prop = property $ do
   functionOutput' -- List of Int Test
     P.const
     [ Right $ tcon tList `tapp` tcon tInt
-    , Left $ list_ tInt $ map int ns
+    , Left $ list_ $ map int ns
     , Right $ tcon tInt
     , Left $ int n
     ]
     20
-    <===> Right (create' $ list_ tInt $ map int ns)
+    <===> Right (create' $ list_ $ map int ns)
 
 tasty_map_prop :: Property
 tasty_map_prop = property $ do
@@ -91,26 +91,26 @@ tasty_map_prop = property $ do
   let addOne = lam "x" $ apps (pfun IntAdd) [lvar "x", int 1]
    in functionOutput' -- Mapping over integers (+1)
         P.map
-        [Right $ tcon tInt, Right $ tcon tInt, Left addOne, Left $ list_ tInt $ map int ns]
+        [Right $ tcon tInt, Right $ tcon tInt, Left addOne, Left $ list_ $ map int ns]
         1000
-        <===> Right (create' $ list_ tInt $ map (int . (+ 1)) ns)
+        <===> Right (create' $ list_ $ map (int . (+ 1)) ns)
   functionOutput' -- Mapping over bools (not)
     P.map
-    [Right $ tcon tBool, Right $ tcon tBool, Left (gvar L.not), Left $ list_ tBool $ map bool_ bs]
+    [Right $ tcon tBool, Right $ tcon tBool, Left (gvar L.not), Left $ list_ $ map bool_ bs]
     1000
-    <===> Right (create' $ list_ tBool $ map (bool_ . not) bs)
+    <===> Right (create' $ list_ $ map (bool_ . not) bs)
 
 -- Right fold over a list of characters with @cons@.
 tasty_foldr_list_char :: Property
 tasty_foldr_list_char = property $ do
   as <- forAll $ G.list (Range.linear 0 10) G.unicode
   as' <- forAll $ G.list (Range.linear 0 10) G.unicode
-  let cons = lam "x" $ lam "xs" $ con cCons [tcon tChar] [lvar "x", lvar "xs"]
+  let cons = lam "x" $ lam "xs" $ con cCons [lvar "x", lvar "xs"]
    in functionOutput'
         P.foldr
-        [Right $ listOf (tcon tChar), Right $ listOf (tcon tChar), Left cons, Left $ list_ tChar $ map char as, Left $ list_ tChar $ map char as']
+        [Right $ listOf (tcon tChar), Right $ listOf (tcon tChar), Left cons, Left $ list_ $ map char as, Left $ list_ $ map char as']
         1000
-        <===> Right (create' $ list_ tChar $ map char (foldr (:) as as'))
+        <===> Right (create' $ list_ $ map char (foldr (:) as as'))
 
 {- HLINT ignore tasty_foldr_bool "Use and" -}
 -- Right fold over a list of bools with logical @and@.
@@ -119,7 +119,7 @@ tasty_foldr_bool = property $ do
   bs <- forAll $ G.list (Range.linear 0 10) G.bool_
   functionOutput'
     P.foldr
-    [Right $ tcon tBool, Right $ tcon tBool, Left (gvar L.and), Left $ bool_ True, Left $ list_ tBool $ map bool_ bs]
+    [Right $ tcon tBool, Right $ tcon tBool, Left (gvar L.and), Left $ bool_ True, Left $ list_ $ map bool_ bs]
     1000
     <===> Right (create' $ bool_ (foldr (&&) True bs))
 
@@ -130,7 +130,7 @@ tasty_foldr_right_assoc = property $ do
   let subtract' = lam "x" $ lam "y" $ apps (pfun IntMinus) [lvar "x", lvar "y"]
   functionOutput'
     P.foldr
-    [Right $ tcon tInt, Right $ tcon tInt, Left subtract', Left $ int 0, Left $ list_ tInt $ map int ns]
+    [Right $ tcon tInt, Right $ tcon tInt, Left subtract', Left $ int 0, Left $ list_ $ map int ns]
     1000
     <===> Right (create' $ int (foldr (-) 0 ns))
 
@@ -142,6 +142,6 @@ unit_foldr_short_circuit =
    in do
         functionOutput'
           P.foldr
-          [Right $ tcon tBool, Right $ tcon tBool, Left (gvar L.and), Left $ bool_ True, Left $ list_ tBool $ map bool_ bs]
+          [Right $ tcon tBool, Right $ tcon tBool, Left (gvar L.and), Left $ bool_ True, Left $ list_ $ map bool_ bs]
           100
           <~==> Right (create' $ bool_ False)
diff --git a/primer/test/Tests/Questions.hs b/primer/test/Tests/Questions.hs
index 14cc81290..ef18fc2a2 100644
--- a/primer/test/Tests/Questions.hs
+++ b/primer/test/Tests/Questions.hs
@@ -228,7 +228,7 @@ unit_variablesInScope_type = do
 unit_variablesInScope_shadowed :: Assertion
 unit_variablesInScope_shadowed = do
   let ty = tforall "a" (KFun KType KType) $ tforall "b" KType $ tcon tNat `tfun` tforall "a" KType (tcon tBool `tfun` (tcon tList `tapp` tvar "b"))
-      expr' = lAM "c" $ lAM "d" $ lam "c" $ lAM "c" $ lam "c" $ con cNil [tvar "d"] []
+      expr' = lAM "c" $ lAM "d" $ lam "c" $ lAM "c" $ lam "c" $ emptyHole `ann` (tcon tList `tapp` tvar "d")
       expr = ann expr' ty
   hasVariablesType ty pure []
   hasVariablesType ty down [("a", KFun KType KType)]
diff --git a/primer/test/Tests/Transform.hs b/primer/test/Tests/Transform.hs
index a12d9ed81..43b6140a1 100644
--- a/primer/test/Tests/Transform.hs
+++ b/primer/test/Tests/Transform.hs
@@ -6,7 +6,7 @@ import Primer.Builtins
 import Primer.Core
 import Primer.Core.DSL
 import Primer.Core.Transform
-import Primer.Test.Util (clearMeta, clearTypeMeta, tcn, vcn)
+import Primer.Test.Util (clearMeta, clearTypeMeta, vcn)
 import Test.Tasty.HUnit (Assertion, assertFailure, (@?=))
 
 -- When renaming we have to be careful of binding sites. If we're renaming x to
@@ -178,7 +178,7 @@ unit_app :: Assertion
 unit_app = afterRename "x" "y" (app (lvar "x") (lvar "x")) (Just (app (lvar "y") (lvar "y")))
 
 unit_con :: Assertion
-unit_con = afterRename "x" "y" (con cJust [tcon tBool] [lvar "x"]) (Just (con cJust [tcon tBool] [lvar "y"]))
+unit_con = afterRename "x" "y" (con cJust [lvar "x"]) (Just (con cJust [lvar "y"]))
 
 unit_case :: Assertion
 unit_case =
@@ -301,6 +301,6 @@ unit_unfoldApp_1 =
 unit_unfoldApp_2 :: Assertion
 unit_unfoldApp_2 =
   let expr :: Expr' () ()
-      expr = Con () (vcn ["M"] "C") [TCon () $ tcn ["M"] "T"] [v "x", v "y"]
+      expr = Con () (vcn ["M"] "C") [v "x", v "y"]
       v = Var () . LocalVarRef
    in unfoldApp expr @?= (expr, [])
diff --git a/primer/test/Tests/Typecheck.hs b/primer/test/Tests/Typecheck.hs
index bf1dd7007..e7f8352b3 100644
--- a/primer/test/Tests/Typecheck.hs
+++ b/primer/test/Tests/Typecheck.hs
@@ -34,7 +34,6 @@ import Primer.Builtins (
   boolDef,
   cCons,
   cFalse,
-  cJust,
   cMakePair,
   cNil,
   cSucc,
@@ -160,42 +159,42 @@ unit_true_hole = expectTyped $ con0 cTrue `ann` tEmptyHole
 -- An empty hole rejects under-saturated constructors
 unit_unsat_con_hole_1 :: Assertion
 unit_unsat_con_hole_1 =
-  (con cSucc [] [] `ann` tEmptyHole)
+  (con cSucc [] `ann` tEmptyHole)
     `expectFailsWith` \_ -> UnsaturatedConstructor cSucc
 
 -- An empty hole rejects over-saturated constructors
 unit_unsat_con_hole_2 :: Assertion
 unit_unsat_con_hole_2 =
-  (con cSucc [] [emptyHole, emptyHole] `ann` tEmptyHole)
+  (con cSucc [emptyHole, emptyHole] `ann` tEmptyHole)
     `expectFailsWith` \_ -> UnsaturatedConstructor cSucc
 
 -- A hole-headed TApp accepts saturated constructors
 unit_con_hole_app_type_1 :: Assertion
 unit_con_hole_app_type_1 =
   expectTyped $
-    con cMakePair [tcon tBool, tcon tNat] [emptyHole, emptyHole]
+    con cMakePair [emptyHole, emptyHole]
       `ann` (tEmptyHole `tapp` tEmptyHole)
 
--- A hole-headed TApp accepts saturated constructors, if given type arguments match
+-- A hole-headed TApp accepts saturated constructors
 -- The application spine can be shorter than that required for the constructor
 unit_con_hole_app_type_2 :: Assertion
 unit_con_hole_app_type_2 =
   expectTyped $
-    con cMakePair [tcon tBool, tcon tNat] [emptyHole, emptyHole]
+    con cMakePair [emptyHole, emptyHole]
       `ann` (tEmptyHole `tapp` tcon tNat)
 
--- A hole-headed TApp accepts saturated constructors, if given type arguments match
+-- A hole-headed TApp accepts saturated constructors
 -- The application spine can match than that required for the constructor
 unit_con_hole_app_type_3 :: Assertion
 unit_con_hole_app_type_3 =
   expectTyped $
-    con cMakePair [tcon tBool, tcon tNat] [emptyHole, emptyHole]
+    con cMakePair [emptyHole, emptyHole]
       `ann` (tEmptyHole `tapp` tcon tBool `tapp` tcon tNat)
 
 -- A hole-headed TApp rejects saturated constructors, if  application spine is too long for the constructor
 unit_con_hole_app_type_4 :: Assertion
 unit_con_hole_app_type_4 =
-  ( con cMakePair [tcon tBool, tcon tNat] [emptyHole, emptyHole]
+  ( con cMakePair [emptyHole, emptyHole]
       `ann` (tEmptyHole `tapp` tcon tBool `tapp` tcon tNat `tapp` tEmptyHole)
   )
     `expectFailsWith` const
@@ -204,28 +203,6 @@ unit_con_hole_app_type_4 =
           cMakePair
       )
 
--- A hole-headed TApp rejects saturated constructors, if given type arguments do not match
-unit_con_hole_app_type_5 :: Assertion
-unit_con_hole_app_type_5 =
-  ( con cMakePair [tcon tBool, tcon tNat] [emptyHole, emptyHole]
-      `ann` (tEmptyHole `tapp` tcon tBool)
-  )
-    `expectFailsWith` const ConstructorTypeArgsInconsistentTypes
-
--- Constructors' type arguments need only be consistent with the type we check against.
--- This is a regression test: during development we messed up what type
--- smartholes would check the term argument against (it elided the hole on the
--- type, but only for the purposes of checking the term). Thus @smartSynthGives@
--- actually gave
---    ann (con cJust [thole (tEmptyHole `tfun` tEmptyHole)] [hole $ con0 cTrue `ann` tEmptyHole])
-unit_con_tyargs_consistent_sh :: Assertion
-unit_con_tyargs_consistent_sh =
-  let tm = con cJust [thole (tEmptyHole `tfun` tEmptyHole)] [con0 cTrue]
-      ty = tcon tMaybe `tapp` tcon tBool
-   in do
-        expectTyped $ ann tm ty
-        ann tm ty `smartSynthGives` ann tm ty
-
 unit_constructor_doesn't_exist :: Assertion
 unit_constructor_doesn't_exist =
   (con0 nope `ann` tEmptyHole) `expectFailsWith` const (UnknownConstructor nope)
@@ -236,7 +213,7 @@ unit_inc :: Assertion
 unit_inc =
   expectTyped $
     ann
-      (lam "n" (con cSucc [] [lvar "n"]))
+      (lam "n" (con cSucc [lvar "n"]))
       (tfun (tcon tNat) (tcon tNat))
 
 -- NB: @Succ :: ?@ is wrong: unsaturated!
diff --git a/primer/test/Tests/Utils.hs b/primer/test/Tests/Utils.hs
index 4e5b00c4d..38298d4c0 100644
--- a/primer/test/Tests/Utils.hs
+++ b/primer/test/Tests/Utils.hs
@@ -29,7 +29,7 @@ genAST example = fst $ create $ example <&> snd
 -- particular next 'ID', only that 'nextID' returns whatever
 -- 'Examples.map''s next 'ID' happens to be.
 unit_nextID_exampleMap :: Assertion
-unit_nextID_exampleMap = nextID (genAST $ Examples.map modName) @?= ID 37
+unit_nextID_exampleMap = nextID (genAST $ Examples.map modName) @?= ID 35
 
 -- See note for 'unit_nextID_exampleMap'.
 unit_nextID_exampleEven :: Assertion
@@ -41,4 +41,4 @@ unit_nextID_exampleOdd = nextID (genAST $ Examples.odd modName) @?= ID 11
 
 -- See note for 'unit_nextID_exampleMap'.
 unit_nextID_exampleComprehensive :: Assertion
-unit_nextID_exampleComprehensive = nextID (genAST $ Examples.comprehensive modName) @?= ID 56
+unit_nextID_exampleComprehensive = nextID (genAST $ Examples.comprehensive modName) @?= ID 52
diff --git a/primer/test/outputs/APITree/Expr b/primer/test/outputs/APITree/Expr
index d424d2f0a..70de6336b 100644
--- a/primer/test/outputs/APITree/Expr
+++ b/primer/test/outputs/APITree/Expr
@@ -92,12 +92,6 @@ Tree
                                             , childTrees =
                                                 [ Tree
                                                     { nodeId = "18"
-                                                    , body = NoBody TEmptyHole
-                                                    , childTrees = []
-                                                    , rightChild = Nothing
-                                                    }
-                                                , Tree
-                                                    { nodeId = "19"
                                                     , body = NoBody EmptyHole
                                                     , childTrees = []
                                                     , rightChild = Nothing
@@ -106,11 +100,11 @@ Tree
                                             , rightChild = Nothing
                                             }
                                         , Tree
-                                            { nodeId = "20"
+                                            { nodeId = "19"
                                             , body = NoBody TApp
                                             , childTrees =
                                                 [ Tree
-                                                    { nodeId = "21"
+                                                    { nodeId = "20"
                                                     , body = TextBody
                                                         ( RecordPair
                                                             { fst = TCon
@@ -127,7 +121,7 @@ Tree
                                                     , rightChild = Nothing
                                                     }
                                                 , Tree
-                                                    { nodeId = "22"
+                                                    { nodeId = "21"
                                                     , body = NoBody TEmptyHole
                                                     , childTrees = []
                                                     , rightChild = Nothing
@@ -142,11 +136,11 @@ Tree
                             , rightChild = Nothing
                             }
                         , Tree
-                            { nodeId = "23"
+                            { nodeId = "22"
                             , body = NoBody Hole
                             , childTrees =
                                 [ Tree
-                                    { nodeId = "24"
+                                    { nodeId = "23"
                                     , body = TextBody
                                         ( RecordPair
                                             { fst = GlobalVar
@@ -169,11 +163,11 @@ Tree
                     , rightChild = Nothing
                     }
                 , Tree
-                    { nodeId = "25"
+                    { nodeId = "24"
                     , body = NoBody THole
                     , childTrees =
                         [ Tree
-                            { nodeId = "26"
+                            { nodeId = "25"
                             , body = TextBody
                                 ( RecordPair
                                     { fst = TCon
@@ -193,11 +187,11 @@ Tree
                     , rightChild = Nothing
                     }
                 , Tree
-                    { nodeId = "27"
+                    { nodeId = "26"
                     , body = NoBody Ann
                     , childTrees =
                         [ Tree
-                            { nodeId = "28"
+                            { nodeId = "27"
                             , body = TextBody
                                 ( RecordPair
                                     { fst = Lam
@@ -209,7 +203,7 @@ Tree
                                 )
                             , childTrees =
                                 [ Tree
-                                    { nodeId = "29"
+                                    { nodeId = "28"
                                     , body = TextBody
                                         ( RecordPair
                                             { fst = LAM
@@ -221,15 +215,15 @@ Tree
                                         )
                                     , childTrees =
                                         [ Tree
-                                            { nodeId = "30"
+                                            { nodeId = "29"
                                             , body = NoBody App
                                             , childTrees =
                                                 [ Tree
-                                                    { nodeId = "31"
+                                                    { nodeId = "30"
                                                     , body = NoBody APP
                                                     , childTrees =
                                                         [ Tree
-                                                            { nodeId = "32"
+                                                            { nodeId = "31"
                                                             , body = TextBody
                                                                 ( RecordPair
                                                                     { fst = LetType
@@ -241,7 +235,7 @@ Tree
                                                                 )
                                                             , childTrees =
                                                                 [ Tree
-                                                                    { nodeId = "34"
+                                                                    { nodeId = "33"
                                                                     , body = TextBody
                                                                         ( RecordPair
                                                                             { fst = Con
@@ -254,55 +248,11 @@ Tree
                                                                                 }
                                                                             }
                                                                         )
-                                                                    , childTrees =
-                                                                        [ Tree
-                                                                            { nodeId = "35"
-                                                                            , body = TextBody
-                                                                                ( RecordPair
-                                                                                    { fst = TLet
-                                                                                    , snd = Name
-                                                                                        { qualifiedModule = Nothing
-                                                                                        , baseName = "c"
-                                                                                        }
-                                                                                    }
-                                                                                )
-                                                                            , childTrees =
-                                                                                [ Tree
-                                                                                    { nodeId = "36"
-                                                                                    , body = TextBody
-                                                                                        ( RecordPair
-                                                                                            { fst = TVar
-                                                                                            , snd = Name
-                                                                                                { qualifiedModule = Nothing
-                                                                                                , baseName = "b"
-                                                                                                }
-                                                                                            }
-                                                                                        )
-                                                                                    , childTrees = []
-                                                                                    , rightChild = Nothing
-                                                                                    }
-                                                                                , Tree
-                                                                                    { nodeId = "37"
-                                                                                    , body = TextBody
-                                                                                        ( RecordPair
-                                                                                            { fst = TVar
-                                                                                            , snd = Name
-                                                                                                { qualifiedModule = Nothing
-                                                                                                , baseName = "c"
-                                                                                                }
-                                                                                            }
-                                                                                        )
-                                                                                    , childTrees = []
-                                                                                    , rightChild = Nothing
-                                                                                    }
-                                                                                ]
-                                                                            , rightChild = Nothing
-                                                                            }
-                                                                        ]
+                                                                    , childTrees = []
                                                                     , rightChild = Nothing
                                                                     }
                                                                 , Tree
-                                                                    { nodeId = "33"
+                                                                    { nodeId = "32"
                                                                     , body = TextBody
                                                                         ( RecordPair
                                                                             { fst = TCon
@@ -322,7 +272,7 @@ Tree
                                                             , rightChild = Nothing
                                                             }
                                                         , Tree
-                                                            { nodeId = "38"
+                                                            { nodeId = "34"
                                                             , body = TextBody
                                                                 ( RecordPair
                                                                     { fst = TVar
@@ -339,11 +289,11 @@ Tree
                                                     , rightChild = Nothing
                                                     }
                                                 , Tree
-                                                    { nodeId = "39"
+                                                    { nodeId = "35"
                                                     , body = NoBody Case
                                                     , childTrees =
                                                         [ Tree
-                                                            { nodeId = "40"
+                                                            { nodeId = "36"
                                                             , body = TextBody
                                                                 ( RecordPair
                                                                     { fst = LocalVar
@@ -359,12 +309,12 @@ Tree
                                                         ]
                                                     , rightChild = Just
                                                         ( Tree
-                                                            { nodeId = "39P0"
+                                                            { nodeId = "35P0"
                                                             , body = BoxBody
                                                                 ( RecordPair
                                                                     { fst = Pattern
                                                                     , snd = Tree
-                                                                        { nodeId = "39P0B"
+                                                                        { nodeId = "35P0B"
                                                                         , body = TextBody
                                                                             ( RecordPair
                                                                                 { fst = PatternCon
@@ -384,7 +334,7 @@ Tree
                                                                 )
                                                             , childTrees =
                                                                 [ Tree
-                                                                    { nodeId = "41"
+                                                                    { nodeId = "37"
                                                                     , body = TextBody
                                                                         ( RecordPair
                                                                             { fst = Con
@@ -403,12 +353,12 @@ Tree
                                                                 ]
                                                             , rightChild = Just
                                                                 ( Tree
-                                                                    { nodeId = "39P1"
+                                                                    { nodeId = "35P1"
                                                                     , body = BoxBody
                                                                         ( RecordPair
                                                                             { fst = Pattern
                                                                             , snd = Tree
-                                                                                { nodeId = "39P1B"
+                                                                                { nodeId = "35P1B"
                                                                                 , body = TextBody
                                                                                     ( RecordPair
                                                                                         { fst = PatternCon
@@ -423,7 +373,7 @@ Tree
                                                                                     )
                                                                                 , childTrees =
                                                                                     [ Tree
-                                                                                        { nodeId = "42"
+                                                                                        { nodeId = "38"
                                                                                         , body = TextBody
                                                                                             ( RecordPair
                                                                                                 { fst = PatternBind
@@ -443,21 +393,21 @@ Tree
                                                                         )
                                                                     , childTrees =
                                                                         [ Tree
-                                                                            { nodeId = "43"
+                                                                            { nodeId = "39"
                                                                             , body = NoBody App
                                                                             , childTrees =
                                                                                 [ Tree
-                                                                                    { nodeId = "44"
+                                                                                    { nodeId = "40"
                                                                                     , body = NoBody App
                                                                                     , childTrees =
                                                                                         [ Tree
-                                                                                            { nodeId = "45"
+                                                                                            { nodeId = "41"
                                                                                             , body = NoBody EmptyHole
                                                                                             , childTrees = []
                                                                                             , rightChild = Nothing
                                                                                             }
                                                                                         , Tree
-                                                                                            { nodeId = "46"
+                                                                                            { nodeId = "42"
                                                                                             , body = TextBody
                                                                                                 ( RecordPair
                                                                                                     { fst = LocalVar
@@ -474,7 +424,7 @@ Tree
                                                                                     , rightChild = Nothing
                                                                                     }
                                                                                 , Tree
-                                                                                    { nodeId = "47"
+                                                                                    { nodeId = "43"
                                                                                     , body = TextBody
                                                                                         ( RecordPair
                                                                                             { fst = LocalVar
@@ -507,11 +457,11 @@ Tree
                             , rightChild = Nothing
                             }
                         , Tree
-                            { nodeId = "48"
+                            { nodeId = "44"
                             , body = NoBody TFun
                             , childTrees =
                                 [ Tree
-                                    { nodeId = "49"
+                                    { nodeId = "45"
                                     , body = TextBody
                                         ( RecordPair
                                             { fst = TCon
@@ -528,7 +478,7 @@ Tree
                                     , rightChild = Nothing
                                     }
                                 , Tree
-                                    { nodeId = "50"
+                                    { nodeId = "46"
                                     , body = TextBody
                                         ( RecordPair
                                             { fst = TForall
@@ -540,15 +490,15 @@ Tree
                                         )
                                     , childTrees =
                                         [ Tree
-                                            { nodeId = "51"
+                                            { nodeId = "47"
                                             , body = NoBody TApp
                                             , childTrees =
                                                 [ Tree
-                                                    { nodeId = "52"
+                                                    { nodeId = "48"
                                                     , body = NoBody TApp
                                                     , childTrees =
                                                         [ Tree
-                                                            { nodeId = "53"
+                                                            { nodeId = "49"
                                                             , body = TextBody
                                                                 ( RecordPair
                                                                     { fst = TCon
@@ -565,7 +515,7 @@ Tree
                                                             , rightChild = Nothing
                                                             }
                                                         , Tree
-                                                            { nodeId = "54"
+                                                            { nodeId = "50"
                                                             , body = TextBody
                                                                 ( RecordPair
                                                                     { fst = TCon
@@ -585,7 +535,7 @@ Tree
                                                     , rightChild = Nothing
                                                     }
                                                 , Tree
-                                                    { nodeId = "55"
+                                                    { nodeId = "51"
                                                     , body = TextBody
                                                         ( RecordPair
                                                             { fst = TVar
diff --git a/primer/test/outputs/Pretty/comprehensive/Expr (Compact).ansi b/primer/test/outputs/Pretty/comprehensive/Expr (Compact).ansi
index 19a9a81e4..fef8c912a 100644
--- a/primer/test/outputs/Pretty/comprehensive/Expr (Compact).ansi	
+++ b/primer/test/outputs/Pretty/comprehensive/Expr (Compact).ansi	
@@ -2,7 +2,7 @@
   let rec y =
     (
       (
-        {?(Just @? (?)) :: ((Maybe) (?))?}
+        {?(Just (?)) :: ((Maybe) (?))?}
       )
       (
         {?unboundName?}
@@ -18,8 +18,7 @@
           (
             (
               let type b = Bool in
-                Left @let c = b in
-                  c
+                Left
             ) @β
           )
           (
diff --git a/primer/test/outputs/Pretty/comprehensive/Expr (Sparse).ansi b/primer/test/outputs/Pretty/comprehensive/Expr (Sparse).ansi
index fe0d24a92..23b6fa5ab 100644
--- a/primer/test/outputs/Pretty/comprehensive/Expr (Sparse).ansi	
+++ b/primer/test/outputs/Pretty/comprehensive/Expr (Sparse).ansi	
@@ -11,7 +11,7 @@
       (
         {?
           (
-            Just @?
+            Just
             (
               ?
             )
@@ -46,10 +46,7 @@
               let type b =
                 Bool
               in
-                Left @let c =
-                  b
-                in
-                  c
+                Left
             ) @β
           )
           (
diff --git a/primer/test/outputs/available-actions/M.comprehensive/Beginner-Editable.fragment b/primer/test/outputs/available-actions/M.comprehensive/Beginner-Editable.fragment
index fdde553b0..820c8f5b3 100644
--- a/primer/test/outputs/available-actions/M.comprehensive/Beginner-Editable.fragment
+++ b/primer/test/outputs/available-actions/M.comprehensive/Beginner-Editable.fragment
@@ -269,7 +269,7 @@ Output
                 ]
             )
         ,
-            ( 19
+            ( 18
             ,
                 [ Input MakeLam
                     ( Options
@@ -344,7 +344,7 @@ Output
                 ]
             )
         ,
-            ( 23
+            ( 22
             ,
                 [ Input MakeLam
                     ( Options
@@ -419,7 +419,7 @@ Output
                 ]
             )
         ,
-            ( 26
+            ( 25
             ,
                 [ Input MakeLam
                     ( Options
@@ -449,7 +449,7 @@ Output
                 ]
             )
         ,
-            ( 27
+            ( 26
             ,
                 [ Input MakeLam
                     ( Options
@@ -502,7 +502,7 @@ Output
                 ]
             )
         ,
-            ( 28
+            ( 27
             ,
                 [ Input MakeLam
                     ( Options
@@ -528,7 +528,7 @@ Output
                 ]
             )
         ,
-            ( 29
+            ( 28
             ,
                 [ Input MakeLam
                     ( Options
@@ -555,7 +555,7 @@ Output
                 ]
             )
         ,
-            ( 30
+            ( 29
             ,
                 [ Input MakeLam
                     ( Options
@@ -581,7 +581,7 @@ Output
                 ]
             )
         ,
-            ( 31
+            ( 30
             ,
                 [ Input MakeLam
                     ( Options
@@ -607,7 +607,7 @@ Output
                 ]
             )
         ,
-            ( 32
+            ( 31
             ,
                 [ Input MakeLam
                     ( Options
@@ -633,7 +633,7 @@ Output
                 ]
             )
         ,
-            ( 33
+            ( 32
             ,
                 [ Input MakeLam
                     ( Options
@@ -670,7 +670,7 @@ Output
                 ]
             )
         ,
-            ( 34
+            ( 33
             ,
                 [ Input MakeLam
                     ( Options
@@ -696,7 +696,7 @@ Output
                 ]
             )
         ,
-            ( 37
+            ( 34
             ,
                 [ Input MakeLam
                     ( Options
@@ -723,7 +723,7 @@ Output
                 ]
             )
         ,
-            ( 47
+            ( 44
             ,
                 [ Input MakeLam
                     ( Options
@@ -749,7 +749,7 @@ Output
                 ]
             )
         ,
-            ( 48
+            ( 45
             ,
                 [ Input MakeLam
                     ( Options
@@ -776,7 +776,7 @@ Output
                 ]
             )
         ,
-            ( 49
+            ( 46
             ,
                 [ Input MakeLam
                     ( Options
@@ -802,7 +802,7 @@ Output
                 ]
             )
         ,
-            ( 50
+            ( 47
             ,
                 [ Input RenamePattern
                     ( Options
@@ -830,7 +830,7 @@ Output
                 ]
             )
         ,
-            ( 51
+            ( 48
             ,
                 [ Input MakeLam
                     ( Options
@@ -857,7 +857,7 @@ Output
                 ]
             )
         ,
-            ( 52
+            ( 49
             ,
                 [ Input MakeLam
                     ( Options
@@ -884,7 +884,7 @@ Output
                 ]
             )
         ,
-            ( 53
+            ( 50
             ,
                 [ Input MakeLam
                     ( Options
@@ -967,7 +967,7 @@ Output
                 ]
             )
         ,
-            ( 54
+            ( 51
             ,
                 [ Input MakeLam
                     ( Options
@@ -994,7 +994,7 @@ Output
                 ]
             )
         ,
-            ( 55
+            ( 52
             ,
                 [ Input MakeLam
                     ( Options
@@ -1028,67 +1028,14 @@ Output
                 ]
             )
         ,
-            ( 18
-            ,
-                [ NoInput MakeFun
-                , Input MakeTCon
-                    ( Options
-                        { opts =
-                            [ Option
-                                { option = "Bool"
-                                , context = Just
-                                    ( "Builtins" :| [] )
-                                }
-                            , Option
-                                { option = "Either"
-                                , context = Just
-                                    ( "Builtins" :| [] )
-                                }
-                            , Option
-                                { option = "List"
-                                , context = Just
-                                    ( "Builtins" :| [] )
-                                }
-                            , Option
-                                { option = "Maybe"
-                                , context = Just
-                                    ( "Builtins" :| [] )
-                                }
-                            , Option
-                                { option = "Nat"
-                                , context = Just
-                                    ( "Builtins" :| [] )
-                                }
-                            , Option
-                                { option = "Pair"
-                                , context = Just
-                                    ( "Builtins" :| [] )
-                                }
-                            , Option
-                                { option = "Char"
-                                , context = Just
-                                    ( "Primitives" :| [] )
-                                }
-                            , Option
-                                { option = "Int"
-                                , context = Just
-                                    ( "Primitives" :| [] )
-                                }
-                            ]
-                        , free = FreeNone
-                        }
-                    )
-                ]
-            )
-        ,
-            ( 20
+            ( 19
             ,
                 [ NoInput MakeFun
                 , NoInput DeleteType
                 ]
             )
         ,
-            ( 21
+            ( 20
             ,
                 [ NoInput MakeFun
                 , NoInput Raise
@@ -1096,7 +1043,7 @@ Output
                 ]
             )
         ,
-            ( 22
+            ( 21
             ,
                 [ NoInput MakeFun
                 , Input MakeTCon
@@ -1150,14 +1097,14 @@ Output
                 ]
             )
         ,
-            ( 24
+            ( 23
             ,
                 [ NoInput MakeFun
                 , NoInput DeleteType
                 ]
             )
         ,
-            ( 25
+            ( 24
             ,
                 [ NoInput MakeFun
                 , NoInput Raise
@@ -1173,20 +1120,6 @@ Output
             )
         ,
             ( 36
-            ,
-                [ NoInput MakeFun
-                , NoInput DeleteType
-                ]
-            )
-        ,
-            ( 38
-            ,
-                [ NoInput MakeFun
-                , NoInput DeleteType
-                ]
-            )
-        ,
-            ( 39
             ,
                 [ NoInput MakeFun
                 , NoInput AddInput
@@ -1195,7 +1128,7 @@ Output
                 ]
             )
         ,
-            ( 40
+            ( 37
             ,
                 [ NoInput MakeFun
                 , NoInput Raise
@@ -1203,7 +1136,7 @@ Output
                 ]
             )
         ,
-            ( 41
+            ( 38
             ,
                 [ NoInput MakeFun
                 , NoInput Raise
@@ -1211,7 +1144,7 @@ Output
                 ]
             )
         ,
-            ( 42
+            ( 39
             ,
                 [ NoInput MakeFun
                 , NoInput Raise
@@ -1219,7 +1152,7 @@ Output
                 ]
             )
         ,
-            ( 43
+            ( 40
             ,
                 [ NoInput MakeFun
                 , NoInput Raise
@@ -1227,7 +1160,7 @@ Output
                 ]
             )
         ,
-            ( 44
+            ( 41
             ,
                 [ NoInput MakeFun
                 , NoInput Raise
@@ -1235,7 +1168,7 @@ Output
                 ]
             )
         ,
-            ( 45
+            ( 42
             ,
                 [ NoInput MakeFun
                 , NoInput Raise
@@ -1243,14 +1176,14 @@ Output
                 ]
             )
         ,
-            ( 46
+            ( 43
             ,
                 [ NoInput MakeFun
                 , NoInput DeleteType
                 ]
             )
         ,
-            ( 56
+            ( 53
             ,
                 [ NoInput MakeFun
                 , NoInput AddInput
@@ -1258,7 +1191,7 @@ Output
                 ]
             )
         ,
-            ( 57
+            ( 54
             ,
                 [ NoInput MakeFun
                 , NoInput Raise
@@ -1266,7 +1199,7 @@ Output
                 ]
             )
         ,
-            ( 58
+            ( 55
             ,
                 [ NoInput MakeFun
                 , NoInput Raise
@@ -1274,7 +1207,7 @@ Output
                 ]
             )
         ,
-            ( 59
+            ( 56
             ,
                 [ NoInput MakeFun
                 , NoInput Raise
@@ -1282,7 +1215,7 @@ Output
                 ]
             )
         ,
-            ( 60
+            ( 57
             ,
                 [ NoInput MakeFun
                 , NoInput Raise
@@ -1290,7 +1223,7 @@ Output
                 ]
             )
         ,
-            ( 61
+            ( 58
             ,
                 [ NoInput MakeFun
                 , NoInput Raise
@@ -1298,7 +1231,7 @@ Output
                 ]
             )
         ,
-            ( 62
+            ( 59
             ,
                 [ NoInput MakeFun
                 , NoInput Raise
@@ -1306,7 +1239,7 @@ Output
                 ]
             )
         ,
-            ( 63
+            ( 60
             ,
                 [ NoInput MakeFun
                 , NoInput Raise
diff --git a/primer/test/outputs/available-actions/M.comprehensive/Beginner-NonEditable.fragment b/primer/test/outputs/available-actions/M.comprehensive/Beginner-NonEditable.fragment
index 6f05aa13c..069a1acdb 100644
--- a/primer/test/outputs/available-actions/M.comprehensive/Beginner-NonEditable.fragment
+++ b/primer/test/outputs/available-actions/M.comprehensive/Beginner-NonEditable.fragment
@@ -34,11 +34,15 @@ Output
             , []
             )
         ,
-            ( 19
+            ( 18
             , []
             )
         ,
-            ( 23
+            ( 22
+            , []
+            )
+        ,
+            ( 25
             , []
             )
         ,
@@ -78,43 +82,39 @@ Output
             , []
             )
         ,
-            ( 37
-            , []
-            )
-        ,
-            ( 47
+            ( 44
             , []
             )
         ,
-            ( 48
+            ( 45
             , []
             )
         ,
-            ( 49
+            ( 46
             , []
             )
         ,
-            ( 50
+            ( 47
             , []
             )
         ,
-            ( 51
+            ( 48
             , []
             )
         ,
-            ( 52
+            ( 49
             , []
             )
         ,
-            ( 53
+            ( 50
             , []
             )
         ,
-            ( 54
+            ( 51
             , []
             )
         ,
-            ( 55
+            ( 52
             , []
             )
         ,
@@ -122,7 +122,7 @@ Output
             , []
             )
         ,
-            ( 18
+            ( 19
             , []
             )
         ,
@@ -134,7 +134,7 @@ Output
             , []
             )
         ,
-            ( 22
+            ( 23
             , []
             )
         ,
@@ -142,15 +142,15 @@ Output
             , []
             )
         ,
-            ( 25
+            ( 35
             , []
             )
         ,
-            ( 35
+            ( 36
             , []
             )
         ,
-            ( 36
+            ( 37
             , []
             )
         ,
@@ -178,15 +178,15 @@ Output
             , []
             )
         ,
-            ( 44
+            ( 53
             , []
             )
         ,
-            ( 45
+            ( 54
             , []
             )
         ,
-            ( 46
+            ( 55
             , []
             )
         ,
@@ -209,18 +209,6 @@ Output
             ( 60
             , []
             )
-        ,
-            ( 61
-            , []
-            )
-        ,
-            ( 62
-            , []
-            )
-        ,
-            ( 63
-            , []
-            )
         ]
     , sigActions =
         [
diff --git a/primer/test/outputs/available-actions/M.comprehensive/Expert-Editable.fragment b/primer/test/outputs/available-actions/M.comprehensive/Expert-Editable.fragment
index bbf5d4408..13217d2ed 100644
--- a/primer/test/outputs/available-actions/M.comprehensive/Expert-Editable.fragment
+++ b/primer/test/outputs/available-actions/M.comprehensive/Expert-Editable.fragment
@@ -445,7 +445,7 @@ Output
                 ]
             )
         ,
-            ( 19
+            ( 18
             ,
                 [ Input MakeLam
                     ( Options
@@ -638,7 +638,7 @@ Output
                 ]
             )
         ,
-            ( 23
+            ( 22
             ,
                 [ Input MakeLam
                     ( Options
@@ -831,7 +831,7 @@ Output
                 ]
             )
         ,
-            ( 26
+            ( 25
             ,
                 [ Input MakeLam
                     ( Options
@@ -883,7 +883,7 @@ Output
                 ]
             )
         ,
-            ( 27
+            ( 26
             ,
                 [ Input MakeLam
                     ( Options
@@ -958,7 +958,7 @@ Output
                 ]
             )
         ,
-            ( 28
+            ( 27
             ,
                 [ Input MakeLam
                     ( Options
@@ -1025,7 +1025,7 @@ Output
                 ]
             )
         ,
-            ( 29
+            ( 28
             ,
                 [ Input MakeLam
                     ( Options
@@ -1074,7 +1074,7 @@ Output
                 ]
             )
         ,
-            ( 30
+            ( 29
             ,
                 [ Input MakeLam
                     ( Options
@@ -1122,7 +1122,7 @@ Output
                 ]
             )
         ,
-            ( 31
+            ( 30
             ,
                 [ Input MakeLam
                     ( Options
@@ -1170,7 +1170,7 @@ Output
                 ]
             )
         ,
-            ( 32
+            ( 31
             ,
                 [ Input MakeLam
                     ( Options
@@ -1237,7 +1237,7 @@ Output
                 ]
             )
         ,
-            ( 33
+            ( 32
             ,
                 [ Input MakeLam
                     ( Options
@@ -1296,7 +1296,7 @@ Output
                 ]
             )
         ,
-            ( 34
+            ( 33
             ,
                 [ Input MakeLam
                     ( Options
@@ -1344,7 +1344,7 @@ Output
                 ]
             )
         ,
-            ( 37
+            ( 34
             ,
                 [ Input MakeLam
                     ( Options
@@ -1393,7 +1393,7 @@ Output
                 ]
             )
         ,
-            ( 47
+            ( 44
             ,
                 [ Input MakeLam
                     ( Options
@@ -1441,7 +1441,7 @@ Output
                 ]
             )
         ,
-            ( 48
+            ( 45
             ,
                 [ Input MakeLam
                     ( Options
@@ -1490,7 +1490,7 @@ Output
                 ]
             )
         ,
-            ( 49
+            ( 46
             ,
                 [ Input MakeLam
                     ( Options
@@ -1538,7 +1538,7 @@ Output
                 ]
             )
         ,
-            ( 50
+            ( 47
             ,
                 [ Input RenamePattern
                     ( Options
@@ -1566,7 +1566,7 @@ Output
                 ]
             )
         ,
-            ( 51
+            ( 48
             ,
                 [ Input MakeLam
                     ( Options
@@ -1615,7 +1615,7 @@ Output
                 ]
             )
         ,
-            ( 52
+            ( 49
             ,
                 [ Input MakeLam
                     ( Options
@@ -1664,7 +1664,7 @@ Output
                 ]
             )
         ,
-            ( 53
+            ( 50
             ,
                 [ Input MakeLam
                     ( Options
@@ -1865,7 +1865,7 @@ Output
                 ]
             )
         ,
-            ( 54
+            ( 51
             ,
                 [ Input MakeLam
                     ( Options
@@ -1914,7 +1914,7 @@ Output
                 ]
             )
         ,
-            ( 55
+            ( 52
             ,
                 [ Input MakeLam
                     ( Options
@@ -1990,86 +1990,7 @@ Output
                 ]
             )
         ,
-            ( 18
-            ,
-                [ NoInput MakeFun
-                , Input MakeTVar
-                    ( Options
-                        { opts = []
-                        , free = FreeNone
-                        }
-                    )
-                , Input MakeTCon
-                    ( Options
-                        { opts =
-                            [ Option
-                                { option = "Bool"
-                                , context = Just
-                                    ( "Builtins" :| [] )
-                                }
-                            , Option
-                                { option = "Either"
-                                , context = Just
-                                    ( "Builtins" :| [] )
-                                }
-                            , Option
-                                { option = "List"
-                                , context = Just
-                                    ( "Builtins" :| [] )
-                                }
-                            , Option
-                                { option = "Maybe"
-                                , context = Just
-                                    ( "Builtins" :| [] )
-                                }
-                            , Option
-                                { option = "Nat"
-                                , context = Just
-                                    ( "Builtins" :| [] )
-                                }
-                            , Option
-                                { option = "Pair"
-                                , context = Just
-                                    ( "Builtins" :| [] )
-                                }
-                            , Option
-                                { option = "Char"
-                                , context = Just
-                                    ( "Primitives" :| [] )
-                                }
-                            , Option
-                                { option = "Int"
-                                , context = Just
-                                    ( "Primitives" :| [] )
-                                }
-                            ]
-                        , free = FreeNone
-                        }
-                    )
-                , NoInput MakeTApp
-                , Input MakeForall
-                    ( Options
-                        { opts =
-                            [ Option
-                                { option = "α"
-                                , context = Nothing
-                                }
-                            , Option
-                                { option = "β"
-                                , context = Nothing
-                                }
-                            , Option
-                                { option = "γ"
-                                , context = Nothing
-                                }
-                            ]
-                        , free = FreeVarName
-                        }
-                    )
-                ]
-            )
-        ,
-            ( 20
+            ( 19
             ,
                 [ NoInput MakeFun
                 , NoInput MakeTApp
@@ -2096,7 +2017,7 @@ Output
                 ]
             )
         ,
-            ( 21
+            ( 20
             ,
                 [ NoInput MakeFun
                 , NoInput MakeTApp
@@ -2124,7 +2045,7 @@ Output
                 ]
             )
         ,
-            ( 22
+            ( 21
             ,
                 [ NoInput MakeFun
                 , Input MakeTVar
@@ -2204,7 +2125,7 @@ Output
                 ]
             )
         ,
-            ( 24
+            ( 23
             ,
                 [ NoInput MakeFun
                 , NoInput MakeTApp
@@ -2231,7 +2152,7 @@ Output
                 ]
             )
         ,
-            ( 25
+            ( 24
             ,
                 [ NoInput MakeFun
                 , NoInput MakeTApp
@@ -2260,60 +2181,6 @@ Output
             )
         ,
             ( 35
-            ,
-                [ NoInput MakeFun
-                , NoInput MakeTApp
-                , Input MakeForall
-                    ( Options
-                        { opts =
-                            [ Option
-                                { option = "α"
-                                , context = Nothing
-                                }
-                            , Option
-                                { option = "γ"
-                                , context = Nothing
-                                }
-                            , Option
-                                { option = "β1"
-                                , context = Nothing
-                                }
-                            ]
-                        , free = FreeVarName
-                        }
-                    )
-                , NoInput DeleteType
-                ]
-            )
-        ,
-            ( 36
-            ,
-                [ NoInput MakeFun
-                , NoInput MakeTApp
-                , Input MakeForall
-                    ( Options
-                        { opts =
-                            [ Option
-                                { option = "α"
-                                , context = Nothing
-                                }
-                            , Option
-                                { option = "γ"
-                                , context = Nothing
-                                }
-                            , Option
-                                { option = "β1"
-                                , context = Nothing
-                                }
-                            ]
-                        , free = FreeVarName
-                        }
-                    )
-                , NoInput DeleteType
-                ]
-            )
-        ,
-            ( 38
             ,
                 [ NoInput MakeFun
                 , NoInput MakeTApp
@@ -2359,7 +2226,7 @@ Output
                 ]
             )
         ,
-            ( 39
+            ( 36
             ,
                 [ NoInput MakeFun
                 , NoInput AddInput
@@ -2388,7 +2255,7 @@ Output
                 ]
             )
         ,
-            ( 40
+            ( 37
             ,
                 [ NoInput MakeFun
                 , NoInput MakeTApp
@@ -2416,7 +2283,7 @@ Output
                 ]
             )
         ,
-            ( 41
+            ( 38
             ,
                 [ NoInput MakeFun
                 , NoInput MakeTApp
@@ -2444,7 +2311,7 @@ Output
                 ]
             )
         ,
-            ( 42
+            ( 39
             ,
                 [ NoInput MakeFun
                 , NoInput MakeTApp
@@ -2472,7 +2339,7 @@ Output
                 ]
             )
         ,
-            ( 43
+            ( 40
             ,
                 [ NoInput MakeFun
                 , NoInput MakeTApp
@@ -2500,7 +2367,7 @@ Output
                 ]
             )
         ,
-            ( 44
+            ( 41
             ,
                 [ NoInput MakeFun
                 , NoInput MakeTApp
@@ -2528,7 +2395,7 @@ Output
                 ]
             )
         ,
-            ( 45
+            ( 42
             ,
                 [ NoInput MakeFun
                 , NoInput MakeTApp
@@ -2556,7 +2423,7 @@ Output
                 ]
             )
         ,
-            ( 46
+            ( 43
             ,
                 [ NoInput MakeFun
                 , NoInput MakeTApp
@@ -2583,7 +2450,7 @@ Output
                 ]
             )
         ,
-            ( 56
+            ( 53
             ,
                 [ NoInput MakeFun
                 , NoInput AddInput
@@ -2611,7 +2478,7 @@ Output
                 ]
             )
         ,
-            ( 57
+            ( 54
             ,
                 [ NoInput MakeFun
                 , NoInput MakeTApp
@@ -2639,7 +2506,7 @@ Output
                 ]
             )
         ,
-            ( 58
+            ( 55
             ,
                 [ NoInput MakeFun
                 , NoInput MakeTApp
@@ -2686,7 +2553,7 @@ Output
                 ]
             )
         ,
-            ( 59
+            ( 56
             ,
                 [ NoInput MakeFun
                 , NoInput MakeTApp
@@ -2714,7 +2581,7 @@ Output
                 ]
             )
         ,
-            ( 60
+            ( 57
             ,
                 [ NoInput MakeFun
                 , NoInput MakeTApp
@@ -2742,7 +2609,7 @@ Output
                 ]
             )
         ,
-            ( 61
+            ( 58
             ,
                 [ NoInput MakeFun
                 , NoInput MakeTApp
@@ -2770,7 +2637,7 @@ Output
                 ]
             )
         ,
-            ( 62
+            ( 59
             ,
                 [ NoInput MakeFun
                 , NoInput MakeTApp
@@ -2798,7 +2665,7 @@ Output
                 ]
             )
         ,
-            ( 63
+            ( 60
             ,
                 [ NoInput MakeFun
                 , NoInput MakeTApp
diff --git a/primer/test/outputs/available-actions/M.comprehensive/Expert-NonEditable.fragment b/primer/test/outputs/available-actions/M.comprehensive/Expert-NonEditable.fragment
index 6f05aa13c..069a1acdb 100644
--- a/primer/test/outputs/available-actions/M.comprehensive/Expert-NonEditable.fragment
+++ b/primer/test/outputs/available-actions/M.comprehensive/Expert-NonEditable.fragment
@@ -34,11 +34,15 @@ Output
             , []
             )
         ,
-            ( 19
+            ( 18
             , []
             )
         ,
-            ( 23
+            ( 22
+            , []
+            )
+        ,
+            ( 25
             , []
             )
         ,
@@ -78,43 +82,39 @@ Output
             , []
             )
         ,
-            ( 37
-            , []
-            )
-        ,
-            ( 47
+            ( 44
             , []
             )
         ,
-            ( 48
+            ( 45
             , []
             )
         ,
-            ( 49
+            ( 46
             , []
             )
         ,
-            ( 50
+            ( 47
             , []
             )
         ,
-            ( 51
+            ( 48
             , []
             )
         ,
-            ( 52
+            ( 49
             , []
             )
         ,
-            ( 53
+            ( 50
             , []
             )
         ,
-            ( 54
+            ( 51
             , []
             )
         ,
-            ( 55
+            ( 52
             , []
             )
         ,
@@ -122,7 +122,7 @@ Output
             , []
             )
         ,
-            ( 18
+            ( 19
             , []
             )
         ,
@@ -134,7 +134,7 @@ Output
             , []
             )
         ,
-            ( 22
+            ( 23
             , []
             )
         ,
@@ -142,15 +142,15 @@ Output
             , []
             )
         ,
-            ( 25
+            ( 35
             , []
             )
         ,
-            ( 35
+            ( 36
             , []
             )
         ,
-            ( 36
+            ( 37
             , []
             )
         ,
@@ -178,15 +178,15 @@ Output
             , []
             )
         ,
-            ( 44
+            ( 53
             , []
             )
         ,
-            ( 45
+            ( 54
             , []
             )
         ,
-            ( 46
+            ( 55
             , []
             )
         ,
@@ -209,18 +209,6 @@ Output
             ( 60
             , []
             )
-        ,
-            ( 61
-            , []
-            )
-        ,
-            ( 62
-            , []
-            )
-        ,
-            ( 63
-            , []
-            )
         ]
     , sigActions =
         [
diff --git a/primer/test/outputs/available-actions/M.comprehensive/Intermediate-Editable.fragment b/primer/test/outputs/available-actions/M.comprehensive/Intermediate-Editable.fragment
index 13816cd19..7e3e6ddd1 100644
--- a/primer/test/outputs/available-actions/M.comprehensive/Intermediate-Editable.fragment
+++ b/primer/test/outputs/available-actions/M.comprehensive/Intermediate-Editable.fragment
@@ -277,7 +277,7 @@ Output
                 ]
             )
         ,
-            ( 19
+            ( 18
             ,
                 [ Input MakeLam
                     ( Options
@@ -449,7 +449,7 @@ Output
                 ]
             )
         ,
-            ( 23
+            ( 22
             ,
                 [ Input MakeLam
                     ( Options
@@ -621,7 +621,7 @@ Output
                 ]
             )
         ,
-            ( 26
+            ( 25
             ,
                 [ Input MakeLam
                     ( Options
@@ -652,7 +652,7 @@ Output
                 ]
             )
         ,
-            ( 27
+            ( 26
             ,
                 [ Input MakeLam
                     ( Options
@@ -706,7 +706,7 @@ Output
                 ]
             )
         ,
-            ( 28
+            ( 27
             ,
                 [ Input MakeLam
                     ( Options
@@ -733,7 +733,7 @@ Output
                 ]
             )
         ,
-            ( 29
+            ( 28
             ,
                 [ Input MakeLam
                     ( Options
@@ -761,7 +761,7 @@ Output
                 ]
             )
         ,
-            ( 30
+            ( 29
             ,
                 [ Input MakeLam
                     ( Options
@@ -788,7 +788,7 @@ Output
                 ]
             )
         ,
-            ( 31
+            ( 30
             ,
                 [ Input MakeLam
                     ( Options
@@ -815,7 +815,7 @@ Output
                 ]
             )
         ,
-            ( 32
+            ( 31
             ,
                 [ Input MakeLam
                     ( Options
@@ -842,7 +842,7 @@ Output
                 ]
             )
         ,
-            ( 33
+            ( 32
             ,
                 [ Input MakeLam
                     ( Options
@@ -880,7 +880,7 @@ Output
                 ]
             )
         ,
-            ( 34
+            ( 33
             ,
                 [ Input MakeLam
                     ( Options
@@ -907,7 +907,7 @@ Output
                 ]
             )
         ,
-            ( 37
+            ( 34
             ,
                 [ Input MakeLam
                     ( Options
@@ -935,7 +935,7 @@ Output
                 ]
             )
         ,
-            ( 47
+            ( 44
             ,
                 [ Input MakeLam
                     ( Options
@@ -962,7 +962,7 @@ Output
                 ]
             )
         ,
-            ( 48
+            ( 45
             ,
                 [ Input MakeLam
                     ( Options
@@ -990,7 +990,7 @@ Output
                 ]
             )
         ,
-            ( 49
+            ( 46
             ,
                 [ Input MakeLam
                     ( Options
@@ -1017,7 +1017,7 @@ Output
                 ]
             )
         ,
-            ( 50
+            ( 47
             ,
                 [ Input RenamePattern
                     ( Options
@@ -1045,7 +1045,7 @@ Output
                 ]
             )
         ,
-            ( 51
+            ( 48
             ,
                 [ Input MakeLam
                     ( Options
@@ -1073,7 +1073,7 @@ Output
                 ]
             )
         ,
-            ( 52
+            ( 49
             ,
                 [ Input MakeLam
                     ( Options
@@ -1101,7 +1101,7 @@ Output
                 ]
             )
         ,
-            ( 53
+            ( 50
             ,
                 [ Input MakeLam
                     ( Options
@@ -1281,7 +1281,7 @@ Output
                 ]
             )
         ,
-            ( 54
+            ( 51
             ,
                 [ Input MakeLam
                     ( Options
@@ -1309,7 +1309,7 @@ Output
                 ]
             )
         ,
-            ( 55
+            ( 52
             ,
                 [ Input MakeLam
                     ( Options
@@ -1344,67 +1344,14 @@ Output
                 ]
             )
         ,
-            ( 18
-            ,
-                [ NoInput MakeFun
-                , Input MakeTCon
-                    ( Options
-                        { opts =
-                            [ Option
-                                { option = "Bool"
-                                , context = Just
-                                    ( "Builtins" :| [] )
-                                }
-                            , Option
-                                { option = "Either"
-                                , context = Just
-                                    ( "Builtins" :| [] )
-                                }
-                            , Option
-                                { option = "List"
-                                , context = Just
-                                    ( "Builtins" :| [] )
-                                }
-                            , Option
-                                { option = "Maybe"
-                                , context = Just
-                                    ( "Builtins" :| [] )
-                                }
-                            , Option
-                                { option = "Nat"
-                                , context = Just
-                                    ( "Builtins" :| [] )
-                                }
-                            , Option
-                                { option = "Pair"
-                                , context = Just
-                                    ( "Builtins" :| [] )
-                                }
-                            , Option
-                                { option = "Char"
-                                , context = Just
-                                    ( "Primitives" :| [] )
-                                }
-                            , Option
-                                { option = "Int"
-                                , context = Just
-                                    ( "Primitives" :| [] )
-                                }
-                            ]
-                        , free = FreeNone
-                        }
-                    )
-                ]
-            )
-        ,
-            ( 20
+            ( 19
             ,
                 [ NoInput MakeFun
                 , NoInput DeleteType
                 ]
             )
         ,
-            ( 21
+            ( 20
             ,
                 [ NoInput MakeFun
                 , NoInput Raise
@@ -1412,7 +1359,7 @@ Output
                 ]
             )
         ,
-            ( 22
+            ( 21
             ,
                 [ NoInput MakeFun
                 , Input MakeTCon
@@ -1466,14 +1413,14 @@ Output
                 ]
             )
         ,
-            ( 24
+            ( 23
             ,
                 [ NoInput MakeFun
                 , NoInput DeleteType
                 ]
             )
         ,
-            ( 25
+            ( 24
             ,
                 [ NoInput MakeFun
                 , NoInput Raise
@@ -1489,20 +1436,6 @@ Output
             )
         ,
             ( 36
-            ,
-                [ NoInput MakeFun
-                , NoInput DeleteType
-                ]
-            )
-        ,
-            ( 38
-            ,
-                [ NoInput MakeFun
-                , NoInput DeleteType
-                ]
-            )
-        ,
-            ( 39
             ,
                 [ NoInput MakeFun
                 , NoInput AddInput
@@ -1511,7 +1444,7 @@ Output
                 ]
             )
         ,
-            ( 40
+            ( 37
             ,
                 [ NoInput MakeFun
                 , NoInput Raise
@@ -1519,7 +1452,7 @@ Output
                 ]
             )
         ,
-            ( 41
+            ( 38
             ,
                 [ NoInput MakeFun
                 , NoInput Raise
@@ -1527,7 +1460,7 @@ Output
                 ]
             )
         ,
-            ( 42
+            ( 39
             ,
                 [ NoInput MakeFun
                 , NoInput Raise
@@ -1535,7 +1468,7 @@ Output
                 ]
             )
         ,
-            ( 43
+            ( 40
             ,
                 [ NoInput MakeFun
                 , NoInput Raise
@@ -1543,7 +1476,7 @@ Output
                 ]
             )
         ,
-            ( 44
+            ( 41
             ,
                 [ NoInput MakeFun
                 , NoInput Raise
@@ -1551,7 +1484,7 @@ Output
                 ]
             )
         ,
-            ( 45
+            ( 42
             ,
                 [ NoInput MakeFun
                 , NoInput Raise
@@ -1559,14 +1492,14 @@ Output
                 ]
             )
         ,
-            ( 46
+            ( 43
             ,
                 [ NoInput MakeFun
                 , NoInput DeleteType
                 ]
             )
         ,
-            ( 56
+            ( 53
             ,
                 [ NoInput MakeFun
                 , NoInput AddInput
@@ -1574,7 +1507,7 @@ Output
                 ]
             )
         ,
-            ( 57
+            ( 54
             ,
                 [ NoInput MakeFun
                 , NoInput Raise
@@ -1582,7 +1515,7 @@ Output
                 ]
             )
         ,
-            ( 58
+            ( 55
             ,
                 [ NoInput MakeFun
                 , NoInput Raise
@@ -1590,7 +1523,7 @@ Output
                 ]
             )
         ,
-            ( 59
+            ( 56
             ,
                 [ NoInput MakeFun
                 , NoInput Raise
@@ -1598,7 +1531,7 @@ Output
                 ]
             )
         ,
-            ( 60
+            ( 57
             ,
                 [ NoInput MakeFun
                 , NoInput Raise
@@ -1606,7 +1539,7 @@ Output
                 ]
             )
         ,
-            ( 61
+            ( 58
             ,
                 [ NoInput MakeFun
                 , NoInput Raise
@@ -1614,7 +1547,7 @@ Output
                 ]
             )
         ,
-            ( 62
+            ( 59
             ,
                 [ NoInput MakeFun
                 , NoInput Raise
@@ -1622,7 +1555,7 @@ Output
                 ]
             )
         ,
-            ( 63
+            ( 60
             ,
                 [ NoInput MakeFun
                 , NoInput Raise
diff --git a/primer/test/outputs/available-actions/M.comprehensive/Intermediate-NonEditable.fragment b/primer/test/outputs/available-actions/M.comprehensive/Intermediate-NonEditable.fragment
index 6f05aa13c..069a1acdb 100644
--- a/primer/test/outputs/available-actions/M.comprehensive/Intermediate-NonEditable.fragment
+++ b/primer/test/outputs/available-actions/M.comprehensive/Intermediate-NonEditable.fragment
@@ -34,11 +34,15 @@ Output
             , []
             )
         ,
-            ( 19
+            ( 18
             , []
             )
         ,
-            ( 23
+            ( 22
+            , []
+            )
+        ,
+            ( 25
             , []
             )
         ,
@@ -78,43 +82,39 @@ Output
             , []
             )
         ,
-            ( 37
-            , []
-            )
-        ,
-            ( 47
+            ( 44
             , []
             )
         ,
-            ( 48
+            ( 45
             , []
             )
         ,
-            ( 49
+            ( 46
             , []
             )
         ,
-            ( 50
+            ( 47
             , []
             )
         ,
-            ( 51
+            ( 48
             , []
             )
         ,
-            ( 52
+            ( 49
             , []
             )
         ,
-            ( 53
+            ( 50
             , []
             )
         ,
-            ( 54
+            ( 51
             , []
             )
         ,
-            ( 55
+            ( 52
             , []
             )
         ,
@@ -122,7 +122,7 @@ Output
             , []
             )
         ,
-            ( 18
+            ( 19
             , []
             )
         ,
@@ -134,7 +134,7 @@ Output
             , []
             )
         ,
-            ( 22
+            ( 23
             , []
             )
         ,
@@ -142,15 +142,15 @@ Output
             , []
             )
         ,
-            ( 25
+            ( 35
             , []
             )
         ,
-            ( 35
+            ( 36
             , []
             )
         ,
-            ( 36
+            ( 37
             , []
             )
         ,
@@ -178,15 +178,15 @@ Output
             , []
             )
         ,
-            ( 44
+            ( 53
             , []
             )
         ,
-            ( 45
+            ( 54
             , []
             )
         ,
-            ( 46
+            ( 55
             , []
             )
         ,
@@ -209,18 +209,6 @@ Output
             ( 60
             , []
             )
-        ,
-            ( 61
-            , []
-            )
-        ,
-            ( 62
-            , []
-            )
-        ,
-            ( 63
-            , []
-            )
         ]
     , sigActions =
         [
diff --git a/primer/testlib/Primer/Test/Expected.hs b/primer/testlib/Primer/Test/Expected.hs
index 86c189ea0..21d66f13d 100644
--- a/primer/testlib/Primer/Test/Expected.hs
+++ b/primer/testlib/Primer/Test/Expected.hs
@@ -59,9 +59,9 @@ mapEven n =
         (mapName, mapDef) <- Examples.map modName
         (evenName, evenDef) <- Examples.even modName
         (oddName, oddDef) <- Examples.odd modName
-        let lst = list_ tNat $ take n $ iterate (con1 cSucc) (con0 cZero)
+        let lst = list_ $ take n $ iterate (con1 cSucc) (con0 cZero)
         expr <- gvar mapName `aPP` tcon tNat `aPP` tcon tBool `app` gvar evenName `app` lst
         let globs = M.fromList [(mapName, mapDef), (evenName, evenDef), (oddName, oddDef)]
-        expect <- list_ tBool (take n $ cycle [con0 cTrue, con0 cFalse]) `ann` (tcon tList `tapp` tcon tBool)
+        expect <- list_ (take n $ cycle [con0 cTrue, con0 cFalse]) `ann` (tcon tList `tapp` tcon tBool)
         pure (globs, expr, expect)
    in Expected globals e id expected
diff --git a/primer/testlib/Primer/Test/Util.hs b/primer/testlib/Primer/Test/Util.hs
index 003d90711..2fdb403bd 100644
--- a/primer/testlib/Primer/Test/Util.hs
+++ b/primer/testlib/Primer/Test/Util.hs
@@ -5,7 +5,6 @@ module Primer.Test.Util (
   assertException,
   primDefs,
   constructTCon,
-  constructRefinedCon,
   constructSaturatedCon,
   tcn,
   vcn,
@@ -40,7 +39,7 @@ import Primer.API (
   runPrimerM,
  )
 import Primer.Action (
-  Action (ConstructRefinedCon, ConstructSaturatedCon, ConstructTCon),
+  Action (ConstructSaturatedCon, ConstructTCon),
  )
 import Primer.Core (
   Expr',
@@ -90,9 +89,6 @@ constructTCon = ConstructTCon . toQualText
 constructSaturatedCon :: ValConName -> Action
 constructSaturatedCon = ConstructSaturatedCon . toQualText
 
-constructRefinedCon :: ValConName -> Action
-constructRefinedCon = ConstructRefinedCon . toQualText
-
 toQualText :: GlobalName k -> (NonEmpty Text, Text)
 toQualText n = (map unName $ unModuleName $ qualifiedModule n, unName $ baseName n)