[feature] constraint-based unification about cicada-plct HOT 5 OPEN

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
}

from cicada-plct.

Solution 1:

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

from cicada-plct.

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

We might read some papers about this.

from cicada-plct.

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

from cicada-plct.

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

Yes, it is :)

from cicada-plct.