canonical does not compile at main: sqlQuery %macro fails with "script is not a data value"

[Lazare-42]

Summary

The canonical example does not compile at main (522057c). The sqlQuery %macro fails to elaborate with Bad elaborator script … (script is not a data value) at every call site (apiViewer, articleSummary, apiArticleFeed, …). This reproduces on the toolchain the repo's own flake pins, and nix build (CI) is red on every recent commit.

(Salut Vincent — tu m'as dit "should work, essaye de faire tourner l'exemple" : voilà, je l'ai fait tourner avec ta toolchain exacte, et ça casse. Détails ci-dessous + un repro minimal de 6 lignes.)

Environment (your exact pinned toolchain)

Ran examples/canonical through its own devenv flake (nix develop on examples/canonical) with a clean ~/.local/state/pack, then sh scripts/build --server:

Package Collection : nightly-260613
Idris2 Commit      : 6ca00e72e32849cb35e5c262904e9c3cffc1a9a4
idris2 --version   : Idris 2, version 0.8.0

(Postgres for the TypedSQL DESCRIBE was provided; that step succeeds — the generated .wire cache is correct. The failure is purely the Idris compile.)

Failure

scripts/build --server gets through framework install, typegen, .idrx view generation, route-refs, and the TypedSQL describe, then fails compiling the controllers:

6/57: Building Web.Controller.Route.ApiArticleFeed (build/generated/Web/Controller/Route/ApiArticleFeed.idr)
Error: While processing right hand side of apiViewer. Sorry, I can't find any elaboration which works. All errors:
Possible error:
    When unifying: Elab ?a  and:  String -> Elab (App ?e ?a)
    ...
Possible error:
    Bad elaborator script case postgresCheckedQuery (MkSqlSchemaMetadata […]) (MkPostgresDescribeMetadata "select id, username, … from users where username = ${username}" "SELECT" […]) of
      { Left error => failSql …
      ; Right (query, types) => case query .columns of { [] => failSql …; _ => pure (preparedQueryTerm types query) }
      } (script is not a data value).
Possible error:
    When unifying: String -> Elab ?a  and:  Elab ?scriptTy
    ...

Same error at articleSummary and apiArticleFeed.

Minimal repro

In a module that imports Iwf and the generated Generated.Schema:

testFn : {auto database : ControllerDatabase} -> String -> ControllerApp (Maybe UsersRow)
testFn username = do
  user <- sqlQuery "select id, username, email, password_hash, bio, image, created_at, updated_at from users where username = ${username}" username
  pure user

→ Bad elaborator script case postgresCheckedQuery … of … (script is not a data value).

Isolation (the interesting part)

I narrowed where the stall is. Calling the macro internals directly inside my own %runElab works; only the sqlQuery %macro expansion at the call site fails:

What I elaborate	Result
sqlQueryTermChecked with literal SqlSchemaMetadata + PostgresDescribeMetadata	✅ compiles
…with the real schemaMetadata (from Generated.Schema) + a literal field referencing users	✅ compiles
schema <- schemaMetadataFromScope then sqlQueryTermChecked	✅ compiles
Full internals in %runElab: schemaMetadataFromScope + describeSqlFromGeneratedCache "…" (real cached metadata) + sqlQueryTermChecked	✅ compiles
The sqlQuery %macro at a controller call site (testFn above)	❌ (script is not a data value)

So case postgresCheckedQuery schema describeMetadata of … (in sqlQueryTermChecked, libs/idris-sql/src/Iwf/TypedSql.idr) reduces fine when driven from %runElab, but stalls when the same path runs as part of the sqlQuery/sqlExec %macro expansion (src/Iwf/Controller.idr). It is not a public-export / visibility issue (describeSqlFromGeneratedCache uses the private parseDescribeWire and reduces fine), not the data, not the describe cache, not the environment.

Likely related

The controller SQL interface was refactored just before this:

• 522057c simplify sql query and routing
• 84bc095 Simplify controller SQL interface
• e2b555b Simplify controller errors and SQL parameters

nix build (CI) is failing on all of these.

Ask

Does main build for you locally right now, and on which idris2 commit? Happy to test a patch — I have a fast repro loop set up (fork at Lazare-42/iwf).