[elab] Delay solving definition type

This way lambda signature can have more information available when they
are solved.

src/main/scala/com/github/tgeng/archon/common/utils.scala

@@ -199,8 +199,8 @@ def topologicalSort[T]
 //  (potentially) diverging recursive calls should show up as `div` effect. In other words, one
 //  can not omit `div` effect on effectful computation because handlers can swallow non-div
 //  effects.
-//  2. non-divergemce is much stronger than saying a function is not self-recursive. A
-//  non-recursive function may still diverge if it invoke some other divergen computation. It's
+//  2. non-divergence is much stronger than saying a function is not self-recursive. A
+//  non-recursive function may still diverge if it invoke some other diverging computation. Its
 //  non-divergence is only true when all computations are non-divergent (also non-recursive).
 //  3. there is a problem with heap and parameterized handler: user can store self-reference into
 //  a heap var (or emulate heap with handler parameter) and makes a seemingly total function

src/main/scala/com/github/tgeng/archon/core/ir/builtins.scala

@@ -20,6 +20,10 @@ private case class SimpleSignature
   override type S = SimpleSignature
 
   override def addDeclaration(d: Declaration): SimpleSignature =
+    assert(!declarations.contains(d.qn))
+    copy(declarations = declarations + (d.qn -> d))
+  override def replaceDeclaration(d: Declaration): SimpleSignature =
+    assert(declarations.contains(d.qn))
     copy(declarations = declarations + (d.qn -> d))
   override def addConstructor(qn: QualifiedName, c: Constructor): SimpleSignature =
     copy(constructors = constructors + (qn -> (constructors.getOrElse(qn, IndexedSeq()) :+ c)))

src/main/scala/com/github/tgeng/archon/core/ir/elaboration.scala

@@ -779,6 +779,12 @@ private def elaborateDefBody
       },
     )
     _Σ.addCaseTree(preDefinition.qn, _Q)
+    // We didn't solve the meta-variables inside the definition type until now because we want to
+    // have the call-site context ready before solving them. Delay solving during body elaboration
+    // works as long as lambda definitions are APPENDED after the call-site declaration. This is
+    // because our topological sort preserves original order of definitions when possible. Hence,
+    // the call-site function body would be elaborated before the lambda body.
+    _Σ.replaceDeclaration(definition.copy(ty = ctx.solveTerm(definition.ty)))
 
 @throws(classOf[IrError])
 private def elaborateEffectHead

src/main/scala/com/github/tgeng/archon/core/ir/signature.scala

@@ -90,6 +90,7 @@ case class Operation
 trait Signature:
   type S <: Signature
   def addDeclaration(d: Declaration): S
+  def replaceDeclaration(d: Declaration): S
 
   def addConstructor(qn: QualifiedName, c: Constructor): S
 

src/main/scala/com/github/tgeng/archon/core/ir/signatureTyping.scala

@@ -258,9 +258,7 @@ private object VarianceChecker extends Visitor[(TContext, Variance, Nat), Seq[Va
 def checkDef(definition: Definition)(using Signature)(using ctx: TypingContext): Definition =
   given Context = definition.context
   ctx.trace(s"checking def signature ${definition.qn}"):
-    // TODO[P0]: delay this part for synthetic lambda definitions because the signature would
-    //  contain many unsolved meta variables that depends on type checking the call-site definition.
-    val ty = ctx.solveTerm(checkIsCType(definition.ty))
+    val ty = checkIsCType(definition.ty)
     Definition(definition.qn, definition.context, ty)
 
 @throws(classOf[IrError])