@[implicit_reducible]

instance Strata.Laurel.instToStringInferHoleTypesStats : ToString InferHoleTypesStats

Equations

• One or more equations did not get rendered due to their size.

Hole Type Inference

Annotate each .Hole node with a type inferred from its surrounding context using the SemanticModel and computeExprType. After this pass every Hole carries some ty so that the hole elimination pass can generate correctly typed uninterpreted functions.

Every node is handled by inferExpr with an expectedType parameter. For statement positions the expected type is TVoid, except for the last statement in a block which inherits the block's expected type, and for return expressions which use the procedure's output type.

TODO: make this pass obsolete by improving Resolution

This pass exists only because Resolution does not currently assign a concrete type to every hole. It should: resolution already type-checks the whole program bidirectionally, so it is the natural place to type holes, and doing so there would make this pass redundant and let us delete it.

The missing piece is in how Resolution synthesizes the type of a hole. Today a hole in synth position synthesizes to Unknown, and that Unknown is discarded rather than being unified with the type its context later imposes. Instead, synthesizing a hole should return a fresh type variable that is recorded on the hole node, so that when the surrounding expression is checked (e.g. via checkSubtype, or by overload selection in Synth.staticCall) the variable is solved to the concrete type and that solution is written back onto the hole. With that, holes such as 1 + <?>, <?> > 0, or a call argument would be typed during resolution exactly as this pass types them now, and Resolution would assign a type to every hole on its own.

inductive Strata.Laurel.InferHoleTypesStats : Type

• holesAnnotated : InferHoleTypesStats

  Number of holes successfully annotated with an inferred type.

• holesLeftUnknown : InferHoleTypesStats

  Number of holes left with Unknown type (context could not determine type).

structure Strata.Laurel.InferHoleState : Type

• model : SemanticModel
• statistics : Statistics
• diagnostics : List Message

def Strata.Laurel.inferHoleTypes (model : SemanticModel) (program : Program) : Program × List Message × Statistics

Annotate every .Hole in the program with a type inferred from context. Returns the updated program and any diagnostics (e.g. holes whose type could not be inferred).

Equations

• One or more equations did not get rendered due to their size.

def Strata.Laurel.inferHoleTypesPass : LoweringPass

Pipeline pass: infer hole types.

Equations

• One or more equations did not get rendered due to their size.