Try the `elimBool` of the paper. about minitt-rs

[ice1000]

Does not check for me as well:

I'm investigating.

[ice1000]

I've found the problem. It's because when I'm generating a Val to instantiate the pi type's closure:

minitt-rs/src/check/expr.rs

Line 247 in 2dcae72

let generated = generate_value(index);

When generating an instance of One, we're still "generating" a variable (instead of using the only possible instance Unit).

Same problem also occurs in:

minitt-rs/src/check/expr.rs

Line 103 in 2dcae72

let generated = generate_value(index);

minitt-rs/src/check/expr.rs

Line 113 in 2dcae72

let generated = generate_value(index + 1);

[ice1000]

It checks in my implementation now:

minitt-rs/samples/sum-split/bool.minitt

Lines 21 to 31 in f35f6b6

	let elimBool
	: \Pi c : bool → Type
	. \Pi _ : c False
	. \Pi _ : c True
	. \Pi b : bool
	. c b
	= λ c . λ h0 . λ h1 . split
	{ True => h1
	| False => h0
	};

[xieyuheng]

Your fix is smart!

1. But why it is enough to only do it for Unit ?
2. Is it also right (or sound) to use unification to compare readbacked norm exps?

[ice1000]

But why it is enough to only do it for Unit ?

'cus in Mini-TT your Sum { True | False } are desugared to Sum { True 1 | False 1 }, note the 1.

[ice1000]

Is it also right (or sound) to use unification to compare readbacked norm exps?

It is, but not necessary. Theoretically, we're supposed to eject beta-normal eta-long normal forms. By eta-long I mean terms like (\ x -> x) : Record { label: Ty } -> Record { label: Ty } are translated to (\ { label } -> { label }), in case the record is empty it becomes \ {} -> {}. The readback function in Mini-TT is not aware of the eta-long property.