Zilin Chen
Zilin Chen
Solution: apply typeargs manually. Improvements: - [x] type holes - [x] type annotations on expressions - [ ] error messages
One thing weird is that is requires me to supply type arguments of `error` function in all invocations in all branches, which I thought one should be enough.
Btw, most (>90%) of the unif vars are introduced in the solver.
For the file I just committed, if I leave out the typearg on the line with a comment, it fails to infer; but for some other branches, good to do...
~~performance is ok.~~ 9s to typecheck BilbyFs (the old one 4.5s). just quite difficult to track them.
Even better, for things that we know, we can suggest possible fixes.
also refer to c7cfe9c
also see 00bbf5a59b8
same for variant types -- can take an alternative more than once. (i.e. overlapping constructor incorrectly allowed)
In the solver, when we `whnf` a type, we never check if this put/take operation is allowed or not. See [here](https://github.com/NICTA/cogent/blob/tc-new-rebase/cogent/src/Cogent/TypeCheck/Solver.hs#L110) and [here](https://github.com/NICTA/cogent/blob/tc-new-rebase/cogent/src/Cogent/TypeCheck/Solver.hs#L120). I think to fix this, we can...