Fix variant constructor type annotations

They were omitting type arguments
informalsystems · Feb 29, 2024 · a788abf · a788abf
1 parent 4b494e8
commit a788abf
Show file tree

Hide file tree

Showing 2 changed files with 47 additions and 34 deletions.
diff --git a/quint/src/parsing/ToIrListener.ts b/quint/src/parsing/ToIrListener.ts
@@ -24,6 +24,7 @@ import {
   QuintConstType,
   QuintSumType,
   QuintType,
+  QuintVarType,
   Row,
   RowField,
   isUnitType,
@@ -405,7 +406,17 @@ export class ToIrListener implements QuintListener {
     this.checkForUndeclaredTypeVariables(id, def)
 
     // Used for annotations in the variant constructors
-    const constructorReturnType: QuintConstType = { id, kind: 'const', name }
+    let constructorReturnType: QuintType
+    // The constant identifying the type definition. E.g. `Result`
+    const typeConst: QuintConstType = { id: this.getId(ctx), kind: 'const', name }
+    if (def.params) {
+      // The type takes parameters, so we need a type application as the return type. E.g., `Result[ok, err]`
+      const args: QuintVarType[] = def.params.map(name => ({ id: this.getId(ctx), kind: 'var', name }))
+      constructorReturnType = { id, kind: 'app', ctor: typeConst, args }
+    } else {
+      // The type takes no parameters, so we only need the constant name
+      constructorReturnType = typeConst
+    }
 
     // Generate all the variant constructors implied by a variant type definition
     // a variant constructor is an operator that injects an expression
@@ -451,7 +462,7 @@ export class ToIrListener implements QuintListener {
           // ```
           qualifier = 'val'
 
-          // The nullary variant constructor is actualy
+          // The nullary variant constructor is actually
           // a variant pairing a label with the unit.
           const wrappedExpr = unitValue(this.getId(variantCtx._sumLabel))
 

diff --git a/quint/test/types/inferrer.test.ts b/quint/test/types/inferrer.test.ts
@@ -164,21 +164,22 @@ describe('inferTypes', () => {
     assert.isEmpty(errors, `Should find no errors, found: ${[...errors.values()].map(errorTreeToString)}`)
 
     const stringTypes = Array.from(types.entries()).map(([id, type]) => [id, typeSchemeToString(type)])
+    // _printUpdatedStringTypes(stringTypes)
     assert.sameDeepMembers(stringTypes, [
-      [14n, 'str'],
-      [15n, 'int'],
-      [16n, '(A(int) | B({}))'],
+      [15n, 'str'],
+      [16n, 'int'],
       [17n, '(A(int) | B({}))'],
-      [10n, 'str'],
-      [11n, '{}'],
-      [12n, '(B({}) | A(int))'],
-      [13n, '(B({}) | A(int))'],
-      [5n, 'int'],
-      [4n, 'str'],
+      [18n, '(A(int) | B({}))'],
       [6n, 'int'],
-      [7n, '(A(int) | B({}))'],
-      [8n, '(int) => (A(int) | B({}))'],
+      [5n, 'str'],
+      [7n, 'int'],
+      [8n, '(A(int) | B({}))'],
       [9n, '(int) => (A(int) | B({}))'],
+      [10n, '(int) => (A(int) | B({}))'],
+      [11n, 'str'],
+      [12n, '{}'],
+      [13n, '(B({}) | A(int))'],
+      [14n, '(B({}) | A(int))'],
     ])
   })
 
@@ -205,34 +206,35 @@ module B {
     assert.isEmpty(errors, `Should find no errors, found: ${[...errors.values()].map(errorTreeToString)}`)
 
     const stringTypes = Array.from(types.entries()).map(([id, type]) => [id, typeSchemeToString(type)])
+    // _printUpdatedStringTypes(stringTypes)
     assert.sameDeepMembers(stringTypes, [
-      [14n, 'str'],
-      [15n, 'int'],
-      [16n, '(A(int) | B({}))'],
+      [15n, 'str'],
+      [16n, 'int'],
       [17n, '(A(int) | B({}))'],
-      [10n, 'str'],
-      [11n, '{}'],
-      [12n, '(B({}) | A(int))'],
-      [13n, '(B({}) | A(int))'],
       [18n, '(A(int) | B({}))'],
-      [24n, 'str'],
-      [26n, 'int'],
-      [19n, 'int'],
+      [6n, 'int'],
+      [5n, 'str'],
+      [7n, 'int'],
+      [8n, '(A(int) | B({}))'],
+      [9n, '(int) => (A(int) | B({}))'],
+      [10n, '(int) => (A(int) | B({}))'],
+      [11n, 'str'],
+      [12n, '{}'],
+      [13n, '(B({}) | A(int))'],
+      [14n, '(B({}) | A(int))'],
+      [19n, '(A(int) | B({}))'],
+      [25n, 'str'],
+      [27n, 'int'],
       [20n, 'int'],
       [21n, 'int'],
-      [25n, '(int) => int'],
-      [27n, 'str'],
-      [29n, '{}'],
       [22n, 'int'],
-      [28n, '({}) => int'],
+      [26n, '(int) => int'],
+      [28n, 'str'],
+      [30n, '{}'],
       [23n, 'int'],
-      [30n, 'int'],
-      [5n, 'int'],
-      [4n, 'str'],
-      [6n, 'int'],
-      [7n, '(A(int) | B({}))'],
-      [8n, '(int) => (A(int) | B({}))'],
-      [9n, '(int) => (A(int) | B({}))'],
+      [29n, '({}) => int'],
+      [24n, 'int'],
+      [31n, 'int'],
     ])
   })