Universe Issues

[marcusrossel]

Inspired by: 1:37:15 of https://www.youtube.com/watch?app=desktop&v=YKN3NLwW1MI
Also by: ~16:30 of https://www.youtube.com/watch?v=AWeT_G04a0A

Instead of encoding interfaces essentially as sigma types, try:

import Lean
open Lean

inductive Types
  | ofRcn1
  | ofInputPort3
  | ofStatVar9
  deriving BEq, Hashable

def Types.type
  | ofRcn1 => Bool
  | ofInputPort3 => String
  | ofStatVar9 => Nat

def Scheme := HashSet Types

#check Scheme

-- Then your runtime is essentially generic over such a `Types` type. 

structure RuntimeState (T : Type) (Ttyp : T → Type) where

#check RuntimeState

-- That is, what we've essentially achieved is to move all of the type info that was previously *inside* of a Scheme
-- into the type level. Before we didn't want to do that because it was essentially untenable, but as we've bundled
-- all of the type info into a single `Types` type it's actually feasible now.