diff --git a/primer/primer.cabal b/primer/primer.cabal
index dffb1994a..9f212402f 100644
--- a/primer/primer.cabal
+++ b/primer/primer.cabal
@@ -15,6 +15,8 @@ library
     Control.Monad.Fresh
     Foreword
     Primer.Action
+    Primer.Action.Available
+    Primer.Action.Priorities
     Primer.API
     Primer.App
     Primer.Core
@@ -25,6 +27,7 @@ library
     Primer.Eval
     Primer.EvalFull
     Primer.Name
+    Primer.Name.Fresh
     Primer.Questions
     Primer.Refine
     Primer.Subst
diff --git a/primer/src/Primer/Action.hs b/primer/src/Primer/Action.hs
index 0e00e959f..b26093637 100644
--- a/primer/src/Primer/Action.hs
+++ b/primer/src/Primer/Action.hs
@@ -1,4 +1,7 @@
 {-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE TupleSections #-}
 {-# LANGUAGE TypeApplications #-}
 
@@ -6,12 +9,20 @@ module Primer.Action (
   Action (..),
   ActionError (..),
   Movement (..),
+  ProgAction (..),
   applyActionsToBody,
   applyActionsToTypeSig,
   applyActionsToExpr,
   moveExpr,
-  mkAvoidForFreshName,
-  mkAvoidForFreshNameTy,
+  OfferedAction (..),
+  ActionType (..),
+  FunctionFiltering (..),
+  UserInput (..),
+  ActionInput (..),
+  ActionName (..),
+  Level (..),
+  nameString,
+  uniquifyDefName,
 ) where
 
 import Foreword
@@ -21,7 +32,7 @@ import Data.Aeson (Value)
 import Data.Generics.Product (typed)
 import Data.List (delete, findIndex, lookup)
 import qualified Data.Map.Strict as Map
-import qualified Data.Set as S
+import qualified Data.Text as T
 import Optics (set, (%), (?~))
 import Primer.Core (
   Def (..),
@@ -66,9 +77,15 @@ import Primer.Core.DSL (
 import Primer.Core.Transform (renameTyVar, renameTyVarExpr, renameVar)
 import Primer.Core.Utils (forgetTypeIDs, generateTypeIDs)
 import Primer.JSON
-import Primer.Name (Name, NameCounter, freshName, unName, unsafeMkName)
+import Primer.Name (Name, NameCounter, unName, unsafeMkName)
+import Primer.Name.Fresh (
+  isFresh,
+  isFreshTy,
+  mkFreshName,
+  mkFreshNameTy,
+ )
+import Primer.Questions (Question)
 import Primer.Refine (Inst (InstAPP, InstApp, InstUnconstrainedAPP), refine)
-import Primer.Subst (freeVars, freeVarsTy)
 import Primer.Typecheck (
   SmartHoles,
   TypeError,
@@ -90,15 +107,10 @@ import Primer.Zipper (
   IsZipper,
   Loc (..),
   TypeZ,
-  bindersAbove,
-  bindersAboveTypeZ,
-  bindersBelow,
-  bindersBelowTy,
   down,
   focus,
   focusLoc,
   focusOn,
-  focusOnlyType,
   focusType,
   locToEither,
   replace,
@@ -114,6 +126,107 @@ import Primer.Zipper (
  )
 import Primer.ZipperCxt (localVariablesInScopeExpr)
 
+-- | An OfferedAction is an option that we show to the user.
+-- It may require some user input (e.g. to choose what to name a binder, or
+-- choose which variable to insert).
+-- If picked, it will submit a particular set of actions to the backend.
+data OfferedAction a = OfferedAction
+  { name :: ActionName
+  , description :: Text
+  , input :: ActionInput a
+  , priority :: Int
+  , -- | Used primarily for display purposes.
+    actionType :: ActionType
+  }
+  deriving (Functor)
+
+-- We will probably add more constructors in future.
+data ActionType
+  = Primary
+  | Destructive
+
+-- | Filter on variables and constructors according to whether they
+-- have a function type.
+data FunctionFiltering
+  = Everything
+  | OnlyFunctions
+  | NoFunctions
+
+-- | Further user input is sometimes required to construct an action.
+-- For example, when inserting a constructor the user must tell us what
+-- constructor.
+-- This type models that input and the corresponding output.
+-- Currently we can only take a single input per action - in the future this
+-- may need to be extended to support multiple inputs.
+-- This type is parameterised because we may need it for other things in
+-- future, and because it lets us derive a useful functor instance.
+data UserInput a
+  = ChooseConstructor FunctionFiltering (Text -> a)
+  | ChooseTypeConstructor (Text -> a)
+  | -- | Renders a choice between some options (as buttons),
+    -- plus a textbox to manually enter a name
+    ChooseOrEnterName
+      Text
+      -- ^ Prompt to show the user, e.g. "choose a name, or enter your own"
+      [Name]
+      -- ^ A bunch of options
+      (Name -> a)
+      -- ^ What to do with whatever name is chosen
+  | ChooseVariable FunctionFiltering (Either Text ID -> a)
+  | ChooseTypeVariable (Text -> a)
+  deriving (Functor)
+
+data ActionInput a where
+  InputRequired :: UserInput a -> ActionInput a
+  NoInputRequired :: a -> ActionInput a
+  AskQuestion :: Question r -> (r -> ActionInput a) -> ActionInput a
+deriving instance Functor ActionInput
+
+-- | Some actions' names are meant to be rendered as code, others as
+-- prose.
+data ActionName
+  = Code Text
+  | Prose Text
+
+-- | The current programming "level". This setting determines which
+-- actions are displayed to the student, the labels on UI elements,
+-- etc.
+data Level
+  = -- | Bare minimum features to define sum types, and functions on
+    -- those types using simple pattern matching.
+    Beginner
+  | -- | Function application & monomorphic HoF. (Support for the latter
+    -- should probably be split into a separate level.)
+    Intermediate
+  | -- | All features.
+    Expert
+
+-- | Sigh, yes, this is required so that Safari doesn't try to
+-- autocomplete these fields with your contact data.
+--
+-- See
+-- https://stackoverflow.com/questions/43058018/how-to-disable-autocomplete-in-address-fields-for-safari
+--
+-- Note that, according to a comment in the above StackOverflow
+-- post, this is screenreader-safe.
+nameString :: Text
+nameString = "n" <> T.singleton '\x200C' <> "ame"
+
+-- | Given a definition name and a program, return a unique variant of
+-- that name. Note that if no definition of the given name already
+-- exists in the program, this function will return the same name
+-- it's been given.
+uniquifyDefName :: Text -> Map ID Def -> Text
+uniquifyDefName name' defs =
+  if name' `notElem` avoid
+    then name'
+    else
+      let go i = if (name' <> "_" <> show i) `notElem` avoid then name' <> "_" <> show i else go (i + 1)
+       in go (1 :: Int)
+  where
+    avoid :: [Text]
+    avoid = Map.elems $ map (unName . defName) defs
+
 -- | Core actions.
 --  These describe edits to the core AST.
 --  Some of them take Text arguments rather than Name because they represent
@@ -237,6 +350,40 @@ data ActionError
   deriving (Eq, Show, Generic)
   deriving (FromJSON, ToJSON) via VJSON ActionError
 
+-- | High level actions
+-- These actions move around the whole program or modify definitions
+data ProgAction
+  = -- | Move the cursor to the definition with the given ID
+    MoveToDef ID
+  | -- | Rename the definition with the given ID
+    RenameDef ID Text
+  | -- | Create a new definition
+    CreateDef (Maybe Text)
+  | -- | Delete a new definition
+    DeleteDef ID
+  | -- | Add a new type definition
+    AddTypeDef TypeDef
+  | -- | Execute a sequence of actions on the body of the definition
+    BodyAction [Action]
+  | -- | Execute a sequence of actions on the type annotation of the definition
+    SigAction [Action]
+  | SetSmartHoles SmartHoles
+  | -- | CopyPaste (d,i) as
+    --   remembers the tree in def d, node i
+    --   runs actions as (in the currently selected def), which should end up in a hole
+    --   and then tries to paste the remembered subtree
+    --   This rather complex setup enables encoding 'raise' operations,
+    --     f s ~> f
+    --   where we remember f, then delete f s, then paste f back
+    --   as well as allowing cross-definition copy+paste
+    --   whilst letting the backend avoid remembering the 'copied' thing in some state.
+    --   The cursor is left on the root of the inserted subtree, which may or may not be inside a hole and/or annotation.
+    --   At the start of the actions, the cursor starts at the root of the definition's type/expression
+    CopyPasteSig (ID, ID) [Action]
+  | CopyPasteBody (ID, ID) [Action]
+  deriving (Eq, Show, Generic)
+  deriving (FromJSON, ToJSON) via VJSON ProgAction
+
 -- | A shorthand for the constraints needed when applying actions
 type ActionM m =
   ( Monad m
@@ -812,9 +959,10 @@ renameLet y ze = case target ze of
       (Nothing, _) -> throwError NameCapture
       (_, Nothing) -> throwError NameCapture
 
-renameCaseBinding :: ActionM m => Text -> CaseBindZ -> m CaseBindZ
+renameCaseBinding :: forall m. ActionM m => Text -> CaseBindZ -> m CaseBindZ
 renameCaseBinding y caseBind = updateCaseBind caseBind $ \bind bindings rhs -> do
-  let failure = throwError . CustomFailure (RenameCaseBinding y)
+  let failure :: Text -> m a
+      failure = throwError . CustomFailure (RenameCaseBinding y)
   let y' = unsafeMkName y
 
   -- Check that 'y' doesn't clash with any of the other branch bindings
@@ -885,54 +1033,3 @@ renameForall b zt = case target zt of
           throwError NameCapture
   _ ->
     throwError $ CustomFailure (RenameForall b) "the focused expression is not a forall type"
-
--- Check that a name is fresh for an expression. I.e. it does not
--- occur as a free variables, and thus binding it will not capture
--- a variable.
--- However, it may shadow a binding in more global scope that happens not to
--- be used in the expression, or a binding in the expression may shadow the
--- name.
-isFresh :: Name -> Expr -> Bool
-isFresh v e = v `S.notMember` freeVars e
-
-isFreshTy :: Name -> Type -> Bool
-isFreshTy v t = v `S.notMember` freeVarsTy t
-
--- We make a fresh name that is appropriate for binding here (i.e. wrapping the
--- target of the zipper).
--- To avoid variable capture we must avoid any name free in the focussed expr;
--- this is important for correctness.
--- To avoid shadowing any other variable we should avoid any more-globally bound
--- name (i.e. "up" in the zipper); this is not a correctness concern, but a
--- usability concern: we don't want automatically generated names inducing
--- shadowing.
--- To avoid being shadowed we should avoid any names bound in the focussed
--- expr; this is also a usability concern only.
---
--- NB: the free names of the target are a subset of the more-globally bound
--- names, so we don't need to explicitly worry about them.
---
--- Because of implementation details, locally bound variables are in a
--- different namespace than top-level definitions and from term/type
--- constructors. However, for the sake of non-confusingness, we don't care
--- about that here. Thus when we avoid more-globally bound names, we will also
--- include globally-scoped things.
-mkFreshName :: ActionM m => ExprZ -> m Name
-mkFreshName e = freshName =<< mkAvoidForFreshName e
-
-mkAvoidForFreshName :: MonadReader TC.Cxt m => ExprZ -> m (S.Set Name)
-mkAvoidForFreshName e = do
-  let moreGlobal = bindersAbove e
-      moreLocal = bindersBelow e
-  globals <- TC.getGlobalNames
-  pure $ S.unions [moreGlobal, moreLocal, globals]
-
-mkFreshNameTy :: ActionM m => TypeZ -> m Name
-mkFreshNameTy t = freshName =<< mkAvoidForFreshNameTy t
-
-mkAvoidForFreshNameTy :: MonadReader TC.Cxt m => TypeZ -> m (S.Set Name)
-mkAvoidForFreshNameTy t = do
-  let moreGlobal = bindersAboveTypeZ t
-      moreLocal = bindersBelowTy $ focusOnlyType t
-  globals <- TC.getGlobalNames
-  pure $ S.unions [moreGlobal, moreLocal, globals]
diff --git a/primer/src/Primer/Action/Available.hs b/primer/src/Primer/Action/Available.hs
new file mode 100644
index 000000000..d32f95ce6
--- /dev/null
+++ b/primer/src/Primer/Action/Available.hs
@@ -0,0 +1,723 @@
+{-# LANGUAGE NamedFieldPuns #-}
+
+-- | Compute all the possible actions which can be performed on a definition
+module Primer.Action.Available (
+  actionsForDef,
+  actionsForDefBody,
+  actionsForDefSig,
+) where
+
+import Foreword
+
+import qualified Data.List.NonEmpty as NE
+import Optics (
+  set,
+  to,
+  (%),
+  (^.),
+  (^?),
+  _Just,
+ )
+import Primer.Action (
+  Action (..),
+  ActionInput (..),
+  ActionName (..),
+  ActionType (..),
+  FunctionFiltering (..),
+  Level (..),
+  Movement (..),
+  OfferedAction (..),
+  ProgAction (..),
+  UserInput (..),
+  nameString,
+  uniquifyDefName,
+ )
+import qualified Primer.Action.Priorities as P
+import Primer.Core (
+  Bind' (..),
+  CaseBranch' (..),
+  Def (..),
+  Expr,
+  Expr' (..),
+  ExprMeta,
+  ID,
+  Kind,
+  Meta (..),
+  Type,
+  Type' (..),
+  TypeCache (..),
+  _bindMeta,
+  _chkedAt,
+  _exprMetaLens,
+  _id,
+  _synthed,
+  _type,
+  _typeMeta,
+  _typeMetaLens,
+ )
+import Primer.Core.Transform (unfoldFun)
+import Primer.Name (unName)
+import Primer.Questions (Question (..))
+
+-- | An AST node tagged with its "sort" - i.e. if it's a type or expression or binding etc.
+-- This is probably useful elsewhere, but we currently just need it here
+data SomeNode a b
+  = ExprNode (Expr' (Meta a) (Meta b))
+  | TypeNode (Type' (Meta b))
+  | -- | If/when we model all bindings with 'Bind'', we will want to generalise this.
+    CaseBindNode (Bind' (Meta a))
+
+actionsForDef ::
+  Level ->
+  -- | only used to generate a unique name for a duplicate definition
+  Map ID Def ->
+  Def ->
+  [OfferedAction [ProgAction]]
+actionsForDef l defs def =
+  [ OfferedAction
+      { name = Prose "r"
+      , description = "Rename this definition"
+      , input =
+          InputRequired $
+            ChooseOrEnterName
+              ("Enter a new " <> nameString <> " for the definition")
+              []
+              (\name -> [RenameDef (defID def) (unName name)])
+      , priority = P.rename l
+      , actionType = Primary
+      }
+  , OfferedAction
+      { name = Prose "d"
+      , description = "Duplicate this definition"
+      , input =
+          let sigID = defType def ^. _typeMetaLens % _id
+
+              bodyID = defExpr def ^. _exprMetaLens % _id
+
+              copyName = uniquifyDefName (unName (defName def) <> "Copy") defs
+           in NoInputRequired
+                [ CreateDef (Just copyName)
+                , CopyPasteSig (defID def, sigID) []
+                , CopyPasteBody (defID def, bodyID) []
+                ]
+      , priority = P.duplicate l
+      , actionType = Primary
+      }
+  , OfferedAction
+      { name = Prose "⌫"
+      , description = "Delete this definition"
+      , input = NoInputRequired [DeleteDef $ defID def]
+      , priority = P.delete l
+      , actionType = Destructive
+      }
+  ]
+
+-- | Given the body of a Def and the ID of a node in it, return the possible actions that can be applied to it
+actionsForDefBody ::
+  Level ->
+  Def ->
+  ID ->
+  Expr ->
+  [OfferedAction [ProgAction]]
+actionsForDefBody l def id expr =
+  let toProgAction actions = [MoveToDef (defID def), BodyAction actions]
+
+      raiseAction' =
+        OfferedAction
+          { name = Prose "↑"
+          , description = "Replace parent with this subtree"
+          , input = NoInputRequired [MoveToDef (defID def), CopyPasteBody (defID def, id) [SetCursor id, Move Parent, Delete]]
+          , priority = P.raise l
+          , actionType = Destructive
+          }
+   in case findNodeWithParent id expr of
+        Nothing -> mempty
+        Just (ExprNode e, p) ->
+          let raiseAction = case p of
+                Nothing -> [] -- at root already, cannot raise
+                Just (ExprNode (Hole _ _)) -> [] -- in a NE hole, don't offer raise (as hole will probably just be recreated)
+                _ -> [raiseAction']
+           in (toProgAction <<$>> basicActionsForExpr l (defID def) e) <> raiseAction
+        Just (TypeNode t, p) ->
+          let raiseAction = case p of
+                Just (ExprNode _) -> [] -- at the root of an annotation, so cannot raise
+                _ -> [raiseAction']
+           in ( toProgAction
+                  <<$>> (basicActionsForType l (defID def) t <> compoundActionsForType l t)
+              )
+                <> raiseAction
+        Just (CaseBindNode b, _) -> toProgAction <<$>> actionsForBinding l (defID def) b
+
+-- | Given a Type and the ID of a node in it, return the possible actions that can be applied to it
+actionsForDefSig ::
+  Level ->
+  Def ->
+  ID ->
+  Type ->
+  [OfferedAction [ProgAction]]
+actionsForDefSig l def id ty =
+  let toProgAction actions = [MoveToDef (defID def), SigAction actions]
+
+      raiseAction =
+        [ OfferedAction
+          { name = Prose "↑"
+          , description = "Replace parent with this subtree"
+          , input = NoInputRequired [MoveToDef (defID def), CopyPasteSig (defID def, id) [SetCursor id, Move Parent, Delete]]
+          , priority = P.raise l
+          , actionType = Destructive
+          }
+        | id /= defType def ^. _typeMetaLens % _id
+        ]
+   in case findType id ty of
+        Nothing -> mempty
+        Just t ->
+          ( toProgAction
+              <<$>> (basicActionsForType l (defID def) t <> compoundActionsForType l t)
+          )
+            <> raiseAction
+
+-- | Bindings support just one action: renaming.
+actionsForBinding ::
+  Level ->
+  ID ->
+  Bind' (Meta (Maybe TypeCache)) ->
+  [OfferedAction [Action]]
+actionsForBinding l defId b =
+  realise
+    b
+    (b ^. _bindMeta)
+    [ \_p m' ->
+        OfferedAction
+          { name = Prose "r"
+          , description = "Rename this pattern variable"
+          , input =
+              actionWithNames
+                defId
+                (Left $ b ^? _bindMeta % _type % _Just % _chkedAt)
+                (\n -> [RenameCaseBinding n])
+                m'
+                ("Choose a new " <> nameString <> " for the pattern variable")
+          , priority = P.rename l
+          , actionType = Primary
+          }
+    ]
+
+-- | Find a node in the AST by its ID, and also return its parent
+findNodeWithParent :: forall a b. ID -> Expr' (Meta a) (Meta b) -> Maybe (SomeNode a b, Maybe (SomeNode a b))
+findNodeWithParent id x = go x Nothing
+  where
+    go expr parent
+      | expr ^. _exprMetaLens % _id == id = Just (ExprNode expr, parent)
+      | otherwise = case expr of
+        Hole _ e -> go e (Just (ExprNode expr))
+        EmptyHole _ -> Nothing
+        Ann _ e t -> go e (Just (ExprNode expr)) <|> goTy t expr
+        App _ a b -> go a (Just (ExprNode expr)) <|> go b (Just (ExprNode expr))
+        APP _ a b -> go a (Just (ExprNode expr)) <|> goTy b expr
+        Con _ _ -> Nothing
+        Lam _ _ e -> go e (Just (ExprNode expr))
+        LAM _ _ e -> go e (Just (ExprNode expr))
+        Var _ _ -> Nothing
+        GlobalVar _ _ -> Nothing
+        Let _ _ a b -> go a (Just (ExprNode expr)) <|> go b (Just (ExprNode expr))
+        Letrec _ _ a ta b -> go a (Just (ExprNode expr)) <|> goTy ta expr <|> go b (Just (ExprNode expr))
+        LetType _ _ t e -> goTy t expr <|> go e (Just (ExprNode expr))
+        Case _ e branches ->
+          let (Alt inBranches) = flip foldMap branches $
+                \(CaseBranch _ binds rhs) ->
+                  Alt (go rhs (Just (ExprNode expr)))
+                    <> foldMap (Alt . map (\b -> (CaseBindNode b, Just (ExprNode expr))) . findBind id) binds
+           in go e (Just (ExprNode expr)) <|> inBranches
+
+    goTy t p = case findTypeWithParent id t of
+      Nothing -> Nothing
+      Just (t', Nothing) -> Just (TypeNode t', Just (ExprNode p))
+      Just (t', Just p') -> Just (TypeNode t', Just (TypeNode p'))
+
+-- | Find a sub-type in a larger type by its ID.
+findType :: forall b. ID -> Type' (Meta b) -> Maybe (Type' (Meta b))
+findType id ty
+  | ty ^. _typeMetaLens % _id == id = Just ty
+  | otherwise = case ty of
+    TEmptyHole _ -> Nothing
+    THole _ t -> findType id t
+    TCon _ _ -> Nothing
+    TVar _ _ -> Nothing
+    TFun _ a b -> findType id a <|> findType id b
+    TApp _ a b -> findType id a <|> findType id b
+    TForall _ _ _ t -> findType id t
+
+-- | Find a sub-type in a larger type by its ID. Also returning its parent
+findTypeWithParent :: forall b. ID -> Type' (Meta b) -> Maybe (Type' (Meta b), Maybe (Type' (Meta b)))
+findTypeWithParent id x = go x Nothing
+  where
+    go ty parent
+      | ty ^. _typeMetaLens % _id == id = Just (ty, parent)
+      | otherwise = case ty of
+        TEmptyHole _ -> Nothing
+        THole _ t -> go t (Just ty)
+        TCon _ _ -> Nothing
+        TVar _ _ -> Nothing
+        TFun _ a b -> go a (Just ty) <|> go b (Just ty)
+        TApp _ a b -> go a (Just ty) <|> go b (Just ty)
+        TForall _ _ _ t -> go t (Just ty)
+
+-- | If the given binding has the given ID, return Just that binding, otherwise return nothing.
+-- This is just a helper for 'findNode'.
+findBind :: forall c. ID -> Bind' (Meta c) -> Maybe (Bind' (Meta c))
+findBind id bind
+  | bind ^. _bindMeta % _id == id = Just bind
+  | otherwise = Nothing
+
+-- | An ActionSpec is an OfferedAction that needs
+-- metadata in order to be used. Typically this is because it starts with
+-- SetCursor, which needs an ID.
+--
+-- Type parameter 'p' is a ghost parameter that provides some type
+-- safety, to prevent the accidental mixing of actions for different
+-- types (e.g., to prevent the mixing of actions for 'Expr's and
+-- 'Type's). The argument of type 'p' in the type signature is not
+-- used other than to provide proof that you have a value of type 'p'.
+type ActionSpec p a =
+  p -> Meta a -> OfferedAction [Action]
+
+-- | From multiple actions, construct an ActionSpec which starts with SetCursor
+action :: forall a p. ActionName -> Text -> Int -> ActionType -> [Action] -> ActionSpec p a
+action name description priority actionType as _p m =
+  OfferedAction
+    { name
+    , description
+    , input = NoInputRequired $ SetCursor (m ^. _id) : as
+    , priority
+    , actionType
+    }
+
+-- | Construct an ActionSpec which requires some input, and then starts with SetCursor
+actionWithInput :: forall a p. ActionName -> Text -> Int -> ActionType -> UserInput [Action] -> ActionSpec p a
+actionWithInput name description priority actionType input _p m =
+  OfferedAction
+    { name
+    , description
+    , input = InputRequired $ map (\as -> SetCursor (m ^. _id) : as) input
+    , priority
+    , actionType
+    }
+
+-- | Construct an ActionSpec which requires the user to select from a bunch of
+-- generated names for the current location (or specify their own), and starts
+-- with SetCursor. Requires the definition id (not the node's id: that is
+-- controlled by the ActionSpec)
+actionWithNames ::
+  forall a.
+  ID ->
+  Either (Maybe (Type' ())) (Maybe Kind) ->
+  (Text -> [Action]) ->
+  Meta a ->
+  Text ->
+  ActionInput [Action]
+actionWithNames defId tk k m prompt =
+  AskQuestion (GenerateName defId (m ^. _id) tk) $ \options ->
+    InputRequired $
+      ChooseOrEnterName
+        prompt
+        options
+        (\n -> SetCursor (m ^. _id) : k (unName n))
+
+-- | A set of ActionSpecs can be realised by providing them with metadata.
+realise :: forall a p. p -> Meta a -> [ActionSpec p a] -> [OfferedAction [Action]]
+realise p m = map (\a -> a p m)
+
+-- | Given an expression, determine what basic actions it supports
+-- Specific projections may provide other actions not listed here
+basicActionsForExpr :: Level -> ID -> Expr -> [OfferedAction [Action]]
+basicActionsForExpr l defID expr = case expr of
+  EmptyHole m -> realise expr m $ universalActions m <> emptyHoleActions m
+  Hole m _ -> realise expr m $ defaultActions m <> holeActions
+  Ann m _ _ -> realise expr m $ defaultActions m <> annotationActions
+  Lam m _ _ -> realise expr m $ defaultActions m <> lambdaActions m
+  LAM m _ _ -> realise expr m $ defaultActions m <> bigLambdaActions m
+  Let m _ e _ -> realise expr m $ defaultActions m <> letActions (e ^? _exprMetaLens % _type % _Just % _synthed)
+  Letrec m _ _ t _ -> realise expr m $ defaultActions m <> letRecActions (Just t)
+  e -> realise expr (e ^. _exprMetaLens) $ defaultActions (e ^. _exprMetaLens)
+  where
+    insertVariable =
+      let filterVars = case l of
+            Beginner -> NoFunctions
+            _ -> Everything
+       in actionWithInput (Code "x") "Use a variable" (P.useVar l) Primary $
+            ChooseVariable filterVars $ \case
+              Left name -> [ConstructVar name]
+              Right id_ -> [ConstructGlobalVar id_]
+
+    -- If we have a useful type, offer the refine action, otherwise offer the
+    offerRefined :: ExprMeta -> Bool
+    offerRefined m = case m ^? _type % _Just % _chkedAt of
+      Just (TEmptyHole _) -> False
+      Just (THole _ _) -> False
+      Just _ -> True
+      _ -> False
+
+    -- NB: Exactly one of the saturated and refined actions will be available
+    -- (depending on whether we have useful type information to hand).
+    -- We put the same labels on each.
+    insertVariableSaturatedRefined :: forall a. ExprMeta -> ActionSpec Expr a
+    insertVariableSaturatedRefined m =
+      actionWithInput (Code "f $ ?") "Apply a function to arguments" (P.useFunction l) Primary $
+        ChooseVariable OnlyFunctions $ \case
+          Left name -> [if offerRefined m then InsertRefinedVar name else InsertSaturatedVar name]
+          Right id_ -> [if offerRefined m then InsertRefinedGlobalVar id_ else InsertSaturatedGlobalVar id_]
+
+    annotateExpression :: forall a. ActionSpec Expr a
+    annotateExpression = action (Code ":") "Annotate this expression with a type" (P.annotateExpr l) Primary [ConstructAnn]
+
+    applyFunction :: forall a. ActionSpec Expr a
+    applyFunction = action (Code "$") "Apply function" (P.applyFunction l) Primary [ConstructApp, Move Child2]
+
+    applyType :: forall a. ActionSpec Expr a
+    applyType = action (Code "@") "Apply type" (P.applyType l) Destructive [ConstructAPP, EnterType]
+
+    patternMatch :: forall a. ActionSpec Expr a
+    patternMatch = action (Code "m") patternMatchProse (P.makeCase l) Destructive [ConstructCase]
+
+    patternMatchProse = case l of
+      Beginner -> "Match a variable with its value"
+      Intermediate -> "Match a variable with its value"
+      Expert -> "Pattern match"
+
+    makeLambda :: forall a. Meta (Maybe TypeCache) -> ActionSpec Expr a
+    makeLambda m _p m' =
+      OfferedAction
+        { name = Code "λx"
+        , description = "Make a function with an input"
+        , input =
+            actionWithNames
+              defID
+              (Left $ join $ m ^? _type % _Just % _chkedAt % to lamVarTy)
+              (\n -> [ConstructLam $ Just n])
+              m'
+              ("Choose a " <> nameString <> " for the input variable")
+        , priority = P.makeLambda l
+        , actionType = Primary
+        }
+
+    makeTypeAbstraction :: forall a. ExprMeta -> ActionSpec Expr a
+    makeTypeAbstraction m _p m' =
+      OfferedAction
+        { name = Code "Λx"
+        , description = "Make a type abstraction"
+        , input =
+            actionWithNames
+              defID
+              (Right $ join $ m ^? _type % _Just % _chkedAt % to lAMVarKind)
+              (\n -> [ConstructLAM $ Just n])
+              m'
+              ("Choose a " <> nameString <> " for the bound type variable")
+        , priority = P.makeTypeAbstraction l
+        , actionType = Primary
+        }
+
+    useValueConstructor :: forall a. ActionSpec Expr a
+    useValueConstructor =
+      let filterCtors = case l of
+            Beginner -> NoFunctions
+            _ -> Everything
+       in actionWithInput
+            (Code "V")
+            "Use a value constructor"
+            (P.useValueCon l)
+            Primary
+            $ ChooseConstructor filterCtors (\c -> [ConstructCon c])
+
+    -- NB: Exactly one of the saturated and refined actions will be available
+    -- (depending on whether we have useful type information to hand).
+    -- We put the same labels on each.
+    useSaturatedRefinedValueConstructor :: forall a. ExprMeta -> ActionSpec Expr a
+    useSaturatedRefinedValueConstructor m =
+      actionWithInput
+        (Code "V $ ?")
+        "Apply a value constructor to arguments"
+        (P.useSaturatedValueCon l)
+        Primary
+        $ ChooseConstructor OnlyFunctions (\c -> [if offerRefined m then ConstructRefinedCon c else ConstructSaturatedCon c])
+
+    makeLetBinding :: forall a. ActionSpec Expr a
+    makeLetBinding _p m' =
+      OfferedAction
+        { name = Code "="
+        , description = "Make a let binding"
+        , input =
+            actionWithNames
+              defID
+              (Left Nothing)
+              (\n -> [ConstructLet $ Just n])
+              m'
+              ("Choose a " <> nameString <> " for the new let binding")
+        , priority = P.makeLet l
+        , actionType = Primary
+        }
+
+    makeLetrec :: forall a. ActionSpec Expr a
+    makeLetrec _p m' =
+      OfferedAction
+        { name = Code "=,="
+        , description = "Make a recursive let binding"
+        , input =
+            actionWithNames
+              defID
+              (Left Nothing)
+              (\n -> [ConstructLetrec $ Just n])
+              m'
+              ("Choose a " <> nameString <> " for the new let binding")
+        , priority = P.makeLetrec l
+        , actionType = Primary
+        }
+
+    enterHole :: forall a. ActionSpec Expr a
+    enterHole = action (Prose "h") "Make this hole into a non-empty hole" (P.enterHole l) Primary [EnterHole]
+
+    finishHole :: forall a. ActionSpec Expr a
+    finishHole = action (Prose "e") "Convert this into a normal expression" (P.finishHole l) Primary [FinishHole]
+
+    removeAnnotation :: forall a. ActionSpec Expr a
+    removeAnnotation = action (Prose "⌫:") "Remove this annotation" (P.removeAnnotation l) Destructive [RemoveAnn]
+
+    renameVariable :: forall a. ExprMeta -> ActionSpec Expr a
+    renameVariable m _p m' =
+      OfferedAction
+        { name = Prose "r"
+        , description = "Rename this input variable"
+        , input =
+            actionWithNames
+              defID
+              (Left $ join $ m ^? _type % _Just % _chkedAt % to lamVarTy)
+              (\n -> [RenameLam n])
+              m'
+              ("Choose a new " <> nameString <> " for the input variable")
+        , priority = P.rename l
+        , actionType = Primary
+        }
+
+    renameTypeVariable :: forall a. ExprMeta -> ActionSpec Expr a
+    renameTypeVariable m _p m' =
+      OfferedAction
+        { name = Prose "r"
+        , description = "Rename this type variable"
+        , input =
+            actionWithNames
+              defID
+              (Right $ join $ m ^? _type % _Just % _chkedAt % to lAMVarKind)
+              (\n -> [RenameLAM n])
+              m'
+              ("Choose a new " <> nameString <> " for the type variable")
+        , priority = P.rename l
+        , actionType = Primary
+        }
+
+    makeLetRecursive :: forall a. ActionSpec Expr a
+    makeLetRecursive = action (Prose "rec") "Make this let recursive" (P.makeLetRecursive l) Primary [ConvertLetToLetrec]
+
+    renameLet :: forall a b. Maybe (Type' b) -> ActionSpec Expr a
+    renameLet t _p m' =
+      OfferedAction
+        { name = Prose "r"
+        , description = "Rename this let binding"
+        , input =
+            actionWithNames
+              defID
+              (Left $ set (_Just % _typeMeta) () t)
+              (\n -> [RenameLet n])
+              m'
+              ("Choose a new " <> nameString <> " for the let binding")
+        , priority = P.rename l
+        , actionType = Primary
+        }
+
+    deleteExpr :: forall a. ActionSpec Expr a
+    deleteExpr = action (Prose "⌫") "Delete this expression" (P.delete l) Destructive [Delete]
+
+    emptyHoleActions :: forall a. ExprMeta -> [ActionSpec Expr a]
+    emptyHoleActions m = case l of
+      Beginner ->
+        [ insertVariable
+        , useValueConstructor
+        ]
+      _ ->
+        [ insertVariable
+        , insertVariableSaturatedRefined m
+        , useValueConstructor
+        , useSaturatedRefinedValueConstructor m
+        , makeLetBinding
+        , makeLetrec
+        , enterHole
+        ]
+
+    holeActions :: forall a. [ActionSpec Expr a]
+    holeActions = [finishHole]
+
+    annotationActions :: forall a. [ActionSpec Expr a]
+    annotationActions = case l of
+      Beginner -> []
+      Intermediate -> []
+      Expert -> [removeAnnotation]
+
+    lambdaActions :: forall a. ExprMeta -> [ActionSpec Expr a]
+    lambdaActions m = [renameVariable m]
+
+    bigLambdaActions :: forall a. ExprMeta -> [ActionSpec Expr a]
+    bigLambdaActions m = case l of
+      Beginner -> []
+      Intermediate -> []
+      Expert -> [renameTypeVariable m]
+
+    letActions :: forall a b. Maybe (Type' b) -> [ActionSpec Expr a]
+    letActions t =
+      [ renameLet t
+      , makeLetRecursive
+      ]
+
+    letRecActions :: forall a b. Maybe (Type' b) -> [ActionSpec Expr a]
+    letRecActions t = [renameLet t]
+
+    -- Actions for every expression node
+    universalActions :: forall a. ExprMeta -> [ActionSpec Expr a]
+    universalActions m = case l of
+      Beginner ->
+        [ makeLambda m
+        , patternMatch
+        ]
+      Intermediate ->
+        [ makeLambda m
+        , patternMatch
+        , applyFunction
+        ]
+      Expert ->
+        [ annotateExpression
+        , applyFunction
+        , applyType
+        , patternMatch
+        , makeLambda m
+        , makeTypeAbstraction m
+        ]
+
+    -- Extract the source of the function type we were checked at
+    -- i.e. the type that a lambda-bound variable would have here
+    lamVarTy :: Type' () -> Maybe (Type' ())
+    lamVarTy = \case
+      TFun _ s _ -> pure s
+      _ -> Nothing
+
+    -- Extract the kind a forall-bound variable would have here
+    lAMVarKind :: Type' () -> Maybe Kind
+    lAMVarKind = \case
+      TForall _ _ k _ -> Just k
+      _ -> Nothing
+
+    -- Actions for every expression node except holes and annotations
+    defaultActions :: forall a. ExprMeta -> [ActionSpec Expr a]
+    defaultActions m = universalActions m <> [deleteExpr]
+
+-- | Given a type, determine what basic actions it supports
+-- Specific projections may provide other actions not listed here
+basicActionsForType :: Level -> ID -> Type -> [OfferedAction [Action]]
+basicActionsForType l defID ty = case ty of
+  TEmptyHole m -> realise ty m $ universalActions <> emptyHoleActions
+  TForall m _ k _ -> realise ty m $ defaultActions <> forAllActions k
+  t -> realise ty (t ^. _typeMetaLens) defaultActions
+  where
+    -- We arbitrarily choose that the "construct a function type" action places the focused expression
+    -- on the domain (left) side of the arrow.
+    constructFunctionType :: forall a. ActionSpec Type a
+    constructFunctionType = action (Code "→") "Construct a function type" (P.constructFunction l) Primary [ConstructArrowL, Move Child1]
+
+    constructPolymorphicType :: forall a. ActionSpec Type a
+    constructPolymorphicType _p m' =
+      OfferedAction
+        { name = Code "∀"
+        , description = "Construct a polymorphic type"
+        , input =
+            actionWithNames
+              defID
+              (Right Nothing)
+              (\n -> [ConstructTForall (Just n), Move Child1])
+              m'
+              ("Choose a " <> nameString <> " for the bound type variable")
+        , priority = P.constructForall l
+        , actionType = Primary
+        }
+
+    constructTypeApplication :: forall a. ActionSpec Type a
+    constructTypeApplication = action (Code "$") "Construct a type application" (P.constructTypeApp l) Primary [ConstructTApp, Move Child1]
+
+    useTypeConstructor :: forall a. ActionSpec Type a
+    useTypeConstructor = actionWithInput (Code "T") "Use a type constructor" (P.useTypeCon l) Primary $ ChooseTypeConstructor (\t -> [ConstructTCon t])
+
+    useTypeVariable :: forall a. ActionSpec Type a
+    useTypeVariable = actionWithInput (Code "t") "Use a type variable" (P.useTypeVar l) Primary $ ChooseTypeVariable (\v -> [ConstructTVar v])
+
+    renameTypeVariable :: forall a. Kind -> ActionSpec Type a
+    renameTypeVariable k _p m' =
+      OfferedAction
+        { name = Prose "r"
+        , description = "Rename this type variable"
+        , input =
+            actionWithNames
+              defID
+              (Right $ Just k)
+              (\n -> [RenameForall n])
+              m'
+              ("Choose a new " <> nameString <> " for the bound type variable")
+        , priority = P.rename l
+        , actionType = Primary
+        }
+
+    deleteType :: forall a. ActionSpec Type a
+    deleteType = action (Prose "⌫") "Delete this type" (P.delete l) Destructive [Delete]
+
+    emptyHoleActions :: forall a. [ActionSpec Type a]
+    emptyHoleActions = case l of
+      Beginner -> [useTypeConstructor]
+      Intermediate -> [useTypeConstructor]
+      Expert ->
+        [ useTypeConstructor
+        , useTypeVariable
+        ]
+
+    forAllActions :: forall a. Kind -> [ActionSpec Type a]
+    forAllActions k = case l of
+      Beginner -> mempty
+      Intermediate -> mempty
+      Expert -> [renameTypeVariable k]
+
+    -- Actions for every type node
+    universalActions :: forall a. [ActionSpec Type a]
+    universalActions = case l of
+      Beginner -> [constructFunctionType]
+      Intermediate -> [constructFunctionType]
+      Expert ->
+        [ constructFunctionType
+        , constructPolymorphicType
+        , constructTypeApplication
+        ]
+
+    -- Actions for every type node except empty holes
+    defaultActions :: forall a. [ActionSpec Type a]
+    defaultActions = universalActions <> [deleteType]
+
+-- | These actions are more involved than the basic actions.
+-- They may involve moving around the AST and performing several basic actions.
+compoundActionsForType :: forall a. Level -> Type' (Meta a) -> [OfferedAction [Action]]
+compoundActionsForType l ty = case ty of
+  TFun m a b -> realise ty m [addFunctionArgument a b]
+  _ -> []
+  where
+    -- This action traverses the function type and adds a function arrow to the end of it,
+    -- resulting in a new argument type. The result type is unchanged.
+    -- The cursor location is also unchanged.
+    -- e.g. A -> B -> C ==> A -> B -> ? -> C
+    addFunctionArgument a b =
+      let (argTypes, _resultType) = unfoldFun a b
+
+          moveToLastArg = replicate (NE.length argTypes) (Move Child2)
+
+          moveBack = replicate (NE.length argTypes) (Move Parent)
+       in action (Code "→A→") "Add an input to this function" (P.addInput l) Primary $ moveToLastArg <> [ConstructArrowR] <> moveBack
diff --git a/primer/src/Primer/Action/Priorities.hs b/primer/src/Primer/Action/Priorities.hs
new file mode 100644
index 000000000..c42b2d433
--- /dev/null
+++ b/primer/src/Primer/Action/Priorities.hs
@@ -0,0 +1,144 @@
+-- | Action priorities. Smaller values are higher priority. They can
+-- be indexed by 'Level', but we currently don't use that
+-- functionality.
+--
+-- The values chosen here are relatively arbitrary, though we expect
+-- the higher priority actions to be used more often than lower
+-- priority actions. Exceptions to the rule are:
+--
+-- - 'makeCase': this is used very early in beginner lessons, so we
+-- make it easy to find near the top of the list. See
+-- https://github.com/hackworthltd/vonnegut/issues/786
+--
+-- - Delete: we always put this last, because it's destructive.
+--
+-- Expression actions.
+--
+-- For reference, the expectation is that variable,
+-- constructor-with-argument, and nullary constructor uses will be
+-- the most frequently used actions; followed by function
+-- application; then special forms like @case@, @let@, etc. Note
+-- that we put the @$@ variant of function application fairly low on
+-- the list because most of the time we expect students to use our
+-- special @f $ ?@ action, instead.
+--
+-- Besides the special case of 'delete' going last as mentioned
+-- above, we also make one other exception: 'makeLambda' goes first,
+-- because it's the first thing students will typically want to do
+-- when building a new definition's expression. (Arguably we should
+-- similarly promote 'makeTypeAbstraction' at intermediate and
+-- expert levels, but we don't currently implement this.)
+module Primer.Action.Priorities (
+  makeLambda,
+  useVar,
+  useValueCon,
+  makeCase,
+  useSaturatedValueCon,
+  useFunction,
+  makeLet,
+  makeLetRecursive,
+  makeLetrec,
+  applyFunction,
+  applyType,
+  makeTypeAbstraction,
+  annotateExpr,
+  removeAnnotation,
+  finishHole,
+  enterHole,
+
+  -- * Type actions.
+  constructFunction,
+  addInput,
+  useTypeVar,
+  useTypeCon,
+  constructTypeApp,
+  constructForall,
+
+  -- * Generic actions.
+  rename,
+  duplicate,
+  raise,
+  delete,
+) where
+
+import Foreword
+
+import Primer.Action (Level)
+
+makeLambda :: Level -> Int
+makeLambda _ = 5
+
+useVar :: Level -> Int
+useVar _ = 10
+
+useValueCon :: Level -> Int
+useValueCon _ = 11
+
+makeCase :: Level -> Int
+makeCase _ = 12
+
+useSaturatedValueCon :: Level -> Int
+useSaturatedValueCon _ = 13
+
+useFunction :: Level -> Int
+useFunction _ = 14
+
+makeLet :: Level -> Int
+makeLet _ = 21
+
+makeLetRecursive :: Level -> Int
+makeLetRecursive _ = 22
+
+makeLetrec :: Level -> Int
+makeLetrec _ = 23
+
+applyFunction :: Level -> Int
+applyFunction _ = 30
+
+applyType :: Level -> Int
+applyType _ = 40
+
+makeTypeAbstraction :: Level -> Int
+makeTypeAbstraction _ = 50
+
+annotateExpr :: Level -> Int
+annotateExpr _ = 51
+
+removeAnnotation :: Level -> Int
+removeAnnotation _ = 52
+
+finishHole :: Level -> Int
+finishHole _ = 500
+
+enterHole :: Level -> Int
+enterHole _ = 501
+
+constructFunction :: Level -> Int
+constructFunction _ = 5
+
+addInput :: Level -> Int
+addInput _ = 6
+
+useTypeVar :: Level -> Int
+useTypeVar _ = 10
+
+useTypeCon :: Level -> Int
+useTypeCon _ = 11
+
+constructTypeApp :: Level -> Int
+constructTypeApp _ = 20
+
+constructForall :: Level -> Int
+constructForall _ = 40
+
+rename :: Level -> Int
+rename _ = 200
+
+duplicate :: Level -> Int
+duplicate _ = 201
+
+raise :: Level -> Int
+raise _ = 300
+
+delete :: Level -> Int
+delete _ = maxBound
diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs
index d115a1c8a..8055f8729 100644
--- a/primer/src/Primer/App.hs
+++ b/primer/src/Primer/App.hs
@@ -58,20 +58,21 @@ import Data.Generics.Uniplate.Zipper (
  )
 import qualified Data.Map.Strict as Map
 import qualified Data.Set as Set
-import Optics (Lens', re, traverseOf, view, (%), (.~), (^.), _Left, _Right)
+import Optics (re, traverseOf, view, (%), (.~), (^.), _Left, _Right)
 import Primer.Action (
   Action,
   ActionError (IDNotFound),
+  ProgAction (..),
   applyActionsToBody,
   applyActionsToTypeSig,
  )
+
 import Primer.Core (
   Def (..),
   Expr,
   Expr' (EmptyHole, Var),
   ExprMeta,
   ID (..),
-  Kind,
   Meta (..),
   Type,
   Type' (TEmptyHole, TVar),
@@ -80,9 +81,11 @@ import Primer.Core (
   defaultTypeDefs,
   getID,
   _exprMeta,
+  _exprMetaLens,
   _exprTypeMeta,
   _id,
   _typeMeta,
+  _typeMetaLens,
  )
 import Primer.Eval (EvalDetail, EvalError)
 import qualified Primer.Eval as Eval
@@ -90,6 +93,7 @@ import Primer.EvalFull (Dir, EvalFullError (TimedOut), TerminationBound, evalFul
 import Primer.JSON
 import Primer.Name (Name, NameCounter, freshName, unsafeMkName)
 import Primer.Questions (
+  Question (..),
   generateNameExpr,
   generateNameTy,
   variablesInScopeExpr,
@@ -198,53 +202,6 @@ data MutationRequest
   deriving (Eq, Show, Generic)
   deriving (FromJSON, ToJSON) via VJSON MutationRequest
 
--- | The type of questions which return information about the program, but do not
--- modify it.
-data Question a where
-  -- Given the ID of a definition and the ID of a type or expression in that
-  -- definition, what variables are in scope at the expression?
-  -- Nested pairs: to make serialisation to PS work easily
-  VariablesInScope :: ID -> ID -> Question (([(Name, Kind)], [(Name, Type' ())]), [(ID, Name, Type' ())])
-  GenerateName ::
-    ID ->
-    ID ->
-    Either (Maybe (Type' ())) (Maybe Kind) ->
-    Question [Name]
-
--- | High level actions
--- These actions move around the whole program or modify definitions
-data ProgAction
-  = -- | Move the cursor to the definition with the given ID
-    MoveToDef ID
-  | -- | Rename the definition with the given ID
-    RenameDef ID Text
-  | -- | Create a new definition
-    CreateDef (Maybe Text)
-  | -- | Delete a new definition
-    DeleteDef ID
-  | -- | Add a new type definition
-    AddTypeDef TypeDef
-  | -- | Execute a sequence of actions on the body of the definition
-    BodyAction [Action]
-  | -- | Execute a sequence of actions on the type annotation of the definition
-    SigAction [Action]
-  | SetSmartHoles SmartHoles
-  | -- | CopyPaste (d,i) as
-    --   remembers the tree in def d, node i
-    --   runs actions as (in the currently selected def), which should end up in a hole
-    --   and then tries to paste the remembered subtree
-    --   This rather complex setup enables encoding 'raise' operations,
-    --     f s ~> f
-    --   where we remember f, then delete f s, then paste f back
-    --   as well as allowing cross-definition copy+paste
-    --   whilst letting the backend avoid remembering the 'copied' thing in some state.
-    --   The cursor is left on the root of the inserted subtree, which may or may not be inside a hole and/or annotation.
-    --   At the start of the actions, the cursor starts at the root of the definition's type/expression
-    CopyPasteSig (ID, ID) [Action]
-  | CopyPasteBody (ID, ID) [Action]
-  deriving (Eq, Show, Generic)
-  deriving (FromJSON, ToJSON) via VJSON ProgAction
-
 data ProgError
   = NoDefSelected
   | DefNotFound ID
@@ -888,9 +845,3 @@ copyPasteBody p (fromDefId, fromId) toDefId setup = do
       let newSel = NodeSelection BodyNode (getID $ target pasted) (pasted ^. _target % _exprMetaLens % re _Left)
       let finalProg = p{progDefs = newDefs, progSelection = Just (Selection newDef $ Just newSel)}
       tcWholeProg finalProg
-
-_typeMetaLens :: Lens' (Type' a) a
-_typeMetaLens = position @1
-
-_exprMetaLens :: Lens' (Expr' a b) a
-_exprMetaLens = position @1
diff --git a/primer/src/Primer/Core.hs b/primer/src/Primer/Core.hs
index 0f3d1f934..6e7859dcc 100644
--- a/primer/src/Primer/Core.hs
+++ b/primer/src/Primer/Core.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE OverloadedLabels #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE UndecidableInstances #-}
 
@@ -20,6 +21,8 @@ module Primer.Core (
   Type' (..),
   TypeCache (..),
   TypeCacheBoth (..),
+  _chkedAt,
+  _synthed,
   Kind (..),
   TypeDef (..),
   typeDefKind,
@@ -33,11 +36,15 @@ module Primer.Core (
   ExprMeta,
   TypeMeta,
   Meta (Meta),
+  _type,
   _exprMeta,
+  _exprMetaLens,
   _exprTypeMeta,
   _typeMeta,
+  _typeMetaLens,
   defaultTypeDefs,
   bindName,
+  _bindMeta,
 ) where
 
 import Foreword
@@ -47,7 +54,7 @@ import Data.Data (Data)
 import Data.Generics.Product
 import Data.Generics.Uniplate.Data ()
 import Data.Generics.Uniplate.Zipper (Zipper, hole, replaceHole)
-import Optics (Lens', Traversal, lens, set, view, (%))
+import Optics (AffineFold, Lens, Lens', Traversal, afailing, lens, set, view, (%))
 import Primer.JSON
 import Primer.Name (Name)
 
@@ -67,6 +74,11 @@ data Meta a = Meta ID a (Maybe Value)
   deriving (Generic, Eq, Show, Data, Functor)
   deriving (FromJSON, ToJSON) via VJSON (Meta a)
 
+-- | This lens is called 'type' because 'a' is most commonly a Type, but it will
+-- work for any 'a'.
+_type :: Lens (Meta a) (Meta b) a b
+_type = position @2
+
 -- | Typechecking will add metadata to each node describing its type.
 -- Some nodes are purely synthesised, some are purely checked, and some
 -- (the "embeddings") are both. These embeddings are synthesisable but in a
@@ -91,6 +103,18 @@ data TypeCacheBoth = TCBoth {tcChkedAt :: Type' (), tcSynthed :: Type' ()}
   deriving (Eq, Show, Generic, Data)
   deriving (FromJSON, ToJSON) via VJSON TypeCacheBoth
 
+--TODO `_chkedAt` and `_synthed` should be `AffineTraversal`s,
+-- but there is currently no `failing` for AffineTraversals, only for AffineFolds (`afailing`).
+-- See https://github.com/well-typed/optics/pull/393
+
+-- | An affine fold getting TCChkedAt or TCEmb's chked-at field
+_chkedAt :: AffineFold TypeCache (Type' ())
+_chkedAt = #_TCChkedAt `afailing` (#_TCEmb % #tcChkedAt)
+
+-- | An affine fold getting TCSynthed or TCEmb's synthed field
+_synthed :: AffineFold TypeCache (Type' ())
+_synthed = #_TCSynthed `afailing` (#_TCEmb % #tcSynthed)
+
 -- Expression metadata. Each expression is annotated with a type (populated by
 -- the typechecker). These types aren't part of the program so they themselves
 -- have no metadata - we indicate this with the '()' argument.
@@ -149,6 +173,12 @@ data Expr' a b
 _exprMeta :: forall a b c. Traversal (Expr' a b) (Expr' c b) a c
 _exprMeta = param @1
 
+-- | A lens on to the metadata of an expression.
+-- Note that unlike '_exprMeta', this is shallow i.e. it does not recurse in to sub-expressions.
+-- And for this reason, it cannot be type-changing.
+_exprMetaLens :: Lens' (Expr' a b) a
+_exprMetaLens = position @1
+
 -- | A traversal over the type metadata of an expression
 _exprTypeMeta :: forall a b c. Traversal (Expr' a b) (Expr' a c) b c
 _exprTypeMeta = param @0
@@ -178,6 +208,10 @@ data Bind' a = Bind a Name
 bindName :: Bind' a -> Name
 bindName (Bind _ n) = n
 
+-- | A type-modifying lens for the metadata of a Bind.
+_bindMeta :: forall a b. Lens (Bind' a) (Bind' b) a b
+_bindMeta = position @1
+
 -- | Core types.
 --  Type variables are currently represented as text, and we have no compile-time
 --  checks on scoping. We may want to introduce de Bruijn indices or use
@@ -204,6 +238,12 @@ data Type' a
 _typeMeta :: Traversal (Type' a) (Type' b) a b
 _typeMeta = param @0
 
+-- | A lens on to the metadata of a type.
+-- Note that unlike '_typeMeta', this is shallow i.e. it does not recurse in to sub-expressions.
+-- And for this reason, it cannot be type-changing.
+_typeMetaLens :: Lens' (Type' a) a
+_typeMetaLens = position @1
+
 -- | Core kinds.
 data Kind = KHole | KType | KFun Kind Kind
   deriving (Eq, Show, Data, Generic)
diff --git a/primer/src/Primer/Core/Transform.hs b/primer/src/Primer/Core/Transform.hs
index 30388dc36..c92e72fb2 100644
--- a/primer/src/Primer/Core/Transform.hs
+++ b/primer/src/Primer/Core/Transform.hs
@@ -4,6 +4,7 @@ module Primer.Core.Transform (
   renameTyVarExpr,
   unfoldApp,
   unfoldAPP,
+  unfoldFun,
   removeAnn,
 ) where
 
@@ -11,6 +12,7 @@ import Foreword
 
 import Data.Data (Data)
 import Data.Generics.Uniplate.Data (descendM)
+import qualified Data.List.NonEmpty as NE
 import Primer.Core (CaseBranch' (..), Expr' (..), Type' (..), bindName)
 import Primer.Name (Name)
 
@@ -88,6 +90,14 @@ unfoldAPP = second reverse . go
     go (APP _ f x) = let (g, args) = go f in (g, x : args)
     go e = (e, [])
 
+-- | Split a function type into an array of argument types and the result type.
+-- Takes two arguments: the lhs and rhs of the topmost function node.
+unfoldFun :: Type' a -> Type' a -> (NonEmpty (Type' a), Type' a)
+unfoldFun a (TFun _ b c) =
+  let (argTypes, resultType) = unfoldFun b c
+   in (NE.cons a argTypes, resultType)
+unfoldFun a t = (pure a, t)
+
 -- | Remove any outer annotations from an expression
 removeAnn :: Expr' a b -> Expr' a b
 removeAnn (Ann _ e _) = removeAnn e
diff --git a/primer/src/Primer/Name/Fresh.hs b/primer/src/Primer/Name/Fresh.hs
new file mode 100644
index 000000000..3c2653854
--- /dev/null
+++ b/primer/src/Primer/Name/Fresh.hs
@@ -0,0 +1,77 @@
+module Primer.Name.Fresh (
+  mkFreshName,
+  mkAvoidForFreshName,
+  mkFreshNameTy,
+  mkAvoidForFreshNameTy,
+  isFresh,
+  isFreshTy,
+) where
+
+import Foreword
+
+import Control.Monad.Fresh (MonadFresh)
+import qualified Data.Set as S
+import Primer.Core (Expr, Type)
+import Primer.Name (Name, NameCounter, freshName)
+import Primer.Subst (freeVars, freeVarsTy)
+import qualified Primer.Typecheck as TC
+import Primer.Zipper (
+  ExprZ,
+  TypeZ,
+  bindersAbove,
+  bindersAboveTypeZ,
+  bindersBelow,
+  bindersBelowTy,
+  focusOnlyType,
+ )
+
+-- Check that a name is fresh for an expression. I.e. it does not
+-- occur as a free variables, and thus binding it will not capture
+-- a variable.
+-- However, it may shadow a binding in more global scope that happens not to
+-- be used in the expression, or a binding in the expression may shadow the
+-- name.
+isFresh :: Name -> Expr -> Bool
+isFresh v e = v `S.notMember` freeVars e
+
+isFreshTy :: Name -> Type -> Bool
+isFreshTy v t = v `S.notMember` freeVarsTy t
+
+-- We make a fresh name that is appropriate for binding here (i.e. wrapping the
+-- target of the zipper).
+-- To avoid variable capture we must avoid any name free in the focussed expr;
+-- this is important for correctness.
+-- To avoid shadowing any other variable we should avoid any more-globally bound
+-- name (i.e. "up" in the zipper); this is not a correctness concern, but a
+-- usability concern: we don't want automatically generated names inducing
+-- shadowing.
+-- To avoid being shadowed we should avoid any names bound in the focussed
+-- expr; this is also a usability concern only.
+--
+-- NB: the free names of the target are a subset of the more-globally bound
+-- names, so we don't need to explicitly worry about them.
+--
+-- Because of implementation details, locally bound variables are in a
+-- different namespace than top-level definitions and from term/type
+-- constructors. However, for the sake of non-confusingness, we don't care
+-- about that here. Thus when we avoid more-globally bound names, we will also
+-- include globally-scoped things.
+mkFreshName :: (MonadFresh NameCounter m, MonadReader TC.Cxt m) => ExprZ -> m Name
+mkFreshName e = freshName =<< mkAvoidForFreshName e
+
+mkAvoidForFreshNameTy :: MonadReader TC.Cxt m => TypeZ -> m (S.Set Name)
+mkAvoidForFreshNameTy t = do
+  let moreGlobal = bindersAboveTypeZ t
+      moreLocal = bindersBelowTy $ focusOnlyType t
+  globals <- TC.getGlobalNames
+  pure $ S.unions [moreGlobal, moreLocal, globals]
+
+mkFreshNameTy :: (MonadFresh NameCounter m, MonadReader TC.Cxt m) => TypeZ -> m Name
+mkFreshNameTy t = freshName =<< mkAvoidForFreshNameTy t
+
+mkAvoidForFreshName :: MonadReader TC.Cxt m => ExprZ -> m (S.Set Name)
+mkAvoidForFreshName e = do
+  let moreGlobal = bindersAbove e
+      moreLocal = bindersBelow e
+  globals <- TC.getGlobalNames
+  pure $ S.unions [moreGlobal, moreLocal, globals]
diff --git a/primer/src/Primer/Questions.hs b/primer/src/Primer/Questions.hs
index 59e710fa8..4d12234ff 100644
--- a/primer/src/Primer/Questions.hs
+++ b/primer/src/Primer/Questions.hs
@@ -1,6 +1,9 @@
+{-# LANGUAGE GADTs #-}
+
 -- Logic for answering API questions
 
 module Primer.Questions (
+  Question (..),
   variablesInScopeExpr,
   variablesInScopeTy,
   ShadowedVarsExpr (..), -- only exported for testing
@@ -13,7 +16,6 @@ import Foreword
 
 import qualified Data.Map.Strict as Map
 import qualified Data.Set as Set
-import Primer.Action (mkAvoidForFreshName, mkAvoidForFreshNameTy)
 import Primer.Core (
   Def (..),
   ID,
@@ -22,6 +24,7 @@ import Primer.Core (
   TypeDef (typeDefNameHints),
  )
 import Primer.Name (Name, unName, unsafeMkName)
+import Primer.Name.Fresh (mkAvoidForFreshName, mkAvoidForFreshNameTy)
 import Primer.Typecheck (Cxt, decomposeTAppCon, getGlobalNames, typeDefs)
 import Primer.Zipper (
   ExprZ,
@@ -39,6 +42,19 @@ import Primer.ZipperCxt (
   variablesInScopeTy,
  )
 
+-- | The type of questions which return information about the program, but do not
+-- modify it.
+data Question a where
+  -- Given the ID of a definition and the ID of a type or expression in that
+  -- definition, what variables are in scope at the expression?
+  -- Nested pairs: to make serialisation to PS work easily
+  VariablesInScope :: ID -> ID -> Question (([(Name, Kind)], [(Name, Type' ())]), [(ID, Name, Type' ())])
+  GenerateName ::
+    ID ->
+    ID ->
+    Either (Maybe (Type' ())) (Maybe Kind) ->
+    Question [Name]
+
 -- | Collect the typing context for the focused node.
 -- We do this by walking back up the tree, collecting variables as we cross
 -- binders.
diff --git a/weeder.dhall b/weeder.dhall
index 75bbe4635..27598a9b7 100644
--- a/weeder.dhall
+++ b/weeder.dhall
@@ -1 +1,6 @@
-{ roots = [ "^Main.main$" ], type-class-roots = False }
+let
+    -- TODO remove these once this code (recently ported from old frontend) is exercised
+    tmpRoots =
+      [ "^Primer.Action.Available", "^Primer.Action.Priorities" ]
+
+in  { roots = [ "^Main.main$" ] # tmpRoots, type-class-roots = False }