TODO

# IILibs: Lens List Eff BitSet
# II: DFA NFA glushkov Charscan
# TT: μ datatypes
# Typer
  * Fns always Typed: Lift constants , lambdas , paps , [alts , cases]
  * Casts: @ret , @fnArg. Must insert during β-env, to respect user annotations
  * Alt casts

  ? biunify type vs finalised type (GraphType vs Term) => coocs? (for each var, + and - co-occs)
  * Subsumption & use annotations
  ? Type params & application & μ
  ? dependents lifted and normalised
  * typeOf : {l : Level}{A : Set l}(a : A) -> Set l
  * typeOf {A = A} _ = A
## Top Priority (PathNames , cross-level mutuality)
  * Label names; @ vs declared => @ may take any type whereas declared labels must respect declared type
  * Profunctor lenses
  * Type params (conv bruijnAbs to THBi) ; Type application vs implicit
  * Add let-capture tests
  * leaf bicasts ; subtype tycon trees (traversals)
  * Case call stream.next to recover nice syntax (? subtype @stream to open top layer)
  * Identify recons (cons over matches) and rewrite to Lens insert / modify
  * Subsumption.ii (also graphType , instantiation , multiplicities)
  * Use VQBindIndex everywhere relevant
  * Bounded Tvars eg. "[Tlo <: a <: Thi] => a -> a" instead of "∀a. a ⊓ T -> a" => 
  * no need to emit a tuple underneath every label
  * Can fuse scope infer hypo if scope saves params to letblock for resumption
## Memory
  * Derived streams (eg. splitAt, where second stream only available after first produced (ie. 2 can mutate 1 to buf)).
## New primitives + Syntax
  * '.' as reverse application: eg. "Cons a.x Nil" == "Cons (x a) Nil"
  * record wildcard: "rw = { x = Int , y }" -- indicates "y = ?"
  * Join text: `"hello" , "world"`
  * List: `# a b c`
  * Union|intersect records&sumdata: V and ^
  * set/get formal semantics, add new fields?
  * Presence variables + quantify `decomp : Label A -> [A _ | ..] -> ([A _] , [..])`
  * generalise all lambda types (unless inlineable?) + check not-recursive (avoid inf β-reduction eg. Y-comb)
  * subtypes: Identity Iso "a <: Identity a" "Identity a <: a" & typeClass dict "{ ret : A } <: A"
  * module import-sig (will help with mutual modules)
  * Meta-record: { ret : A , ... } <: A
  * mkSimd, some functions map directly to simd version
  * '.' , reservedChar for "r.f" , but want ".&." , ".." names => reserve '.' => let words start with "."?
  * ~> = implicit arg: A ~> A -> A ; ~ for app of implicit: "identity ~Int 3"
  * record type syntax: { x = Int , y } -- indicates y = ? (makes sense as a type, else is bottom)
  * record union (| : |) , difference (\\ : \\)
  * `$ ls -l --reverse`: '$' runs opt-parse on text to end-of-line
  * scope of field/label names: topnames or label names?
      {x = 3} . x .~ "hello" -- { x : Int } -> { x : String }
  * (constexpr : a -> a) => Guarantee a compile time constant
  * (constReadFile : String -> String) => read file at compile time
  ? `setBit` infix syntax
  ? Sum-of-Record
  ? argCase => f = \argCase { a b => _ }
### Linearity ; free variables (type must be known) ; β vs always-inline
  ! β-opt: Specialise on paps iff dupd (or all paps?) (polymorphic functions may miss pap-specs)
  * dup node scope: global / device / thread ?
      f x = x x => f x = let a b = DUP x in a b
      ! see when lambdas are duplicated (also reduce computations on free-vars when papped)
  ? compute containement
# ASM: sum & prod , polymorphism , recursives (µ combinator + memory management mark)
  * Count ERA through case
  * pass down cc hints
  * mov V push (overwrite vs preserve for call)
  * Topo-sort bindings
  * FunArg: fn ptr + ptr to papstruct (requires specialisation / new function per pap!)
  * CC: 1 arg = 1 reg. poly = (64bit , YMM). FnArg = (fnPtr , memPtr)
## Notes. Modules / records. (! Modules have an IConv + File)
  Topo-sort so dependents always computed first, mark mutuals
    Record = Vector ([?Mutuals | Vector ?Record])
  export list & bind Import list
  Cap field number?
  Eraser argument is a form of function subtyping
  add-specs to imported binds
  unInline case-branch lambdas for bypass/cross-module specialisation
  open / required (also locally)
  record-field patterns ((a , b) = rhs) => (\case { (a , b) => rhs })
    ? need to case over whole record since lhs is in scope mutually
  * sealing (effect): module becomes only accessible through its signature
  ? mutual functions within separate records = eg. let a = { f = b.g } ; b = { g = a.f }
  * Mutual modules = (λimports -> λM[m1 , m2] -> (m1 , m2)) i1..in M1 M2
  * record-field patterns: ? make mutual λ over whole record -- (f , g) = (2 , 3)
  * type/term scope; Idris: (names bound in types are also bound as @-patterns)
    vlength : {n : Nat} -> Vect n a -> Nat
    vlength _ = n
## !?
  * Non-regular recursive types (cannot be encoded direclty with μ)
  * prec/assoc as partial order
  * Higher kinded polymorphism: abstracting over type constructors
  * short-circuit fns: _&&_
  * named arguments (perhaps by subtype from a record arg)
  * shared streams (eg. MUL)
  * derived streams: splitAt creates 2 streams from 1, but the second is only available after the first
  * reflection; dynamic fuse pap: (+1) << (+1) => (+2)
  * type application (eg. perfect tree) `PTree a = Leaves a | Cons (PTree (a , a))` (μ insufficient here)
  * Sum of record [l : { f : int } | l2 : { f : int }] <: { f : int }
  * expand lambda-mixfixes with explicit holes
  * mixfix re-arrange let-ins `if y then let x = 3 in x else y` (Juxt x else y) or (; Juxt else y)
  * typecase: inspect type arg; eg. if arg : t1 return t2 , else if T1 , return T2
    This function has type (t1 → t2) u (T1 → T2), but not (t1 ^ T1) → (t2 U T2)
  * subsumption requires initiality and distributivity of ⊓ and ⊔ over → and ×
## Parse / Pretty / Repl
  * lambda case type annotation, \case : scrut -> ret
  * Parse Intrinsics (eg. readConstFile , getFnName , getSourceLine , getSourceFile etc..)
  * repl parser: multiline case / let
  * edit-distance
  * pretty case-case formats wrong
## Types
  * Ad-hoc polymorphism: `Int <: [ NumInt Int ]` show (esp for repl JIT) (? mempty : Monoid a => a)
  * THFieldCollision
  * Dependent normalisation
  * first class polymorphism: eg. require instantiating with polytypes
    '<<' in let f : [a] -> [a] -> Int ; g : Bool -> [a] -> [a] in f << g
  * Linear types; dependent types required to quantify relative linearity `Lin t >= Lin f => t -> u`
## Beta-optimality: Specialise paps (tough to detect paps on polymorphic data)
  * λ Minimise normal forms: λ-encoding + lifting + sharing
  * λ-lifting: if all subterms of App or Match share λ, lift it
  * case-splitters as data for runtime optimisation
  * Partial applications extracted and specialised for beta optimality
  * fns that do case-splits lazy in arguments they may not need
## Error messages
  * Warn nonsense type joins | dependent case?
## Unimportant
  * Use System.OsPath instead of FilePath: System.File.OsPath.readFile
  * let-scope depends on mixfix parse: "letscopeAfterMixfix y = if y then let x = 3 in x else y"
  * mode to print type-var bounds
  * Insta-unwrap/specialise single branch cases
  * Completion based on types (Type -> Bind)
  * tabs vs spaces
  * Termination checker, if a Refl type diverges it proves nothing
  * strictly positive recursion
  * underdetermined recursion: https://counterexamples.org/underdetermined-recursion.html
    equirecursive => A = F[A] ; B = F[B] => A = B (unsound for arbitrary type-level functions F!)
    if multiple solutions for X = F X; eg. F X = X ; A = Int ; B = String
  * don't assume injectivity! (or. distinguish between type constructors and type-functions)
  * equality constraints are central to GADTs `Gabriel Scherer and Didier Rémy. GADTs meet subtyping.` `https://okmij.org/ftp/ML/first-class-modules/#GADT`
  * switch to codeberg
  * Allow dynamic inspection of papped args
  * Pattern PTT: custom unPat function to support any patterns eg. `fact (<? 2) = 1`
  * error messages via prettyprinter Doc
  * language server
  * mergetyhead indicates if merge was a noop (so bisub knows it has already seen that input)
  * Function = Constructor + rewrite rules ?
  * `typeOf : (t : Type) -> Type` shortcut to access (and alias) an inferred type
  * surround notes: cs"' cs'<q> cst" ds" ysiw] cs]{ yssb ds{ds) ysiw<em>
  * https://documentation.divio.com/
  * phase distinction: meaning of static expr not dependent on executing dynamic exprs
  * prevent β-env loops
  * https://arxiv.org/pdf/2202.13633v1.pdf has text on GADT and fixpoints