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