Anders Mörtberg

> With `--experimental-lossy-unification` some unification variables will be solved even if they might have more than one correct solution, which means that you might have expected them to be solved...

> > Right, but what we noticed (especially when working on the Z-cohomology stuff) is that it's pretty much impossible to do anything without the `--experimental-lossy-unification` flag as Agda gets...

Very interesting! Can you redo the redtt experiment with iterated path types so that we can see if it's the extension types that are helping or not? An obvious difference...

> I do want to try that, but I cannot find any document for redtt. Do you know any? I don't think there is any detailed documentation yet. But the...

I think the conclusion of this experiment is that we need extension types in Cubical Agda. These are not only great from the point of view of efficiency; they should...

The problem is that our test whether a parameter is recursive or not is not smart enough. We evaluate the type of x and get `Join Bool Bool` and because...

No, but we are currently working on it. It is quite subtle and we want to find a solution without hacks, hopefully we can figure it out soon.

I don't think so...

Very strange. It is working for me. I suspect that you have an old version of BNFC: http://hackage.haskell.org/package/BNFC We are using this tool to generate the parser. I have version...

Thanks for testing and reporting the bug! The following code works: ``` foo : S1 -> Unit = split base -> tt loop @ _ -> tt c2t' : S1...