Documentation

Unify two types, returning a substitution if successful This is a wrapper around unifyWithConstraints with empty constraints Discards the flag since it's not needed in basic unification

Strict unification that does NOT allow Tensor a to unify with a This is a wrapper around unifyStrictWithConstraints with empty constraints This is used for checking type class instances in TensorMapInsertion to ensure that Tensor types are properly distinguished from scalar types

Strict unification with type class constraints This is like unifyStrict but considers type class constraints when unifying type variables. IMPORTANT: This does NOT allow Tensor a to unify with a (strict unification). When unifying a constrained type variable with Tensor type, it checks if Tensor has instances for all the constraints.

Unify two types, allowing Tensor a to unify with a at top-level definitions This is used only for top-level definitions with type annotations According to type-tensor-simple.md: "トップレベル定義のテンソルについてのみ、Tensor a型が a型とunifyするとa型になる。"

Unify two types while considering type class constraints This function chooses unifiers that satisfy type class constraints Specifically, when unifying Tensor a with a constrained type variable t: - If C t constraint exists and C (Tensor a) is not satisfiable, prefer t = a over t = Tensor a Returns (Subst, Bool) where Bool indicates if Tensor was unwrapped during unification

Unify a list of type pairs

Unification errors