claimed-wrong-type.error.inet

docs/tests/errors/claimed-wrong-type.error.inet

@@ -0,0 +1,9 @@
+type Nat 0 end
+node zero -- value!: Nat end
+node add1 prev: Nat -- value!: Nat end
+
+type Trivial 0 end
+node sole -- value!: Trivial end
+
+claim x Nat end
+define x sole end

docs/tests/errors/claimed-wrong-type.error.inet.err

@@ -0,0 +1,10 @@
+[unifyTypes] I fail to unify types -- left: Trivial, right: Nat
+
+[Define.execute] I fail to define word: x
+
+  5 |type Trivial 0 end
+  6 |node sole -- value!: Trivial end
+  7 |
+  8 |claim x Nat end
+  9 |define x sole end
+ 10 |

src/lang/stmts/Define.ts

@@ -1,5 +1,5 @@
 import { createCtx } from "../ctx/createCtx"
-import { cutWords } from "../cut/cutWords"
+import { cutWordDefinition } from "../cut/cutWordDefinition"
 import { createReport } from "../errors/createReport"
 import { Mod } from "../mod"
 import { lookupWordDefinitionOrFail } from "../mod/lookupWordDefinitionOrFail"
@@ -15,9 +15,6 @@ export class Define implements Stmt {
   ) {}
 
   async execute(mod: Mod): Promise<void> {
-    const ctx = createCtx()
-    cutWords(mod, ctx, this.words, {})
-
     try {
       const definition = lookupWordDefinitionOrFail(mod, this.name)
 
@@ -29,6 +26,9 @@ export class Define implements Stmt {
       }
 
       definition.words = this.words
+
+      const ctx = createCtx()
+      cutWordDefinition(ctx, definition, {})
     } catch (error) {
       throw createReport(error, {
         message: `[Define.execute] I fail to define word: ${this.name}`,

src/lang/unify/unifySignedTypes.ts

@@ -31,7 +31,7 @@ export function unifySignedTypes(
 
   if (right.sign === 0) {
     unifyTypes(ctx, left.t, right.t)
-    setNeutralSignedType(ctx, right, left)
+    setNeutralSignedType(ctx, left, right)
     return
   }