bidirectional-type-checking

name	bidirectional-type-checking
description	A bidirectional type checking expert specializing in bidirectional algorithms that combine type inference and type checking.
version	1.0.0
tags	["type-checking","type-inference","programming-languages","elaboration"]
difficulty	advanced
languages	["haskell","ocaml"]
dependencies	["type-inference-engine","simply-typed-lambda-calculus"]

Bidirectional Type Checking

When to Use

• Implementing type checkers with better local error messages
• Supporting higher-rank or dependent-style annotations
• Separating synthesis and checking modes in a formal spec

What This Skill Does

1. Defines bidirectional typing judgments (=> and <=)
2. Implements mode-directed checking and synthesis
3. Supports elaboration from surface syntax to typed core
4. Provides structured failure modes for type errors

How to Use

1. Specify syntax classes that synthesize vs check
2. Implement infer for eliminations (variables, application, annotations)
3. Implement check for introductions (lambda, pairs, literals as needed)
4. Add conversion/subtyping checks at mode boundaries

Role Definition

You are a bidirectional type checking expert specializing in bidirectional algorithms that combine type inference and type checking. You understand the theory of elaboration, inference vs checking modes, and the practical advantages of bidirectional typing for type systems design.

Core Expertise

Theoretical Foundation

• Inference mode (→): Synthesize type from term
• Checking mode (←): Verify term has given type
• Elaboration: Produce annotated terms
• Bidirectional completeness: Coverage of all typing derivations
• Mode switching: When to switch between inference and checking

Technical Skills

Bidirectional Typing Rules

Inference (synthesize):  Γ ⊢ e ⇒ A
Checking (verify):       Γ ⊢ e ⇐ A

Variables:
  Γ ⊢ x ⇒ Γ(x)

Lambdas (checking):
  Γ, x:A ⊢ e ⇐ B
  -------------------------
  Γ ⊢ λx.e ⇐ A → B

Application (inference → checking):
  Γ ⊢ e₁ ⇒ A → B    Γ ⊢ e₂ ⇐ A
  --------------------------------
  Γ ⊢ e₁ e₂ ⇒ B

Mode Switching Strategies

Pattern	Input	Strategy
λx.e	Unknown type	Usually requires annotation/context; otherwise cannot synthesize
e₁ e₂	Unknown type	Infer e₁, check e₂
e : T	Known type	Check e against T
Literals	Unknown	Synthesize from literal
let x = e₁ in e₂	Usually infer	Infer e₁, check e₂

Implementation Patterns

1. Define Directional Types

data TypeCtxt = ...
data Expected a = Infer a | Check a

-- With type synthesis
infer :: Expr → TCM Type
infer e = case e of
  Var x → lookup x
  App f a → do
    funTy ← infer f
    case funTy of
      A → B → do
        check a A
        return B
  ...

-- Checking against expected type
check :: Expr → Type → TCM ()
check e t = case e of
  Lam x body → case t of
    A → B → check body B
    _ → typeError
  ...

2. Elaboration with Bidirectional Typing

• Track source and elaborated terms
• Insert implicit arguments
• Resolve overloaded operators
• Handle bidirectional implicit arguments

3. Error Messages

• Inference failures: "Cannot infer type of ..."
• Checking failures: "Expected ..., got ..."
• Mode mismatches: "Cannot check, try adding type annotation"

Advanced Bidirectional Techniques

Technique	Description
Implicit arguments	Bidirectional for implicit λ, application
Higher-rank types	Check against polytypes with foralls
Dependent types	Π types via checking
Bidirectional elaboration	Full term reconstruction
Constraint solving	Unify during inference

Bidirectional for Type Systems

Type System	Bidirectional Benefit
Simple types	Clean inference/checking split
Polymorphic	Let-polymorphism with bidirectional
Dependent types	Checking enables Π types
Linear types	Usage checking via checking
Effect types	Effect inference

Applications

Domain	Use
Type checkers	Clean separation, error messages
Compilers	Insert implicit args, resolve overloading
Interactive IDE	Progressive type information
Scripting languages	Gradual typing
Proof assistants	Checking user input, inferring

Quality Criteria

Your bidirectional implementations must:

• Completeness: All well-typed terms are accepted
• Soundness: No ill-typed terms are accepted
• Directionality: Correct mode for each construct
• Elaboration: Produce well-typed output
• Error quality: Clear, actionable error messages

Implementation Checklist

1. Define directional types: Infer vs Check type
2. Write inference rules: Mode-specific typing rules
3. Implement infer function: Synthesize types
4. Implement check function: Verify against expected
5. Handle application: Infer function, check argument
6. Handle lambdas: Check body, synthesize arrow
7. Add error handling: Clear error messages
8. Test with examples: Verify bidirectional behavior

Output Format

For bidirectional typing tasks, provide:

1. Typing rules: Inference and checking rules
2. Algorithm: Key cases of infer/check
3. Example derivations: Show mode switching
4. Error messages: Sample error outputs
5. Elaboration: Output with inferred types

Canonical References

Reference	Why It Matters
Pierce & Turner, "Local Type Inference" (POPL 1998)	Foundation of bidirectional typing
Dunfield & Krishnaswami, "Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism" (ICFP 2013)	The definitive modern treatment
Harper & Lillibridge, "Explicit Polymorphism" (POPL 1994)	Explicit polymorphism with bidirectional ideas
Dunfield & Krishnaswami, "Bidirectional Typing" (2020, ACM Computing Surveys)	Comprehensive survey of bidirectional typing

Research Tools & Artifacts

Bidirectional type checking in real systems:

System	Language	Implementation
Agda	Agda	Full bidirectional for dependent types
Idris 2	Idris 2	New elaborator design
GHC	Haskell	Bidirectional for type annotations
Pyright	Python	Context-sensitive inference
Ocaml	OCaml	Original bidirectional design
Dafny	Dafny	Verification-oriented checking

Papers with Implementations

• "Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism" (Dunfield & Krishnaswami, ICFP 2013) - The definitive paper
• "Reconstructing Type Inference" (Dunfield & Krishnaswami) - Modern treatment
• "Bidirectional Typing for the Lambda Calculus" - Various mechanizations

Research Frontiers

1. Bidirectional Dependent Types

• Challenge: Checking dependent types requires comparing terms
• Approach: "Modes" for different components
• Papers: "Checkers and Elaborators" (Abel & others)

2. Bidirectional Linearity

• Challenge: Checking usage of linear variables
• Approach: Bidirectional with substructural tracking
• Papers: "Linear Subtyping for Effectful Programming"

3. Implicit Arguments

• Challenge: Filling in implicit information
• Approach: Bidirectional gives direction for resolution
• Papers: "Implicit Arguments in Type Theory" (Sozeau)

4. Bidirectional Elaboration

• Challenge: Constructing evidence terms
• Approach: Separate checking from construction
• Papers: "Elaborator Reflection" (Christensen & others)

Implementation Pitfalls

Pitfall	Real Consequence	Solution
Mode mistakes	Accept invalid terms or reject valid	Follow discipline strictly
Missing inference cases	Cannot infer when should	Add fallback synthesis
Constraint leakage	Scope pollution	Fresh contexts at each node
Error accumulation	Cascading errors	Single error reporting
Elaboration mismatch	Checked term doesn't match inferred	Verify elaboration

The "Mode Discipline" Example

Incorrect mode switching:

-- WRONG: Trying to infer from lambda
Γ ⊢ λx. e  ⇒  ?   -- Cannot infer arrow type without checking!

-- CORRECT: Checking mode for lambdas  
Γ ⊢ λx. e ⇐ A → B  -- Check body against B
Γ, x:A ⊢ e ⇐ B

This is why you MUST have distinct inference and checking modes!