[feature] constraint-based unification

[xieyuheng]

• pass test "check Cons -- my_cons -- constraint-based unification"
• globals.cons
• add test compute just cons

[xieyuheng]

In the following example,

function my_cons(
  implicit A: Type,
  implicit B: (A) -> Type,
  x: A,
  y: B(x),
): exists (x: A) B(x) {
  return cons(x, y)
}

check my_cons("ratatouille", "baguette"): Pair(String, String)

during inferAp, we will meet:

unify B(x) = String

but only after the outer unification (during checkByInfer):

unfiy exists (x: A) B(x) = Pair(String, String)

We know:

{
  B: (_) => String
}

[xieyuheng]

Solution 1:

During inferAp, save unify B(x) = String as a constraint.

[xieyuheng]

I think this is called "constraint-based unification".

We might read some papers about this.

[xieyuheng]

Maybe learn from: https://en.wikipedia.org/wiki/Constraint_logic_programming

[ice1000]

I think this is called "constraint-based unification".

Yes, it is :)