Error when interpreting examples/reddit-haskell.ffg

[evanrelf]

Everything here was run from 4d32d09. I get this error when trying to run the Reddit r/haskell example:

λ grace interpret examples/reddit-haskell.ffg
Unbound fields variable: b

examples/reddit-haskell.ffg:6:23:
  │
6 │               { data: { children: List
  │                       ↑

---

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:

λ cat bad.ffg
let bad = { a: 42 } : exists (etc : Fields) . { a: Natural, etc }

in  bad.a

λ grace interpret bad.ffg
Unbound fields variable: etc

bad.ffg:1:47:
  │
1 │ let bad = { a: 42 } : exists (etc : Fields) . { a: Natural, etc }
  │                                                 ↑

When I stop trying to get the a field, and just get the whole thing back, it works:

 let bad = { a: 42 } : exists (etc : Fields) . { a: Natural, etc }

-in  bad.a
+in  bad

λ grace interpret bad.ffg
{ "a":
    42
}

[Gabriella439]

Yeah, this is a known issue. I'm working on fixing it by implementing the algorithm from the Existential Crisis Resolved paper

[Gabriella439]

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