Resumption not taking type unification into account #88

New Issue

aniva · 2024-08-31T19:57:41-07:00

aniva commented

2024-08-31 19:57:41 -07:00

In aniva/Trillium#124, during atomization of

fun (a b: List Nat) => HAppend.hAppend a b

We got the trace

?0
⊢ Π a: @List @Nat, Π b: @List @Nat, @List @Nat
[#0] G[0]T"intro"→#2
?0
[0]a: @List @Nat
⊢ Π b: @List @Nat, @List @Nat
[#2] G[0]T"intro"→#4
?0
[0]a: @List @Nat
[1]b: @List @Nat
⊢ @List @Nat
[#4] G[0]T"apply @HAppend.hAppend"→#6
?0 α
[0]a: @List @Nat
[1]b: @List @Nat
⊢ Type
?1 β
[0]a: @List @Nat
[1]b: @List @Nat
⊢ Type
?2 self
[0]a: @List @Nat
[1]b: @List @Nat
⊢ @HAppend ?0 ?1 (@List @Nat)
?3 a._@.Init.Prelude._hyg.2577
[0]a: @List @Nat
[1]b: @List @Nat
⊢ ?0
?4 a._@.Init.Prelude._hyg.2579
[0]a: @List @Nat
[1]b: @List @Nat
⊢ ?1
[#6] G[3]T"exact [0]a"→#8 G[0]R0→#13 G[1]R1→#13 G[2]R2→#13 G[4]R3→#13
[#8] (dormant) C→#13
?0 α
[0]a: @List @Nat
[1]b: @List @Nat
⊢ Type
?1 β
[0]a: @List @Nat
[1]b: @List @Nat
⊢ Type
?2 self
[0]a: @List @Nat
[1]b: @List @Nat
⊢ @HAppend ?0 ?1 (@List @Nat)
?3 a._@.Init.Prelude._hyg.2579
[0]a: @List @Nat
[1]b: @List @Nat
⊢ ?1
[#13] G[2]T"apply @instHAppendOfAppend"→#15 G[0]R0→#19 G[1]R1→#19 G[3]R2→#19
[#15] (dormant) C→#19
?0 a._@.Init.Prelude._hyg.2579
[0]a: @List @Nat
[1]b: @List @Nat
⊢ @List @Nat
[#19] G[0]T"exact [1]b"→#21
[#21] (solved)

Note that after exact a, the resumed state still has ?0 α as a goal. This should definitely not happen. Is there any reason why α was not solved in passing?

In https://git.leni.sh/aniva/Trillium/pulls/124, during atomization of ```lean fun (a b: List Nat) => HAppend.hAppend a b ``` We got the trace ``` ?0 ⊢ Π a: @List @Nat, Π b: @List @Nat, @List @Nat [#0] G[0]T"intro"→#2 ?0 [0]a: @List @Nat ⊢ Π b: @List @Nat, @List @Nat [#2] G[0]T"intro"→#4 ?0 [0]a: @List @Nat [1]b: @List @Nat ⊢ @List @Nat [#4] G[0]T"apply @HAppend.hAppend"→#6 ?0 α [0]a: @List @Nat [1]b: @List @Nat ⊢ Type ?1 β [0]a: @List @Nat [1]b: @List @Nat ⊢ Type ?2 self [0]a: @List @Nat [1]b: @List @Nat ⊢ @HAppend ?0 ?1 (@List @Nat) ?3 a._@.Init.Prelude._hyg.2577 [0]a: @List @Nat [1]b: @List @Nat ⊢ ?0 ?4 a._@.Init.Prelude._hyg.2579 [0]a: @List @Nat [1]b: @List @Nat ⊢ ?1 [#6] G[3]T"exact [0]a"→#8 G[0]R0→#13 G[1]R1→#13 G[2]R2→#13 G[4]R3→#13 [#8] (dormant) C→#13 ?0 α [0]a: @List @Nat [1]b: @List @Nat ⊢ Type ?1 β [0]a: @List @Nat [1]b: @List @Nat ⊢ Type ?2 self [0]a: @List @Nat [1]b: @List @Nat ⊢ @HAppend ?0 ?1 (@List @Nat) ?3 a._@.Init.Prelude._hyg.2579 [0]a: @List @Nat [1]b: @List @Nat ⊢ ?1 [#13] G[2]T"apply @instHAppendOfAppend"→#15 G[0]R0→#19 G[1]R1→#19 G[3]R2→#19 [#15] (dormant) C→#19 ?0 a._@.Init.Prelude._hyg.2579 [0]a: @List @Nat [1]b: @List @Nat ⊢ @List @Nat [#19] G[0]T"exact [1]b"→#21 [#21] (solved) ``` Note that after `exact a`, the resumed state still has `?0 α` as a goal. This should definitely not happen. Is there any reason why `α` was not solved in passing?

aniva added this to the 0.3 milestone 2024-08-31 19:57:41 -07:00

aniva added the

labels 2024-08-31 19:57:41 -07:00

aniva self-assigned this 2024-08-31 19:57:41 -07:00

aniva changed title from ~~Resumption not taking into account type unification~~ to Resumption not taking type unification into account

2024-08-31 19:57:54 -07:00

aniva referenced this issue