Unification should schedule and normalize constraints

[BinderDavid]

The following example should typecheck, but it doesn't:

data Bool { True, False }

data Nat { Z, S(n: Nat) }

def Bool.ite(a: Type, x y: a): a {
    True => x,
    False => y
}

-- We want to unify the telescope (True, Nat) with (x, x.ite(Type, Nat, Bool))

data T(x : Bool, a : Type) {
    C : T(True, Nat)
}

def T(x, x.ite(Type,Nat, Bool) : Type).foo(x : Bool) : Type {
    C => ?
}

The tricky bit is that we get the following constraint:

(True, Nat) = (x, x.ite(Type, Nat,Bool))

which can be decomposed into two constraints:

True = x
Nat = x.ite(Type,Nat,Bool)

which can be solved if done in the correct order and by interleaving normalization with unification.

[BinderDavid]

Current output with --trace option:

pol --trace check examples/counterexample.pol 
[] |- True =>
[] |- True =>
[] |- foo =>
[[]] |- Bool <= Type
[[]] |- Bool => ?
[[]] |- Bool => Type
Type =? Type
Type =? Type
[[]] |- Bool <= Type
[[]] |- Bool ▷ ?
[[]] |- Bool ▷ Bool
↓Bool ~> ?
↓Bool ~> Bool
[[[email protected]]] |- [email protected] ▷ ?
[[[email protected]]] |- [email protected] ▷ [email protected]
[[[email protected]]] |- ([email protected](Type, Nat, Bool)):Type ▷ ?
[[[email protected]]] |- [email protected](Type, Nat, Bool) ▷ ?
[[[email protected]]] |- [email protected] ▷ ?
[[[email protected]]] |- [email protected] ▷ [email protected]
[[[email protected]]] |- Type ▷ ?
[[[email protected]]] |- Type ▷ Type
[[[email protected]]] |- Nat ▷ ?
[[[email protected]]] |- Nat ▷ Nat
[[[email protected]]] |- Bool ▷ ?
[[[email protected]]] |- Bool ▷ Bool
[[[email protected]]] |- [email protected](Type, Nat, Bool) ▷ [email protected](Type, Nat, Bool)
[[[email protected]]] |- ([email protected](Type, Nat, Bool)):Type ▷ [email protected](Type, Nat, Bool)
↓[email protected] ~> ?
↓[email protected] ~> [email protected]
↓[email protected](Type, Nat, Bool) ~> ?
↓Type ~> ?
↓Type ~> Type
↓Nat ~> ?
↓Nat ~> Nat
↓Bool ~> ?
↓Bool ~> Bool
↓[email protected](Type, Nat, Bool) ~> [email protected](Type, Nat, Bool)
[[[email protected]]] |- T([email protected], ([email protected](Type, Nat, Bool)):Type) ▷ ?
[[[email protected]]] |- [email protected] ▷ ?
[[[email protected]]] |- [email protected] ▷ [email protected]
[[[email protected]]] |- ([email protected](Type, Nat, Bool)):Type ▷ ?
[[[email protected]]] |- [email protected](Type, Nat, Bool) ▷ ?
[[[email protected]]] |- [email protected] ▷ ?
[[[email protected]]] |- [email protected] ▷ [email protected]
[[[email protected]]] |- Type ▷ ?
[[[email protected]]] |- Type ▷ Type
[[[email protected]]] |- Nat ▷ ?
[[[email protected]]] |- Nat ▷ Nat
[[[email protected]]] |- Bool ▷ ?
[[[email protected]]] |- Bool ▷ Bool
[[[email protected]]] |- [email protected](Type, Nat, Bool) ▷ [email protected](Type, Nat, Bool)
[[[email protected]]] |- ([email protected](Type, Nat, Bool)):Type ▷ [email protected](Type, Nat, Bool)
[[[email protected]]] |- T([email protected], ([email protected](Type, Nat, Bool)):Type) ▷ T([email protected], [email protected](Type, Nat, Bool))
↓T([email protected], [email protected](Type, Nat, Bool)) ~> ?
↓[email protected] ~> ?
↓[email protected] ~> [email protected]
↓[email protected](Type, Nat, Bool) ~> ?
↓Type ~> ?
↓Type ~> Type
↓Nat ~> ?
↓Nat ~> Nat
↓Bool ~> ?
↓Bool ~> Bool
↓[email protected](Type, Nat, Bool) ~> [email protected](Type, Nat, Bool)
↓T([email protected], [email protected](Type, Nat, Bool)) ~> T([email protected], [email protected](Type, Nat, Bool))
[[[email protected]]] |- Bool ▷ ?
[[[email protected]]] |- Bool ▷ Bool
↓Bool ~> ?
↓Bool ~> Bool
[[Bool]] |- [email protected] <= Bool
[[Bool]] |- [email protected] => ?
[[Bool]] |- [email protected] => Bool
Bool =? Bool
Bool =? Bool
[[Bool]] |- [email protected] <= Bool
[[[email protected]]] |- Type ▷ ?
[[[email protected]]] |- Type ▷ Type
↓Type ~> ?
↓Type ~> Type
[[Bool]] |- ([email protected](Type, Nat, Bool)):Type <= Type
[[Bool]] |- ([email protected](Type, Nat, Bool)):Type => ?
[[Bool]] |- Type <= Type
[[Bool]] |- Type => ?
[[Bool]] |- Type => Type
Type =? Type
Type =? Type
[[Bool]] |- Type <= Type
[[[email protected]]] |- Type ▷ ?
[[[email protected]]] |- Type ▷ Type
↓Type ~> ?
↓Type ~> Type
[[Bool]] |- [email protected](Type, Nat, Bool) <= Type
[[Bool]] |- [email protected](Type, Nat, Bool) => ?
[[[email protected]]] |- Type ▷ ?
[[[email protected]]] |- Type ▷ Type
↓Type ~> ?
↓Type ~> Type
[[Bool]] |- Type <= Type
[[Bool]] |- Type => ?
[[Bool]] |- Type => Type
Type =? Type
Type =? Type
[[Bool]] |- Type <= Type
[[[email protected]]] |- Type ▷ ?
[[[email protected]]] |- Type ▷ Type
↓Type ~> ?
↓Type ~> Type
[[Bool]] |- Nat <= Type
[[Bool]] |- Nat => ?
[[Bool]] |- Nat => Type
Type =? Type
Type =? Type
[[Bool]] |- Nat <= Type
[[[email protected]]] |- Type ▷ ?
[[[email protected]]] |- Type ▷ Type
↓Type ~> ?
↓Type ~> Type
[[Bool]] |- Bool <= Type
[[Bool]] |- Bool => ?
[[Bool]] |- Bool => Type
Type =? Type
Type =? Type
[[Bool]] |- Bool <= Type
[[[email protected]]] |- Bool ▷ ?
[[[email protected]]] |- Bool ▷ Bool
↓Bool ~> ?
↓Bool ~> Bool
[[Bool]] |- [email protected] <= Bool
[[Bool]] |- [email protected] => ?
[[Bool]] |- [email protected] => Bool
Bool =? Bool
Bool =? Bool
[[Bool]] |- [email protected] <= Bool
[[[email protected]]] |- Type ▷ ?
[[[email protected]]] |- Type ▷ Type
↓Type ~> ?
↓Type ~> Type
[[Bool]] |- [email protected](Type, Nat, Bool) => Type
Type =? Type
Type =? Type
[[Bool]] |- [email protected](Type, Nat, Bool) <= Type
[[Bool]] |- ([email protected](Type, Nat, Bool)):Type => Type
Type =? Type
Type =? Type
[[Bool]] |- ([email protected](Type, Nat, Bool)):Type <= Type
[[Bool],[T([email protected], [email protected](Type, Nat, Bool))]] |- Type => ?
[[Bool],[T([email protected], [email protected](Type, Nat, Bool))]] |- Type => Type
[[[email protected]],[@0.0]] |- Type ▷ ?
[[[email protected]],[@0.0]] |- Type ▷ Type
↓Type ~> ?
↓Type ~> Type
[[]] |- True ▷ ?
[[]] |- True ▷ True
[[]] |- Nat ▷ ?
[[]] |- Nat ▷ Nat
↓True ~> ?
↓True ~> True
↓Nat ~> ?
↓Nat ~> Nat
[[Bool]] |- C => ? <= Type
[[Bool]] |- C => ? <= Type
Error: U-003

  × Cannot automatically decide whether Nat and x.ite(Type, Nat, Bool) unify
    ╭─[examples/counterexample.pol:12:1]
 12 │ data T(x : Bool, a : Type) {
 13 │     C : T(True, Nat)
    ·                 ───
 14 │ }
 15 │ 
 16 │ def T(x, x.ite(Type,Nat, Bool) : Type).foo(x : Bool) : Type {
    ·          ─────────────────────
 17 │     C => ?
    ╰────

[BinderDavid]

Requires #170 to be implemented first. From the error message it is also clear that the substitution is only recorded in the subst data structure, but not applied to the remaining constraints: The error message would say "Cannot automatically decide whether Nat and True.ite(Type, Nat, Bool) unify" otherwise.