diff --git a/tntc/src/types/constraintGenerator.ts b/tntc/src/types/constraintGenerator.ts
index 89f573855..6ca3ba8af 100644
--- a/tntc/src/types/constraintGenerator.ts
+++ b/tntc/src/types/constraintGenerator.ts
@@ -25,7 +25,8 @@ import { ScopeTree, treeFromModule } from '../scoping'
 import { LookupTable, LookupTableByModule, lookupValue, newTable } from '../lookupTable'
 import { specialConstraints } from './specialConstraints'
 
-type solvingFunctionType = (_constraint: Constraint) => Either<Map<bigint, ErrorTree>, Substitutions>
+type solvingFunctionType = (_table: LookupTable,_constraint: Constraint) 
+  => Either<Map<bigint, ErrorTree>, Substitutions>
 
 // A visitor that collects types and constraints for a module's expressions
 export class ConstraintGeneratorVisitor implements IRVisitor {
@@ -182,13 +183,13 @@ export class ConstraintGeneratorVisitor implements IRVisitor {
         }
 
         const constraint: Constraint = { kind: 'conjunction', constraints: this.constraints, sourceId: 0n }
-        this.solvingFunction(constraint)
+        this.solvingFunction(this.currentTable, constraint)
           .mapLeft(errors => errors.forEach((err, id) => this.errors.set(id, err)))
           .map((subs) => {
             // Apply substitution to environment
             this.types = new Map<bigint, TypeScheme>(
               [...this.types.entries()].map(([id, te]) => {
-                const newType = applySubstitution(subs, te.type)
+                const newType = applySubstitution(this.currentTable, subs, te.type)
                 const scheme: TypeScheme = { ...typeNames(newType), type: newType }
                 return [id, scheme]
               })
@@ -263,8 +264,8 @@ export class ConstraintGeneratorVisitor implements IRVisitor {
       return { kind: 'row', name: name, value: { kind: 'var', name: this.freshVar() } }
     })
 
-    const subs = compose(typeSubs, rowSubs)
-    return applySubstitution(subs, t.type)
+    const subs = compose(this.currentTable, typeSubs, rowSubs)
+    return applySubstitution(this.currentTable, subs, t.type)
   }
 
   private updateCurrentModule(): void {
diff --git a/tntc/src/types/constraintSolver.ts b/tntc/src/types/constraintSolver.ts
index a55812f0c..3ecd49435 100644
--- a/tntc/src/types/constraintSolver.ts
+++ b/tntc/src/types/constraintSolver.ts
@@ -15,24 +15,28 @@
 import { Either, left, right } from '@sweet-monads/either'
 import { Error, ErrorTree, buildErrorLeaf, buildErrorTree } from '../errorTree'
 import { rowToString, typeToString } from '../IRprinting'
-import { Row, TntType, rowNames, typeNames } from '../tntTypes'
+import { Row, TntConstType, TntType, rowNames, typeNames } from '../tntTypes'
 import { Constraint } from './base'
 import { Substitutions, applySubstitution, applySubstitutionToConstraint, compose } from './substitutions'
 import { unzip } from 'lodash'
+import { LookupTable, lookupType } from '../lookupTable'
 
 /*
  * Try to solve a constraint by unifying all pairs of types in equality
  * constraints inside it.
  *
+ * @param table the lookup table for the module
  * @param constraint the constraint to be solved
  *
  * @returns the substitutions from the unifications, if successful. Otherwise, a
  *          map from source ids to errors.
  */
-export function solveConstraint(constraint: Constraint): Either<Map<bigint, ErrorTree>, Substitutions> {
+export function solveConstraint(
+  table: LookupTable, constraint: Constraint
+): Either<Map<bigint, ErrorTree>, Substitutions> {
   const errors: Map<bigint, ErrorTree> = new Map<bigint, ErrorTree>()
   switch (constraint.kind) {
-    case 'eq': return unify(constraint.types[0], constraint.types[1]).mapLeft(e => {
+    case 'eq': return unify(table, constraint.types[0], constraint.types[1]).mapLeft(e => {
       errors.set(constraint.sourceId, e)
       return errors
     })
@@ -43,14 +47,14 @@ export function solveConstraint(constraint: Constraint): Either<Map<bigint, Erro
         // to gather all errors instead of just propagating the first one
         let newCons = con
         result.map(s => {
-          newCons = applySubstitutionToConstraint(s, con)
+          newCons = applySubstitutionToConstraint(table, s, con)
         })
-        return solveConstraint(newCons)
+        return solveConstraint(table, newCons)
           .mapLeft(e => {
             e.forEach((error, id) => errors.set(id, error))
             return errors
           })
-          .chain(newSubs => result.map(s => compose(newSubs, s)))
+          .chain(newSubs => result.map(s => compose(table, newSubs, s)))
       }, right([]))
     }
     case 'empty': return right([])
@@ -66,8 +70,7 @@ export function solveConstraint(constraint: Constraint): Either<Map<bigint, Erro
  * @returns an array of substitutions that unifies both types, when possible.
  *          Otherwise, an error tree with an error message and its trace.
  */
-export function unify(t1: TntType, t2: TntType): Either<ErrorTree, Substitutions> {
-  // TODO: resolve type aliases
+export function unify(table: LookupTable, t1: TntType, t2: TntType): Either<ErrorTree, Substitutions> {
   const location = `Trying to unify ${typeToString(t1)} and ${typeToString(t2)}`
 
   if (typeToString(t1) === typeToString(t2)) {
@@ -78,26 +81,27 @@ export function unify(t1: TntType, t2: TntType): Either<ErrorTree, Substitutions
     return bindType(t2.name, t1).mapLeft(msg => buildErrorLeaf(location, msg))
   } else if (t1.kind === 'oper' && t2.kind === 'oper') {
     return checkSameLength(location, t1.args, t2.args)
-      .chain(([args1, args2]) => chainUnifications([...args1, t1.res], [...args2, t2.res]))
+      .chain(([args1, args2]) => chainUnifications(table, [...args1, t1.res], [...args2, t2.res]))
       .mapLeft(error => buildErrorTree(location, error))
   } else if (t1.kind === 'set' && t2.kind === 'set') {
-    return unify(t1.elem, t2.elem)
+    return unify(table, t1.elem, t2.elem)
   } else if (t1.kind === 'list' && t2.kind === 'list') {
-    return unify(t1.elem, t2.elem)
+    return unify(table, t1.elem, t2.elem)
   } else if (t1.kind === 'fun' && t2.kind === 'fun') {
-    const result = unify(t1.arg, t2.arg)
+    const result = unify(table, t1.arg, t2.arg)
     return result.chain(subs => {
-      const subs2 = unify(applySubstitution(subs, t1.res), applySubstitution(subs, t2.res))
-      return subs2.map(s => compose(subs, s))
+      const subs2 = unify(table, applySubstitution(table, subs, t1.res), applySubstitution(table, subs, t2.res))
+      return subs2.map(s => compose(table, subs, s))
     })
   } else if (t1.kind === 'tup' && t2.kind === 'tup') {
-    return unifyRows(t1.fields, t2.fields)
+    return unifyRows(table, t1.fields, t2.fields)
       .mapLeft(error => buildErrorTree(location, error))
-  } else if (t1.kind === 'const' || t2.kind === 'const') {
-    // FIXME: Type aliases unify with anything for now
-    return right([])
+  } else if (t1.kind === 'const') {
+    return unifyWithAlias(table, t1, t2)
+  } else if (t2.kind === 'const') {
+    return unifyWithAlias(table, t2, t1)
   } else if (t1.kind === 'rec' && t2.kind === 'rec') {
-    return unifyRows(t1.fields, t2.fields)
+    return unifyRows(table, t1.fields, t2.fields)
       .mapLeft(error => buildErrorTree(location, error))
   } else {
     return left(buildErrorLeaf(
@@ -116,7 +120,7 @@ export function unify(t1: TntType, t2: TntType): Either<ErrorTree, Substitutions
  * @returns an array of substitutions that unifies both rows, when possible.
  *          Otherwise, an error tree with an error message and its trace.
  */
-export function unifyRows(r1: Row, r2: Row): Either<ErrorTree, Substitutions> {
+export function unifyRows(table: LookupTable, r1: Row, r2: Row): Either<ErrorTree, Substitutions> {
   // The unification algorithm assumes that rows are simplified to a normal form.
   // That means that the `other` field is either a row variable or an empty row
   // and `fields` is never an empty list
@@ -144,7 +148,7 @@ export function unifyRows(r1: Row, r2: Row): Either<ErrorTree, Substitutions> {
         const s1 = bindRow(ra.other.name, { ...rb, other: tailVar })
         const s2 = bindRow(rb.other.name, { ...ra, other: tailVar })
         // These bindings + composition should always succeed. I couldn't find a scenario where they don't.
-        return s1.chain(sa => s2.map(sb => compose(sa, sb)))
+        return s1.chain(sa => s2.map(sb => compose(table, sa, sb)))
           .mapLeft(msg => buildErrorLeaf(location, msg))
       } else {
         return left(buildErrorLeaf(
@@ -159,7 +163,7 @@ export function unifyRows(r1: Row, r2: Row): Either<ErrorTree, Substitutions> {
 
       // Unify the disjoint fields with tail variables
       // This call will fit in the above case of row unification
-      const tailSubs = unifyRows({ ...ra, fields: uniqueFields1 }, { ...rb, fields: uniqueFields2 })
+      const tailSubs = unifyRows(table, { ...ra, fields: uniqueFields1 }, { ...rb, fields: uniqueFields2 })
 
       // Sort shared fields by field name, and get the their types
       const fieldTypes: [TntType, TntType][] = sharedFieldNames.map(n => {
@@ -169,10 +173,10 @@ export function unifyRows(r1: Row, r2: Row): Either<ErrorTree, Substitutions> {
       })
 
       // Now, for each shared field, we need to unify the types
-      const fieldSubs = chainUnifications(...unzip(fieldTypes) as [TntType[], TntType[]])
+      const fieldSubs = chainUnifications(table, ...unzip(fieldTypes) as [TntType[], TntType[]])
 
       // Return the composition of the two substitutions
-      return tailSubs.chain(subs => fieldSubs.map(s => compose(subs, s)))
+      return tailSubs.chain(subs => fieldSubs.map(s => compose(table, subs, s)))
         .mapLeft(error => buildErrorTree(location, error))
     }
   } else {
@@ -180,6 +184,25 @@ export function unifyRows(r1: Row, r2: Row): Either<ErrorTree, Substitutions> {
   }
 }
 
+function unifyWithAlias(table: LookupTable, t1: TntConstType, t2: TntType) {
+  const aliasValue = lookupType(table, t1.name)
+  if (!aliasValue) {
+    return left(buildErrorLeaf(
+      `Trying to unify ${t1.name} and ${typeToString(t2)}`,
+      `Couldn't find type alias ${t1.name}`
+    ))
+  }
+
+  if(!aliasValue.type) {
+    return left(buildErrorLeaf(
+      `Trying to unify ${t1.name} and ${typeToString(t2)}`,
+      `Couldn't unify uninterpreted type ${t1.name} with different type`
+    ))
+  }
+
+  return unify(table, aliasValue.type, t2)
+}
+
 function bindType(name: string, type: TntType): Either<string, Substitutions> {
   if (typeNames(type).typeVariables.has(name)) {
     return left(`Can't bind ${name} to ${typeToString(type)}: cyclical binding`)
@@ -196,12 +219,14 @@ function bindRow(name: string, row: Row): Either<string, Substitutions> {
   }
 }
 
-function applySubstitutionsAndUnify(subs: Substitutions, t1: TntType, t2: TntType): Either<Error, Substitutions> {
-  const newSubstitutions = unify(
-    applySubstitution(subs, t1),
-    applySubstitution(subs, t2)
+function applySubstitutionsAndunify(
+  table: LookupTable, subs: Substitutions, t1: TntType, t2: TntType
+): Either<Error, Substitutions> {
+  const newSubstitutions = unify(table, 
+    applySubstitution(table, subs, t1),
+    applySubstitution(table, subs, t2)
   )
-  return newSubstitutions.map(newSubs => compose(newSubs, subs))
+  return newSubstitutions.map(newSubs => compose(table, newSubs, subs))
 }
 
 function checkSameLength(
@@ -214,9 +239,9 @@ function checkSameLength(
   return right([types1, types2])
 }
 
-function chainUnifications(types1: TntType[], types2: TntType[]): Either<Error, Substitutions> {
+function chainUnifications(table: LookupTable, types1: TntType[], types2: TntType[]): Either<Error, Substitutions> {
   return types1.reduce((result: Either<Error, Substitutions>, t, i) => {
-    return result.chain(subs => applySubstitutionsAndUnify(subs, t, types2[i]))
+    return result.chain(subs => applySubstitutionsAndunify(table, subs, t, types2[i]))
   }, right([]))
 }
 
diff --git a/tntc/src/types/printing.ts b/tntc/src/types/printing.ts
index e0230a6a1..759cc02c2 100644
--- a/tntc/src/types/printing.ts
+++ b/tntc/src/types/printing.ts
@@ -1,4 +1,5 @@
 import { rowToString, typeToString } from '../IRprinting'
+import { newTable } from '../lookupTable'
 import { Constraint, TypeScheme } from './base'
 import { Substitutions, applySubstitution, compose } from './substitutions'
 
@@ -39,8 +40,8 @@ export function typeSchemeToString(t: TypeScheme): string {
     return { kind: 'row', name: name, value: { kind: 'var', name: `r${i}` } }
   })
 
-  const subs = compose(typeSubs, rowSubs)
-  const type = applySubstitution(subs, t.type)
+  const subs = compose(newTable({}), typeSubs, rowSubs)
+  const type = applySubstitution(newTable({}), subs, t.type)
 
   const varsString = vars.length > 0 ? `∀ ${vars.join(', ')} . ` : ''
   return `${varsString}${typeToString(type)}`
diff --git a/tntc/src/types/substitutions.ts b/tntc/src/types/substitutions.ts
index 61bebb7de..f4cb58653 100644
--- a/tntc/src/types/substitutions.ts
+++ b/tntc/src/types/substitutions.ts
@@ -14,6 +14,7 @@
 
 import { Either } from '@sweet-monads/either'
 import { ErrorTree, errorTreeToString } from '../errorTree'
+import { LookupTable } from '../lookupTable'
 import { Row, TntType } from '../tntTypes'
 import { Constraint } from './base'
 import { unify, unifyRows } from './constraintSolver'
@@ -36,8 +37,8 @@ type Substitution =
  *
  * @returns a new substitutions list containing the composition of given substitutions
  */
-export function compose(s1: Substitutions, s2: Substitutions): Substitutions {
-  const newS2 = applySubstitutionsToSubstitutions(s1, s2)
+export function compose(table: LookupTable, s1: Substitutions, s2: Substitutions): Substitutions {
+  const newS2 = applySubstitutionsToSubstitutions(table, s1, s2)
   return newS2.concat(s1)
 }
 
@@ -51,7 +52,7 @@ export function compose(s1: Substitutions, s2: Substitutions): Substitutions {
  * @returns the type resulting from the substitutions' application on the
  *          given type
  */
-export function applySubstitution(subs: Substitutions, t: TntType): TntType {
+export function applySubstitution(table: LookupTable, subs: Substitutions, t: TntType): TntType {
   let result = t
   switch (t.kind) {
     case 'var': {
@@ -62,28 +63,30 @@ export function applySubstitution(subs: Substitutions, t: TntType): TntType {
       break
     }
     case 'oper': {
-      const arrowParams = t.args.map(ef => applySubstitution(subs, ef))
-      const arrowResult = applySubstitution(subs, t.res)
+      const arrowParams = t.args.map(ef => applySubstitution(table, subs, ef))
+      const arrowResult = applySubstitution(table, subs, t.res)
       result = { kind: t.kind, args: arrowParams, res: arrowResult, id: t.id }
       break
     }
     case 'list':
     case 'set': {
-      result = { kind: t.kind, elem: applySubstitution(subs, t.elem), id: t.id }
+      result = { kind: t.kind, elem: applySubstitution(table, subs, t.elem), id: t.id }
       break
     }
     case 'fun': {
-      result = { kind: t.kind, arg: applySubstitution(subs, t.arg), res: applySubstitution(subs, t.res), id: t.id }
+      result = {
+        kind: t.kind, arg: applySubstitution(table, subs, t.arg), res: applySubstitution(table, subs, t.res), id: t.id,
+      }
       break
     }
     case 'tup': {
-      result = { kind: t.kind, fields: applySubstitutionToRow(subs, t.fields), id: t.id }
+      result = { kind: t.kind, fields: applySubstitutionToRow(table, subs, t.fields), id: t.id }
       break
     }
     case 'rec': {
       result = {
         kind: t.kind,
-        fields: applySubstitutionToRow(subs, t.fields),
+        fields: applySubstitutionToRow(table, subs, t.fields),
         id: t.id,
       }
       break
@@ -95,7 +98,7 @@ export function applySubstitution(subs: Substitutions, t: TntType): TntType {
         records: t.records.map(r => {
           return {
             tagValue: r.tagValue,
-            fields: applySubstitutionToRow(subs, r.fields),
+            fields: applySubstitutionToRow(table, subs, r.fields),
           }
         }),
         id: t.id,
@@ -117,29 +120,32 @@ export function applySubstitution(subs: Substitutions, t: TntType): TntType {
  * @returns the constraint resulting from the substitutions' application on the
  *          given constraint
  */
-export function applySubstitutionToConstraint(subs: Substitutions, c: Constraint): Constraint {
+export function applySubstitutionToConstraint(table: LookupTable, subs: Substitutions, c: Constraint): Constraint {
   switch (c.kind) {
     case 'eq': {
-      const ts: [TntType, TntType] = [applySubstitution(subs, c.types[0]), applySubstitution(subs, c.types[1])]
+      const ts: [TntType, TntType] = [
+        applySubstitution(table, subs, c.types[0]),
+        applySubstitution(table, subs, c.types[1]),
+      ]
       return { kind: c.kind, types: ts, sourceId: c.sourceId }
     }
     case 'empty': return c
     case 'conjunction': {
-      const cs = c.constraints.map(con => applySubstitutionToConstraint(subs, con))
+      const cs = c.constraints.map(con => applySubstitutionToConstraint(table, subs, con))
       return { kind: 'conjunction', constraints: cs, sourceId: c.sourceId }
     }
   }
 }
 
-function applySubstitutionsToSubstitutions(s1: Substitutions, s2: Substitutions): Substitutions {
+function applySubstitutionsToSubstitutions(table: LookupTable, s1: Substitutions, s2: Substitutions): Substitutions {
   return s2.flatMap(s => {
     const sub = s1.find(sub => s.name === sub.name)
     if (sub) {
       let result: Either<ErrorTree, Substitutions>
       if (sub.kind === 'type' && s.kind === 'type') {
-        result = unify(s.value, sub.value)
+        result = unify(table, s.value, sub.value)
       } else if (sub.kind === 'row' && s.kind === 'row') {
-        result = unifyRows(s.value, sub.value)
+        result = unifyRows(table, s.value, sub.value)
       } else {
         throw new Error(`Substitutions with same name (${s.name}) but incompatible kinds: ${substitutionsToString([sub, s])}`)
       }
@@ -152,19 +158,19 @@ function applySubstitutionsToSubstitutions(s1: Substitutions, s2: Substitutions)
     }
 
     switch (s.kind) {
-      case 'type': return [{ kind: s.kind, name: s.name, value: applySubstitution(s1, s.value) }]
-      case 'row': return [{ kind: s.kind, name: s.name, value: applySubstitutionToRow(s1, s.value) }]
+      case 'type': return [{ kind: s.kind, name: s.name, value: applySubstitution(table, s1, s.value) }]
+      case 'row': return [{ kind: s.kind, name: s.name, value: applySubstitutionToRow(table, s1, s.value) }]
     }
   })
 }
 
-function applySubstitutionToRow(s: Substitutions, r: Row): Row {
+function applySubstitutionToRow(table: LookupTable, s: Substitutions, r: Row): Row {
   switch (r.kind) {
     case 'row':
       return {
         kind: 'row',
-        fields: r.fields.map(f => ({ fieldName: f.fieldName, fieldType: applySubstitution(s, f.fieldType) })),
-        other: applySubstitutionToRow(s, r.other),
+        fields: r.fields.map(f => ({ fieldName: f.fieldName, fieldType: applySubstitution(table, s, f.fieldType) })),
+        other: applySubstitutionToRow(table, s, r.other),
       }
     case 'var': {
       const sub = s.find(s => s.name === r.name)
diff --git a/tntc/test/types/constraintGenerator.test.ts b/tntc/test/types/constraintGenerator.test.ts
index 1301faed2..1b7b2f4d2 100644
--- a/tntc/test/types/constraintGenerator.test.ts
+++ b/tntc/test/types/constraintGenerator.test.ts
@@ -34,7 +34,7 @@ describe('ConstraintGeneratorVisitor', () => {
     const expectedConstraint =
       '(int, int) => int ~ (t_x_3, int) => t0 /\\ (Set[t1], (t1) => t2) => Set[t2] ~ (t_S_6, (t_x_3) => t0) => t3'
 
-    const solvingFunction = (c: Constraint) => {
+    const solvingFunction = (_: LookupTable, c: Constraint) => {
       assert.deepEqual(constraintToString(c), expectedConstraint)
       return right([])
     }
@@ -50,7 +50,7 @@ describe('ConstraintGeneratorVisitor', () => {
 
     const expectedConstraint = '(Set[t1], (t1) => t2) => Set[t2] ~ (t_S_6, (t0) => int) => t3'
 
-    const solvingFunction = (c: Constraint) => {
+    const solvingFunction = (_: LookupTable, c: Constraint) => {
       assert.deepEqual(constraintToString(c), expectedConstraint)
       return right([])
     }
@@ -67,7 +67,7 @@ describe('ConstraintGeneratorVisitor', () => {
       'def b = N',
     ])
 
-    const solvingFunction = (_: Constraint) => right([])
+    const solvingFunction = (_: LookupTable, _c: Constraint) => right([])
 
     const visitor = new ConstraintGeneratorVisitor(solvingFunction, definitionsTable)
     walkModule(visitor, tntModule)
@@ -91,7 +91,7 @@ describe('ConstraintGeneratorVisitor', () => {
 
     const errors = new Map<bigint, ErrorTree>([[1n, error]])
 
-    const solvingFunction = (_: Constraint) => left(errors)
+    const solvingFunction = (_: LookupTable, _c: Constraint) => left(errors)
 
     const visitor = new ConstraintGeneratorVisitor(solvingFunction, definitionsTable)
     walkModule(visitor, tntModule)
@@ -118,7 +118,7 @@ describe('ConstraintGeneratorVisitor', () => {
 
     const errors = new Map<bigint, ErrorTree>([[1n, error]])
 
-    const solvingFunction = (_: Constraint) => right([])
+    const solvingFunction = (_: LookupTable, _c: Constraint) => right([])
     const visitor = new ConstraintGeneratorVisitor(solvingFunction, definitionsTable)
     walkModule(visitor, tntModule)
 
diff --git a/tntc/test/types/constraintSolver.test.ts b/tntc/test/types/constraintSolver.test.ts
index 3999ff14d..96d92959d 100644
--- a/tntc/test/types/constraintSolver.test.ts
+++ b/tntc/test/types/constraintSolver.test.ts
@@ -7,6 +7,16 @@ import { substitutionsToString } from '../../src/types/printing'
 import { Substitutions } from '../../src/types/substitutions'
 import { Row } from '../../src/tntTypes'
 import { errorTreeToString } from '../../src/errorTree'
+import { LookupTable, newTable } from '../../src/lookupTable'
+import { defaultValueDefinitions } from '../../src'
+
+const table: LookupTable = newTable({
+  valueDefinitions: defaultValueDefinitions(),
+  typeDefinitions: [
+    { identifier: 'MY_ALIAS', type: { kind: 'int' } },
+    { identifier: 'MY_UNINTERPRETED' },
+  ],
+})
 
 describe('solveConstraint', () => {
   it('solves simple equality', () => {
@@ -19,7 +29,7 @@ describe('solveConstraint', () => {
       sourceId: 1n,
     }
 
-    const result = solveConstraint(constraint)
+    const result = solveConstraint(table, constraint)
 
     assert.isTrue(result.isRight())
     result.map(subs => assert.deepEqual(substitutionsToString(subs),
@@ -52,7 +62,7 @@ describe('solveConstraint', () => {
       sourceId: 3n,
     }
 
-    const result = solveConstraint(constraint)
+    const result = solveConstraint(table, constraint)
 
     assert.isTrue(result.isRight())
     result.map(subs => assert.deepEqual(substitutionsToString(subs),
@@ -63,7 +73,7 @@ describe('solveConstraint', () => {
   it('solves empty constraint', () => {
     const constraint: Constraint = { kind: 'empty' }
 
-    const result = solveConstraint(constraint)
+    const result = solveConstraint(table, constraint)
 
     assert.isTrue(result.isRight())
     result.map(subs => assert.sameDeepMembers(subs, []))
@@ -94,7 +104,7 @@ describe('solveConstraint', () => {
       sourceId: 3n,
     }
 
-    const result = solveConstraint(constraint)
+    const result = solveConstraint(table, constraint)
 
     assert.isTrue(result.isLeft())
     result.mapLeft(errors => {
@@ -117,6 +127,7 @@ describe('solveConstraint', () => {
 describe('unify', () => {
   it('unifies variable with other type', () => {
     const result = unify(
+      table,
       parseTypeOrThrow('a'),
       parseTypeOrThrow('(Set[b]) => List[b]')
     )
@@ -129,6 +140,7 @@ describe('unify', () => {
 
   it('returns empty substitution for equal types', () => {
     const result = unify(
+      table,
       parseTypeOrThrow('(Set[b]) => List[b]'),
       parseTypeOrThrow('(Set[b]) => List[b]')
     )
@@ -137,8 +149,62 @@ describe('unify', () => {
     result.map(subs => assert.sameDeepMembers(subs, []))
   })
 
+  it('returns empty substitution for equal types with alias', () => {
+    const result = unify(
+      table,
+      parseTypeOrThrow('(Set[b]) => MY_ALIAS'),
+      parseTypeOrThrow('(Set[b]) => int')
+    )
+
+    assert.isTrue(result.isRight())
+    result.map(subs => assert.sameDeepMembers(subs, []))
+  })
+
+
+  it('returns empty substitution for equal uninterpreted types', () => {
+    const result = unify(
+      table,
+      parseTypeOrThrow('(Set[b]) => MY_UNINTERPRETED'),
+      parseTypeOrThrow('(Set[b]) => MY_UNINTERPRETED')
+    )
+
+    assert.isTrue(result.isRight())
+    result.map(subs => assert.sameDeepMembers(subs, []))
+  })
+
+  it('returns error when uninterpreted type is unified with other type', () => {
+    const result = unify(
+      table,
+      parseTypeOrThrow('MY_UNINTERPRETED'),
+      parseTypeOrThrow('int')
+    )
+
+    assert.isTrue(result.isLeft())
+    result.mapLeft(err => assert.deepEqual(err, {
+      message: "Couldn't unify uninterpreted type MY_UNINTERPRETED with different type",
+      location: "Trying to unify MY_UNINTERPRETED and int",
+      children: [],
+    }))
+  })
+
+  it('returns error when type alias is not found', () => {
+    const result = unify(
+      table,
+      parseTypeOrThrow('UNEXISTING_ALIAS'),
+      parseTypeOrThrow('int')
+    )
+
+    assert.isTrue(result.isLeft())
+    result.mapLeft(err => assert.deepEqual(err, {
+      message: "Couldn't find type alias UNEXISTING_ALIAS",
+      location: "Trying to unify UNEXISTING_ALIAS and int",
+      children: [],
+    }))
+  })
+
   it('unifies args and results of arrow and function types', () => {
     const result = unify(
+      table,
       parseTypeOrThrow('(a) => int -> bool'),
       parseTypeOrThrow('((Set[b]) => List[b]) => b -> c')
     )
@@ -151,6 +217,7 @@ describe('unify', () => {
 
   it('unifies elements of tuples, set and list types', () => {
     const result = unify(
+      table,
       parseTypeOrThrow('(Set[a], List[b])'),
       parseTypeOrThrow('(Set[int], List[bool])')
     )
@@ -163,6 +230,7 @@ describe('unify', () => {
 
   it("returns error when variable occurs in the other type's body", () => {
     const result = unify(
+      table,
       parseTypeOrThrow('a'),
       parseTypeOrThrow('Set[a]')
     )
@@ -177,6 +245,7 @@ describe('unify', () => {
 
   it('returns error when unifying operator with different number of args', () => {
     const result = unify(
+      table,
       parseTypeOrThrow('(a, b) => c'),
       parseTypeOrThrow('(int) => c')
     )
@@ -191,6 +260,7 @@ describe('unify', () => {
 
   it('returns error when unifying tuples with different number of args', () => {
     const result = unify(
+      table,
       parseTypeOrThrow('(a, b, c)'),
       parseTypeOrThrow('(int, bool)')
     )
@@ -219,7 +289,7 @@ describe('unifyRows', () => {
     const row1: Row = parseRowOrThrow('')
     const row2: Row = parseRowOrThrow('| a')
 
-    const result = unifyRows(row1, row2)
+    const result = unifyRows(table, row1, row2)
     const expectedSubs: Substitutions = [{ kind: 'row', name: 'a', value: { kind: 'empty' } }]
 
     result.map(subs => assert.sameDeepMembers(subs, expectedSubs))
@@ -230,7 +300,7 @@ describe('unifyRows', () => {
     const row1: Row = parseRowOrThrow('f: int')
     const row2: Row = parseRowOrThrow('| a')
 
-    const result = unifyRows(row1, row2)
+    const result = unifyRows(table, row1, row2)
     const expectedSubs: Substitutions = [{ kind: 'row', name: 'a', value: row1 }]
 
     result.map(subs => assert.sameDeepMembers(subs, expectedSubs))
@@ -241,7 +311,7 @@ describe('unifyRows', () => {
     const row1: Row = parseRowOrThrow('f1: int, f2: str | a')
     const row2: Row = parseRowOrThrow('f3: bool | b')
 
-    const result = unifyRows(row1, row2)
+    const result = unifyRows(table, row1, row2)
     const expectedSubs: Substitutions = [
       {
         kind: 'row',
@@ -276,7 +346,7 @@ describe('unifyRows', () => {
     const row1: Row = parseRowOrThrow('f1: int, f2: str | a')
     const row2: Row = parseRowOrThrow('f3: bool, f2: str, f1: int')
 
-    const result = unifyRows(row1, row2)
+    const result = unifyRows(table, row1, row2)
     const expectedSubs: Substitutions = [{
       kind: 'row',
       name: 'a',
@@ -291,7 +361,7 @@ describe('unifyRows', () => {
     const row1: Row = parseRowOrThrow('| a')
     const row2: Row = parseRowOrThrow('| b')
 
-    const result = unifyRows(row1, row2)
+    const result = unifyRows(table, row1, row2)
     const expectedSubs: Substitutions = [{ kind: 'row', name: 'a', value: { kind: 'var', name: 'b' } }]
 
     result.map(subs => assert.sameDeepMembers(subs, expectedSubs))
@@ -302,7 +372,7 @@ describe('unifyRows', () => {
     const row1: Row = parseRowOrThrow('f1: int')
     const row2: Row = parseRowOrThrow('f1: str')
 
-    const result = unifyRows(row1, row2)
+    const result = unifyRows(table, row1, row2)
 
     result.mapLeft(err => assert.deepEqual(err, {
       location: 'Trying to unify { f1: int } and { f1: str }',
@@ -318,7 +388,7 @@ describe('unifyRows', () => {
     const row1: Row = parseRowOrThrow('shared: bool, f1: int')
     const row2: Row = parseRowOrThrow('shared: bool, f2: str')
 
-    const result = unifyRows(row1, row2)
+    const result = unifyRows(table, row1, row2)
 
     result.mapLeft(err => assert.deepEqual(err, {
       location: 'Trying to unify { shared: bool, f1: int } and { shared: bool, f2: str }',
@@ -334,7 +404,7 @@ describe('unifyRows', () => {
     const row1: Row = parseRowOrThrow('| a')
     const row2: Row = parseRowOrThrow('f1: str | a')
 
-    const result = unifyRows(row1, row2)
+    const result = unifyRows(table, row1, row2)
 
     result.mapLeft(err => assert.deepEqual(err, {
       message: "Can't bind a to { f1: str | a }: cyclical binding",
@@ -347,7 +417,7 @@ describe('unifyRows', () => {
     const row1: Row = parseRowOrThrow('f1: str | a')
     const row2: Row = parseRowOrThrow('f2: int | a')
 
-    const result = unifyRows(row1, row2)
+    const result = unifyRows(table, row1, row2)
 
     result.mapLeft(err => assert.deepEqual(err, {
       location: 'Trying to unify { f1: str | a } and { f2: int | a }',
@@ -360,7 +430,7 @@ describe('unifyRows', () => {
     const row1: Row = parseRowOrThrow('')
     const row2: Row = parseRowOrThrow('f1: str | a')
 
-    const result = unifyRows(row1, row2)
+    const result = unifyRows(table, row1, row2)
 
     result.mapLeft(err => assert.deepEqual(err, {
       message: "Couldn't unify empty and row",
diff --git a/tntc/test/types/substitutions.test.ts b/tntc/test/types/substitutions.test.ts
index 92b4e11fe..49bd7389f 100644
--- a/tntc/test/types/substitutions.test.ts
+++ b/tntc/test/types/substitutions.test.ts
@@ -5,6 +5,9 @@ import { Substitutions, applySubstitution, applySubstitutionToConstraint, compos
 import { Constraint } from '../../src/types/base'
 import { constraintToString } from '../../src/types/printing'
 import { Row } from '../../src'
+import { newTable } from '../../src/lookupTable'
+
+const table = newTable({})
 
 describe('compose', () => {
   it('composes two substitutions', () => {
@@ -24,7 +27,7 @@ describe('compose', () => {
       value: row,
     }]
 
-    const result = compose(s1, s2)
+    const result = compose(table, s1, s2)
 
     assert.sameDeepMembers(result, [
       { kind: 'type', name: 'a', value: parseTypeOrThrow('int') },
@@ -36,7 +39,7 @@ describe('compose', () => {
     const s1: Substitutions = [{ kind: 'type', name: 'v1', value: parseTypeOrThrow('int') }]
     const s2: Substitutions = [{ kind: 'type', name: 'v1', value: { kind: 'var', name: 'q' } }]
 
-    const result = compose(s1, s2)
+    const result = compose(table, s1, s2)
 
     assert.sameDeepMembers(result, s1.concat([
       { kind: 'type', name: 'q', value: parseTypeOrThrow('int') },
@@ -53,7 +56,7 @@ describe('applySubstitution', () => {
 
     const t = parseTypeOrThrow('(a) => b')
 
-    const result = applySubstitution(s, t)
+    const result = applySubstitution(table, s, t)
 
     assert.deepEqual(result, parseTypeOrThrow('(int) => bool'))
   })
@@ -66,7 +69,7 @@ describe('applySubstitution', () => {
 
     const t = parseTypeOrThrow('a -> b')
 
-    const result = applySubstitution(s, t)
+    const result = applySubstitution(table, s, t)
 
     assert.deepEqual(result, parseTypeOrThrow('int -> bool'))
   })
@@ -80,7 +83,7 @@ describe('applySubstitution', () => {
 
     const t = parseTypeOrThrow('(List[a], Set[b], c)')
 
-    const result = applySubstitution(s, t)
+    const result = applySubstitution(table, s, t)
 
     assert.deepEqual(result, parseTypeOrThrow('(List[int], Set[bool], str)'))
   })
@@ -93,7 +96,7 @@ describe('applySubstitution', () => {
 
     const t = parseTypeOrThrow('{ a: a, b: b }')
 
-    const result = applySubstitution(s, t)
+    const result = applySubstitution(table, s, t)
 
     assert.deepEqual(result, parseTypeOrThrow('{ a: int, b: bool }'))
   })
@@ -107,7 +110,7 @@ describe('applySubstitution', () => {
 
     const t = parseTypeOrThrow('{ a: a, b: b | r }')
 
-    const result = applySubstitution(s, t)
+    const result = applySubstitution(table, s, t)
 
     assert.deepEqual(result, parseTypeOrThrow('{ a: int, b: bool }'))
   })
@@ -120,7 +123,7 @@ describe('applySubstitution', () => {
 
     const t = parseTypeOrThrow('| { tag: "a", a: a }\n| { tag: "b", b: b }')
 
-    const result = applySubstitution(s, t)
+    const result = applySubstitution(table, s, t)
 
     assert.deepEqual(result, parseTypeOrThrow('| { tag: "a", a: int }\n| { tag: "b", b: bool }'))
   })
@@ -136,7 +139,7 @@ describe('applySubstitutionToConstraint', () => {
     const t1 = parseTypeOrThrow('a')
     const t2 = parseTypeOrThrow('b')
 
-    const result = applySubstitutionToConstraint(s, { kind: 'eq', types: [t1, t2], sourceId: 1n })
+    const result = applySubstitutionToConstraint(table, s, { kind: 'eq', types: [t1, t2], sourceId: 1n })
     const expectedResult: Constraint =
       { kind: 'eq', types: [parseTypeOrThrow('int'), parseTypeOrThrow('bool')], sourceId: 1n }
 
@@ -145,7 +148,7 @@ describe('applySubstitutionToConstraint', () => {
   })
 
   it('does nothing to empty constraint', () => {
-    const result = applySubstitutionToConstraint(s, { kind: 'empty' })
+    const result = applySubstitutionToConstraint(table, s, { kind: 'empty' })
     const expectedResult: Constraint = { kind: 'empty' }
 
     assert.deepEqual(result, expectedResult,
@@ -155,7 +158,7 @@ describe('applySubstitutionToConstraint', () => {
   it('applies substitution recursively to constraints in conjunction', () => {
     const c1: Constraint = { kind: 'eq', types: [parseTypeOrThrow('a'), parseTypeOrThrow('b')], sourceId: 1n }
     const c2: Constraint = { kind: 'eq', types: [parseTypeOrThrow('b'), parseTypeOrThrow('b')], sourceId: 1n }
-    const result = applySubstitutionToConstraint(s, { kind: 'conjunction', constraints: [c1, c2], sourceId: 1n })
+    const result = applySubstitutionToConstraint(table, s, { kind: 'conjunction', constraints: [c1, c2], sourceId: 1n })
 
     const expected1: Constraint =
       { kind: 'eq', types: [parseTypeOrThrow('int'), parseTypeOrThrow('bool')], sourceId: 1n }