diff options
| author | krasimir <krasimir@chalmers.se> | 2010-10-25 15:47:33 +0000 |
|---|---|---|
| committer | krasimir <krasimir@chalmers.se> | 2010-10-25 15:47:33 +0000 |
| commit | 0ba1daf5eb4108e57edf8e7e09eb5fa5422815dc (patch) | |
| tree | 02c0ed4b19532d5e48888630b28e516b8e89f18d /testsuite/runtime | |
| parent | aa6b07afdb53461ba2f6b8596b3f6eb1e246961b (diff) | |
when faced with hard unification problem the type checker should just postpone the decision instead of failing immediately. added test case as well
Diffstat (limited to 'testsuite/runtime')
| -rw-r--r-- | testsuite/runtime/typecheck/Hard.gf | 14 | ||||
| -rw-r--r-- | testsuite/runtime/typecheck/hard-unification.gfs | 3 | ||||
| -rw-r--r-- | testsuite/runtime/typecheck/hard-unification.gfs.gold | 5 |
3 files changed, 22 insertions, 0 deletions
diff --git a/testsuite/runtime/typecheck/Hard.gf b/testsuite/runtime/typecheck/Hard.gf new file mode 100644 index 000000000..dea18d456 --- /dev/null +++ b/testsuite/runtime/typecheck/Hard.gf @@ -0,0 +1,14 @@ +abstract Hard = { + +cat I ; + F (I -> I) ; + A (I -> I) I ; + S ; + +fun + app : (f : I -> I) -> A f (f i) ; + ex : F (\x -> x) ; + i : I ; + s : (f : I -> I) -> A f i -> F f -> S ; + +} diff --git a/testsuite/runtime/typecheck/hard-unification.gfs b/testsuite/runtime/typecheck/hard-unification.gfs new file mode 100644 index 000000000..512163c0f --- /dev/null +++ b/testsuite/runtime/typecheck/hard-unification.gfs @@ -0,0 +1,3 @@ +i testsuite/runtime/typecheck/Hard.gf +ai s ? (app ?) ex +ai s ? (app ?) ? diff --git a/testsuite/runtime/typecheck/hard-unification.gfs.gold b/testsuite/runtime/typecheck/hard-unification.gfs.gold new file mode 100644 index 000000000..c83c4f620 --- /dev/null +++ b/testsuite/runtime/typecheck/hard-unification.gfs.gold @@ -0,0 +1,5 @@ +Expression: s (\v0 -> v0) (app (\v0 -> v0)) ex
+Type: S
+
+Meta variable(s) ?2 should be resolved
+in the expression: s ?2 (app ?2) ?4
|