From c71982fe5dc6a37acb20ef66994f391fa4b571dd Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Fri, 29 May 2026 19:52:18 +0000 Subject: [PATCH 1/5] Report arity mismatch for type aliases instead of silently returning original type (#1239) Add LMonoTy.checkAliasArity that detects when a type constructor name matches a registered alias but with the wrong number of type arguments. Use it in tconsAlias and aliasDef? to produce a clear error message instead of silently returning the unresolved type. The pure tconsAliasSimple and resolveAliases functions are unchanged to avoid impacting the many proofs that depend on their structure. --- Strata/DL/Lambda/LExprTypeEnv.lean | 36 +++++++++++++++++---- Strata/DL/Lambda/LExprTypeSpec.lean | 7 ++-- StrataTest/DL/Lambda/LExprTypeEnvTests.lean | 13 +++++++- 3 files changed, 46 insertions(+), 10 deletions(-) diff --git a/Strata/DL/Lambda/LExprTypeEnv.lean b/Strata/DL/Lambda/LExprTypeEnv.lean index a1a2d41510..31ec92dfa6 100644 --- a/Strata/DL/Lambda/LExprTypeEnv.lean +++ b/Strata/DL/Lambda/LExprTypeEnv.lean @@ -855,6 +855,18 @@ theorem LTy_subst_instantiate {IDMeta : Type} [ToFormat IDMeta] instance : Inhabited (Option LMonoTy × TEnv IDMeta) where default := (none, TEnv.default) +/-- Check whether `name` matches an alias but with the wrong number of type + arguments. Returns an error on arity mismatch, or `.ok ()` otherwise. -/ +def LMonoTy.checkAliasArity (name : String) (args : LMonoTys) + (aliases : List TypeAlias) : Except Format Unit := + match aliases.find? (fun a => a.name == name) with + | none => .ok () + | some alias => + if alias.typeArgs.length == args.length then .ok () + else .error f!"Arity mismatch for type alias '{name}': \ + expected {alias.typeArgs.length} type argument(s), \ + got {args.length}" + /-- Return the instantiated definition of `.tcons name args` if it is a registered type alias. @@ -869,7 +881,10 @@ def LMonoTy.tconsAlias [ToFormat IDMeta] (name : String) (args : LMonoTys) let matchingAlias := Env.context.aliases.find? (fun a => a.name == name && a.typeArgs.length == args.length) match matchingAlias with - | none => return (inputMty, Env) + | none => + -- Check for arity mismatch: name matches but arity doesn't. + LMonoTy.checkAliasArity name args Env.context.aliases + return (inputMty, Env) | some alias => -- Create instantiation pair: [alias pattern, alias definition]. -- The alias pattern and definition share the same type variables here. @@ -918,7 +933,9 @@ check whether the de-aliased types are registered/known. def LMonoTy.aliasDef? [ToFormat IDMeta] (mty : LMonoTy) (Env : TEnv IDMeta) : Except Format (LMonoTy × TEnv IDMeta) := do match mty with - | .tcons name args => return (LMonoTy.tconsAliasSimple name args Env.context.aliases, Env) + | .tcons name args => + LMonoTy.checkAliasArity name args Env.context.aliases + return (LMonoTy.tconsAliasSimple name args Env.context.aliases, Env) | .bitvec _ | .ftvar _ => return (mty, Env) mutual @@ -1644,8 +1661,11 @@ theorem tconsAlias_tyGen_mono -- Case split on whether a matching alias is found split at h case h_1 => - -- No matching alias: Env' = Env - simp [Pure.pure, Except.pure] at h; obtain ⟨_, h2⟩ := h; subst h2; omega + -- No matching alias: split on checkAliasArity + simp only [Bind.bind, Except.bind] at h + split at h + · simp at h + · simp [Pure.pure, Except.pure] at h; obtain ⟨_, h2⟩ := h; subst h2; omega case h_2 alias_val => -- Matching alias found: calls instantiateEnv then unify + updateSubst split at h @@ -1664,10 +1684,12 @@ theorem aliasDef_tyGen_mono (mty' : LMonoTy) (Env' : TEnv T.IDMeta) (h : LMonoTy.aliasDef? mty Env = .ok (mty', Env')) : Env'.genEnv.genState.tyGen ≥ Env.genEnv.genState.tyGen := by - simp only [LMonoTy.aliasDef?] at h + simp only [LMonoTy.aliasDef?, Bind.bind, Except.bind] at h split at h - · -- tconsAliasSimple doesn't change Env - simp [Pure.pure, Except.pure] at h; obtain ⟨_, h2⟩ := h; subst h2; omega + · -- .tcons case: split on checkAliasArity + split at h + · simp at h + · simp [Pure.pure, Except.pure] at h; obtain ⟨_, h2⟩ := h; subst h2; omega · simp [Pure.pure, Except.pure] at h; obtain ⟨_, h2⟩ := h; subst h2; omega · simp [Pure.pure, Except.pure] at h; obtain ⟨_, h2⟩ := h; subst h2; omega diff --git a/Strata/DL/Lambda/LExprTypeSpec.lean b/Strata/DL/Lambda/LExprTypeSpec.lean index 559483a301..054556dde3 100644 --- a/Strata/DL/Lambda/LExprTypeSpec.lean +++ b/Strata/DL/Lambda/LExprTypeSpec.lean @@ -4467,8 +4467,11 @@ theorem tconsAlias_eq_simple match ma with | none => unfold LMonoTy.tconsAlias at h_tcons; rw [h_find] at h_tcons - simp at h_tcons - obtain ⟨h1, h2⟩ := h_tcons; rw [← h1, ← h2] + simp only [Bind.bind, Except.bind] at h_tcons + split at h_tcons + · contradiction + · simp at h_tcons + obtain ⟨h1, h2⟩ := h_tcons; rw [← h1, ← h2] | some alias => have h_alias_wf := h_aliases_wf alias (List.mem_of_find?_eq_some h_find) have h_pred := List.find?_some h_find diff --git a/StrataTest/DL/Lambda/LExprTypeEnvTests.lean b/StrataTest/DL/Lambda/LExprTypeEnvTests.lean index 84fa52b542..cfe089f9b3 100644 --- a/StrataTest/DL/Lambda/LExprTypeEnvTests.lean +++ b/StrataTest/DL/Lambda/LExprTypeEnvTests.lean @@ -69,7 +69,7 @@ Subst: type := mty[bool]}]} ) return format ans -/-- info: ok: myInt -/ +/-- info: error: Arity mismatch for type alias 'myInt': expected 1 type argument(s), got 0 -/ #guard_msgs in #eval do let (ans, _) ← LMonoTy.aliasDef? mty[myInt] ( (@TEnv.default String).updateContext @@ -119,6 +119,17 @@ Subst: type := mty[bool]}]} ) return (format ans) +-- Test: arity mismatch produces a clear error (issue #1239) +/-- info: error: Arity mismatch for type alias 'MyAlias': expected 1 type argument(s), got 2 -/ +#guard_msgs in +#eval do let (ans, _) ← LMonoTy.aliasDef? mty[MyAlias int bool] + ( (@TEnv.default String).updateContext + { aliases := [{ + typeArgs := ["a"], + name := "MyAlias", + type := mty[Wrapped %a]}] }) + return format ans + /-- info: false -/ #guard_msgs in #eval isInstanceOfKnownType mty[myTy (myTy)] From d4812e6f93107b771dafa425ecb011f7d2373381 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Fri, 29 May 2026 21:27:28 +0000 Subject: [PATCH 2/5] ci: retry after transient cache miss in downstream jobs From 717327297c05f9eede6e2cd310eccd0cc8836e1c Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 11 Jun 2026 15:07:58 +0000 Subject: [PATCH 3/5] ci: delete stale cache before saving to prevent downstream cache misses actions/cache/save is a no-op when the key already exists. If a previous run partially saved or the cache became stale, downstream jobs that use fail-on-cache-miss fail permanently. Delete the existing entry first so that the save always succeeds with fresh artifacts. --- .github/actions/save-lake-cache/action.yml | 7 +++++++ .github/workflows/ci.yml | 3 +++ 2 files changed, 10 insertions(+) diff --git a/.github/actions/save-lake-cache/action.yml b/.github/actions/save-lake-cache/action.yml index 5754371b87..7c6f2ea5fd 100644 --- a/.github/actions/save-lake-cache/action.yml +++ b/.github/actions/save-lake-cache/action.yml @@ -28,6 +28,13 @@ inputs: runs: using: composite steps: + - name: Delete existing cache entry (if any) + shell: bash + env: + GH_TOKEN: ${{ github.token }} + CACHE_KEY: ${{ inputs.key-prefix }}-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ hashFiles('**/*.st') }}-${{ github.sha }} + run: | + gh actions-cache delete "$CACHE_KEY" --repo "$GITHUB_REPOSITORY" --confirm 2>/dev/null || true - name: Save lake cache uses: actions/cache/save@v5 with: diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 35202f6b57..62b338439e 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -24,6 +24,9 @@ jobs: build_and_test_lean: name: Build and test Lean runs-on: ubuntu-latest + permissions: + contents: read + actions: write strategy: matrix: toolchain: From 170315bd78d6134f4151ebc5a5a33cb0969b4cab Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 11 Jun 2026 15:40:33 +0000 Subject: [PATCH 4/5] ci: save lake cache even when a prior step fails Add if: '!cancelled()' to the save-lake-cache step so that downstream jobs can still find the cache when an unrelated step (e.g. tests or syntax verification) fails before the save. --- .github/workflows/ci.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 62b338439e..4dba846280 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -86,6 +86,7 @@ jobs: lake-package-directory: StrataCLI use-github-cache: false - name: Save lake cache + if: '!cancelled()' uses: ./.github/actions/save-lake-cache with: path: | From eaa2c93821fcd22f774f5504a5641a728ddf5647 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 11 Jun 2026 16:10:46 +0000 Subject: [PATCH 5/5] ci: revert cache delete step that caused downstream cache miss The gh actions-cache delete step (added in 717327297) and the explicit permissions block were causing downstream jobs to fail with cache miss errors. Revert to the main2 behavior (simple save without pre-delete) while keeping the !cancelled() guard so the cache is saved even when earlier steps fail. --- .github/actions/save-lake-cache/action.yml | 7 ------- .github/workflows/ci.yml | 3 --- 2 files changed, 10 deletions(-) diff --git a/.github/actions/save-lake-cache/action.yml b/.github/actions/save-lake-cache/action.yml index 7c6f2ea5fd..5754371b87 100644 --- a/.github/actions/save-lake-cache/action.yml +++ b/.github/actions/save-lake-cache/action.yml @@ -28,13 +28,6 @@ inputs: runs: using: composite steps: - - name: Delete existing cache entry (if any) - shell: bash - env: - GH_TOKEN: ${{ github.token }} - CACHE_KEY: ${{ inputs.key-prefix }}-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ hashFiles('**/*.st') }}-${{ github.sha }} - run: | - gh actions-cache delete "$CACHE_KEY" --repo "$GITHUB_REPOSITORY" --confirm 2>/dev/null || true - name: Save lake cache uses: actions/cache/save@v5 with: diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 4dba846280..58954ec31e 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -24,9 +24,6 @@ jobs: build_and_test_lean: name: Build and test Lean runs-on: ubuntu-latest - permissions: - contents: read - actions: write strategy: matrix: toolchain: