#Morphir Typing

#The infer API

let filled = @typing.infer(file, deps, Fill) catch {
  InferenceFailed(problems) => ...
}

• file is an @ir.IRFile: a Library, an Application or a Specs distribution.
• deps maps each package name to its @ir.PackageSpecification. The file's own dependencies are added to it.
• infer raises InferenceFailed(problems) when there is any problem, in either mode. It collects the problems of every binding group first, and sorts them by logical path.

#Facts

• a value signature: the declaration, value:<package>:<module>#<name>;
• a let signature: the definition, …/definition or …/definitions/<name>;
• the declared type of a hole: the hole;
• an alias body or a constructor argument: the type, type:<package>:<module>#<name>.

• one bijection holds for every type of the declaration, because inference names the variables of a declaration consistently;
• each signature variable of the declaration (one without the unknown marker) maps only to itself;
• two paired variables must have the same class set, from the typeclass constraint or the name prefix.

#Native untagged unions

#The caller supplies the SDK

let deps = Map::from_array([
  (@sdk_spec.sdk_package_name(), @sdk_spec.sdk_specification()),
])

#The unknown marker

• All occurrences of one unknown name in one signature are the same variable.
• A top-level value is declared when it has an output type and no signature variable is unknown. Other values are undeclared.
• Classic IR has no markers, so inference checks it strictly.

#Rigid variables

• A rigid variable stands for any type. The body must work for every type.
• When the body needs a narrower type, the problem is rigid_variable. For example, id : a -> a with the body \x -> 1 fails, because 1 is a number and a is any type.
• A class failure at a rigid variable is also rigid_variable, not no_instance. For example, a body that needs comparable for a rigid a fails with rigid_variable. This includes a rigid inside a type, as in List a used as comparable.
• A rigid variable takes its class from its typeclass constraint, else from its name prefix.
• The rigid variables of a signature belong to its declaration. Two declarations that both write a have two different variables, also inside one binding group. When the group is generalized, the scheme of an undeclared member quantifies the rigid variables of every member, so f x = g x is as general as g. A let annotation that writes a variable of its declaration's signature means that variable. Output and messages show the plain name, such as a.
• The other rigid variables of a let annotation belong to that let. If one escapes into the type of an outer value, the problem is rigid_variable. Two LetRecursion siblings that both write a have two different variables.
• A declared value is used through its scheme everywhere, also in its own body. So it can be polymorphically recursive.

#Classic let placeholders

#How inference works

1. The environment holds the types, constructors and values of every dependency, and the types and constructors of the file.
2. Each declared signature enters the environment as a scheme before any body is solved.
3. The undeclared values form binding groups: the strongly connected components of the references between them. The groups are solved in dependency order. Inside a group, the undeclared values are monomorphic. They are generalized after the group.
4. Each group stops at its first problem. Other groups go on. A value of a failed group gets an unconstrained scheme, so its dependants do not report the same problem again.
5. LetDefinition generalizes, which is let-polymorphism. LetRecursion is one group: a sibling with a complete annotation is used through the scheme of its annotation in the whole group, and the other siblings are monomorphic until the group is generalized. Destructure binds its variables monomorphically.

#Literals

#Other bodies

• A NativeBody or an IncompleteBody uses its signature as declared. Inference does not walk an incomplete body's value.
• An ExternalBody checks its fallback value against the signature.
• A Hole is a todo: it stands for code that is not written yet and does not fail the run by itself. A variable of its declared type that is in scope (a signature or let-annotation variable) is that rigid variable. Any other variable is a fresh variable for each occurrence of the hole, and keeps the class of its typeclass constraint or name prefix. A hole without a declared type is a fresh variable.

#Output

• Inference expands an alias only when unification needs it. So a type keeps the alias references that it got from a signature or a constructor.
• Variables are named in walk order: a, b, …. A constrained variable takes its class as a prefix: comparable-a. Names of rigid variables are reserved first, so a new name never captures one.
• The output is deterministic: the same input gives the same bytes.

#Constraint classes

• comparable and appendable together give compappend.
• number and comparable together give number.
• Any other pair is no_instance.
• Decimal and LocalDate belong to no class.
• A typeclass constraint that names any other class is unsupported, with the message "inference does not support the type class <name>". The problem is at the declaration's root for a top-level signature, at /definition (or /definitions/<name>) for a let signature, at the hole for a hole's type, and at the node that uses a global value or constructor whose signature has such a class. Inference never treats it as a class.

#Records and rows

#Diagnostics

#Aliases that ignore a parameter

#Cyclic aliases

• The problem is at the type path type:<package>:<module>#<name>, in both modes.
• This includes cyclic aliases in dependencies. A file then fails even when it does not use the alias.

#Logical paths

• A declaration's root is value:<package>:<module>#<name>, with canonical names, for example value:acme/app:orders#total.
• Each step below adds /<step> to the path of the parent. <i> is a 0-based index and <name> is a canonical name.

#Out of scope

• Type classes other than the four built-in classes.
• Inference across a package whose specification is missing. That is missing_dependency.
• Expansion of cyclic aliases. They are unsupported.
• Document literals when no morphir/SDK:document#document type is known. The SDK specification has no such type today, so they are unsupported.
• Source languages. This module reads only IR. The engine stage, which runs inference inside the Morphir pipeline, comes in a later plan.