Zilin Chen
Zilin Chen
Better error messages (and in general) is much appreciated, otherwise it will force me to be around when someone is using the language :P
Alternatively an easier workaround would be to have some type holes syntax, so that users can help the compiler know the instantiation of the outstanding typevars, without having to annotate...
What about things like `wordarray_get: all(a :< DSE). ((WordArray a)!, WordArrayIndex) -> a`? Is there a way to utilise kind system? This one gives leftover constraints, expectedly.
I got ``` Leftover constraint! U8 :< (?1)! Leftover constraint! (?1)! :< (?1)! Leftover constraint! Escape ?1 Leftover constraint! Drop ?1 Leftover constraint! Share ?1 ```
With/out the `[a]`s I get different errors.
If it's `w`, then `_|_`; `r` needs some guessing, I think.
With what we have now, typeargs are not in a situation that's much better than what we had before. Selectively removing/adding them is brain intensive. Doing a bit more keystrokes...
Do we have to know what `?0` is for well-typedness? Can we solve up to `(?0)!` (i.e. make it an atomic unif. var-ish thing) and substitute `(?0)!`, and in a...
Some real examples: in `rbt.cogent`, there're things like: ``` rbt_next: all (k :< DS, v :< DS). ((Rbt k v)!, k!) -> R k () type RbtConsumeF k v acc...
~~Need to check if the Isabelle side agrees with the compiler.~~