This should evolve into a feature request, but for now I want to record some thoughts.
I wonder how feasible it is to work mostly-checkable-only, and have good type information pushed in more often. This would require giving the head of eliminations before their parameters: we already require this for case, so the change would be forcing users to specify which function to apply before talking about its arguments. This is thus related to #69, as there once the function is specified, we automatically create holes for its arguments.
This does make it hard to do "I know I need to build the result out of t, so let's write ? $ t, and search for things to fill the hole". I do this often in GHC, where I get good inference telling the type of the hole, and suggestions to fill it. Currently vonnegut does not do this - it has no inference. You could however write {? t ?} and then look at the required R and synth'd S types, and we could add an action to replace this with (? : S -> R) t, which would be just as good.
I don't know how annoying this sort of feature would be though! Perhaps it is not worth codifying, but just telling students that if they fill in the function before the arguments, they get better information from vonnegut?
This should evolve into a feature request, but for now I want to record some thoughts.
I wonder how feasible it is to work mostly-checkable-only, and have good type information pushed in more often. This would require giving the head of eliminations before their parameters: we already require this for case, so the change would be forcing users to specify which function to apply before talking about its arguments. This is thus related to #69, as there once the function is specified, we automatically create holes for its arguments.
This does make it hard to do "I know I need to build the result out of
t, so let's write? $ t, and search for things to fill the hole". I do this often in GHC, where I get good inference telling the type of the hole, and suggestions to fill it. Currently vonnegut does not do this - it has no inference. You could however write{? t ?}and then look at the requiredRand synth'dStypes, and we could add an action to replace this with(? : S -> R) t, which would be just as good.I don't know how annoying this sort of feature would be though! Perhaps it is not worth codifying, but just telling students that if they fill in the function before the arguments, they get better information from vonnegut?