---

"so no higher-order functions"

I think we can get read-time arity information for local variables, but only if our read-time arity information for the lambda syntax is detailed enough to tell us how to obtain the arity information for its parameter. For instance...

  -- To parse 3: We've completed an expression.
  3 =:: Expr
  
  -- To parse +: Parse an expression. Parse an expression. We've
  -- completed an expression.
  + =:: Expr -> Expr -> Expr
  
  -- To parse fn: Parse a variable. Parse an expression where that
  -- variable is parsed by (We've completed an expression.). We've
  -- completed an expression.
  fn =:: (arg : Var) -> LetArity arg Expr Expr -> Expr
  
  -- To parse letArity: Parse a variable. Parse an arity specification.
  -- Parse an expression where that variable is parsed by that arity
  -- specification. We've completed an expression.
  letArity =:: (arg : Var) -> Arity n -> LetArity arg n Expr -> Expr
  
  -- To parse arityExpr: We've completed a specification of arity
  -- (Expr).
  arityExpr =:: Arity Expr
  
  -- To parse arityArrow: Parse a specification of some arity m. Parse a
  -- specification of some arity n. We've completed a specification of
  -- arity (Parse according to arity specification m. We've completed a
  -- parse according to arity specification n.).
  arityArrow =:: Arity m -> Arity n -> Arity (m -> n)
  
  -- ...likewise for many of the other syntaxes I'm using in these arity
  -- specifications, which isn't to say they're all *easy* or even
  -- *possible* to specify in this metacircular way...