# `ShotDs.Util.TypeInference`
[🔗](https://github.com/jcschuster/ShotDs/blob/v1.1.1/lib/shot_ds/util/type_inference.ex#L1)

Robinson first-order unification for the rank-1 HM type system.

Used by the parser in W-style: each application/connective node calls unify/3
immediately during the AST traversal, updating the running substitution.

# `general_type`

```elixir
@type general_type() :: ShotDs.Data.Type.t() | reference() | atom()
```

A type-shaped value accepted by `unify/3` and `apply_subst/2`: a full
`Type.t()` struct, a bare reference (type variable), or an atom (concrete
base type).

# `type_substitution`

```elixir
@type type_substitution() :: %{
  required(reference()) => ShotDs.Data.Type.t() | atom() | reference()
}
```

A substitution map mapping type variable references to resolved types.

# `apply_subst`

```elixir
@spec apply_subst(general_type(), type_substitution()) :: general_type()
```

Applies a type substitution to a given type or reference.

# `unify`

```elixir
@spec unify(general_type(), general_type(), type_substitution()) ::
  {:ok, type_substitution()} | {:error, String.t()}
```

Unifies two types under the given substitution. Returns either an updated
substitution that reconciles `t1` with `t2`, or an error.

Both arguments are first resolved through the current substitution, so
callers do not need to pre-apply themselves. Standard Robinson first-order
unification with occurs check.

# `unify!`

```elixir
@spec unify!(general_type(), general_type(), type_substitution()) ::
  type_substitution()
```

Unifies two types, raising a `TypeError` on failure.

---

*Consult [api-reference.md](api-reference.md) for complete listing*