Unification can produce circular solutions

[Ailrun]

With the next beluga code and input, harpoon consumes indefinite amount of time to finish.

% nats_and_bools_tps.bel
LF term : type =
| true : term
| false : term
| if_then_else : term -> term -> term -> term
| z : term
| succ : term -> term
| pred : term -> term
| iszero : term -> term
;

LF value : term -> type =
| v_z : value z
| v_succ : value V -> value (succ V)
| v_true : value true
| v_false : value false
;

LF step : term → term → type =
| e_if_true : step (if_then_else true M2 M3) M2
| e_if_false : step (if_then_else false M2 M3) M3
| e_pred_zero : step (pred z) z
| e_pred_succ : value V -> step (pred (succ V)) V
| e_iszero_zero : step (iszero z) true
| e_iszero_succ : value V -> step (iszero (succ V)) false
| e_if_then_else : step M1 M1' -> step (if_then_else M1 M2 M3) (if_then_else M1' M2 M3)
| e_succ : step M N -> step (succ M) (succ N)
| e_pred : step M N -> step (pred M) (pred N)
| e_iszero : step M N -> step (iszero M) (iszero N)
;

LF tp : type =
| bool : tp
| nat : tp
;

LF hastype : term -> tp -> type =
| t_true : hastype true bool
| t_false : hastype false bool
| t_zero : hastype z nat
| t_if : hastype M1 bool -> hastype M2 T -> hastype M3 T -> hastype (if_then_else M1 M2 M3) T
| t_succ : hastype M nat -> hastype (succ M) nat
| t_pred : hastype M nat -> hastype (pred M) nat
| t_iszero : hastype M nat -> hastype (iszero M) bool
;

%: load nats_and_bools_tps.bel
%: prove tps
[|- hastype M T] -> [|- step M N] -> [|- hastype N T]
2
split x8
split x8

Namely, the second split x8 causes the problem.

[Ailrun]

Following is a beluga reproduction for this issue.

LF term : type =
| true : term
| false : term
| if_then_else : term -> term -> term -> term
| z : term
| succ : term -> term
| pred : term -> term
| iszero : term -> term
;

LF value : term -> type =
| v_z : value z
| v_succ : value V -> value (succ V)
| v_true : value true
| v_false : value false
;

LF step : term → term → type =
| e_if_true : step (if_then_else true M2 M3) M2
| e_if_false : step (if_then_else false M2 M3) M3
| e_pred_zero : step (pred z) z
| e_pred_succ : value V -> step (pred (succ V)) V
| e_iszero_zero : step (iszero z) true
| e_iszero_succ : value V -> step (iszero (succ V)) false
| e_if_then_else : step M1 M1' -> step (if_then_else M1 M2 M3) (if_then_else M1' M2 M3)
| e_succ : step M N -> step (succ M) (succ N)
| e_pred : step M N -> step (pred M) (pred N)
| e_iszero : step M N -> step (iszero M) (iszero N)
;

LF tp : type =
| bool : tp
| nat : tp
;

LF hastype : term -> tp -> type =
| t_true : hastype true bool
| t_false : hastype false bool
| t_zero : hastype z nat
| t_if : hastype M1 bool -> hastype M2 T -> hastype M3 T -> hastype (if_then_else M1 M2 M3) T
| t_succ : hastype M nat -> hastype (succ M) nat
| t_pred : hastype M nat -> hastype (pred M) nat
| t_iszero : hastype M nat -> hastype (iszero M) bool
;

rec tps : [|- hastype M A] -> [|- step M N] -> [|- hastype N A] =
/ total x (tps _ _ _ _ x) /
fn y => fn x =>
   case x of
   | [|- e_if_true ] =>
   case x of
       | [|- e_if_true ] => ?;

[Ailrun]

Following is a minimal beluga reproduction for this issue.

LF term : type =
| true : term
| if_then : term -> term -> term
;

LF step : term → term → type =
| e_if_true : step (if_then true M2) M2
| e_if_then : step M1 M1' -> step (if_then M1 M2) (if_then M1' M2)
;

rec tada : [|- step (if_then true M2) M2] -> [|- term] =
/ total x (tada _ x) /
fn x =>
case x of
  | [|- e_if_true ] => ?;

[tsani]

I discussed this issue with Brigitte last week and it genuinely seems to be a bug in unification. Some kind of occurs-check needs to take place to prevent this bad sequence of MMVar instantiations from occurring. There is no occurs-check implemented independently; occurrence-checking is implemented as part of pruning, which is a technique used to improve higher-order unification.

I tried to use unifyMMVarTerm (which should invoke pruning & hence the occurs-check) instead of instantiateMMVar at https://github.com/Beluga-lang/Beluga/blob/4d1f50004ce2a8e6ee261b50d6efebade1f6f541/src/core/unify.ml#L1921 but this does not resolve the issue.