[bug] Scope problem of implicit argument and fulfilling class type

[xieyuheng]

class Isomorphism {
  cat: Category
  dom: cat.Object
  cod: cat.Object
  morphism: cat.Morphism(dom, cod)
  inverse: cat.Morphism(cod, dom)

  inverse_left: Equal(
    cat.Morphism(dom, dom),
    cat.compose(morphism, inverse),
    cat.id(dom),
  )

  inverse_right: Equal(
    cat.Morphism(cod, cod),
    cat.compose(inverse, morphism),
    cat.id(cod),
  )
}

Problem：

• cat.compose is a PiImplicit.
• take the cat.compose(morphism, inverse) in inverse_left as example.
• elaboration will insert ApImplicit based on the type of morphism,
  get cat.compose(implicit x1, implicit x2, morphism, implicit x3, inverse).
• solve it, get cat.compose(implicit dom, implicit dom, morphism, implicit dom, inverse),
  we write it like this, but actually solved value will not be substituted in place,
  but be saved in the env of the closure as x1 => dom.
• now dom is in scope, but only have type dom: cat.Object, no value, thus it is a neutral variable.
• in the following code block, fulfilling class type Isomorphism(cat, x.object, y.object)
  will provide the value of dom -- x.object.
• during fulfilling class type, when evaluating inverse_left's type,
  we have dom => x.object and x1 => dom in scope,
  evaluate variable x1 will only get the neutral variable dom,
  but not going further to get the value of dom -- x.object,
  this is the problem.

import { Isomorphism } from "../category/index.cic"
import { equal_swap, equal_compose } from "../equality/index.cic"

function terminal_object_isomorphism(
  cat: Category,
  x: Terminal(cat),
  y: Terminal(cat),
): Isomorphism(cat, x.object, y.object) {
  let f = x.morphism(y.object)
  let g = y.morphism(x.object)

  return {
    cat,
    dom: x.object,
    cod: y.object,
    morphism: y.morphism(x.object),
    inverse: x.morphism(y.object),

    inverse_left: equal_compose(
      x.morphism_unique(cat.compose(g, f)),
      equal_swap(x.morphism_unique(cat.id(x.object))),
    ),

    inverse_right: equal_compose(
      y.morphism_unique(cat.compose(f, g)),
      equal_swap(y.morphism_unique(cat.id(y.object))),
    ),
  }
}

Solution 1:

Use substInEnv.

---

It might be not enough for substInEnv to only handle variable,
maybe we also need to handle all Values
-- like deep walk
-- maybe called advanceByEnv (v.s. advanceBySolution).