Make note of unapplied unifiation solutions

i.e. when an argument is given explicitly, but can be solved by
unification, make sure that the given argument and the inferred argument
themselves unify. Keep track in the ProofState structure, and unify when
'solve' tactic is applied for the given hole.

Fixes #765

CHANGELOG

@@ -1,6 +1,8 @@
 New in 0.9.11:
 -------------
+
 * Agda-style equational reasoning (in Syntax.PreorderReasoning)
+* 'case' construct now abstracts over the scrutinee in its type
 
 New in 0.9.10:
 --------------

src/Idris/Core/ProofState.hs

@@ -184,24 +184,25 @@ unify' ctxt env topx topy =
                          " in " ++ show env ++
                          "\nHoles: " ++ show (holes ps) ++ "\n") $
                      lift $ unify ctxt env topx topy dont (holes ps)
+      let notu = filter (\ (n, t) -> case t of
+                                        P _ _ _ -> False
+                                        _ -> n `elem` dont) u
       traceWhen (unifylog ps)
             ("Unified " ++ show (topx, topy) ++ " without " ++ show dont ++
              "\nSolved: " ++ show u ++ "\nNew problems: " ++ qshow fails
              ++ "\nCurrent problems:\n" ++ qshow (problems ps)
 --              ++ show (pterm ps)
              ++ "\n----------") $
-       case fails of
---            [] -> return u
-           err ->
-               do ps <- get
-                  let (h, ns) = unified ps
-                  let (ns', probs') = updateProblems (context ps) (u ++ ns)
-                                                     (err ++ problems ps)
-                                                     (injective ps)
-                                                     (holes ps)
-                  put (ps { problems = probs',
-                            unified = (h, ns') })
-                  return u
+        do ps <- get
+           let (h, ns) = unified ps
+           let (ns', probs') = updateProblems (context ps) (u ++ ns)
+                                              (fails ++ problems ps)
+                                              (injective ps)
+                                              (holes ps)
+           put (ps { problems = probs',
+                     unified = (h, ns'),
+                     notunified = notu ++ notunified ps })
+           return u
 
 getName :: Monad m => String -> StateT TState m Name
 getName tag = do ps <- get

test/reg005/reg005.idr

@@ -48,3 +48,4 @@ Main.eqCharOK = proof {
   exact x = x;
 }
 
+