/**
 * Simple-sub inference engine for Dvala.
 *
 * Adapted from Parreaux's Simple-sub — a simplified implementation of
 * Dolan's algebraic subtyping. Type variables accumulate bounds via
 * biunification (constrain lhs <: rhs). Let-polymorphism uses levels.
 *
 * This module provides:
 * - InferenceContext: manages type variable allocation and levels
 * - constrain(lhs, rhs): the core biunification function
 * - inferExpr(node, ctx, env): infers a type for an AST node
 */
import type { Type, EffectSet } from './types';
import type { AstNode } from '../parser/types';
interface ResumeContext {
    argType: Type;
    answerType: Type;
}
type HandledSignatureMap = Map<string, {
    argType: Type;
    retType: Type;
}>;
/**
 * A mutable type variable. During inference, variables accumulate lower and
 * upper bounds. After inference, the bounds are resolved into a concrete type.
 *
 * The `level` field supports let-polymorphism: variables at a higher level
 * than the current scope are generalized (copied fresh) when referenced.
 */
export interface TypeVar {
    tag: 'Var';
    id: number;
    level: number;
    lowerBounds: Type[];
    upperBounds: Type[];
    displayLowerBounds?: Type[];
    displayUpperBounds?: Type[];
}
/**
 * Manages type variable allocation, level tracking, and constraint caching.
 */
export declare class InferenceContext {
    private nextId;
    private _level;
    /** Cycle guard: tracks (lhs, rhs) pairs already processed by constrain. */
    private constraintCache;
    /** Type annotations from the parser side-table. Keyed by binding target nodeId. */
    typeAnnotations: Map<number, string>;
    /** Resolves file imports for cross-file type checking. */
    resolveFileType?: (importPath: string) => Type;
    /**
     * Whether constant folding runs during this inference pass. Defaults to
     * the `FOLD_ENABLED` env-var value; callers (typecheck entry points)
     * may override via the `fold` option on TypecheckOptions.
     */
    foldEnabled: boolean;
    /** Stack of effect sets — each function body pushes a new set. */
    private effectStack;
    /** Stack of active handler clause resume contexts. */
    private resumeStack;
    /** Active handled signatures available to direct perform() sites. */
    private handledSignatureStack;
    /** Parameter vars proven to feed directly into a handler thunk call.
     * Stores both the handled signatures (for subtraction) and the introduced
     * effect set (for the application law's union). */
    private wrappedThunkVarHandled;
    /** Recoverable inference errors collected while continuing analysis. */
    private deferredErrors;
    get level(): number;
    /** Get the current (innermost) effect set being built. */
    get currentEffects(): EffectSet;
    /** Push a fresh effect set (entering a function body). */
    pushEffects(): void;
    /** Pop and return the effect set (leaving a function body). */
    popEffects(): EffectSet;
    get currentResume(): ResumeContext | undefined;
    pushResume(argType: Type, answerType: Type): void;
    popResume(): void;
    get currentHandledSignatures(): HandledSignatureMap | undefined;
    pushHandledSignatures(signatures: HandledSignatureMap): void;
    popHandledSignatures(): void;
    noteWrappedThunkVar(varId: number, signatures: HandledSignatureMap, introduced: EffectSet): void;
    getWrappedThunkVar(varId: number): {
        handled: HandledSignatureMap;
        introduced: EffectSet;
    } | undefined;
    deferError(error: TypeInferenceError): void;
    takeDeferredErrors(): TypeInferenceError[];
    /** Record an effect in the current effect set. */
    addEffect(name: string): void;
    /** Merge an inferred effect set into the current effect context. */
    addEffects(effects: EffectSet): void;
    /** Remove handled effects from the current set. */
    handleEffects(handled: Set<string>): void;
    /** Allocate a fresh type variable at the current level. */
    freshVar(): TypeVar;
    /** Enter a new let-binding scope (raises the level). */
    enterLevel(): void;
    /** Leave a let-binding scope (lowers the level). */
    leaveLevel(): void;
    /** Reset the constraint cache (for fresh inference passes). */
    resetCache(): void;
    /** Snapshot the constraint cache size (for overload rollback). */
    snapshotCacheSize(): number;
    /** Roll back the constraint cache to a previous size by removing recent entries. */
    restoreCacheSize(size: number): void;
    /**
     * Check if a constraint pair has been seen before (cycle guard).
     * Returns true if the pair was already in the cache.
     */
    checkAndAddConstraint(lhs: Type, rhs: Type): boolean;
}
/**
 * The core of Simple-sub: propagate `lhs <: rhs` until everything
 * reduces to bounds on type variables.
 *
 * When a variable appears on the left, it gains an upper bound.
 * When a variable appears on the right, it gains a lower bound.
 * Existing bounds are then propagated transitively.
 */
export declare function constrain(ctx: InferenceContext, lhs: Type, rhs: Type): void;
/** Maps variable names to their inferred types. Supports scoping via linked list. */
export declare class TypeEnv {
    private bindings;
    private parent;
    /**
     * Side map: function-value ASTs associated with `let` bindings whose RHS
     * is a `Function` node. Used by C6 (user-function fold) to reconstruct a
     * Call AST whose callee is the function body directly. Captured via
     * `bindFunctionAst` alongside the normal type binding.
     */
    private functionAsts;
    constructor(parent?: TypeEnv | null);
    /** Look up a variable's type in this scope or any parent. */
    lookup(name: string): Type | undefined;
    /**
     * Look up a function AST associated with a binding. Returns the
     * Function-node AST that was bound via `let name = (...) -> ...` or
     * undefined if the binding isn't a direct function-literal.
     */
    lookupFunctionAst(name: string): AstNode | undefined;
    /** Bind a variable in the current scope. */
    bind(name: string, type: Type): void;
    /** Record that `name` was bound to a Function-node AST (C6). */
    bindFunctionAst(name: string, ast: AstNode): void;
    /** Create a child scope. */
    child(): TypeEnv;
}
/**
 * Infer the type of an AST expression.
 * Returns the inferred type and populates the type map (nodeId → Type).
 */
export declare function inferExpr(node: AstNode, ctx: InferenceContext, env: TypeEnv, typeMap: Map<number, Type>): Type;
/**
 * Resolve a type by expanding all type variables to their bounds.
 * Positive polarity: variables expand to their lower bounds (union).
 * Negative polarity: variables expand to their upper bounds (intersection).
 */
export declare function expandType(t: Type, polarity?: 'positive' | 'negative', visited?: Set<string>): Type;
/**
 * Expand a type for IDE display. Unlike semantic expansion, this prefers
 * readable upper-bound information over `Never` when a variable has no lower
 * bounds yet, and reconstructs record shapes from property-access constraints.
 */
export declare function expandTypeForDisplay(t: Type, polarity?: 'positive' | 'negative', visited?: Set<string>): Type;
export declare function sanitizeDisplayType(t: Type, nested?: boolean): Type;
export declare class TypeInferenceError extends Error {
    nodeId?: number;
    severity: 'error' | 'warning';
    constructor(message: string, nodeId?: number, severity?: 'error' | 'warning');
}
export {};