diff --git a/hugr-py/src/hugr/serialization/tys.py b/hugr-py/src/hugr/serialization/tys.py
index cea1a40cc..d3c562608 100644
--- a/hugr-py/src/hugr/serialization/tys.py
+++ b/hugr-py/src/hugr/serialization/tys.py
@@ -172,7 +172,7 @@ class SumType(RootModel):
 
 
 class Variable(BaseModel):
-    """A type variable identified by a de Bruijn index."""
+    """A type variable identified by an index into the array of TypeParams."""
 
     t: Literal["V"] = "V"
     i: int
@@ -189,6 +189,8 @@ class FunctionType(BaseModel):
     """A graph encoded as a value. It contains a concrete signature and a set of
     required resources."""
 
+    t: Literal["G"] = "G"
+
     input: "TypeRow"  # Value inputs of the function.
     output: "TypeRow"  # Value outputs of the function.
     # The extension requirements which are added by the operation
@@ -209,15 +211,12 @@ class Config:
 
 
 class PolyFuncType(BaseModel):
-    """A graph encoded as a value. It contains a concrete signature and a set of
-    required resources."""
-
-    t: Literal["G"] = "G"
+    """A polymorphic type scheme, i.e. of a FuncDecl, FuncDefn or OpDef.
+    (Nodes/operations in the Hugr are not polymorphic.)"""
 
     # The declared type parameters, i.e., these must be instantiated with the same
-    # number of TypeArgs before the function can be called. Note that within the body,
-    # variable (DeBruijn) index 0 is element 0 of this array, i.e. the variables are
-    # bound from right to left.
+    # number of TypeArgs before the function can be called. This defines the indices
+    # used for variables within the body.
     params: list[TypeParam]
 
     # Template for the function. May contain variables up to length of `params`
@@ -231,8 +230,8 @@ class Config:
         # Needed to avoid random '\n's in the pydantic description
         json_schema_extra = {
             "description": (
-                "A graph encoded as a value. It contains a concrete signature and "
-                "a set of required resources."
+                "A polymorphic type scheme, i.e. of a FuncDecl, FuncDefn or OpDef.  "
+                "(Nodes/operations in the Hugr are not polymorphic.)"
             )
         }
 
@@ -279,7 +278,7 @@ class Type(RootModel):
     """A HUGR type."""
 
     root: Annotated[
-        Qubit | Variable | USize | PolyFuncType | Array | SumType | Opaque,
+        Qubit | Variable | USize | FunctionType | Array | SumType | Opaque,
         WrapValidator(_json_custom_error_validator),
     ] = Field(discriminator="t")
 
diff --git a/hugr/src/extension.rs b/hugr/src/extension.rs
index a15dd66da..c1eca4225 100644
--- a/hugr/src/extension.rs
+++ b/hugr/src/extension.rs
@@ -17,9 +17,8 @@ use crate::ops;
 use crate::ops::custom::{ExtensionOp, OpaqueOp};
 use crate::types::type_param::{check_type_args, TypeArgError};
 use crate::types::type_param::{TypeArg, TypeParam};
-use crate::types::{
-    check_typevar_decl, CustomType, PolyFuncType, Substitution, TypeBound, TypeName,
-};
+use crate::types::FunctionType;
+use crate::types::{check_typevar_decl, CustomType, Substitution, TypeBound, TypeName};
 
 #[allow(dead_code)]
 mod infer;
@@ -163,14 +162,16 @@ pub enum SignatureError {
     /// A type variable that was used has not been declared
     #[error("Type variable {idx} was not declared ({num_decls} in scope)")]
     FreeTypeVar { idx: usize, num_decls: usize },
-    /// The type stored in a [LeafOp::TypeApply] is not what we compute from the
-    /// [ExtensionRegistry].
+    /// The result of the type application stored in a [Call]
+    /// is not what we get by applying the type-args to the polymorphic function
     ///
-    /// [LeafOp::TypeApply]: crate::ops::LeafOp::TypeApply
-    #[error("Incorrect result of type application - cached {cached} but expected {expected}")]
-    TypeApplyIncorrectCache {
-        cached: PolyFuncType,
-        expected: PolyFuncType,
+    /// [Call]: crate::ops::dataflow::Call
+    #[error(
+        "Incorrect result of type application in Call - cached {cached} but expected {expected}"
+    )]
+    CallIncorrectlyAppliesType {
+        cached: FunctionType,
+        expected: FunctionType,
     },
 }
 
@@ -418,7 +419,7 @@ impl ExtensionSet {
 
     /// Adds a type var (which must have been declared as a [TypeParam::Extensions]) to this set
     pub fn insert_type_var(&mut self, idx: usize) {
-        // Represent type vars as string representation of DeBruijn index.
+        // Represent type vars as string representation of variable index.
         // This is not a legal IdentList or ExtensionId so should not conflict.
         self.0
             .insert(ExtensionId::new_unchecked(idx.to_string().as_str()));
@@ -491,7 +492,7 @@ impl ExtensionSet {
             .try_for_each(|var_idx| check_typevar_decl(params, var_idx, &TypeParam::Extensions))
     }
 
-    pub(crate) fn substitute(&self, t: &impl Substitution) -> Self {
+    pub(crate) fn substitute(&self, t: &Substitution) -> Self {
         Self::from_iter(self.0.iter().flat_map(|e| match as_typevar(e) {
             None => vec![e.clone()],
             Some(i) => match t.apply_var(i, &TypeParam::Extensions) {
diff --git a/hugr/src/extension/infer.rs b/hugr/src/extension/infer.rs
index 64fca0265..e08a23e78 100644
--- a/hugr/src/extension/infer.rs
+++ b/hugr/src/extension/infer.rs
@@ -332,12 +332,9 @@ impl UnificationContext {
             let sig = hugr.get_nodetype(tgt_node).op();
             // Incoming ports with an edge that should mean equal extension reqs
             for port in hugr.node_inputs(tgt_node).filter(|src_port| {
-                matches!(
-                    sig.port_kind(*src_port),
-                    Some(EdgeKind::Value(_))
-                        | Some(EdgeKind::Static(_))
-                        | Some(EdgeKind::ControlFlow)
-                )
+                let kind = sig.port_kind(*src_port);
+                kind.as_ref().is_some_and(EdgeKind::is_static)
+                    || matches!(kind, Some(EdgeKind::Value(_)) | Some(EdgeKind::ControlFlow))
             }) {
                 let m_tgt = *self
                     .extensions
diff --git a/hugr/src/extension/op_def.rs b/hugr/src/extension/op_def.rs
index 4eefeb61f..9c9510e80 100644
--- a/hugr/src/extension/op_def.rs
+++ b/hugr/src/extension/op_def.rs
@@ -399,7 +399,7 @@ impl OpDef {
         // TODO https://github.com/CQCL/hugr/issues/624 validate declared TypeParams
         // for both type scheme and custom binary
         if let SignatureFunc::TypeScheme(ts) = &self.signature_func {
-            ts.poly_func.validate(exts, &[])?;
+            ts.poly_func.validate(exts)?;
         }
         Ok(())
     }
diff --git a/hugr/src/hugr/rewrite/replace.rs b/hugr/src/hugr/rewrite/replace.rs
index dc54f6652..972a81440 100644
--- a/hugr/src/hugr/rewrite/replace.rs
+++ b/hugr/src/hugr/rewrite/replace.rs
@@ -38,7 +38,7 @@ pub enum NewEdgeKind {
         /// The target port
         tgt_pos: IncomingPort,
     },
-    /// An [EdgeKind::Static] edge
+    /// An [EdgeKind::Const] or [EdgeKind::Function] edge
     Static {
         /// The source port
         src_pos: OutgoingPort,
@@ -90,9 +90,10 @@ impl NewEdgeSpec {
             NewEdgeKind::Value { src_pos, .. } => {
                 matches!(optype.port_kind(src_pos), Some(EdgeKind::Value(_)))
             }
-            NewEdgeKind::Static { src_pos, .. } => {
-                matches!(optype.port_kind(src_pos), Some(EdgeKind::Static(_)))
-            }
+            NewEdgeKind::Static { src_pos, .. } => optype
+                .port_kind(src_pos)
+                .as_ref()
+                .is_some_and(EdgeKind::is_static),
             NewEdgeKind::ControlFlow { src_pos } => {
                 matches!(optype.port_kind(src_pos), Some(EdgeKind::ControlFlow))
             }
@@ -107,9 +108,10 @@ impl NewEdgeSpec {
             NewEdgeKind::Value { tgt_pos, .. } => {
                 matches!(optype.port_kind(tgt_pos), Some(EdgeKind::Value(_)))
             }
-            NewEdgeKind::Static { tgt_pos, .. } => {
-                matches!(optype.port_kind(tgt_pos), Some(EdgeKind::Static(_)))
-            }
+            NewEdgeKind::Static { tgt_pos, .. } => optype
+                .port_kind(tgt_pos)
+                .as_ref()
+                .is_some_and(EdgeKind::is_static),
             NewEdgeKind::ControlFlow { .. } => matches!(
                 optype.port_kind(IncomingPort::from(0)),
                 Some(EdgeKind::ControlFlow)
diff --git a/hugr/src/hugr/serialize.rs b/hugr/src/hugr/serialize.rs
index 5c6110f49..f1253a0a4 100644
--- a/hugr/src/hugr/serialize.rs
+++ b/hugr/src/hugr/serialize.rs
@@ -502,6 +502,17 @@ pub mod test {
         Ok(())
     }
 
+    #[test]
+    fn function_type() -> Result<(), Box<dyn std::error::Error>> {
+        let fn_ty = Type::new_function(FunctionType::new_endo(type_row![BOOL_T]));
+        let mut bldr = DFGBuilder::new(FunctionType::new_endo(vec![fn_ty.clone()]))?;
+        let op = bldr.add_dataflow_op(LeafOp::Noop { ty: fn_ty }, bldr.input_wires())?;
+        let h = bldr.finish_prelude_hugr_with_outputs(op.outputs())?;
+
+        check_hugr_roundtrip(&h);
+        Ok(())
+    }
+
     #[test]
     fn hierarchy_order() -> Result<(), Box<dyn std::error::Error>> {
         let mut hugr = closed_dfg_root_hugr(FunctionType::new(vec![QB], vec![QB]));
diff --git a/hugr/src/hugr/validate.rs b/hugr/src/hugr/validate.rs
index 2466059b0..6853746ca 100644
--- a/hugr/src/hugr/validate.rs
+++ b/hugr/src/hugr/validate.rs
@@ -20,7 +20,7 @@ use crate::ops::custom::{resolve_opaque_op, ExternalOp};
 use crate::ops::validate::{ChildrenEdgeData, ChildrenValidationError, EdgeValidationError};
 use crate::ops::{FuncDefn, OpTag, OpTrait, OpType, ValidateOp};
 use crate::types::type_param::TypeParam;
-use crate::types::{EdgeKind, Type};
+use crate::types::EdgeKind;
 use crate::{Direction, Hugr, Node, Port};
 
 use super::views::{HierarchyView, HugrView, SiblingGraph};
@@ -219,17 +219,8 @@ impl<'a, 'b> ValidationContext<'a, 'b> {
             return Ok(());
         }
 
-        match &port_kind {
-            EdgeKind::Value(ty) => ty
-                .validate(self.extension_registry, var_decls)
-                .map_err(|cause| ValidationError::SignatureError { node, cause })?,
-            // Static edges must *not* refer to type variables declared by enclosing FuncDefns
-            // as these are only types at runtime.
-            EdgeKind::Static(ty) => ty
-                .validate(self.extension_registry, &[])
-                .map_err(|cause| ValidationError::SignatureError { node, cause })?,
-            _ => (),
-        }
+        self.validate_port_kind(&port_kind, var_decls)
+            .map_err(|cause| ValidationError::SignatureError { node, cause })?;
 
         let mut link_cnt = 0;
         for (_, link) in links {
@@ -271,6 +262,21 @@ impl<'a, 'b> ValidationContext<'a, 'b> {
         Ok(())
     }
 
+    fn validate_port_kind(
+        &self,
+        port_kind: &EdgeKind,
+        var_decls: &[TypeParam],
+    ) -> Result<(), SignatureError> {
+        match &port_kind {
+            EdgeKind::Value(ty) => ty.validate(self.extension_registry, var_decls),
+            // Static edges must *not* refer to type variables declared by enclosing FuncDefns
+            // as these are only types at runtime.
+            EdgeKind::Const(ty) => ty.validate(self.extension_registry, &[]),
+            EdgeKind::Function(pf) => pf.validate(self.extension_registry),
+            _ => Ok(()),
+        }
+    }
+
     /// Check operation-specific constraints.
     ///
     /// These are flags defined for each operation type as an [`OpValidityFlags`] object.
@@ -409,45 +415,26 @@ impl<'a, 'b> ValidationContext<'a, 'b> {
         from_optype: &OpType,
         to: Node,
         to_offset: Port,
-    ) -> Result<(), ValidationError> {
+    ) -> Result<(), InterGraphEdgeError> {
         let from_parent = self
             .hugr
             .get_parent(from)
             .expect("Root nodes cannot have ports");
         let to_parent = self.hugr.get_parent(to);
-        let local = Some(from_parent) == to_parent;
-
-        let is_static = match from_optype.port_kind(from_offset).unwrap() {
-            EdgeKind::Static(typ) => {
-                if !(OpTag::Const.is_superset(from_optype.tag())
-                    || OpTag::Function.is_superset(from_optype.tag()))
-                {
-                    return Err(InterGraphEdgeError::InvalidConstSrc {
-                        from,
-                        from_offset,
-                        typ,
-                    }
-                    .into());
-                };
-                true
-            }
-            ty => {
-                if !local && !matches!(&ty, EdgeKind::Value(t) if t.copyable()) {
-                    return Err(InterGraphEdgeError::NonCopyableData {
-                        from,
-                        from_offset,
-                        to,
-                        to_offset,
-                        ty,
-                    }
-                    .into());
-                }
-                false
-            }
-        };
-        if local {
-            return Ok(());
+        let edge_kind = from_optype.port_kind(from_offset).unwrap();
+        if Some(from_parent) == to_parent {
+            return Ok(()); // Local edge
         }
+        let is_static = edge_kind.is_static();
+        if !is_static && !matches!(&edge_kind, EdgeKind::Value(t) if t.copyable()) {
+            return Err(InterGraphEdgeError::NonCopyableData {
+                from,
+                from_offset,
+                to,
+                to_offset,
+                ty: edge_kind,
+            });
+        };
 
         // To detect either external or dominator edges, we traverse the ancestors
         // of the target until we find either `from_parent` (in the external
@@ -489,8 +476,7 @@ impl<'a, 'b> ValidationContext<'a, 'b> {
                         to,
                         to_offset,
                         ancestor_parent_op: ancestor_parent_op.clone(),
-                    }
-                    .into());
+                    });
                 }
 
                 // Check domination
@@ -513,8 +499,7 @@ impl<'a, 'b> ValidationContext<'a, 'b> {
                         to_offset,
                         from_parent,
                         ancestor,
-                    }
-                    .into());
+                    });
                 }
 
                 return Ok(());
@@ -526,8 +511,7 @@ impl<'a, 'b> ValidationContext<'a, 'b> {
             from_offset,
             to,
             to_offset,
-        }
-        .into())
+        })
     }
 
     /// Validates that TypeArgs are valid wrt the [ExtensionRegistry] and that nodes
@@ -573,8 +557,8 @@ impl<'a, 'b> ValidationContext<'a, 'b> {
                     }
                 }
             }
-            OpType::LeafOp(crate::ops::LeafOp::TypeApply { ta }) => {
-                ta.validate(self.extension_registry)
+            OpType::Call(c) => {
+                c.validate(self.extension_registry)
                     .map_err(|cause| ValidationError::SignatureError { node, cause })?;
             }
             _ => (),
@@ -768,14 +752,6 @@ pub enum InterGraphEdgeError {
         from_parent: Node,
         ancestor: Node,
     },
-    #[error(
-        "Const edge comes from an invalid node type: {from:?} ({from_offset:?}). Edge type: {typ}"
-    )]
-    InvalidConstSrc {
-        from: Node,
-        from_offset: Port,
-        typ: Type,
-    },
 }
 
 #[cfg(test)]
diff --git a/hugr/src/hugr/views/render.rs b/hugr/src/hugr/views/render.rs
index e876ac6d2..e7b3ce41a 100644
--- a/hugr/src/hugr/views/render.rs
+++ b/hugr/src/hugr/views/render.rs
@@ -59,8 +59,10 @@ pub(super) fn port_style<H: HugrView + ?Sized>(
         let optype = h.get_optype(node.into());
         let offset = graph.port_offset(port).unwrap();
         match optype.port_kind(offset).unwrap() {
-            EdgeKind::Static(ty) => PortStyle::new(html_escape::encode_text(&format!("{}", ty))),
-            EdgeKind::Value(ty) => PortStyle::new(html_escape::encode_text(&format!("{}", ty))),
+            EdgeKind::Function(pf) => PortStyle::new(html_escape::encode_text(&format!("{}", pf))),
+            EdgeKind::Const(ty) | EdgeKind::Value(ty) => {
+                PortStyle::new(html_escape::encode_text(&format!("{}", ty)))
+            }
             EdgeKind::StateOrder => match graph.port_links(port).count() > 0 {
                 true => PortStyle::text("", false),
                 false => PortStyle::Hidden,
@@ -97,22 +99,28 @@ pub(super) fn edge_style<H: HugrView + ?Sized>(
         let style = match port_kind {
             EdgeKind::StateOrder => EdgeStyle::Dotted,
             EdgeKind::ControlFlow => EdgeStyle::Dashed,
-            EdgeKind::Static(_) | EdgeKind::Value(_) => EdgeStyle::Solid,
+            EdgeKind::Const(_) | EdgeKind::Function(_) | EdgeKind::Value(_) => EdgeStyle::Solid,
         };
 
         // Compute the label for the edge, given the setting flags.
+        fn type_label(e: EdgeKind) -> Option<String> {
+            match e {
+                EdgeKind::Const(ty) | EdgeKind::Value(ty) => Some(format!("{}", ty)),
+                EdgeKind::Function(pf) => Some(format!("{}", pf)),
+                _ => None,
+            }
+        }
         //
         // Only static and value edges have types to display.
         let label = match (
             config.port_offsets_in_edges,
-            config.type_labels_in_edges,
-            port_kind,
+            type_label(port_kind).filter(|_| config.type_labels_in_edges),
         ) {
-            (true, true, EdgeKind::Static(ty) | EdgeKind::Value(ty)) => {
+            (true, Some(ty)) => {
                 format!("{}:{}\n{ty}", src_offset.index(), tgt_offset.index())
             }
-            (true, _, _) => format!("{}:{}", src_offset.index(), tgt_offset.index()),
-            (false, true, EdgeKind::Static(ty) | EdgeKind::Value(ty)) => format!("{}", ty),
+            (true, _) => format!("{}:{}", src_offset.index(), tgt_offset.index()),
+            (false, Some(ty)) => ty.to_string(),
             _ => return style,
         };
         style.with_label(label)
diff --git a/hugr/src/ops/constant.rs b/hugr/src/ops/constant.rs
index d18cff4dd..058dd16e2 100644
--- a/hugr/src/ops/constant.rs
+++ b/hugr/src/ops/constant.rs
@@ -5,7 +5,7 @@ mod custom;
 use super::{OpName, OpTrait, StaticTag};
 use super::{OpTag, OpType};
 use crate::extension::ExtensionSet;
-use crate::types::{CustomType, EdgeKind, SumType, SumTypeError, Type};
+use crate::types::{CustomType, EdgeKind, FunctionType, SumType, SumTypeError, Type};
 use crate::{Hugr, HugrView};
 
 use itertools::Itertools;
@@ -93,11 +93,10 @@ pub enum ConstTypeError {
     SumType(#[from] SumTypeError),
     /// Function constant missing a function type.
     #[error(
-        "A function constant cannot be defined using a Hugr with root of type {}.",
-        .hugr_root_type.name()
+        "A function constant cannot be defined using a Hugr with root of type {hugr_root_type:?}. Must be a monomorphic function.",
     )]
-    FunctionTypeMissing {
-        /// The root node type of the Hugr defining the function constant.
+    NotMonomorphicFunction {
+        /// The root node type of the Hugr that (claims to) define the function constant.
         hugr_root_type: OpType,
     },
     /// A mismatch between the type expected and the value.
@@ -108,6 +107,18 @@ pub enum ConstTypeError {
     CustomCheckFail(#[from] CustomCheckFailure),
 }
 
+/// Hugrs (even functions) inside Consts must be monomorphic
+fn mono_fn_type(h: &Hugr) -> Result<FunctionType, ConstTypeError> {
+    if let Some(pf) = h.get_function_type() {
+        if let Ok(ft) = pf.try_into() {
+            return Ok(ft);
+        }
+    }
+    Err(ConstTypeError::NotMonomorphicFunction {
+        hugr_root_type: h.root_type().op().clone(),
+    })
+}
+
 impl Const {
     /// Returns a reference to the type of this [`Const`].
     pub fn const_type(&self) -> Type {
@@ -116,14 +127,7 @@ impl Const {
             Self::Tuple { vs } => Type::new_tuple(vs.iter().map(Self::const_type).collect_vec()),
             Self::Sum { sum_type, .. } => sum_type.clone().into(),
             Self::Function { hugr } => {
-                let func_type = hugr.get_function_type().unwrap_or_else(|| {
-                    panic!(
-                        "{}",
-                        ConstTypeError::FunctionTypeMissing {
-                            hugr_root_type: hugr.get_optype(hugr.root()).clone()
-                        }
-                    )
-                });
+                let func_type = mono_fn_type(hugr).unwrap_or_else(|e| panic!("{}", e));
                 Type::new_function(func_type)
             }
         }
@@ -159,11 +163,7 @@ impl Const {
     /// Returns an error if the Hugr root node does not define a function.
     pub fn function(hugr: impl Into<Hugr>) -> Result<Self, ConstTypeError> {
         let hugr = hugr.into();
-        if hugr.get_function_type().is_none() {
-            Err(ConstTypeError::FunctionTypeMissing {
-                hugr_root_type: hugr.get_optype(hugr.root()).clone(),
-            })?;
-        }
+        mono_fn_type(&hugr)?;
         Ok(Self::Function {
             hugr: Box::new(hugr),
         })
@@ -266,7 +266,7 @@ impl OpTrait for Const {
     }
 
     fn static_output(&self) -> Option<EdgeKind> {
-        Some(EdgeKind::Static(self.const_type()))
+        Some(EdgeKind::Const(self.const_type()))
     }
 }
 
diff --git a/hugr/src/ops/dataflow.rs b/hugr/src/ops/dataflow.rs
index 9929ac5ac..d8a6ed4fc 100644
--- a/hugr/src/ops/dataflow.rs
+++ b/hugr/src/ops/dataflow.rs
@@ -149,7 +149,7 @@ impl<T: DataflowOpTrait> StaticTag for T {
 ///
 /// The first ports correspond to the signature of the function being called.
 /// The port immediately following those those is connected to the def/declare
-/// block with a [`EdgeKind::Static`] edge.
+/// block with a [`EdgeKind::Function`] edge.
 #[derive(Debug, Clone, PartialEq, Eq, serde::Serialize, serde::Deserialize)]
 pub struct Call {
     /// Signature of function being called
@@ -171,8 +171,7 @@ impl DataflowOpTrait for Call {
     }
 
     fn static_input(&self) -> Option<EdgeKind> {
-        let fn_typ = Type::new_function(self.called_function_type().clone());
-        Some(EdgeKind::Static(fn_typ))
+        Some(EdgeKind::Function(self.called_function_type().clone()))
     }
 }
 impl Call {
@@ -221,13 +220,29 @@ impl Call {
     pub fn called_function_port(&self) -> IncomingPort {
         self.instantiation.input_count().into()
     }
+
+    pub(crate) fn validate(
+        &self,
+        extension_registry: &ExtensionRegistry,
+    ) -> Result<(), SignatureError> {
+        let other = Self::try_new(
+            self.func_sig.clone(),
+            self.type_args.clone(),
+            extension_registry,
+        )?;
+        if other.instantiation == self.instantiation {
+            Ok(())
+        } else {
+            Err(SignatureError::CallIncorrectlyAppliesType {
+                cached: self.instantiation.clone(),
+                expected: other.instantiation.clone(),
+            })
+        }
+    }
 }
 
 /// Call a function indirectly. Like call, but the function input is a value
-/// (runtime, not static) dataflow edge, and we assume all its binders have
-/// already been given [TypeArg]s by [TypeApply] nodes.
-///
-/// [TypeApply]: crate::ops::LeafOp::TypeApply
+/// (runtime, not static) dataflow edge, and thus does not need any type-args.
 #[derive(Debug, Clone, PartialEq, Eq, serde::Serialize, serde::Deserialize)]
 pub struct CallIndirect {
     /// Signature of function being called
@@ -270,7 +285,7 @@ impl DataflowOpTrait for LoadConstant {
     }
 
     fn static_input(&self) -> Option<EdgeKind> {
-        Some(EdgeKind::Static(self.constant_type().clone()))
+        Some(EdgeKind::Const(self.constant_type().clone()))
     }
 }
 impl LoadConstant {
diff --git a/hugr/src/ops/leaf.rs b/hugr/src/ops/leaf.rs
index 07476ff7a..878fcec2a 100644
--- a/hugr/src/ops/leaf.rs
+++ b/hugr/src/ops/leaf.rs
@@ -6,9 +6,8 @@ use super::custom::{ExtensionOp, ExternalOp};
 use super::dataflow::DataflowOpTrait;
 use super::{OpName, OpTag};
 
-use crate::extension::{ExtensionRegistry, ExtensionSet, SignatureError};
-use crate::types::type_param::TypeArg;
-use crate::types::PolyFuncType;
+use crate::extension::ExtensionSet;
+
 use crate::{
     extension::ExtensionId,
     types::{EdgeKind, FunctionType, Type, TypeRow},
@@ -53,13 +52,6 @@ pub enum LeafOp {
         /// The extensions which we're adding to the inputs
         new_extension: ExtensionId,
     },
-    /// Fixes some [TypeParam]s of a polymorphic type by providing [TypeArg]s
-    ///
-    /// [TypeParam]: crate::types::type_param::TypeParam
-    TypeApply {
-        /// The type and args, plus a cache of the resulting type
-        ta: TypeApplication,
-    },
 }
 
 impl LeafOp {
@@ -76,67 +68,6 @@ impl LeafOp {
     }
 }
 
-/// Records details of an application of a [PolyFuncType] to some [TypeArg]s
-/// and the result (a less-, but still potentially-, polymorphic type).
-#[derive(Clone, Debug, PartialEq, Eq, serde::Serialize, serde::Deserialize)]
-pub struct TypeApplication {
-    input: PolyFuncType,
-    args: Vec<TypeArg>,
-    output: PolyFuncType, // cached
-}
-
-impl TypeApplication {
-    /// Checks that the specified args are correct for the [TypeParam]s of the polymorphic input.
-    /// Note the extension registry is required here to recompute [Type::least_upper_bound]s.
-    ///
-    /// [TypeParam]: crate::types::type_param::TypeParam
-    pub fn try_new(
-        input: PolyFuncType,
-        args: impl Into<Vec<TypeArg>>,
-        extension_registry: &ExtensionRegistry,
-    ) -> Result<Self, SignatureError> {
-        let args = args.into();
-        // Should we require >=1 `arg`s here? Or that input declares >=1 params?
-        // At the moment we allow an identity TypeApply on a monomorphic function type.
-        let output = input.instantiate_poly(&args, extension_registry)?;
-        Ok(Self {
-            input,
-            args,
-            output,
-        })
-    }
-
-    pub(crate) fn validate(
-        &self,
-        extension_registry: &ExtensionRegistry,
-    ) -> Result<(), SignatureError> {
-        let other = Self::try_new(self.input.clone(), self.args.clone(), extension_registry)?;
-        if other.output == self.output {
-            Ok(())
-        } else {
-            Err(SignatureError::TypeApplyIncorrectCache {
-                cached: self.output.clone(),
-                expected: other.output.clone(),
-            })
-        }
-    }
-
-    /// Returns the type of the input function.
-    pub fn input(&self) -> &PolyFuncType {
-        &self.input
-    }
-
-    /// Returns the args applied to the input function.
-    pub fn args(&self) -> &[TypeArg] {
-        &self.args
-    }
-
-    /// Returns the type of the output function.
-    pub fn output(&self) -> &PolyFuncType {
-        &self.output
-    }
-}
-
 impl Default for LeafOp {
     fn default() -> Self {
         Self::Noop { ty: Type::UNIT }
@@ -152,7 +83,6 @@ impl OpName for LeafOp {
             LeafOp::UnpackTuple { tys: _ } => "UnpackTuple",
             LeafOp::Tag { .. } => "Tag",
             LeafOp::Lift { .. } => "Lift",
-            LeafOp::TypeApply { .. } => "TypeApply",
         }
         .into()
     }
@@ -172,9 +102,6 @@ impl DataflowOpTrait for LeafOp {
             LeafOp::UnpackTuple { tys: _ } => "UnpackTuple operation",
             LeafOp::Tag { .. } => "Tag Sum operation",
             LeafOp::Lift { .. } => "Add a extension requirement to an edge",
-            LeafOp::TypeApply { .. } => {
-                "Instantiate (perhaps partially) a polymorphic type with some type arguments"
-            }
         }
     }
 
@@ -201,10 +128,6 @@ impl DataflowOpTrait for LeafOp {
                 new_extension,
             } => FunctionType::new(type_row.clone(), type_row.clone())
                 .with_extension_delta(ExtensionSet::singleton(new_extension)),
-            LeafOp::TypeApply { ta } => FunctionType::new(
-                vec![Type::new_function(ta.input.clone())],
-                vec![Type::new_function(ta.output.clone())],
-            ),
         }
     }
 
@@ -216,73 +139,3 @@ impl DataflowOpTrait for LeafOp {
         Some(EdgeKind::StateOrder)
     }
 }
-
-#[cfg(test)]
-mod test {
-    use crate::builder::{BuildError, DFGBuilder, Dataflow, DataflowHugr};
-    use crate::extension::prelude::BOOL_T;
-    use crate::extension::{prelude::USIZE_T, PRELUDE};
-    use crate::extension::{ExtensionRegistry, SignatureError};
-    use crate::hugr::ValidationError;
-    use crate::ops::handle::NodeHandle;
-    use crate::std_extensions::collections::EXTENSION;
-    use crate::types::Type;
-    use crate::types::{test::nested_func, FunctionType, TypeArg};
-
-    use super::{LeafOp, TypeApplication};
-
-    const USIZE_TA: TypeArg = TypeArg::Type { ty: USIZE_T };
-
-    #[test]
-    fn hugr_with_type_apply() -> Result<(), Box<dyn std::error::Error>> {
-        let reg = ExtensionRegistry::try_new([PRELUDE.to_owned(), EXTENSION.to_owned()]).unwrap();
-        let pf_in = nested_func();
-        let pf_out = pf_in.instantiate(&[USIZE_TA], &reg)?;
-        let mut dfg = DFGBuilder::new(FunctionType::new(
-            vec![Type::new_function(pf_in.clone())],
-            vec![Type::new_function(pf_out)],
-        ))?;
-        let ta = dfg.add_dataflow_op(
-            LeafOp::TypeApply {
-                ta: TypeApplication::try_new(pf_in, [USIZE_TA], &reg).unwrap(),
-            },
-            dfg.input_wires(),
-        )?;
-        dfg.finish_hugr_with_outputs(ta.outputs(), &reg)?;
-        Ok(())
-    }
-
-    #[test]
-    fn bad_type_apply() -> Result<(), Box<dyn std::error::Error>> {
-        let reg = ExtensionRegistry::try_new([PRELUDE.to_owned(), EXTENSION.to_owned()]).unwrap();
-        let pf = nested_func();
-        let pf_usz = pf.instantiate_poly(&[USIZE_TA], &reg)?;
-        let pf_bool = pf.instantiate_poly(&[TypeArg::Type { ty: BOOL_T }], &reg)?;
-        let mut dfg = DFGBuilder::new(FunctionType::new(
-            vec![Type::new_function(pf.clone())],
-            vec![Type::new_function(pf_usz.clone())],
-        ))?;
-        let ta = dfg.add_dataflow_op(
-            LeafOp::TypeApply {
-                ta: TypeApplication {
-                    input: pf,
-                    args: vec![TypeArg::Type { ty: BOOL_T }],
-                    output: pf_usz.clone(),
-                },
-            },
-            dfg.input_wires(),
-        )?;
-        let res = dfg.finish_hugr_with_outputs(ta.outputs(), &reg);
-        assert_eq!(
-            res.unwrap_err(),
-            BuildError::InvalidHUGR(ValidationError::SignatureError {
-                node: ta.node(),
-                cause: SignatureError::TypeApplyIncorrectCache {
-                    cached: pf_usz,
-                    expected: pf_bool
-                }
-            })
-        );
-        Ok(())
-    }
-}
diff --git a/hugr/src/ops/module.rs b/hugr/src/ops/module.rs
index 060b3354a..5557ac802 100644
--- a/hugr/src/ops/module.rs
+++ b/hugr/src/ops/module.rs
@@ -61,7 +61,7 @@ impl OpTrait for FuncDefn {
     }
 
     fn static_output(&self) -> Option<EdgeKind> {
-        Some(EdgeKind::Static(Type::new_function(self.signature.clone())))
+        Some(EdgeKind::Function(self.signature.clone()))
     }
 }
 
@@ -89,7 +89,7 @@ impl OpTrait for FuncDecl {
     }
 
     fn static_output(&self) -> Option<EdgeKind> {
-        Some(EdgeKind::Static(Type::new_function(self.signature.clone())))
+        Some(EdgeKind::Function(self.signature.clone()))
     }
 }
 
diff --git a/hugr/src/types.rs b/hugr/src/types.rs
index 08c91159e..bb7a91f19 100644
--- a/hugr/src/types.rs
+++ b/hugr/src/types.rs
@@ -9,6 +9,7 @@ pub mod type_param;
 pub mod type_row;
 
 pub use crate::ops::constant::{ConstTypeError, CustomCheckFailure};
+use crate::types::type_param::check_type_arg;
 use crate::utils::display_list_with_separator;
 pub use check::SumTypeError;
 pub use custom::CustomType;
@@ -40,8 +41,13 @@ pub enum EdgeKind {
     ControlFlow,
     /// Data edges of a DDG region, also known as "wires".
     Value(Type),
-    /// A reference to a static value definition.
-    Static(Type),
+    /// A reference to a static constant value - must be a Copyable type
+    Const(Type),
+    /// A reference to a function i.e. [FuncDecl] or [FuncDefn]
+    ///
+    /// [FuncDecl]: crate::ops::FuncDecl
+    /// [FuncDefn]: crate::ops::FuncDefn
+    Function(PolyFuncType),
     /// Explicitly enforce an ordering between nodes in a DDG.
     StateOrder,
 }
@@ -51,6 +57,12 @@ impl EdgeKind {
     pub fn is_linear(&self) -> bool {
         matches!(self, EdgeKind::Value(t) if !t.copyable())
     }
+
+    /// Whether this EdgeKind represents a Static edge (in the spec)
+    /// - i.e. the value is statically known
+    pub fn is_static(&self) -> bool {
+        matches!(self, EdgeKind::Const(_) | EdgeKind::Function(_))
+    }
 }
 
 #[derive(
@@ -185,8 +197,8 @@ pub enum TypeEnum {
     Alias(AliasDecl),
     #[allow(missing_docs)]
     #[display(fmt = "Function({})", "_0")]
-    Function(Box<PolyFuncType>),
-    // DeBruijn index, and cache of TypeBound (checked in validation)
+    Function(Box<FunctionType>),
+    // Index into TypeParams, and cache of TypeBound (checked in validation)
     #[allow(missing_docs)]
     #[display(fmt = "Variable({})", _0)]
     Variable(usize, TypeBound),
@@ -217,7 +229,7 @@ impl TypeEnum {
 )]
 #[display(fmt = "{}", "_0")]
 #[serde(into = "serialize::SerSimpleType", from = "serialize::SerSimpleType")]
-/// A HUGR type - the valid types of [EdgeKind::Value] and [EdgeKind::Static] edges.
+/// A HUGR type - the valid types of [EdgeKind::Value] and [EdgeKind::Const] edges.
 /// Such an edge is valid if the ports on either end agree on the [Type].
 /// Types have an optional [TypeBound] which places limits on the valid
 /// operations on a type.
@@ -259,7 +271,7 @@ impl Type {
     const EMPTY_TYPEROW_REF: &'static TypeRow = &Self::EMPTY_TYPEROW;
 
     /// Initialize a new function type.
-    pub fn new_function(fun_ty: impl Into<PolyFuncType>) -> Self {
+    pub fn new_function(fun_ty: impl Into<FunctionType>) -> Self {
         Self::new(TypeEnum::Function(Box::new(fun_ty.into())))
     }
 
@@ -302,7 +314,7 @@ impl Type {
         Self(TypeEnum::Sum(SumType::Unit { size }), TypeBound::Eq)
     }
 
-    /// New use (occurrence) of the type variable with specified DeBruijn index.
+    /// New use (occurrence) of the type variable with specified index.
     /// For use in type schemes only: `bound` must match that with which the
     /// variable was declared (i.e. as a [TypeParam::Type]`(bound)`).
     pub fn new_var_use(idx: usize, bound: TypeBound) -> Self {
@@ -355,10 +367,15 @@ impl Type {
         }
     }
 
-    pub(crate) fn substitute(&self, t: &impl Substitution) -> Self {
+    pub(crate) fn substitute(&self, t: &Substitution) -> Self {
         match &self.0 {
             TypeEnum::Alias(_) | TypeEnum::Sum(SumType::Unit { .. }) => self.clone(),
-            TypeEnum::Variable(idx, bound) => t.apply_typevar(*idx, *bound),
+            TypeEnum::Variable(idx, bound) => {
+                let TypeArg::Type { ty } = t.apply_var(*idx, &((*bound).into())) else {
+                    panic!("Variable was not a type - try validate() first")
+                };
+                ty
+            }
             TypeEnum::Extension(cty) => Type::new_extension(cty.substitute(t)),
             TypeEnum::Function(bf) => Type::new_function(bf.substitute(t)),
             TypeEnum::Sum(SumType::General { rows }) => {
@@ -368,26 +385,26 @@ impl Type {
     }
 }
 
-/// A function that replaces type variables with values.
-/// (The values depend upon the implementation, to allow dynamic computation;
-/// and [Substitution] deals only with type variables, other/containing types/typeargs
-/// are handled by [Type::substitute], [TypeArg::substitute] and friends.)
-pub(crate) trait Substitution {
-    /// Apply to a variable of kind [TypeParam::Type]
-    fn apply_typevar(&self, idx: usize, bound: TypeBound) -> Type {
-        let TypeArg::Type { ty } = self.apply_var(idx, &bound.into()) else {
-            panic!("Variable was not a type - try validate() first")
-        };
-        ty
+/// Details a replacement of type variables with a finite list of known values.
+/// (Variables out of the range of the list will result in a panic)
+pub(crate) struct Substitution<'a>(&'a [TypeArg], &'a ExtensionRegistry);
+
+impl<'a> Substitution<'a> {
+    pub(crate) fn apply_var(&self, idx: usize, decl: &TypeParam) -> TypeArg {
+        let arg = self
+            .0
+            .get(idx)
+            .expect("Undeclared type variable - call validate() ?");
+        debug_assert_eq!(check_type_arg(arg, decl), Ok(()));
+        arg.clone()
     }
 
-    /// Apply to a variable whose kind is any given [TypeParam]
-    fn apply_var(&self, idx: usize, decl: &TypeParam) -> TypeArg;
-
-    fn extension_registry(&self) -> &ExtensionRegistry;
+    fn extension_registry(&self) -> &ExtensionRegistry {
+        self.1
+    }
 }
 
-fn subst_row(row: &TypeRow, tr: &impl Substitution) -> TypeRow {
+fn subst_row(row: &TypeRow, tr: &Substitution) -> TypeRow {
     let res = row
         .iter()
         .map(|ty| ty.substitute(tr))
@@ -423,8 +440,6 @@ pub(crate) fn check_typevar_decl(
 
 #[cfg(test)]
 pub(crate) mod test {
-    pub(crate) use poly_func::test::nested_func;
-
     use super::*;
     use crate::{extension::prelude::USIZE_T, ops::AliasDecl};
 
@@ -445,7 +460,7 @@ pub(crate) mod test {
         ]);
         assert_eq!(
             &t.to_string(),
-            "[usize, Function(forall . [[]][]), my_custom, Alias(my_alias)]"
+            "[usize, Function([[]][]), my_custom, Alias(my_alias)]"
         );
     }
 
diff --git a/hugr/src/types/custom.rs b/hugr/src/types/custom.rs
index ba738227a..e575bdf3f 100644
--- a/hugr/src/types/custom.rs
+++ b/hugr/src/types/custom.rs
@@ -88,7 +88,7 @@ impl CustomType {
             })
     }
 
-    pub(super) fn substitute(&self, tr: &impl Substitution) -> Self {
+    pub(super) fn substitute(&self, tr: &Substitution) -> Self {
         let args = self
             .args
             .iter()
diff --git a/hugr/src/types/poly_func.rs b/hugr/src/types/poly_func.rs
index 6916924b1..d3717ece3 100644
--- a/hugr/src/types/poly_func.rs
+++ b/hugr/src/types/poly_func.rs
@@ -1,18 +1,16 @@
 //! Polymorphic Function Types
 
-use crate::{
-    extension::{ExtensionRegistry, SignatureError},
-    types::type_param::check_type_arg,
-};
+use crate::extension::{ExtensionRegistry, SignatureError};
 use itertools::Itertools;
 
 use super::type_param::{check_type_args, TypeArg, TypeParam};
 use super::{FunctionType, Substitution};
 
-/// A polymorphic function type, e.g. of a [Graph], or perhaps an [OpDef].
+/// A polymorphic type scheme, i.e. of a [FuncDecl], [FuncDefn] or [OpDef].
 /// (Nodes/operations in the Hugr are not polymorphic.)
 ///
-/// [Graph]: crate::ops::constant::Const::Function
+/// [FuncDecl]: crate::ops::module::FuncDecl
+/// [FuncDefn]: crate::ops::module::FuncDefn
 /// [OpDef]: crate::extension::OpDef
 #[derive(
     Clone, PartialEq, Debug, Default, Eq, derive_more::Display, serde::Serialize, serde::Deserialize,
@@ -24,11 +22,8 @@ use super::{FunctionType, Substitution};
 )]
 pub struct PolyFuncType {
     /// The declared type parameters, i.e., these must be instantiated with
-    /// the same number of [TypeArg]s before the function can be called. Note that within
-    /// the [Self::body], variable (DeBruijn) index 0 is element 0 of this array, i.e. the
-    /// variables are bound from right to left.
-    ///
-    /// [TypeArg]: super::type_param::TypeArg
+    /// the same number of [TypeArg]s before the function can be called. This
+    /// defines the indices used by variables inside the body.
     params: Vec<TypeParam>,
     /// Template for the function. May contain variables up to length of [Self::params]
     body: FunctionType,
@@ -43,6 +38,19 @@ impl From<FunctionType> for PolyFuncType {
     }
 }
 
+impl TryFrom<PolyFuncType> for FunctionType {
+    /// If the PolyFuncType is not a monomorphic FunctionType, fail with the binders
+    type Error = Vec<TypeParam>;
+
+    fn try_from(value: PolyFuncType) -> Result<Self, Self::Error> {
+        if value.params.is_empty() {
+            Ok(value.body)
+        } else {
+            Err(value.params)
+        }
+    }
+}
+
 impl PolyFuncType {
     /// The type parameters, aka binders, over which this type is polymorphic
     pub fn params(&self) -> &[TypeParam] {
@@ -64,68 +72,10 @@ impl PolyFuncType {
     }
 
     /// Validates this instance, checking that the types in the body are
-    /// wellformed with respect to the registry, and that all type variables
-    /// are declared (perhaps in an enclosing scope, kinds passed in).
-    pub fn validate(
-        &self,
-        reg: &ExtensionRegistry,
-        external_var_decls: &[TypeParam],
-    ) -> Result<(), SignatureError> {
+    /// wellformed with respect to the registry, and the type variables declared.
+    pub fn validate(&self, reg: &ExtensionRegistry) -> Result<(), SignatureError> {
         // TODO https://github.com/CQCL/hugr/issues/624 validate TypeParams declared here, too
-        let mut v; // Declared here so live until end of scope
-        let all_var_decls = if self.params.is_empty() {
-            external_var_decls
-        } else {
-            // Type vars declared here go at lowest indices (as per DeBruijn)
-            v = self.params.clone();
-            v.extend_from_slice(external_var_decls);
-            v.as_slice()
-        };
-        self.body.validate(reg, all_var_decls)
-    }
-
-    pub(super) fn substitute(&self, t: &impl Substitution) -> Self {
-        if self.params.is_empty() {
-            // Avoid using complex code for simple Monomorphic case
-            return self.body.substitute(t).into();
-        }
-        PolyFuncType {
-            params: self.params.clone(),
-            body: self.body.substitute(&InsideBinders {
-                num_binders: self.params.len(),
-                underlying: t,
-            }),
-        }
-    }
-
-    /// (Perhaps-partially) instantiates this [PolyFuncType] into another with fewer binders.
-    /// Note that indices into `args` correspond to the same index within [Self::params],
-    /// so we instantiate the lowest-index [Self::params] first, even though these
-    /// would be considered "innermost" / "closest" according to DeBruijn numbering.
-    pub(crate) fn instantiate_poly(
-        &self,
-        args: &[TypeArg],
-        exts: &ExtensionRegistry,
-    ) -> Result<Self, SignatureError> {
-        let remaining = self.params.get(args.len()..).unwrap_or_default();
-        let mut v;
-        let args = if remaining.is_empty() {
-            args // instantiate below will fail if there were too many
-        } else {
-            // Partial application - renumber remaining params (still bound) downward
-            v = args.to_vec();
-            v.extend(
-                remaining
-                    .iter()
-                    .enumerate()
-                    .map(|(i, decl)| TypeArg::new_var_use(i, decl.clone())),
-            );
-            v.as_slice()
-        };
-        Ok(Self {
-            params: remaining.to_vec(),
-            body: self.instantiate(args, exts)?,
-        })
+        self.body.validate(reg, &self.params)
     }
 
     /// Instantiates an outer [PolyFuncType], i.e. with no free variables
@@ -142,75 +92,7 @@ impl PolyFuncType {
         // Check that args are applicable, and that we have a value for each binder,
         // i.e. each possible free variable within the body.
         check_type_args(args, &self.params)?;
-        Ok(self.body.substitute(&SubstValues(args, ext_reg)))
-    }
-}
-
-/// A [Substitution] with a finite list of known values.
-/// (Variables out of the range of the list will result in a panic)
-struct SubstValues<'a>(&'a [TypeArg], &'a ExtensionRegistry);
-
-impl<'a> Substitution for SubstValues<'a> {
-    fn apply_var(&self, idx: usize, decl: &TypeParam) -> TypeArg {
-        let arg = self
-            .0
-            .get(idx)
-            .expect("Undeclared type variable - call validate() ?");
-        debug_assert_eq!(check_type_arg(arg, decl), Ok(()));
-        arg.clone()
-    }
-
-    fn extension_registry(&self) -> &ExtensionRegistry {
-        self.1
-    }
-}
-
-/// A [Substitution] that renumbers any type variable to another (of the same kind)
-/// with a index increased by a fixed `usize``.
-struct Renumber<'a> {
-    offset: usize,
-    exts: &'a ExtensionRegistry,
-}
-
-impl<'a> Substitution for Renumber<'a> {
-    fn apply_var(&self, idx: usize, decl: &TypeParam) -> TypeArg {
-        TypeArg::new_var_use(idx + self.offset, decl.clone())
-    }
-
-    fn extension_registry(&self) -> &ExtensionRegistry {
-        self.exts
-    }
-}
-
-/// Given a [Substitution] defined outside a binder (i.e. [PolyFuncType]),
-/// applies that transformer to types inside the binder (i.e. arguments/results of said function)
-struct InsideBinders<'a> {
-    /// The number of binders we have entered since (beneath where) we started to apply
-    /// [Self::underlying]).
-    /// That is, the lowest `num_binders` variable indices refer to locals bound since then.
-    num_binders: usize,
-    /// Substitution that was being applied outside those binders (i.e. in outer scope)
-    underlying: &'a dyn Substitution,
-}
-
-impl<'a> Substitution for InsideBinders<'a> {
-    fn apply_var(&self, idx: usize, decl: &TypeParam) -> TypeArg {
-        // Convert variable index into outer scope
-        match idx.checked_sub(self.num_binders) {
-            None => TypeArg::new_var_use(idx, decl.clone()), // Bound locally, unknown to `underlying`
-            Some(idx_in_outer_scope) => {
-                let result_in_outer_scope = self.underlying.apply_var(idx_in_outer_scope, decl);
-                // Transform returned value into the current scope, i.e. avoid the variables newly bound
-                result_in_outer_scope.substitute(&Renumber {
-                    offset: self.num_binders,
-                    exts: self.extension_registry(),
-                })
-            }
-        }
-    }
-
-    fn extension_registry(&self) -> &ExtensionRegistry {
-        self.underlying.extension_registry()
+        Ok(self.body.substitute(&Substitution(args, ext_reg)))
     }
 }
 
@@ -221,7 +103,7 @@ pub(crate) mod test {
     use lazy_static::lazy_static;
     use smol_str::SmolStr;
 
-    use crate::extension::prelude::{array_type, PRELUDE_ID, USIZE_CUSTOM_T, USIZE_T};
+    use crate::extension::prelude::{PRELUDE_ID, USIZE_CUSTOM_T, USIZE_T};
     use crate::extension::{
         ExtensionId, ExtensionRegistry, SignatureError, TypeDefBound, PRELUDE, PRELUDE_REGISTRY,
     };
@@ -244,7 +126,7 @@ pub(crate) mod test {
             extension_registry: &ExtensionRegistry,
         ) -> Result<Self, SignatureError> {
             let res = Self::new(params, body);
-            res.validate(extension_registry, &[])?;
+            res.validate(extension_registry)?;
             Ok(res)
         }
     }
@@ -451,171 +333,4 @@ pub(crate) mod test {
         )?;
         Ok(())
     }
-
-    fn new_pf1(param: TypeParam, input: Type, output: Type) -> PolyFuncType {
-        PolyFuncType {
-            params: vec![param],
-            body: FunctionType::new(vec![input], vec![output]),
-        }
-    }
-
-    const USIZE_TA: TypeArg = TypeArg::Type { ty: USIZE_T };
-
-    #[test]
-    fn partial_instantiate() -> Result<(), SignatureError> {
-        // forall A,N.(Array<A,N> -> A)
-        let array_max = PolyFuncType::new_validated(
-            vec![TypeBound::Any.into(), TypeParam::max_nat()],
-            FunctionType::new(
-                vec![array_type(
-                    TypeArg::new_var_use(1, TypeParam::max_nat()),
-                    Type::new_var_use(0, TypeBound::Any),
-                )],
-                vec![Type::new_var_use(0, TypeBound::Any)],
-            ),
-            &PRELUDE_REGISTRY,
-        )?;
-
-        let concrete = FunctionType::new(
-            vec![array_type(TypeArg::BoundedNat { n: 3 }, USIZE_T)],
-            vec![USIZE_T],
-        );
-        let actual = array_max
-            .instantiate_poly(&[USIZE_TA, TypeArg::BoundedNat { n: 3 }], &PRELUDE_REGISTRY)?;
-
-        assert_eq!(actual, concrete.into());
-
-        // forall N.(Array<usize,N> -> usize)
-        let partial = PolyFuncType::new_validated(
-            vec![TypeParam::max_nat()],
-            FunctionType::new(
-                vec![array_type(
-                    TypeArg::new_var_use(0, TypeParam::max_nat()),
-                    USIZE_T,
-                )],
-                vec![USIZE_T],
-            ),
-            &PRELUDE_REGISTRY,
-        )?;
-        let res = array_max.instantiate_poly(&[USIZE_TA], &PRELUDE_REGISTRY)?;
-        assert_eq!(res, partial);
-
-        Ok(())
-    }
-
-    fn list_of_tup(t1: Type, t2: Type) -> Type {
-        let list_def = EXTENSION.get_type(LIST_TYPENAME.as_str()).unwrap();
-        Type::new_extension(
-            list_def
-                .instantiate([TypeArg::Type {
-                    ty: Type::new_tuple(vec![t1, t2]),
-                }])
-                .unwrap(),
-        )
-    }
-
-    // forall A. A -> (forall C. C -> List(Tuple(C, A))
-    pub(crate) fn nested_func() -> PolyFuncType {
-        PolyFuncType::new_validated(
-            vec![TypeBound::Any.into()],
-            FunctionType::new(
-                vec![Type::new_var_use(0, TypeBound::Any)],
-                vec![Type::new_function(new_pf1(
-                    TypeBound::Copyable.into(),
-                    Type::new_var_use(0, TypeBound::Copyable),
-                    list_of_tup(
-                        Type::new_var_use(0, TypeBound::Copyable),
-                        Type::new_var_use(1, TypeBound::Any), // The outer variable (renumbered)
-                    ),
-                ))],
-            ),
-            &REGISTRY,
-        )
-        .unwrap()
-    }
-
-    #[test]
-    fn test_instantiate_nested() -> Result<(), SignatureError> {
-        let outer = nested_func();
-
-        let arg = array_type(TypeArg::BoundedNat { n: 5 }, USIZE_T);
-        // `arg` -> (forall C. C -> List(Tuple(C, `arg`)))
-        let outer_applied = FunctionType::new(
-            vec![arg.clone()], // This had index 0, but is replaced
-            vec![Type::new_function(new_pf1(
-                TypeBound::Copyable.into(),
-                // We are checking that the substitution has been applied to the right var
-                // - NOT to the inner_var which has index 0 here
-                Type::new_var_use(0, TypeBound::Copyable),
-                list_of_tup(
-                    Type::new_var_use(0, TypeBound::Copyable),
-                    arg.clone(), // This had index 1, but is replaced
-                ),
-            ))],
-        );
-
-        let res = outer.instantiate(&[TypeArg::Type { ty: arg }], &REGISTRY)?;
-        assert_eq!(res, outer_applied);
-        Ok(())
-    }
-
-    #[test]
-    fn free_var_under_binder() {
-        let outer = nested_func();
-
-        // Now substitute in a free var from further outside
-        const FREE: usize = 3;
-        const TP_EQ: TypeParam = TypeParam::Type { b: TypeBound::Eq };
-        let res = outer
-            .instantiate(&[TypeArg::new_var_use(FREE, TP_EQ)], &REGISTRY)
-            .unwrap();
-        assert_eq!(
-            res,
-            // F -> forall C. (C -> List(Tuple(C, F)))
-            FunctionType::new(
-                vec![Type::new_var_use(FREE, TypeBound::Eq)],
-                vec![Type::new_function(new_pf1(
-                    TypeBound::Copyable.into(),
-                    Type::new_var_use(0, TypeBound::Copyable), // unchanged
-                    list_of_tup(
-                        Type::new_var_use(0, TypeBound::Copyable),
-                        // Next is the free variable that we substituted in (hence Eq)
-                        // - renumbered because of the intervening forall (Copyable)
-                        Type::new_var_use(FREE + 1, TypeBound::Eq)
-                    )
-                ))]
-            )
-        );
-
-        // Also try substituting in a type containing both free and bound vars
-        let rhs = |i| {
-            Type::new_function(new_pf1(
-                TP_EQ,
-                Type::new_var_use(0, TypeBound::Eq),
-                array_type(
-                    TypeArg::new_var_use(i, TypeParam::max_nat()),
-                    Type::new_var_use(0, TypeBound::Eq),
-                ),
-            ))
-        };
-
-        let res = outer
-            .instantiate(&[TypeArg::Type { ty: rhs(FREE) }], &REGISTRY)
-            .unwrap();
-        assert_eq!(
-            res,
-            FunctionType::new(
-                vec![rhs(FREE)], // Input: forall TEQ. (TEQ -> Array(TEQ, FREE))
-                // Output: forall C. C -> List(Tuple(C, Input))
-                vec![Type::new_function(new_pf1(
-                    TypeBound::Copyable.into(),
-                    Type::new_var_use(0, TypeBound::Copyable),
-                    list_of_tup(
-                        Type::new_var_use(0, TypeBound::Copyable), // not renumbered...
-                        rhs(FREE + 1)                              // renumbered
-                    )
-                ))]
-            )
-        )
-    }
 }
diff --git a/hugr/src/types/serialize.rs b/hugr/src/types/serialize.rs
index f2299ffb7..1e80cce65 100644
--- a/hugr/src/types/serialize.rs
+++ b/hugr/src/types/serialize.rs
@@ -1,4 +1,4 @@
-use super::{PolyFuncType, SumType, Type, TypeArg, TypeBound, TypeEnum};
+use super::{FunctionType, SumType, Type, TypeArg, TypeBound, TypeEnum};
 
 use super::custom::CustomType;
 
@@ -10,7 +10,7 @@ use crate::ops::AliasDecl;
 pub(super) enum SerSimpleType {
     Q,
     I,
-    G(Box<PolyFuncType>),
+    G(Box<FunctionType>),
     Sum(SumType),
     Array { inner: Box<SerSimpleType>, len: u64 },
     Opaque(CustomType),
diff --git a/hugr/src/types/signature.rs b/hugr/src/types/signature.rs
index 38641f13c..c7a4f2e85 100644
--- a/hugr/src/types/signature.rs
+++ b/hugr/src/types/signature.rs
@@ -11,8 +11,11 @@ use crate::extension::{ExtensionRegistry, ExtensionSet, SignatureError};
 use crate::{Direction, IncomingPort, OutgoingPort, Port};
 
 #[derive(Clone, Debug, Default, PartialEq, Eq, serde::Serialize, serde::Deserialize)]
-/// Describes the edges required to/from a node. This includes both the concept of "signature" in the spec,
+/// Describes the edges required to/from a node, and thus, also the type of a [Graph].
+/// This includes both the concept of "signature" in the spec,
 /// and also the target (value) of a call (static).
+///
+/// [Graph]: crate::ops::constant::Const::Function
 pub struct FunctionType {
     /// Value inputs of the function.
     pub input: TypeRow,
@@ -41,7 +44,7 @@ impl FunctionType {
         self.extension_reqs.validate(var_decls)
     }
 
-    pub(crate) fn substitute(&self, tr: &impl Substitution) -> Self {
+    pub(crate) fn substitute(&self, tr: &Substitution) -> Self {
         FunctionType {
             input: subst_row(&self.input, tr),
             output: subst_row(&self.output, tr),
diff --git a/hugr/src/types/type_param.rs b/hugr/src/types/type_param.rs
index e6d90a249..601dfda14 100644
--- a/hugr/src/types/type_param.rs
+++ b/hugr/src/types/type_param.rs
@@ -178,7 +178,7 @@ pub struct TypeArgVariable {
 
 impl TypeArg {
     /// Makes a TypeArg representing a use (occurrence) of the type variable
-    /// with the specified DeBruijn index. For use within type schemes only:
+    /// with the specified index. For use within type schemes only:
     /// `bound` must match that with which the variable was declared.
     pub fn new_var_use(idx: usize, decl: TypeParam) -> Self {
         match decl {
@@ -224,7 +224,7 @@ impl TypeArg {
         }
     }
 
-    pub(crate) fn substitute(&self, t: &impl Substitution) -> Self {
+    pub(crate) fn substitute(&self, t: &Substitution) -> Self {
         match self {
             TypeArg::Type { ty } => TypeArg::Type {
                 ty: ty.substitute(t),
diff --git a/specification/hugr.md b/specification/hugr.md
index 8944fb859..4d99bfb21 100644
--- a/specification/hugr.md
+++ b/specification/hugr.md
@@ -123,33 +123,40 @@ carry an edge weight:
   ordering. They have no edge weight.
 - `Value` edges carry typed data at runtime. They have a *port* at each end, associated
   with the source and target nodes. They have an `AnyType`as an edge weight.
-- `Static` edges are similar to `Value` edges but carry static data (knowable at
-  compilation time). They have a `CopyableType` as an edge weight.
+- `Const` edges are similar to `Value` edges but carry static data (knowable at
+  compilation time). These have as edge weight a `CopyableType`.
+- `Function` edges refer to a statically-known function, but with a type scheme
+  that (unlike values) may be polymorphic---see [Polymorphism](#polymorphism).
 - `ControlFlow` edges represent possible flows of control from one part of the
   program to another. They have no edge weight.
 - `Hierarchy` edges express the relationship between container nodes and their
   children. They have no edge weight.
 
-`Value` and `Static` edges are sometimes referred to as *dataflow* edges.
+It is useful to introduce some terms for broader classes of edge:
+* *Static* edges are the union of the `Const` and `Function` edges
+* *Dataflow* edges are the union of `Value` and Static (thus, `Value`, `Const` and `Function`)
+
 A `Value` edge can carry data of any `AnyType`: these include the `CopyableType`s
 (which can be freely copied or discarded - i.e. ordinary classical data)
 as well as anything which cannot - e.g. quantum data.
-A `Static` edge can only carry a `CopyableType`. For
+A `Const` edge can only carry a `CopyableType`. For
 more details see the [Type System](#type-system) section.
 
-As well as the type, dataflow edges are also parametrized by a
+As well as the type, Dataflow edges are also parametrized by a
 `Locality`, which declares whether the edge crosses levels in the hierarchy. See
 [Edge Locality](#edge-locality) for details.
 
 ```haskell
 AnyType ⊃ CopyableType
 
-EdgeKind ::= Hierarchy | Value(Locality, AnyType) | Static(Local | Ext, CopyableType) | Order | ControlFlow
+EdgeKind ::= Value(Locality, AnyType)
+             | Const(Local | Ext, CopyableType) | Function(Local | Ext, PolyFuncType)
+             | Hierarchy | Order | ControlFlow
 ```
 
-Note that a port is associated with a node and zero or more dataflow edges.
+Note that a port is associated with a node and zero or more Dataflow edges.
 Incoming ports are associated with exactly one edge, or many `ControlFlow` edges.
-All dataflow edges associated with a port have the same type; thus a port has a
+All Dataflow edges associated with a port have the same type; thus a port has a
 well defined type, matching that of its adjoining edges. The incoming and
 outgoing ports of a node are each ordered independently, meaning that the first
 output port will be "0" regardless of how many input ports there are.
@@ -190,11 +197,11 @@ source of the edge will, at runtime, produce a value that is consumed by
 the edge's target. Value edges are from an outgoing port of the
 source node, to an incoming port of the target node.
 
-#### `Static` edges
+#### Static edges (`Const` and `Function`)
 
-A `Static` edge represents dataflow that is statically knowable - i.e.
+A Static edge represents dataflow that is statically knowable - i.e.
 the source is a compile-time constant defined in the program. Hence, the types on these edges
-are classical, and do not include an extension specification. Only a few nodes may be
+are classical. Only a few nodes may be
 sources (`FuncDefn`, `FuncDecl` and `Const`) and targets (`Call` and `LoadConstant`) of
 these edges; see [operations](#node-operations).
 
@@ -231,7 +238,7 @@ edges. The following operations are *only* valid as immediate children of a
 - `FuncDecl`: an external function declaration. The name of the function,
   a list of type parameters (TypeParams, see [Type System](#type-system))
   and function attributes (relevant for compilation)
-  define the node weight. The node has an outgoing `Static<Function>`
+  define the node weight. The node has an outgoing `Function`
   edge for each use of the function. The function name is used at link time to
   look up definitions in linked
   modules (other hugr instances specified to the linker).
@@ -247,7 +254,7 @@ The following operations are valid at the module level as well as in dataflow
 regions and control-flow regions:
 
 - `Const<T>` : a static constant value of type T stored in the node
-  weight. Like `FuncDecl` and `FuncDefn` this has one `Static<T>` out-edge per use.
+  weight. Like `FuncDecl` and `FuncDefn` this has one `Const<T>` out-edge per use.
 - `FuncDefn` : a function definition. Like `FuncDecl` but with a function body.
   The function body is defined by the sibling graph formed by its children.
   At link time `FuncDecl` nodes are replaced by `FuncDefn`.
@@ -272,16 +279,11 @@ the following basic dataflow operations are available (in addition to the
   the inputs to the function, and the inputs to `Output` are the
   outputs of the function.
 - `Call`: Call a statically defined function. There is an incoming
-  `Static<Function>` edge to specify the graph being called. The `Call`
+  `Function` edge to specify the graph being called. The `Call`
   node specifies any type arguments to the function in the node weight,
   and the signature of the node (defined by its incoming and outgoing `Value` edges)
   matches the (type-instantiated) function being called.
-- `TypeApply`: has a `Value<Function>` input, whose type is polymorphic (i.e. declares some type parameters);
-  the node specifies some number of type arguments (matching those parameters) in the node weight;
-  and there is  a `Value<Function>` output (corresponding to the type instantiation of the input
-  - for a *partial* type application, i.e. with fewer arguments than declared type parameters,
-  the output type will also be polymorphic).
-- `LoadConstant<T>`: has an incoming `Static<T>` edge, where `T` is a `CopyableType`, and a
+- `LoadConstant<T>`: has an incoming `Const<T>` edge, where `T` is a `CopyableType`, and a
   `Value<T>` output, used to load a static constant into the local
   dataflow graph.
 - `identity<T>`: pass-through, no operation is performed.
@@ -325,7 +327,7 @@ flowchart
 
 In a dataflow graph, the evaluation semantics are simple: all nodes in
 the graph are necessarily evaluated, in some order (perhaps parallel)
-respecting the dataflow edges. The following operations are used to
+respecting the Dataflow edges. The following operations are used to
 express control flow, i.e. conditional or repeated evaluation.
 
 ##### `Conditional` nodes
@@ -501,8 +503,8 @@ has no parent).
 | Conditional               | **D**                          | `Conditional`      | **C**         | `Case`                   | No edges                                 |
 | **C:** Dataflow container | **D**                          | `TailLoop`         | **C**         |  **D**                   | First(second) is `Input`(`Output`)       |
 | **C**                     | **D**                          | `DFG`              | **C**         |  **D**                   | First(second) is `Input`(`Output`)       |
-| **C**                     | Static                         | `FuncDefn`         | **C**         |  **D**                   | First(second) is `Input`(`Output`)       |
-| **C**                     | ControlFlow                    | `DFB`              | CFG           |  **D**                   | First(second) is `Input`(`Output`)       |
+| **C**                     | `Function`                     | `FuncDefn`         | **C**         |  **D**                   | First(second) is `Input`(`Output`)       |
+| **C**                     | `ControlFlow`                  | `DFB`              | CFG           |  **D**                   | First(second) is `Input`(`Output`)       |
 | **C**                     | \-                             | `Case`             | `Conditional` |  **D**                   | First(second) is `Input`(`Output`)       |
 | Root                      | \-                             | `Module`           | none          |  **D**                   | Contains main `FuncDefn` for executable HUGR. |
 
@@ -535,7 +537,7 @@ There are three possible `CopyableType` edge localities:
 - `Ext`: Edges "in" from a dataflow ancestor.
 - `Dom`: Edges from a dominating basic block in a control-flow graph.
 
-We allow non-local dataflow edges
+We allow non-local Dataflow edges
 n<sub>1</sub>→n<sub>2</sub> where parent(n<sub>1</sub>) \!=
 parent(n<sub>2</sub>) when the edge's locality is:
 
@@ -604,7 +606,7 @@ bypassing the input/output nodes, and we expect this form to make
 rewrites easier to spot. The constraints on input/output node signatures
 remain as before.
 
-HUGRs with only local dataflow edges may still be useful for e.g. register
+HUGRs with only local Dataflow edges may still be useful for e.g. register
 allocation, as that representation makes storage explicit. For example,
 when a true/false subgraph of a Conditional-node wants a value from the
 outside, we add an outgoing port to the Input node of each subgraph, a
@@ -777,7 +779,7 @@ There are three classes of type: `AnyType` $\supset$ `CopyableType` $\supset$ `E
 - The next class is `CopyableType`, i.e. types holding ordinary classical
   data, where values can be copied (and discarded, the 0-ary copy). This
   allows multiple (or 0) outgoing edges from an outport; also these types can
-  be sent down `Static` edges. Note: dataflow inputs (`Value` and `Static`) always
+  be sent down `Const` edges. Note: dataflow inputs (`Value`, `Const` and `Function`) always
   require a single connection.
 
 - The final class is `EqType`: these are copyable types with a well-defined
@@ -796,8 +798,7 @@ Extensions ::= (Extension)* -- a set, not a list
 
 Type ::= Sum([#]) -- disjoint union of rows of other types, tagged by unsigned int
        | Opaque(Name, [TypeArg]) -- a (instantiation of a) custom type defined by an extension
-       | Function(TypeParams, #, #, Extensions) -- polymorphic with type parameters,
-                                                -- function arguments + results, and delta (see below)
+       | Function(#, #, Extensions) -- monomorphic function: arguments, results, and delta (see below)
        | Variable -- refers to a TypeParam bound by the nearest enclosing FuncDefn node, or an enclosing Function Type
 ```
 
@@ -813,7 +814,9 @@ Sums are `CopyableType` (respectively, `EqType`) if all their components are; th
 
 ### Polymorphism
 
-`Function` types are polymorphic: they may declare a number of type parameters of kinds as follows:
+While function *values* passed around the graph at runtime have types that are monomorphic,
+`FuncDecl` and `FuncDefn` nodes have not types but *type schemes* that are *polymorphic*---that is,
+such declarations may include (bind) any number of type parameters, of kinds as follows:
 
 ```haskell
 TypeParam ::= Type(Any|Copyable|Eq)
@@ -824,33 +827,34 @@ TypeParam ::= Type(Any|Copyable|Eq)
             | Opaque(Name, [TypeArg]) -- e.g. Opaque("Array", [5, Opaque("usize", [])])
 ```
 
-For each such TypeParam, the body of the FunctionType (input, output, and extensions - see [Extension Tracking](#extension-tracking))
-may contain "type variables" referring to that TypeParam, i.e. the binder. (The type variable is typically a type, but
-not necessarily, depending upon the TypeParam.)
+The same mechanism is also used for polymorphic OpDefs, see [Extension Implementation](#extension-implementation).
+
+Within the type of the Function node, and within the body (Hugr) of a `FuncDefn`,
+types may contain "type variables" referring to those TypeParams.
+The type variable is typically a type, but not necessarily, depending upon the TypeParam.
 
-When a `FuncDefn` or `FuncDecl` with such a `Function` type is `Call`ed, the `Call` node statically provides
-TypeArgs appropriate for the TypeParams (and similarly for `TypeApply` nodes):
+When a `FuncDefn` or `FuncDecl` is `Call`ed, the `Call` node statically provides
+TypeArgs appropriate for the function's TypeParams:
 
 ```haskell
-TypeArg ::= Type(Type)
+TypeArg ::= Type(Type) -- could be a variable of kind Type, or contain variable(s)
+          | Extensions(Extensions) -- may contain TypeArg's of kind Extensions
+          | Variable -- refers to an enclosing TypeParam (binder) of any kind below
           | BoundedUSize(u64)
-          | Extensions(Extensions)
-          | Sequence([TypeArg])
+          | Sequence([TypeArg]) -- fits either a List or Tuple TypeParam
           | Opaque(Value)
-          | Variable -- refers to an enclosing TypeParam (binder)
 ```
 
-A `Sequence` argument is appropriate for a parameter of kind either `List` or `Tuple`.
-For example, a Function declaring a `TypeParam::Opaque("Array", [5, TypeArg::Type(Type::Opaque("usize"))])`
+For example, a Function node declaring a `TypeParam::Opaque("Array", [5, TypeArg::Type(Type::Opaque("usize"))])`
 means that any `Call` to it must statically provide a *value* that is an array of 5 `usize`s;
-or a Function declaring a `TypeParam::BoundedUSize(5)` and a `TypeParam::Type(Any)` requires two TypeArgs,
+or a Function node declaring a `TypeParam::BoundedUSize(5)` and a `TypeParam::Type(Any)` requires two TypeArgs,
 firstly a non-negative integer less than 5, secondly a type (which might be from an extension, e.g. `usize`).
 
-Given TypeArgs, the body of the `Function` type can be converted to a monomorphic signature by substitution,
+Given TypeArgs, the body of the Function node's type can be converted to a monomorphic signature by substitution,
 i.e. replacing each type variable in the body with the corresponding TypeArg. This is guaranteed to produce
 a valid type as long as the TypeArgs match the declared TypeParams, which can be checked in advance.
 
-(Note that when within a `Function` type, type variables of kind `List`, `Tuple` or `Opaque` will only be usable
+(Note that within a polymorphic type scheme, type variables of kind `Sequence` or `Opaque` will only be usable
 as arguments to Opaque types---see [Extension System](#extension-system).)
 
 ### Extension Tracking
@@ -998,19 +1002,20 @@ at runtime. In many cases this is desirable.
 To strike a balance then, every extension provides declarative structs containing
 named **TypeDef**s and **OpDef**s---see [Declarative Format](#declarative-format).
 These are (potentially polymorphic) definitions of types and operations, respectively---polymorphism arises because both may
-declare any number of TypeParams (as per [Type System](#type-system)). To use a TypeDef as a type,
+declare any number of TypeParams, as per [Polymorphism](#polymorphism). To use a TypeDef as a type,
 it must be instantiated with TypeArgs appropriate for its TypeParams, and similarly
 to use an OpDef as a node operation: each `OpaqueOp` node stores a static-constant list of TypeArgs.
 
 For TypeDef's, any set of TypeArgs conforming to its TypeParams, produces a valid type.
 However, for OpDef's, greater flexibility is allowed: each OpDef *either*
 
-1. Provides a `Function` type, as per [Type System](#type-system), which may declare TypeParams; *or*
+1. Provides a polymorphic type scheme, as per [Type System](#type-system), which may declare TypeParams;
+   values (TypeArgs) provided for those params will be substituted in. *Or*
 2. The extension may self-register binary code (e.g. a Rust trait) providing a function
-   `compute_signature` that fallibly computes a `Function` type given some type arguments.
+   `compute_signature` that fallibly computes a (perhaps-polymorphic) type scheme given some initial type arguments.
    The operation declares the arguments required by the `compute_signature` function as a list
-   of TypeParams; if this successfully returns a `Function` type, then that may then require
-   additional TypeParams.
+   of TypeParams; if this successfully returns a type scheme, that may have additional TypeParams
+   for which TypeArgs must also be provided.
 
 For example, the TypeDef for `array` in the prelude declares two TypeParams: a `BoundedUSize`
 (the array length) and a `Type`. Any valid instantiation (e.g. `array<5, usize>`) is a type.
@@ -1048,7 +1053,7 @@ either or both:
 Whether a particular OpDef provides binary code for `try_lower` is independent
 of whether it provides a binary `compute_signature`, but it will not generally
 be possible to provide a HUGR for an operation whose type cannot be expressed
-as a constant (polymorphic) `Function` type
+using a polymorphic type scheme.
 
 ### Declarative format
 
@@ -1309,10 +1314,10 @@ The new hugr is then derived as follows:
    the existing edges are replaced.
 3. For each $\sigma\_\mathrm{out} \in \mu\_\textrm{out}$, insert a new edge going out of the new
    copy of the `SrcNode` of $\sigma\_\mathrm{out}$ according to the specification $\sigma\_\mathrm{out}$.
-   For Value or Static edges, the target port must have an existing edge whose source is in $R$;
+   For `Value` or Static edges, the target port must have an existing edge whose source is in $R$;
    this edge is removed.
 4. For each $\sigma\_\mathrm{new} \in \mu\_\textrm{new}$, insert a new edge
-   between the existing `SrcNode` and `TgtNode` in $\Gamma$. For Value/Static edges,
+   between the existing `SrcNode` and `TgtNode` in $\Gamma$. For `Value` or Static edges,
    the target port must have an existing edge whose source is in $R$; this edge is removed.
 5. Let $N$ be the ordered list of the copies made in $\Gamma$ of the children of the root node of $G$.
    For each child $C$ of $P$ (in order), if $C \in S$, redirect the hierarchy edge $P \rightarrow C$ to
@@ -1401,7 +1406,7 @@ remove it. (If there is an non-local edge from `n0` to a descendent of
 ###### `InsertConstIgnore`
 
 Given a `Const<T>` node `c`, and optionally `P`, a parent of a DSG, add a new
-`LoadConstant<T>` node `n` as a child of `P` with a `Static<T>` edge
+`LoadConstant<T>` node `n` as a child of `P` with a `Const<T>` edge
 from `c` to `n` and no outgoing edges from `n`.  Return the ID of `n`. If `P` is
 omitted it defaults to the parent of `c` (in this case said `c` will
 have to be in a DSG or CSG rather than under the Module Root.) If `P` is
@@ -1451,7 +1456,7 @@ Similarly, replacement of a CFG node having a single BasicBlock child
 with a DFG node can be achieved using `Replace` (specifying the
 BasicBlock node as the surrogate parent for the new DFG's children).
 
-Arbitrary node insertion on dataflow edges can be achieved using
+Arbitrary node insertion on Dataflow edges can be achieved using
 `InsertIdentity` followed by `Replace`. Removal of a node in a DSG
 having input wires and output wires of the same type can be achieved
 using `Replace` (with a set of `identity<T>` nodes) followed by
@@ -1815,7 +1820,7 @@ Conversions between integers and floats:
   node, with all the edges between them. Includes exactly one entry
   and one exit node. Nodes are basic blocks, edges point to possible
   successors.
-- **Dataflow edge** either a Value edge or a Static edge; has a type,
+- **Dataflow edge** either a `Value` edge or a Static edge; has a type,
   and runs between an output port and an input port.
 - **Dataflow Sibling Graph (DSG)**: The set of all children of a given
   Dataflow container node, with all edges between them. Includes
@@ -1828,14 +1833,14 @@ Conversions between integers and floats:
   value edges.
 - **FuncDecl node**: child of a module, indicates that an external
   function exists but without giving a definition. May be the source
-  of Static-edges to Call nodes and others.
+  of `Function`-edges to Call nodes.
 - **FuncDefn node**: child of a module node, defines a function (by being
-  parent to the function's body). May be the source of Static-edges to
-  Call nodes and others.
+  parent to the function's body). May be the source of `Function`-edges
+  to Call nodes.
 - **DFG node**: A node representing a data-flow graph. Its children
   are all data-dependency nodes.
-- **edge kind**: There are five kinds of edge: value edge, order edge,
-  control-flow edge, Static edge, and hierarchy edge.
+- **edge kind**: There are six kinds of edge: `Value` edge, order edge, hierarchy edge,
+  control-flow edge, `Const` edge and `Function` edge.
 - **edge type:** Typing information attached to a value edge or Static
   edge (representing the data type of value that the edge carries).
 - **entry node**: The distinguished node of a CFG representing the
@@ -1883,6 +1888,7 @@ Conversions between integers and floats:
   input and output signatures.
 - **simple type**: a quantum or classical type annotated with the
   Extensions required to produce the value
+- **Static edge**: either a `Const` or `Function` edge
 - **order edge**: An edge implying dependency of the target node on
   the source node.
 - **TailLoop node**: TODO
@@ -1981,26 +1987,26 @@ one". For example, "1, ✱" means "one edge in, any number out".
 The "Root" row of the table applies to whichever node is the HUGR root,
 including `Module`.
 
-| Node type      | `Value` | `Order` | `Static` | `ControlFlow` | `Hierarchy` | Children |
-| -------------- | ------- | ------- |--------- | ------------- | ----------- | -------- |
-| Root           | 0, 0    | 0, 0    | 0, 0     | 0, 0          | 0, ✱        |          |
-| `FuncDefn`     | 0, 0    | 0, 0    | 0, ✱     | 0, 0          | 1, +        | DSG      |
-| `FuncDecl`     | 0, 0    | 0, 0    | 0, ✱     | 0, 0          | 1, 0        |          |
-| `AliasDefn`    | 0, 0    | 0, 0    | 0, 0     | 0, 0          | 1, 0        |          |
-| `AliasDecl`    | 0, 0    | 0, 0    | 0, 0     | 0, 0          | 1, 0        |          |
-| `Const`        | 0, 0    | 0, 0    | 0, ✱     | 0, 0          | 1, 0        |          |
-| `LoadConstant` | 0, 1    | +, ✱    | 1, 0     | 0, 0          | 1, 0        |          |
-| `Input`        | 0, ✱    | 0, ✱    | 0, 0     | 0, 0          | 1, 0        |          |
-| `Output`       | ✱, 0    | ✱, 0    | 0, 0     | 0, 0          | 1, 0        |          |
-| `LeafOp`       | ✱, ✱    | ✱, ✱    | ✱, 0     | 0, 0          | 1, 0        |          |
-| `Call`         | ✱, ✱    | ✱, ✱    | 1, 0     | 0, 0          | 1, 0        |          |
-| `DFG`          | ✱, ✱    | ✱, ✱    | 0, 0     | 0, 0          | 1, +        | DSG      |
-| `CFG`          | ✱, ✱    | ✱, ✱    | 0, 0     | 0, 0          | 1, +        | CSG      |
-| `DFB`          | 0, 0    | 0, 0    | 0, 0     | ✱, ✱          | 1, +        | DSG      |
-| `Exit`         | 0, 0    | 0, 0    | 0, 0     | +, 0          | 1, 0        |          |
-| `TailLoop`     | ✱, ✱    | ✱, ✱    | 0, 0     | 0, 0          | 1, +        | DSG      |
-| `Conditional`  | ✱, ✱    | ✱, ✱    | 0, 0     | 0, 0          | 1, +        | `Case`   |
-| `Case`         | 0, 0    | 0, 0    | 0, 0     | 0, 0          | 1, +        | DSG      |
+| Node type      | `Value` | `Order` | `Const` | `Function` | `ControlFlow` | `Hierarchy` | Children |
+| -------------- | ------- | ------- |-------- | ---------- | ------------- | ----------- | -------- |
+| Root           | 0, 0    | 0, 0    | 0, 0    | 0, 0       | 0, 0          | 0, ✱        |          |
+| `FuncDefn`     | 0, 0    | 0, 0    | 0, 0    | 0, *       | 0, 0          | 1, +        | DSG      |
+| `FuncDecl`     | 0, 0    | 0, 0    | 0, 0    | 0, *       | 0, 0          | 1, 0        |          |
+| `AliasDefn`    | 0, 0    | 0, 0    | 0, 0    | 0, 0       | 0, 0          | 1, 0        |          |
+| `AliasDecl`    | 0, 0    | 0, 0    | 0, 0    | 0, 0       | 0, 0          | 1, 0        |          |
+| `Const`        | 0, 0    | 0, 0    | 0, ✱    | 0, 0       | 0, 0          | 1, 0        |          |
+| `LoadConstant` | 0, 1    | +, ✱    | 1, 0    | 0, 0       | 0, 0          | 1, 0        |          |
+| `Input`        | 0, ✱    | 0, ✱    | 0, 0    | 0, 0       | 0, 0          | 1, 0        |          |
+| `Output`       | ✱, 0    | ✱, 0    | 0, 0    | 0, 0       | 0, 0          | 1, 0        |          |
+| `LeafOp`       | ✱, ✱    | ✱, ✱    | 0, 0    | 0, 0       | 0, 0          | 1, 0        |          |
+| `Call`         | ✱, ✱    | ✱, ✱    | 0, 0    | 1, 0       | 0, 0          | 1, 0        |          |
+| `DFG`          | ✱, ✱    | ✱, ✱    | 0, 0    | 0, 0       | 0, 0          | 1, +        | DSG      |
+| `CFG`          | ✱, ✱    | ✱, ✱    | 0, 0    | 0, 0       | 0, 0          | 1, +        | CSG      |
+| `DFB`          | 0, 0    | 0, 0    | 0, 0    | 0, 0       | ✱, ✱          | 1, +        | DSG      |
+| `Exit`         | 0, 0    | 0, 0    | 0, 0    | 0, 0       | +, 0          | 1, 0        |          |
+| `TailLoop`     | ✱, ✱    | ✱, ✱    | 0, 0    | 0, 0       | 0, 0          | 1, +        | DSG      |
+| `Conditional`  | ✱, ✱    | ✱, ✱    | 0, 0    | 0, 0       | 0, 0          | 1, +        | `Case`   |
+| `Case`         | 0, 0    | 0, 0    | 0, 0    | 0, 0       | 0, 0          | 1, +        | DSG      |
 
 ### Appendix 3: Binary `compute_signature`
 
@@ -2009,11 +2015,11 @@ When an OpDef provides a binary `compute_signature` function, and an operation n
 - the node provides a list of TypeArgs, at least as many as the $n$ TypeParams declared by the OpDef
 - the first $n$ of those are passed to the binary `compute_signature`
 - if the binary function returns an error, the operation is invalid;
-- otherwise, `compute_signature` returns a `Function` type (which may itself be polymorphic)
-- any remaining TypeArgs in the node (after the first $n$) are then substituted into that returned `Function` type
+- otherwise, `compute_signature` returns a type scheme (which may itself be polymorphic)
+- any remaining TypeArgs in the node (after the first $n$) are then substituted into that returned type scheme
   (the number remaining in the node must match exactly).
   **Note** this allows the binary function to use the values (TypeArgs) passed in---e.g.
-  by looking inside `List` or `Opaque` TypeArgs---to determine the structure (and degree of polymorphism) of the returned `Function` type.
+  by looking inside `List` or `Opaque` TypeArgs---to determine the structure (and degree of polymorphism) of the returned type scheme.
 - We require that the TypeArgs to be passed to `compute_signature` (the first $n$)
   must *not* refer to any type variables (declared by ancestor nodes in the Hugr - the nearest enclosing FuncDefn);
   these first $n$ must be static constants unaffected by substitution.
diff --git a/specification/schema/hugr_schema_v1.json b/specification/schema/hugr_schema_v1.json
index 1ca87f089..6b6731be5 100644
--- a/specification/schema/hugr_schema_v1.json
+++ b/specification/schema/hugr_schema_v1.json
@@ -585,6 +585,11 @@
         "FunctionType": {
             "description": "A graph encoded as a value. It contains a concrete signature and a set of required resources.",
             "properties": {
+                "t": {
+                    "const": "G",
+                    "default": "G",
+                    "title": "T"
+                },
                 "input": {
                     "items": {
                         "$ref": "#/$defs/Type"
@@ -1013,13 +1018,8 @@
             "type": "object"
         },
         "PolyFuncType": {
-            "description": "A graph encoded as a value. It contains a concrete signature and a set of required resources.",
+            "description": "A polymorphic type scheme, i.e. of a FuncDecl, FuncDefn or OpDef.  (Nodes/operations in the Hugr are not polymorphic.)",
             "properties": {
-                "t": {
-                    "const": "G",
-                    "default": "G",
-                    "title": "T"
-                },
                 "params": {
                     "items": {
                         "$ref": "#/$defs/TypeParam"
@@ -1281,7 +1281,7 @@
             "discriminator": {
                 "mapping": {
                     "Array": "#/$defs/Array",
-                    "G": "#/$defs/PolyFuncType",
+                    "G": "#/$defs/FunctionType",
                     "I": "#/$defs/USize",
                     "Opaque": "#/$defs/Opaque",
                     "Q": "#/$defs/Qubit",
@@ -1301,7 +1301,7 @@
                     "$ref": "#/$defs/USize"
                 },
                 {
-                    "$ref": "#/$defs/PolyFuncType"
+                    "$ref": "#/$defs/FunctionType"
                 },
                 {
                     "$ref": "#/$defs/Array"
@@ -1547,7 +1547,7 @@
             "type": "object"
         },
         "Variable": {
-            "description": "A type variable identified by a de Bruijn index.",
+            "description": "A type variable identified by an index into the array of TypeParams.",
             "properties": {
                 "t": {
                     "const": "V",