Open evanrelf opened 2 years ago
Yeah, this is a known issue. I'm working on fixing it by implementing the algorithm from the Existential Crisis Resolved paper
It looks like that this also needs to be combined with A Quick Look at Impredicativity
Specifically, in Grace we need impredicative existential quantification such as List (exists (a : Fields) . { x: Bool, a })
. Fortunately, the "Existential Crisis Resolved" paper seems to explain how to integrate their work with the "A Quick Look at Impredicativity" paper
Everything here was run from 4d32d09260f7a77748cdb1647a0d82a630130c3e. I get this error when trying to run the Reddit r/haskell example:
I fiddled with this for quite a while, trying to narrow down what's going wrong. Here's a more minimal reproducing case which produces the same error:
When I stop trying to get the
a
field, and just get the whole thing back, it works: