From 0ba1daf5eb4108e57edf8e7e09eb5fa5422815dc Mon Sep 17 00:00:00 2001 From: krasimir Date: Mon, 25 Oct 2010 15:47:33 +0000 Subject: when faced with hard unification problem the type checker should just postpone the decision instead of failing immediately. added test case as well --- testsuite/runtime/typecheck/Hard.gf | 14 ++++++++++++++ testsuite/runtime/typecheck/hard-unification.gfs | 3 +++ testsuite/runtime/typecheck/hard-unification.gfs.gold | 5 +++++ 3 files changed, 22 insertions(+) create mode 100644 testsuite/runtime/typecheck/Hard.gf create mode 100644 testsuite/runtime/typecheck/hard-unification.gfs create mode 100644 testsuite/runtime/typecheck/hard-unification.gfs.gold (limited to 'testsuite') 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 -- cgit v1.2.3