Non-termination at inductive predicate

[leodemoura]

Example:

inductive Cover : (x y z : List α) -> Type u
  | done  : Cover [] [] []
  | left  : Cover x y z -> Cover (t :: x) y (t :: z)
  | right : Cover x y z -> Cover x (t :: y) (t :: z)
  | both  : Cover x y z -> Cover (t :: x) (t :: y) (t :: z)

inductive Linear : Cover x y z -> Prop
  | done : Linear .done
  | left : Linear c -> Linear (.left c)
  | right : Linear c -> Linear (.right c)

Reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Compiler.20stuck.20computing.20something.2E.2E.2E/near/299193185

[cppio]

I took a look at this and found that elaborating the inductive type hangs on this line:

lean4/src/Lean/Elab/Inductive.lean

Line 357 in 0b243f0

let extraCtorParams ← Term.collectUnassignedMVars (← instantiateMVars type) #[] except

I inserted logging into

lean4/src/Lean/Elab/Term.lean

Lines 1503 to 1526 in 0b243f0

	partial def collectUnassignedMVars (type : Expr) (init : Array Expr := #[]) (except : MVarId → Bool := fun _ => false)
	: TermElabM (Array Expr) := do
	let mvarIds ← getMVars type
	if mvarIds.isEmpty then
	return init
	else
	go mvarIds.toList init
	where
	go (mvarIds : List MVarId) (result : Array Expr) : TermElabM (Array Expr) := do
	match mvarIds with
	| [] => return result
	| mvarId :: mvarIds => do
	if (← mvarId.isAssigned) then
	go mvarIds result
	else if result.contains (mkMVar mvarId) || except mvarId then
	go mvarIds result
	else
	let mvarType := (← getMVarDecl mvarId).type
	let mvarIdsNew ← getMVars mvarType
	let mvarIdsNew := mvarIdsNew.filter fun mvarId => !result.contains (mkMVar mvarId)
	if mvarIdsNew.isEmpty then
	go mvarIds (result.push (mkMVar mvarId))
	else
	go (mvarIdsNew.toList ++ mvarId :: mvarIds) result

and found that go was being executed in an infinite loop:

go [_uniq.202, _uniq.203, _uniq.212] #[]
go [_uniq.203, _uniq.212] #[]
go [_uniq.212] #[]
go [_uniq.202, _uniq.212] #[]
go [_uniq.212] #[]
go [_uniq.202, _uniq.212] #[]
go [_uniq.212] #[]
go [_uniq.202, _uniq.212] #[]
go [_uniq.212] #[]
...

The fix I came up with filters out previously seen mvars to stop this case, though there may be a more efficient solution.

partial def collectUnassignedMVars (type : Expr) (init : Array Expr := #[]) (except : MVarId → Bool := fun _ => false)
    : TermElabM (Array Expr) := do
  let mvarIds ← getMVars type
  if mvarIds.isEmpty then
    return init
  else
    go mvarIds.toList init init
where
  go (mvarIds : List MVarId) (result visited : Array Expr) : TermElabM (Array Expr) := do
    match mvarIds with
    | [] => return result
    | mvarId :: mvarIds => do
      let visited := visited.push (mkMVar mvarId)
      if (← mvarId.isAssigned) then
        go mvarIds result visited
      else if result.contains (mkMVar mvarId) || except mvarId then
        go mvarIds result visited
      else
        let mvarType := (← getMVarDecl mvarId).type
        let mvarIdsNew ← getMVars mvarType
        let mvarIdsNew := mvarIdsNew.filter fun mvarId => !visited.contains (mkMVar mvarId)
        if mvarIdsNew.isEmpty then
          go mvarIds (result.push (mkMVar mvarId)) visited
        else
          go (mvarIdsNew.toList ++ mvarId :: mvarIds) result visited