Merge pull request #1204 from informalsystems/gabriela/type-substitut…

…ion-improvements

Apply improvements from effects system to the type system

quint/src/types/constraintGenerator.ts

@@ -194,7 +194,7 @@ export class ConstraintGeneratorVisitor implements IRVisitor {
     // numbering of ther fresh variables stays in order, with `a`, used for return types,
     // bearing the highest number.
     const definedSignature = this.typeForName(e.opcode, e.id, e.args.length)
-    const a: QuintType = { kind: 'var', name: this.freshVarGenerator.freshVar('t') }
+    const a: QuintType = { kind: 'var', name: this.freshVarGenerator.freshVar('_t') }
     const result = argsResult
       .chain(results => {
         switch (e.opcode) {
@@ -242,7 +242,7 @@ export class ConstraintGeneratorVisitor implements IRVisitor {
       rowVariables: new Set(lastParamNames.rowVariables),
     }
     expr.params.forEach(p => {
-      const varName = p.name === '_' ? this.freshVarGenerator.freshVar('t') : `t_${p.name}_${p.id}`
+      const varName = p.name === '_' ? this.freshVarGenerator.freshVar('_t') : `t_${p.name}_${p.id}`
       paramNames.typeVariables.add(varName)
       this.addToResults(p.id, right(toScheme({ kind: 'var', name: varName })))
     })
@@ -387,11 +387,11 @@ export class ConstraintGeneratorVisitor implements IRVisitor {
     const rowNames = Array.from(t.rowVariables)
 
     const typeSubs: Substitutions = typeNames.map(name => {
-      return { kind: 'type', name: name, value: { kind: 'var', name: this.freshVarGenerator.freshVar('t') } }
+      return { kind: 'type', name: name, value: { kind: 'var', name: this.freshVarGenerator.freshVar('_t') } }
     })
 
     const rowSubs: Substitutions = rowNames.map(name => {
-      return { kind: 'row', name: name, value: { kind: 'var', name: this.freshVarGenerator.freshVar('t') } }
+      return { kind: 'row', name: name, value: { kind: 'var', name: this.freshVarGenerator.freshVar('_t') } }
     })
 
     const subs = compose(this.table, typeSubs, rowSubs)

quint/src/types/substitutions.ts

@@ -19,6 +19,7 @@ import { ConcreteFixedRow, QuintType, Row } from '../ir/quintTypes'
 import { Constraint } from './base'
 import { unify, unifyRows } from './constraintSolver'
 import { substitutionsToString } from './printing'
+import { isEqual } from 'lodash'
 
 /*
  * Substitutions can be applied to Quint types, type variables with another type
@@ -51,69 +52,79 @@ export function compose(table: LookupTable, s1: Substitutions, s2: Substitutions
  *          given type
  */
 export function applySubstitution(table: LookupTable, subs: Substitutions, t: QuintType): QuintType {
-  switch (t.kind) {
-    case 'var': {
-      const sub = subs.find(s => s.name === t.name)
-      if (sub && sub.kind === 'type') {
-        return sub.value
-      } else {
-        return t
+  // We cannot assign the result of a switch to a value, so we use an arrow function instead
+  const singleApplication = () => {
+    switch (t.kind) {
+      case 'var': {
+        const sub = subs.find(s => s.name === t.name)
+        if (sub && sub.kind === 'type') {
+          return sub.value
+        } else {
+          return t
+        }
       }
-    }
-    case 'oper': {
-      const arrowParams = t.args.map(ef => applySubstitution(table, subs, ef))
-      const arrowResult = applySubstitution(table, subs, t.res)
-      return { kind: t.kind, args: arrowParams, res: arrowResult, id: t.id }
-    }
-    case 'list':
-    case 'set': {
-      return { kind: t.kind, elem: applySubstitution(table, subs, t.elem), id: t.id }
-    }
-    case 'fun': {
-      return {
-        kind: t.kind,
-        arg: applySubstitution(table, subs, t.arg),
-        res: applySubstitution(table, subs, t.res),
-        id: t.id,
+      case 'oper': {
+        const arrowParams = t.args.map(ef => applySubstitution(table, subs, ef))
+        const arrowResult = applySubstitution(table, subs, t.res)
+        return { kind: t.kind, args: arrowParams, res: arrowResult, id: t.id }
       }
-    }
-    case 'tup': {
-      return { kind: t.kind, fields: applySubstitutionToRow(table, subs, t.fields), id: t.id }
-    }
-    case 'rec': {
-      return {
-        kind: t.kind,
-        fields: applySubstitutionToRow(table, subs, t.fields),
-        id: t.id,
+      case 'list':
+      case 'set': {
+        return { kind: t.kind, elem: applySubstitution(table, subs, t.elem), id: t.id }
       }
-    }
-    case 'union': {
-      return {
-        kind: t.kind,
-        tag: t.tag,
-        records: t.records.map(r => {
-          return {
-            tagValue: r.tagValue,
-            fields: applySubstitutionToRow(table, subs, r.fields),
-          }
-        }),
-        id: t.id,
+      case 'fun': {
+        return {
+          kind: t.kind,
+          arg: applySubstitution(table, subs, t.arg),
+          res: applySubstitution(table, subs, t.res),
+          id: t.id,
+        }
       }
-    }
-    case 'sum':
-      return {
-        ...t,
-        // We know this has to end up as a concrete fixed row, since it must
-        // start as one, and applying substitions cannot result in a wider type
-        fields: applySubstitutionToRow(table, subs, t.fields) as ConcreteFixedRow,
+      case 'tup': {
+        return { kind: t.kind, fields: applySubstitutionToRow(table, subs, t.fields), id: t.id }
+      }
+      case 'rec': {
+        return {
+          kind: t.kind,
+          fields: applySubstitutionToRow(table, subs, t.fields),
+          id: t.id,
+        }
       }
+      case 'union': {
+        return {
+          kind: t.kind,
+          tag: t.tag,
+          records: t.records.map(r => {
+            return {
+              tagValue: r.tagValue,
+              fields: applySubstitutionToRow(table, subs, r.fields),
+            }
+          }),
+          id: t.id,
+        }
+      }
+      case 'sum':
+        return {
+          ...t,
+          // We know this has to end up as a concrete fixed row, since it must
+          // start as one, and applying substitions cannot result in a wider type
+          fields: applySubstitutionToRow(table, subs, t.fields) as ConcreteFixedRow,
+        }
+
+      // The basic types have no variables, so cannot
+      case 'int':
+      case 'bool':
+      case 'str':
+      case 'const':
+        return t
+    }
+  }
 
-    // The basic types have no variables, so cannot
-    case 'int':
-    case 'bool':
-    case 'str':
-    case 'const':
-      return t
+  const result = singleApplication()
+  if (isEqual(result, t)) {
+    return t
+  } else {
+    return applySubstitution(table, subs, result)
   }
 }
 

quint/test/repl.test.ts

@@ -142,7 +142,7 @@ describe('repl ok', () => {
       `>>> 1 + false
       |static analysis error: error: [QNT000] Couldn't unify int and bool
       |Trying to unify int and bool
-      |Trying to unify (int, int) => int and (int, bool) => t0
+      |Trying to unify (int, int) => int and (int, bool) => _t0
       |
       |1 + false
       |^^^^^^^^^

quint/test/types/constraintGenerator.test.ts

@@ -26,7 +26,7 @@ describe('ConstraintGeneratorVisitor', () => {
     const defs = ['def d(S) = S.map(x => x + 10)']
 
     const expectedConstraint =
-      '(int, int) => int ~ (t_x_9, int) => t0 /\\ (Set[t1], (t1) => t2) => Set[t2] ~ (t_S_7, (t_x_9) => t0) => t3'
+      '(int, int) => int ~ (t_x_9, int) => _t0 /\\ (Set[_t1], (_t1) => _t2) => Set[_t2] ~ (t_S_7, (t_x_9) => _t0) => _t3'
 
     const solvingFunction = (_: LookupTable, c: Constraint) => {
       assert.deepEqual(constraintToString(c), expectedConstraint)
@@ -39,7 +39,7 @@ describe('ConstraintGeneratorVisitor', () => {
   it('handles underscore', () => {
     const defs = ['def d(S) = S.map(_ => 10)']
 
-    const expectedConstraint = '(Set[t1], (t1) => t2) => Set[t2] ~ (t_S_7, (t0) => int) => t3'
+    const expectedConstraint = '(Set[_t1], (_t1) => _t2) => Set[_t2] ~ (t_S_7, (_t0) => int) => _t3'
 
     const solvingFunction = (_: LookupTable, c: Constraint) => {
       assert.deepEqual(constraintToString(c), expectedConstraint)

quint/test/types/inferrer.test.ts

@@ -211,10 +211,10 @@ describe('inferTypes', () => {
         [
           7n,
           {
-            location: 'Trying to unify (Set[t1], (t1) => t2) => Set[t2] and (int, (int) => int) => t3',
+            location: 'Trying to unify (Set[_t1], (_t1) => _t2) => Set[_t2] and (int, (int) => int) => _t3',
             children: [
               {
-                location: 'Trying to unify Set[t1] and int',
+                location: 'Trying to unify Set[_t1] and int',
                 message: "Couldn't unify set and int",
                 children: [],
               },

quint/test/types/substitutions.test.ts

@@ -129,6 +129,19 @@ describe('applySubstitution', () => {
 
     assert.deepEqual(result, parseTypeOrThrow('| { tag: "a", a: int }\n| { tag: "b", b: bool }'))
   })
+
+  it('substitutes with transitivity', () => {
+    const s: Substitutions = [
+      { kind: 'type', name: 'a', value: { kind: 'var', id: 1n, name: 'b' } },
+      { kind: 'type', name: 'b', value: { kind: 'bool', id: 2n } },
+    ]
+
+    const t = parseTypeOrThrow('a')
+
+    const result = applySubstitution(table, s, t)
+
+    assert.deepEqual(result, { kind: 'bool', id: 2n })
+  })
 })
 
 describe('applySubstitutionToConstraint', () => {