diff --git a/shared/typeinference/codeql/typeinference/internal/TypeInference.qll b/shared/typeinference/codeql/typeinference/internal/TypeInference.qll
index ca79740a2ceb..6c73d9c29c87 100644
--- a/shared/typeinference/codeql/typeinference/internal/TypeInference.qll
+++ b/shared/typeinference/codeql/typeinference/internal/TypeInference.qll
@@ -1,12 +1,126 @@
 /**
  * Provides shared functionality for computing type inference in QL.
  *
- * The code examples in this file use C# syntax, but the concepts should
- * carry over to other languages as well.
+ * The code examples in this file use C# syntax, but the concepts should carry
+ * over to other languages as well.
  *
- * The library is initialized in two phases: `Make1`, which constructs
- * the `TypePath` type, and `Make2`, which (using `TypePath` in the input
- * signature) constructs the `Matching` module.
+ * The library is initialized in two phases: `Make1`, which constructs the
+ * `TypePath` type, and `Make2`, which (using `TypePath` in the input signature)
+ * constructs the `Matching` and `IsInstantiationOf` modules.
+ *
+ * The intended use of this library is to define a predicate
+ *
+ * ```ql
+ * Type inferType(AstNode n, TypePath path)
+ * ```
+ *
+ * for recursively inferring the type-path-indexed types of AST nodes. For example,
+ * one may have a base case for literals like
+ *
+ * ```ql
+ * Type inferType(AstNode n, TypePath path) {
+ *   ...
+ *   n instanceof IntegerLiteral and
+ *   result instanceof IntType and
+ *   path.isEmpty()
+ *   ...
+ * }
+ * ```
+ *
+ * and recursive cases for local variables like
+ *
+ * ```ql
+ * Type inferType(AstNode n, TypePath path) {
+ *   ...
+ *   exists(LocalVariable v |
+ *     // propagate type information from the initializer to any access
+ *     n = v.getAnAccess() and
+ *     result = inferType(v.getInitializer(), path)
+ *     or
+ *     // propagate type information from any access back to the initializer; note
+ *     // that this case may not be relevant for all languages, but e.g. in Rust
+ *     // it is
+ *     n = v.getInitializer() and
+ *     result = inferType(v.getAnAccess(), path)
+ *   )
+ *   ...
+ * }
+ * ```
+ *
+ * The `Matching` module is used when an AST node references a potentially generic
+ * declaration, where the type of the node depends on the type of some of its sub
+ * nodes. For example, if we have a generic method like `T Identity<T>(T t)`, then
+ * the type of `Identity(42)` should be `int`, while the type of `Identity("foo")`
+ * should be `string`; in both cases it should _not_ be `T`.
+ *
+ * In order to infer the type of method calls, one would define something like
+ *
+ * ```ql
+ * private module MethodCallMatchingInput implements MatchingInputSig {
+ *   private newtype TDeclarationPosition =
+ *     TSelfDeclarationPosition() or
+ *     TPositionalDeclarationPosition(int pos) { ... } or
+ *     TReturnDeclarationPosition()
+ *
+ *   // A position inside a method with a declared type.
+ *   class DeclarationPosition extends TDeclarationPosition {
+ *     ...
+ *   }
+ *
+ *   class Declaration extends MethodCall {
+ *     // Gets a type parameter at `tppos` belonging to this method.
+ *     //
+ *     // For example, if this method is `T Identity<T>(T t)`, then `T`
+ *     // is at position `0`.
+ *     TypeParameter getTypeParameter(TypeParameterPosition tppos) { ... }
+ *
+ *     // Gets the declared type of this method at `dpos` and `path`.
+ *     //
+ *     // For example, if this method is `T Identity<T>(T t)`, then both the
+ *     // the return type and parameter position `0` is `T` with `path.isEmpty()`.
+ *     Type getDeclaredType(DeclarationPosition dpos, TypePath path) { ... }
+ *   }
+ *
+ *   // A position inside a method call with an inferred type
+ *   class AccessPosition = DeclarationPosition;
+ *
+ *   class Access extends MethodCall {
+ *     AstNode getNodeAt(AccessPosition apos) { ... }
+ *
+ *     // Gets the inferred type of the node at `apos` and `path`.
+ *     //
+ *     // For example, if this method call is `Identity(42)`, then the type
+ *     // at argument position `0` is `int` with `path.isEmpty()"`.
+ *     Type getInferredType(AccessPosition apos, TypePath path) {
+ *       result = inferType(this.getNodeAt(apos), path)
+ *     }
+ *
+ *     // Gets the method that this method call resolves to.
+ *     //
+ *     // This will typically be defined in mutual recursion with the `inferType`
+ *     // predicate, as we need to know the type of the receiver in order to
+ *     // resolve calls to instance methods.
+ *     Declaration getTarget() { ... }
+ *   }
+ *
+ *   predicate accessDeclarationPositionMatch(AccessPosition apos, DeclarationPosition dpos) {
+ *     apos = dpos
+ *   }
+ * }
+ *
+ * private module MethodCallMatching = Matching<MethodCallMatchingInput>;
+ *
+ * Type inferType(AstNode n, TypePath path) {
+ *   ...
+ *   exists(MethodCall mc, MethodCallMatchingInput::AccessPosition apos |
+ *     // Some languages may want to restrict `apos` to be the return position, but in
+ *     // e.g. Rust type information can flow out of all positions
+ *     n = a.getNodeAt(apos) and
+ *     result = MethodCallMatching::inferAccessType(a, apos, path)
+ *   )
+ *   ...
+ * }
+ * ```
  */
 
 private import codeql.util.Location