Closed dougalm closed 1 year ago
This almost works, but it fails at unpacking top-level data constructors that hide existentials, like this:
(MkImage rows cols img_camera_rgb) = ...
I tried a different approach to top-level pattern matching based on explicitly turning [a,b,c]
into (a, b, c)
and similar, rather than using the generic telecscope: https://github.com/google-research/dex-lang/tree/alternative-top-level-pattern-matching. But that didn't work either. The problem there is that it's hard to construct the correct dependent pair type to represent an ADT when you're modifying both the rhs and lhs of the pair. Also, the pattern-matching code for records is ridiculously complicated. I'm tempted to get rid of records altogether...
Anyway, since the original error has to do with Nat/IdxRepTy confusion, there's a chance that it fixes itself when we apply the newtype stripping patch on top. So I'll try that next.
Since we moved to codegen-based printing the only remaining use of the interpreter is during inference. There, we use use it for (1) top-level pattern-matching and (2) to figure out the size of non-Fin table literals. We can handle (1) by codegen and a telescope. And (2) is a lot of complexity for a small feature, especially one that was always going to be incomplete anyway. Instead we can just use
coerce_table
which does a runtime check on the size.