🐛🕳 Debug holes

[jonsterling]

Resolves #13

[jonsterling]

So what is very strange is that the "bug" I fixed in 61c28eb seems to not be detectable...

Consider the following example:

def _ : univ -> univ -> univ := ?

The correct output is:

Unleashed hole _.0 : VirPi (TpULvl,    
                            VirPi (Univ Var 0,
                                   VirPi (Univ Var 1, Univ Var 2))) 

I would expect that before fixing the bug, it would have incorrectly printed the following output, since the goal quotation would be happening in the environment containing only the ambient level variable:

Unleashed hole _.0 : VirPi (TpULvl,    
                            VirPi (Univ Var 0,
                                   VirPi (Univ Var 1, Univ Var 0))) 

But nonetheless, it behaved correctly. What is going on?

Edit: In fact, the behavior remains the same even when I remove all the with_top_env!

[mmcqd]

@jonsterling The behavior you're observing makes sense and is not a bug. First note that the two inner VirPis should be Pis, your printer just printed Pi as VirPi. In this example:

def _ : univ -> univ -> univ := ?

The goal is univ -> univ -> univ (not univ!) and the context contains only the blessed_ulvl. So quote_ctx gives the empty list, and with_top_env is actually a noop! The env is already the top_env. If you change the test to

def _ : univ -> univ -> univ = x => ?

Then the old code gives

Unleashed hole _.0 : VirPi (TpULvl,    
                            Pi (Univ Var 0, Pi (Univ Var 0, Univ Var 1))) 

Which is wrong in the way we would expect. The goal type is univ -> univ, which gets quoted in the top_env to

Pi (Univ Var 0, Univ Var 1)

With the new code, we get the correct result

Unleashed hole _.0 : VirPi (TpULvl,    
                            Pi (Univ Var 0, Pi (Univ Var 1, Univ Var 2))) 

This actually produces this error

Fatal error: exception Invalid_argument("result is Error _")

for unknown reasons lol, but it happens after the hole getting printed so it's not because of the aforementioned stuff.

[jonsterling]

oh wow, you are so right!

[favonia]

I rebased the PR.