Use 'unify' rather than 'convert' if possible

'convert' doesn't solve holes, so might reject things that are solvable.
This can be an issue when resolving interfaces, because we were using
convert for arguments of the invertible holes that arise when trying to
resolve them. Fixes #66.

Author: edwinb

src/Core/Unify.idr

@@ -668,18 +668,22 @@ mutual
 
   headsConvert : {vars : _} ->
                  {auto c : Ref Ctxt Defs} ->
-                 Env Term vars ->
+                 {auto u : Ref UST UState} ->
+                 UnifyInfo ->
+                 FC -> Env Term vars ->
                  Maybe (List (NF vars)) -> Maybe (List (NF vars)) ->
                  Core Bool
-  headsConvert env (Just vs) (Just ns)
+  headsConvert mode fc env (Just vs) (Just ns)
       = case (reverse vs, reverse ns) of
              (v :: _, n :: _) =>
-                do logNF 10 "Converting" env v
-                   logNF 10 "......with" env n
-                   defs <- get Ctxt
-                   convert defs env v n
+                do logNF 10 "Unifying head" env v
+                   logNF 10 ".........with" env n
+                   res <- unify mode fc env v n
+                   -- If there's constraints, we postpone the whole equation
+                   -- so no need to record them
+                   pure (isNil (constraints res ))
              _ => pure False
-  headsConvert env _ _
+  headsConvert mode fc env _ _
       = do log 10 "Nothing to convert"
            pure True
 
@@ -707,7 +711,7 @@ mutual
                             nty
            -- If the rightmost arguments have the same type, or we don't
            -- know the types of the arguments, we'll get on with it.
-           if !(headsConvert env vargTys nargTys)
+           if !(headsConvert mode fc env vargTys nargTys)
               then
                 -- Unify the rightmost arguments, with the goal of turning the
                 -- hole application into a pattern form
@@ -1436,7 +1440,7 @@ retryGuess mode smode (hid, (loc, hname))
                                     do logTerm 5 ("Failed (det " ++ show hname ++ " " ++ show n ++ ")")
                                                  (type def)
                                        setInvertible loc (Resolved i)
-                                       pure False -- progress made!
+                                       pure False -- progress not made yet!
                                 _ => do logTermNF 5 ("Search failed at " ++ show rig ++ " for " ++ show hname)
                                                   [] (type def)
                                         case smode of

tests/Main.idr

@@ -97,7 +97,7 @@ idrisTests
        "reg001", "reg002", "reg003", "reg004", "reg005", "reg006", "reg007",
        "reg008", "reg009", "reg010", "reg011", "reg012", "reg013", "reg014",
        "reg015", "reg016", "reg017", "reg018", "reg019", "reg020", "reg021",
-       "reg022", "reg023", "reg024", "reg025", "reg026", "reg027",
+       "reg022", "reg023", "reg024", "reg025", "reg026", "reg027", "reg028",
        -- Totality checking
        "total001", "total002", "total003", "total004", "total005",
        "total006", "total007", "total008",