when faced with hard unification problem the type checker should just postpone the decision instead of failing immediately. added test case as well

4 files changed, 33 insertions, 14 deletions

diff --git a/src/runtime/haskell/PGF/TypeCheck.hs b/src/runtime/haskell/PGF/TypeCheck.hs
index 6220c3585..d68e9cf40 100644
--- a/src/runtime/haskell/PGF/TypeCheck.hs
+++ b/src/runtime/haskell/PGF/TypeCheck.hs
@@ -184,7 +184,7 @@ addConstraint :: MetaId -> MetaId -> (Expr -> TcM s ()) -> TcM s ()
 addConstraint i j c = do
   mv   <- getMeta j
   case mv of
-    MUnbound s scope tty cs       -> addRef >> setMeta j (MUnbound s scope tty ((\e -> release >> c e) : cs))
+    MUnbound s scope tty cs     -> addRef >> setMeta j (MUnbound s scope tty ((\e -> release >> c e) : cs))
     MBound   e                  -> c e
     MGuarded e cs x | x == 0    -> c e
                     | otherwise -> addRef >> setMeta j (MGuarded e ((\e -> release >> c e) : cs) x)
@@ -477,15 +477,11 @@ eqValue fail suspend k v1 v2 = do
     eqValue' k (VMeta i env1 vs1)             (VMeta j env2 vs2) | i  == j   = zipWithM_ (eqValue fail suspend k) vs1 vs2
     eqValue' k (VMeta i env1 vs1)             v2                             = do mv <- getMeta i
                                                                                   case mv of
-                                                                                    MUnbound _ scopei _ cs -> do e2 <- mkLam i scopei env1 vs1 v2
-                                                                                                                 setMeta i (MBound e2)
-                                                                                                                 sequence_ [c e2 | c <- cs]
+                                                                                    MUnbound _ scopei _ cs -> bind i scopei cs env1 vs1 v2
                                                                                     MGuarded e cs x        -> setMeta i (MGuarded e ((\e -> apply env1 e vs1 >>= \v1 -> eqValue' k v1 v2) : cs) x)
     eqValue' k v1                             (VMeta i env2 vs2)             = do mv <- getMeta i
                                                                                   case mv of
-                                                                                    MUnbound _ scopei _ cs -> do e1 <- mkLam i scopei env2 vs2 v1
-                                                                                                                 setMeta i (MBound e1)
-                                                                                                                 sequence_ [c e1 | c <- cs]
+                                                                                    MUnbound _ scopei _ cs -> bind i scopei cs env2 vs2 v1
                                                                                     MGuarded e cs x        -> setMeta i (MGuarded e ((\e -> apply env2 e vs2 >>= \v2 -> eqValue' k v1 v2) : cs) x)
     eqValue' k (VApp f1 vs1)                  (VApp f2 vs2)   | f1 == f2     = zipWithM_ (eqValue fail suspend k) vs1 vs2
     eqValue' k (VConst f1 vs1)                (VConst f2 vs2) | f1 == f2     = zipWithM_ (eqValue fail suspend k) vs1 vs2
@@ -495,16 +491,17 @@ eqValue fail suspend k v1 v2 = do
                                                                                in eqExpr fail suspend (k+1) (v:env1) e1 (v:env2) e2
     eqValue' k v1                             v2                             = fail
 
-    mkLam i scope env vs0 v = do
+    bind i scope cs env vs0 v = do
       let k  = scopeSize scope
           vs  = reverse (take k env) ++ vs0
           xs  = nub [i | VGen i [] <- vs]
-      if length vs == length xs
-        then return ()
-        else fail
-      v <- occurCheck i k xs v
-      e <- value2expr (length xs) v
-      return (addLam vs0 e)
+      if length vs /= length xs
+        then suspend i (\e -> apply env e vs0 >>= \iv -> eqValue fail suspend k iv v)
+        else do v <- occurCheck i k xs v
+                e0 <- value2expr (length xs) v
+                let e = addLam vs0 e0
+                setMeta i (MBound e)
+                sequence_ [c e | c <- cs]
       where
         addLam []     e = e
         addLam (v:vs) e = EAbs Explicit var (addLam vs e)
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