Fix order of metavariable substitution

Need to substitute the one applied to most things, or it won't want to
substitute at all. Fixes #226

src/Core/TT.idr

@@ -949,6 +949,39 @@ mutual
   shrinkTerm (Erased fc i) prf = Just (Erased fc i)
   shrinkTerm (TType fc) prf = Just (TType fc)
 
+varEmbedSub : SubVars small vars ->
+              {idx : Nat} -> .(IsVar n idx small) ->
+              Var vars
+varEmbedSub SubRefl y = MkVar y
+varEmbedSub (DropCons prf) y
+    = let MkVar y' = varEmbedSub prf y in
+          MkVar (Later y')
+varEmbedSub (KeepCons prf) First = MkVar First
+varEmbedSub (KeepCons prf) (Later p)
+    = let MkVar p' = varEmbedSub prf p in
+          MkVar (Later p')
+
+export
+embedSub : SubVars small vars -> Term small -> Term vars
+embedSub sub (Local fc x idx y)
+    = let MkVar y' = varEmbedSub sub y in Local fc x _ y'
+embedSub sub (Ref fc x name) = Ref fc x name
+embedSub sub (Meta fc x y xs)
+    = Meta fc x y (map (embedSub sub) xs)
+embedSub sub (Bind fc x b scope)
+    = Bind fc x (map (embedSub sub) b) (embedSub (KeepCons sub) scope)
+embedSub sub (App fc fn arg)
+    = App fc (embedSub sub fn) (embedSub sub arg)
+embedSub sub (As fc s nm pat)
+    = As fc s (embedSub sub nm) (embedSub sub pat)
+embedSub sub (TDelayed fc x y) = TDelayed fc x (embedSub sub y)
+embedSub sub (TDelay fc x t y)
+    = TDelay fc x (embedSub sub t) (embedSub sub y)
+embedSub sub (TForce fc r x) = TForce fc r (embedSub sub x)
+embedSub sub (PrimVal fc c) = PrimVal fc c
+embedSub sub (Erased fc i) = Erased fc i
+embedSub sub (TType fc) = TType fc
+
 namespace Bounds
   public export
   data Bounds : List Name -> Type where

src/Core/Unify.idr

@@ -773,7 +773,13 @@ mutual
                                           (yargs ++ yargs')
               else do xlocs <- localsIn xargs
                       ylocs <- localsIn yargs
-                      if (xlocs >= ylocs || mode == InMatch) && not (pv xn)
+                      -- Solve the one with the bigger context, and if they're
+                      -- equal, the one that's applied to fewest things (because
+                      -- then they arguments get substituted in)
+                      let xbigger = xlocs > ylocs
+                                      || (xlocs == ylocs &&
+                                           length xargs' <= length yargs')
+                      if (xbigger || mode == InMatch) && not (pv xn)
                         then unifyApp False mode loc env xfc (NMeta xn xi xargs) xargs'
                                             (NApp yfc (NMeta yn yi yargs) yargs')
                         else unifyApp True mode loc env yfc (NMeta yn yi yargs) yargs'

src/TTImp/Elab/ImplicitBind.idr

@@ -19,39 +19,6 @@ import Data.NameMap
 
 %default covering
 
-varEmbedSub : SubVars small vars ->
-              {idx : Nat} -> .(IsVar n idx small) ->
-              Var vars
-varEmbedSub SubRefl y = MkVar y
-varEmbedSub (DropCons prf) y
-    = let MkVar y' = varEmbedSub prf y in
-          MkVar (Later y')
-varEmbedSub (KeepCons prf) First = MkVar First
-varEmbedSub (KeepCons prf) (Later p)
-    = let MkVar p' = varEmbedSub prf p in
-          MkVar (Later p')
-
-mutual
-  embedSub : SubVars small vars -> Term small -> Term vars
-  embedSub sub (Local fc x idx y)
-      = let MkVar y' = varEmbedSub sub y in Local fc x _ y'
-  embedSub sub (Ref fc x name) = Ref fc x name
-  embedSub sub (Meta fc x y xs)
-      = Meta fc x y (map (embedSub sub) xs)
-  embedSub sub (Bind fc x b scope)
-      = Bind fc x (map (embedSub sub) b) (embedSub (KeepCons sub) scope)
-  embedSub sub (App fc fn arg)
-      = App fc (embedSub sub fn) (embedSub sub arg)
-  embedSub sub (As fc s nm pat)
-      = As fc s (embedSub sub nm) (embedSub sub pat)
-  embedSub sub (TDelayed fc x y) = TDelayed fc x (embedSub sub y)
-  embedSub sub (TDelay fc x t y)
-      = TDelay fc x (embedSub sub t) (embedSub sub y)
-  embedSub sub (TForce fc r x) = TForce fc r (embedSub sub x)
-  embedSub sub (PrimVal fc c) = PrimVal fc c
-  embedSub sub (Erased fc i) = Erased fc i
-  embedSub sub (TType fc) = TType fc
-
 -- Make a hole for an unbound implicit in the outer environment
 export
 mkOuterHole : {auto e : Ref EST (EState vars)} ->

tests/idris2/basic017/expected

@@ -1,6 +1,6 @@
 1/1: Building CaseInf (CaseInf.idr)
 CaseInf.idr:7:24--9:1:While processing right hand side of Main.test3bad at CaseInf.idr:6:1--9:1:
-While processing right hand side of Main.case block in 1153(179) at CaseInf.idr:7:14--9:1:
+While processing right hand side of Main.case block in 1160(179) at CaseInf.idr:7:14--9:1:
 When unifying Integer and Nat
 Mismatch between:
 	Integer