| name | afferent-reactive-universe-levels |
| description | Fix universe level mismatch errors when defining Lean 4 structures containing Reactive.Event
or Reactive.Dynamic types in Afferent/Canopy widgets. Use when: (1) compiler error "Type 1
of sort Type 2 but expected Type of sort Type 1", (2) WidgetM won't accept your result
structure, (3) structure contains Reactive.Event Spider or Reactive.Dynamic Spider fields.
The fix is to place `open Reactive Reactive.Host` BEFORE structure definitions.
|
| author | Claude Code |
| version | 1.0.0 |
| date | 2026-01-24T00:00:00.000Z |
Afferent Reactive Universe Levels
Problem
When creating Canopy widgets that return structures containing Reactive.Event Spider α or
Reactive.Dynamic Spider α fields, the compiler reports universe level mismatches like:
Application type mismatch: The argument MyResult has type Type 1 of sort Type 2
but is expected to have type Type of sort Type 1 in the application WidgetM MyResult
Context / Trigger Conditions
- Defining a new Canopy widget in
Afferent/Canopy/Widget/
- Widget returns a result structure containing
Reactive.Event or Reactive.Dynamic
- Error occurs at function signature like
def myWidget (...) : WidgetM MyResult
- Identical pattern works in other widget files (e.g., ListBox.lean)
Solution
The open statements must appear BEFORE any structure definitions that use reactive types.
Broken pattern:
namespace Afferent.Canopy
open Afferent.Arbor hiding Event
/-- This structure ends up in Type 1 -/
structure MyResult where
onClick : Reactive.Event Spider Unit
/-! ## Reactive Section -/
open Reactive Reactive.Host -- Too late!
open Afferent.Canopy.Reactive
def myWidget : WidgetM MyResult := ... -- Error: Type 1 vs Type
Fixed pattern:
namespace Afferent.Canopy
open Afferent.Arbor hiding Event
open Reactive Reactive.Host -- Before structure!
open Afferent.Canopy.Reactive
/-- Now correctly in Type 0 -/
structure MyResult where
onClick : Reactive.Event Spider Unit
def myWidget : WidgetM MyResult := ... -- Works
Verification
After reordering, rebuild with ./build.sh. The universe error should disappear and
the widget should compile successfully.
Example
From Toolbar.lean - the working structure:
namespace Afferent.Canopy
open Afferent.Arbor hiding Event
open Reactive Reactive.Host
open Afferent.Canopy.Reactive
structure ToolbarResult where
onAction : Reactive.Event Spider String
def toolbar (actions : Array ToolbarAction) (theme : Theme)
(variant : ToolbarVariant := .filled) : WidgetM ToolbarResult := do
...
Notes
- This affects the
Spider timeline type resolution
- The
hiding Event on Afferent.Arbor is necessary because Arbor has its own Event type
- Compare with working files like
ListBox.lean or Dropdown.lean which have opens at the top
- Pure WidgetBuilder functions (not WidgetM) don't have this issue since they don't return reactive types
References
- Afferent/Canopy/Widget/Data/ListBox.lean - working example pattern
- Afferent/Canopy/Widget/Input/Dropdown.lean - working example pattern
