Commit Graph

6 Commits

Author SHA1 Message Date
Edwin Brady
85a9d5063c Update error messages in tests 2015-05-31 21:22:36 +01:00
Niklas Larsson
8cc2312715 Don't let tests depend on colouring. 2015-04-01 20:50:06 +02:00
Andreas Reuleaux
5de1cd81dc adjust tests with --consolewidth for use with -f curses 2015-03-19 16:50:50 +00:00
Edwin Brady
40f6534cf0 Better typecase check
Only allow matching on polymorphic arguments if they have been refined
to something concrete due to some other argument by the time they're
elaborated.
2014-12-22 11:22:42 +00:00
Edwin Brady
87897174e5 Hide other unmatchable patterns
Lambdas, in particular. Fixes #1671
2014-12-20 22:17:03 +00:00
Edwin Brady
0d8a153cb0 New way of dealing with unmatchable patterns
Any term which is not matchable, i.e. a function application or a
repeated variable on the left hand side, is automatically put in a
PHidden. The effect of elaborating PHidden t is to:

1. Delay the elaboration of 't' to the end of elaboration
2. When elaborating t, ensure that its value is already known due to
solving some other unification problem.

If something is PHidden, but not solvable by unification, elaboration
fails.
This finally fixes #323, and probably several other things.
2014-12-20 20:52:46 +00:00