Merge pull request #1392 from informalsystems/1391/resolve-apps-on-IR

Resolve type applications at the IR level

examples/.scripts/run-example.sh

@@ -61,7 +61,7 @@ result () {
       elif [[ "$file" == "classic/distributed/TwoPhaseCommit/two_phase_commit_modules.qnt" && "$cmd" =~ (test|verify) ]] ; then
         printf "<sup>https://github.com/informalsystems/quint/issues/1299</sup>"
       elif [[ "$file" == "language-features/option.qnt" && "$cmd" == "verify" ]] ; then
-        printf "<sup>https://github.com/informalsystems/quint/issues/1391</sup>"
+        printf "<sup>https://github.com/informalsystems/quint/issues/1393</sup>"
       fi
     fi
 }

examples/README.md

@@ -86,7 +86,7 @@ listed without any additional command line arguments.
 | [language-features/lists.qnt](./language-features/lists.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [language-features/maps.qnt](./language-features/maps.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [language-features/nondetEx.qnt](./language-features/nondetEx.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
-| [language-features/option.qnt](./language-features/option.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/issues/1391</sup> |
+| [language-features/option.qnt](./language-features/option.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/issues/1393</sup> |
 | [language-features/records.qnt](./language-features/records.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [language-features/sets.qnt](./language-features/sets.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [language-features/tuples.qnt](./language-features/tuples.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |

quint/src/quintAnalyzer.ts

@@ -22,6 +22,7 @@ import { ModeChecker } from './effects/modeChecker'
 import { QuintError } from './quintError'
 import { errorTreeToString } from './errorTree'
 import { MultipleUpdatesChecker } from './effects/MultipleUpdatesChecker'
+import { TypeApplicationResolver } from './types/typeApplicationResolution'
 
 /* Products from static analysis */
 export type AnalysisOutput = {
@@ -36,19 +37,26 @@ export type AnalysisResult = [QuintError[], AnalysisOutput]
 /**
  * Analyzes multiple Quint modules and returns the analysis result.
  *
+ * NOTE: This is modifies the `lookupTable` and the `quintModules`!
+ * See XXX for the mutation sites.
+ *
  * @param lookupTable - The lookup tables for the modules.
  * @param quintModules - The Quint modules to be analyzed.
  * @returns A tuple with a list of errors and the analysis output.
  */
 export function analyzeModules(lookupTable: LookupTable, quintModules: QuintModule[]): AnalysisResult {
   const analyzer = new QuintAnalyzer(lookupTable)
-  quintModules.map(m => analyzer.analyzeDeclarations(m.declarations))
+  // XXX: the modules are mutated here.
+  quintModules.forEach(m => (m.declarations = analyzer.analyzeDeclarations(m.declarations)))
   return analyzer.getResult()
 }
 
 /**
  * Analyzes declarations incrementally and returns the analysis result.
  *
+ * NOTE: This is modifies the `lookupTable`!
+ * See XXX for the mutation sites.
+ *
  * @param analysisOutput - The previous analysis output to be used as a starting point.
  * @param lookupTable - The lookup tables for the modules.
  * @param declarations - The Quint declarations to be analyzed.
@@ -75,6 +83,7 @@ export function analyzeInc(
  * @param previousOutput - The previous analysis output to be used as a starting point.
  */
 class QuintAnalyzer {
+  private typeApplicationResolver: TypeApplicationResolver
   private effectInferrer: EffectInferrer
   private typeInferrer: TypeInferrer
   private modeChecker: ModeChecker
@@ -84,19 +93,24 @@ class QuintAnalyzer {
   private output: AnalysisOutput = { types: new Map(), effects: new Map(), modes: new Map() }
 
   constructor(lookupTable: LookupTable, previousOutput?: AnalysisOutput) {
+    // XXX: the lookUp table is mutated when TypeApplicationResolver is instantiated
+    this.typeApplicationResolver = new TypeApplicationResolver(lookupTable)
     this.typeInferrer = new TypeInferrer(lookupTable, previousOutput?.types)
     this.effectInferrer = new EffectInferrer(lookupTable, previousOutput?.effects)
     this.multipleUpdatesChecker = new MultipleUpdatesChecker()
     this.modeChecker = new ModeChecker(previousOutput?.modes)
   }
 
-  analyzeDeclarations(decls: QuintDeclaration[]): void {
-    const [typeErrMap, types] = this.typeInferrer.inferTypes(decls)
-    const [effectErrMap, effects] = this.effectInferrer.inferEffects(decls)
+  analyzeDeclarations(decls: QuintDeclaration[]): QuintDeclaration[] {
+    const [typAppErrMap, resolvedDecls] = this.typeApplicationResolver.resolveTypeApplications(decls)
+
+    // XXX: the lookUp table is mutated during type inference
+    const [typeErrMap, types] = this.typeInferrer.inferTypes(resolvedDecls)
+    const [effectErrMap, effects] = this.effectInferrer.inferEffects(resolvedDecls)
     const updatesErrMap = this.multipleUpdatesChecker.checkEffects([...effects.values()])
-    const [modeErrMap, modes] = this.modeChecker.checkModes(decls, effects)
+    const [modeErrMap, modes] = this.modeChecker.checkModes(resolvedDecls, effects)
 
-    const errorTrees = [...typeErrMap, ...effectErrMap]
+    const errorTrees = [...typeErrMap, ...effectErrMap, ...typAppErrMap]
 
     // TODO: Type and effect checking should return QuintErrors instead of error trees
     this.errors.push(
@@ -114,6 +128,8 @@ class QuintAnalyzer {
       effects: new Map([...this.output.effects, ...effects]),
       modes: new Map([...this.output.modes, ...modes]),
     }
+
+    return resolvedDecls
   }
 
   getResult(): AnalysisResult {

quint/src/types/inferrer.ts

@@ -21,16 +21,12 @@ import { TypeScheme } from './base'
 import { ConstraintGeneratorVisitor } from './constraintGenerator'
 import { solveConstraint } from './constraintSolver'
 import { simplify } from './simplification'
-import { TypeApplicationResolver } from './typeApplicationResolution'
-import { transformDeclaration, transformLookupDefinition } from '../ir/IRTransformer'
 
 export type TypeInferenceResult = [Map<bigint, ErrorTree>, Map<bigint, TypeScheme>]
 
 export class TypeInferrer extends ConstraintGeneratorVisitor {
-  private resolver: TypeApplicationResolver
   constructor(table: LookupTable, types?: Map<bigint, TypeScheme>) {
     super(solveConstraint, table, types)
-    this.resolver = new TypeApplicationResolver(this.table, this.freshVarGenerator)
   }
 
   /**
@@ -43,17 +39,8 @@ export class TypeInferrer extends ConstraintGeneratorVisitor {
    */
   inferTypes(declarations: QuintDeclaration[]): TypeInferenceResult {
     // Resolve all type applications used in expressions in the lookup table
-    this.table.forEach((def, id) => {
-      // Don't resolve type definitions, since those should keep their original type variable names
-      // They are our source of truth for all resolutions
-      if (def.kind !== 'typedef') {
-        const resolvedLookupDef = transformLookupDefinition(this.resolver, def)
-        this.table.set(id, resolvedLookupDef)
-      }
-    })
     declarations.forEach(decl => {
-      const resolvedDecl = transformDeclaration(this.resolver, decl)
-      walkDeclaration(this, resolvedDecl)
+      walkDeclaration(this, decl)
     })
     const simplifiedTypes = new Map([...this.types.entries()].map(([id, t]) => [id, simplify(t)]))
     return [this.errors, simplifiedTypes]

quint/src/types/typeApplicationResolution.ts

@@ -12,30 +12,45 @@
  * @module
  */
 
-import { fail } from 'assert'
+import { ErrorTree, buildErrorLeaf } from '../errorTree'
 import { FreshVarGenerator } from '../FreshVarGenerator'
+
 import { typeToString } from '../ir/IRprinting'
-import { IRTransformer, transformType } from '../ir/IRTransformer'
-import { QuintTypeAlias } from '../ir/quintIr'
+import { IRTransformer, transformDeclaration, transformLookupDefinition, transformType } from '../ir/IRTransformer'
+import { QuintDeclaration, QuintTypeAlias } from '../ir/quintIr'
 import { QuintAppType, QuintType, QuintVarType, Row } from '../ir/quintTypes'
 import { LookupTable } from '../names/base'
 import { zip } from '../util'
 import { Substitutions, applySubstitution } from './substitutions'
+import assert from 'assert'
 
 /** Resolves all type applications in an IR object */
 export class TypeApplicationResolver implements IRTransformer {
+  // Errors found during type application resolution
+  private errors: Map<bigint, ErrorTree> = new Map<bigint, ErrorTree>()
   // Fresh variable generator, shared with the TypeInferrer
   private freshVarGenerator: FreshVarGenerator
   // Lookup table from the parser
   private table: LookupTable
 
-  constructor(table: LookupTable, freshVarGenerator: FreshVarGenerator) {
+  constructor(table: LookupTable) {
     this.table = table
-    this.freshVarGenerator = freshVarGenerator
+    this.freshVarGenerator = new FreshVarGenerator()
+
+    this.table.forEach((def, id) => {
+      const resolvedLookupDef = transformLookupDefinition(this, def)
+      this.table.set(id, resolvedLookupDef)
+    })
+  }
+
+  resolveTypeApplications(decls: QuintDeclaration[]): [Map<bigint, ErrorTree>, QuintDeclaration[]] {
+    const resolvedDecls = decls.map(decl => transformDeclaration(this, decl))
+    const errors = this.errors
+    return [errors, resolvedDecls]
   }
 
   exitType(t: QuintType): QuintType {
-    return this.resolveTypeApplications(t)
+    return this.resolveTypeApplicationsForType(t)
   }
 
   // Transforms `t` by resolving all the type applications in all its sub-terms
@@ -46,33 +61,46 @@ export class TypeApplicationResolver implements IRTransformer {
   //   type Bar[x, y] = {i: x, j: y}
   //
   //
-  // resolveTypeApplications(Foo[a, {f: Bar[int, str]}]) = (a, {f: {i: int, j: str}})
-  resolveTypeApplications(t: QuintType): QuintType {
+  // resolveTypeApplicationsForType(Foo[a, {f: Bar[int, str]}]) = (a, {f: {i: int, j: str}})
+  private resolveTypeApplicationsForType(t: QuintType): QuintType {
     const f: (_: QuintType) => QuintType = x => (x.kind !== 'app' ? x : this.resolveTypeApp(x))
     return mapType(f, t)
   }
 
   private resolveTypeApp(t: QuintAppType): QuintType {
-    if (!t.ctor.id) {
-      // This should be ensured by parsing
-      fail(
-        `invalid IR node: type constructor ${t.ctor.name} in type application ${typeToString(t)} id ${t.id} has no id`
-      )
-    }
+    // Ensured by parsing
+    assert(t.id, `invalid IR node: type application ${typeToString(t)} has no id`)
+    // Ensured by parsing
+    assert(
+      t.ctor.id,
+      `invalid IR node: type constructor ${t.ctor.name} in type application ${typeToString(t)} id ${t.id} has no id`
+    )
 
     const typeDef = this.table.get(t.ctor.id)
-    if (!typeDef) {
-      // This should be ensured by name resolution
-      fail(`invalid IR reference: type constructor ${t.ctor.name} with id ${t.ctor.id} has no type definition`)
-    }
-
-    if (typeDef.kind !== 'typedef' || !typeDef.type) {
-      // This should be ensured by the grammar and by name resolution
-      fail(`invalid kind looked up for constructor of type application with id ${t.ctor.id} `)
-    }
+    // Ensured by name resolution
+    assert(typeDef, `invalid IR reference: type constructor ${t.ctor.name} with id ${t.ctor.id} has no type definition`)
+    // Ensured by the grammar and by name resolution
+    assert(
+      typeDef.kind === 'typedef' && typeDef.type,
+      `invalid kind looked up for constructor of type application with id ${t.ctor.id} `
+    )
 
     const { params, type } = this.freshTypeFromDef(typeDef as QuintTypeAlias)
 
+    // NOTE: Early exit on error
+    // Check for arity mismatch in type application
+    if (params.length !== t.args.length) {
+      const ctorMsg = typeToString(t.ctor)
+      const typeArgsMsg = t.args.map(typeToString).join(', ')
+      const manyOrFew = params.length > t.args.length ? 'few' : 'many'
+      const err = buildErrorLeaf(
+        `applying type constructor ${ctorMsg} to arguments ${typeArgsMsg}`,
+        `too ${manyOrFew} arguments supplied: ${ctorMsg} only accepts ${params.length} parameters`
+      )
+      this.errors.set(t.id, err)
+      return t
+    }
+
     // Substitute the type `args` for each corresponding fresh variable
     const subs: Substitutions = zip(params, t.args).map(([param, arg]) => ({
       kind: 'type',

quint/test/flattening/fullFlattener.test.ts

@@ -235,4 +235,19 @@ describe('flattenModules', () => {
 
     assertFlattenedModule(text)
   })
+
+  // Regression test for https://github.com/informalsystems/quint/issues/1391
+  describe('can flatten with polymorphic types between different modules (#802)', () => {
+    const text = `module A {
+      type Foo[a] = F(a)
+      def mapFoo(x: Foo[a], f: a => b): Foo[b] = match x { F(v) => F(f(v)) }
+    }
+
+    module B {
+      import A.*
+      val b: Foo[int] = F("one").mapFoo(_ => 1)
+    }`
+
+    assertFlattenedModule(text)
+  })
 })

quint/test/types/inferrer.test.ts

@@ -2,8 +2,9 @@ import { describe, it } from 'mocha'
 import { assert } from 'chai'
 import { TypeInferenceResult, TypeInferrer } from '../../src/types/inferrer'
 import { typeSchemeToString } from '../../src/types/printing'
-import { errorTreeToString } from '../../src/errorTree'
+import { ErrorTree, errorTreeToString } from '../../src/errorTree'
 import { parseMockedModule } from '../util'
+import { TypeApplicationResolver } from '../../src/types/typeApplicationResolution'
 
 // Utility used to print update `stringType` values to make
 // updating the expected values in the following tests less
@@ -16,10 +17,22 @@ function _printUpdatedStringTypes(stringTypes: (string | bigint)[][]) {
 
 describe('inferTypes', () => {
   function inferTypesForModules(text: string): TypeInferenceResult {
-    const { modules, table } = parseMockedModule(text)
+    const { modules: parsedModules, table } = parseMockedModule(text)
 
+    // Type inference assumes all type applications (e.g., `Foo[int, str]`) have been resolved.
+    const resolver = new TypeApplicationResolver(table)
     const inferrer = new TypeInferrer(table)
-    return inferrer.inferTypes(modules.flatMap(m => m.declarations))
+
+    // Used to collect errors found during type application
+    let typeAppErrs: Map<bigint, ErrorTree> = new Map()
+    const modules = parsedModules.map(m => {
+      const [errs, declarations] = resolver.resolveTypeApplications(m.declarations)
+      typeAppErrs = new Map([...typeAppErrs, ...errs])
+      return { ...m, declarations }
+    })
+    const [inferenceErrors, inferenceSchemes] = inferrer.inferTypes(modules.flatMap(m => m.declarations))
+    const combinedErrors = new Map([...inferenceErrors, ...typeAppErrs])
+    return [combinedErrors, inferenceSchemes]
   }
 
   function inferTypesForDefs(defs: string[]): TypeInferenceResult {
@@ -441,6 +454,31 @@ Trying to unify ((Ok(bool) | Err(_t5))) => (Ok(bool) | Err(_t5)) and ((Ok(bool)
     assert.deepEqual(actualErrors, [expectedError])
   })
 
+  it('errors when polymorphic types are applied to invalid numbers of arguments', () => {
+    const defs = [
+      'type Result[ok, err] = Ok(ok) | Err(err)',
+      `val too_many: Result[a, b, c] = Ok(1)`,
+      `val too_few: Result[a] = Ok(1)`,
+    ]
+
+    const [errors] = inferTypesForDefs(defs)
+    assert.isNotEmpty([...errors.entries()])
+
+    const actualErrors = [...errors.entries()].map(e => errorTreeToString(e[1]))
+    const expectedErrors = [
+      `Couldn't unify sum and app
+Trying to unify (Ok(int) | Err(_t3)) and Result[a, b, c]
+`,
+      `too many arguments supplied: Result only accepts 2 parameters
+applying type constructor Result to arguments a, b, c
+`,
+      `too few arguments supplied: Result only accepts 2 parameters
+applying type constructor Result to arguments a
+`,
+    ]
+    assert.deepEqual(actualErrors, expectedErrors)
+  })
+
   it('fails when types are not unifiable', () => {
     const defs = ['def a = 1.map(p => p + 10)']