Crash while compiling creation of infinite type

[s15n]

type Inf = recursive either { .next self }

type U = recursive either { .u! }
def u: U = .u!

def inf: Inf = u unfounded begin {
  .u! => .next u loop
}

crashes the playground when trying to compile.

[NoamDev]

this happens because compilation also pre-evaluates code. This code can't terminate.
I wonder what behavior are you expecting. If you want an infinite generator, you likely want iterative, recursive is for finite things.

[NoamDev]

It's probably better to display a "stack overflow" or something, instead of crashing.

[s15n]

The compiler shouldn't crash. For this code, it should even typecheck

[NoamDev]

In modern syntax:

type Inf = recursive either { .next self }

type U = recursive either { .u! }
def U: U = .u!

def Inf: Inf = 
  U.unfounded.case {
    .u! => .next U.loop
  }

[NoamDev]

@s15n The type checking succeeds. The compilation to icombs, and the attempt to pre-reduce it is what seems to fail.

[NoamDev]

Or rather, get stuck in an infinite loop

[notJoon]

It looks like an issue where the unfounded type creates a circular reference to itself, causing an infinite loop during type expansion.

The problematic code has this flow:

• Type expansion is attemped with U.unfolded
• .next U.loop -> references U again
• and reference U again

In most case, totality checking using LoopId prevents infinite loops, but in the case of unfounded, no LoopId is generated.

par-lang/src/par/types/checking.rs

Lines 340 to 343 in 2e6049e

	if !*unfounded {
	let loop_id = LoopId::new();
	typ_asc.insert(loop_id);
	}

and I think this likely cause this issue.

It could be resolved by either detecting self-references in unfounded types or by setting a limit on the depth of type extension.

[NoamDev]

@notJoon I really doubt this is an issue in the type checking part. I rather believe it happens during compilation to icombs. And that the issue is infinite expansion of the package there because we always try to pre-reduce during compilation as much as possible.

Have you debugged and verified it gets stuck during type checking?

[NoamDev]

In particular, there is no circular reference in the type here. And the type system already checks for circular references in types, it is not allowed.

You may be confused by the fact the same names are used for definitions and types here.