Inline small metavariables

Where 'small' means they don't refer to other metavariables, except
right at the top level, and they don't go beyond a certain small depth,
arrived at by experimenting.

We already did a bit of this, but only for depth 0. The effect of this
is that we don't need to save out lots of metavariables, so ttc loading
is faster. This takes about 8s off the Idris build time!

src/Core/Binary.idr

@@ -1,5 +1,6 @@
 module Core.Binary
 
+import Core.CaseTree
 import Core.Context
 import Core.Context.Log
 import Core.Core

src/Core/Unify.idr

@@ -489,14 +489,28 @@ instantiate {newvars} loc mode env mname mref num mdef locs otm tm
                Hole _ p => precisetype p
                _ => False
 
+    -- A solution is deemed simple enough to inline if either:
+    --   * It is smaller than some threshold and has no metavariables in it
+    --   * It's just a metavariable itself
+    noMeta : Term vs -> Nat -> Bool
+    noMeta (App _ f a) (S k) = noMeta f k && noMeta a k
+    noMeta (Bind _ _ b sc) (S k) = noMeta (binderType b) k && noMeta sc k
+    noMeta (Meta _ _ _ _) d = False
+    noMeta (TDelayed _ _ t) d = noMeta t d
+    noMeta (TDelay _ _ t a) d = noMeta t d && noMeta a d
+    noMeta (TForce _ _ t) d = noMeta t d
+    noMeta (As _ _ a p) d = noMeta a d && noMeta p d
+    noMeta (Local _ _ _ _) _ = True
+    noMeta (Ref _ _ _) _ = True
+    noMeta (PrimVal _ _) _ = True
+    noMeta (TType _) _ = True
+    noMeta _ _ = False
+
     isSimple : Term vs -> Bool
-    isSimple (Local _ _ _ _) = True
-    isSimple (Ref _ _ _) = True
     isSimple (Meta _ _ _ _) = True
     isSimple (Bind _ _ (Lam _ _ _ _) sc) = isSimple sc
-    isSimple (PrimVal _ _) = True
-    isSimple (TType _) = True
-    isSimple _ = False
+    isSimple (App _ f a) = noMeta f 6 && noMeta a 3
+    isSimple tm = noMeta tm 0
 
     updateIVar : {v : Nat} ->
                  forall vs, newvars . IVars vs newvars -> (0 p : IsVar nm v newvars) ->

src/Idris/Main.idr

@@ -1,6 +1,7 @@
 module Idris.Main
 
 import Idris.Driver
+import Compiler.Common
 
 main : IO ()
 main = mainWithCodegens []

src/Libraries/Utils/Path.idr

@@ -1,6 +1,7 @@
 module Libraries.Utils.Path
 
 import Data.List
+import Data.List1
 import Data.Maybe
 import Data.Nat
 import Data.Strings

tests/idris2/basic044/expected

@@ -98,7 +98,7 @@ Term> Bye for now!
 LOG declare.type:1: Processing Vec.Vec
 LOG declare.def:2: Case tree for Vec.Vec: [0] ({arg:N} : (Data.Fin.Fin {arg:N}[1])) -> {arg:N}[1])
 LOG declare.type:1: Processing Vec.Nil
-LOG declare.def:2: Case tree for Vec.Nil: [0] (Prelude.Uninhabited.absurd {arg:N}[0] ?Vec.{t:N}_[{arg:N}[0]] Data.Fin.Uninhabited implementation at Data/Fin.idr:L:C--L:C)
+LOG declare.def:2: Case tree for Vec.Nil: [0] (Prelude.Uninhabited.absurd {arg:N}[0] (Data.Fin.Fin Prelude.Types.Z) Data.Fin.Uninhabited implementation at Data/Fin.idr:L:C--L:C)
 LOG declare.type:1: Processing Vec.::
 LOG declare.def:2: Case tree for Vec.::: case {arg:N}[4] : (Data.Fin.Fin (Prelude.Types.S {arg:N}[0])) of
  { Data.Fin.FZ {e:N} => [0] {arg:N}[3]
@@ -129,5 +129,5 @@ LOG elab.ambiguous:5: Ambiguous elaboration [($resolvedN 0), ($resolvedN 0)] at
 With default. Target type : Prelude.Types.Nat
 LOG elab.ambiguous:5: Ambiguous elaboration True [$resolvedN] at Vec.idr:L:C--L:C
 Target type : (Prelude.Basics.List Prelude.Types.Nat)
-LOG declare.def:2: Case tree for Vec.test: [0] (Vec.:: ?Vec.{n:N}_[] ?Vec.{a:N}_[] (Prelude.Basics.Nil Prelude.Types.Nat) (Vec.:: Prelude.Types.Z ?Vec.{a:N}_[] (Prelude.Basics.:: Prelude.Types.Nat Prelude.Types.Z (Prelude.Basics.Nil Prelude.Types.Nat)) (Vec.Nil ?Vec.{a:N}_[])))
+LOG declare.def:2: Case tree for Vec.test: [0] (Vec.:: (Prelude.Types.S Prelude.Types.Z) (Prelude.Basics.List Prelude.Types.Nat) (Prelude.Basics.Nil Prelude.Types.Nat) (Vec.:: Prelude.Types.Z (Prelude.Basics.List Prelude.Types.Nat) (Prelude.Basics.:: Prelude.Types.Nat Prelude.Types.Z (Prelude.Basics.Nil Prelude.Types.Nat)) (Vec.Nil (Prelude.Basics.List Prelude.Types.Nat))))
 Vec> Bye for now!