Add heuristic for when to normalise metavars

If they're big, they take a long time to instantiate, and if they
consist of a lot of functions, chances are that normalising them will
make them much smaller. This significantly improves type checking
performance for some programs with lots of type level computation going
on.

The threshold is set with %nf_metavar_threshold, but the default value
of 50 is probably fine. Set it to 0 to always normalise metavar
solutions, or something higher than 1000 to essentially never do it.
It's roughly a count of nodes in the typechecked syntax tree under the
first function application.

Makefile

@@ -82,7 +82,7 @@ test-lib: contrib
 
 libs : prelude base contrib network test-lib
 
-testbin: test-lib install
+testbin: test-lib
 	@${MAKE} -C tests testbin IDRIS2=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
 
 test: testbin

src/Core/Context.idr

@@ -2210,6 +2210,13 @@ setAutoImplicitLimit max
     = do defs <- get Ctxt
          put Ctxt (record { options->elabDirectives->autoImplicitLimit = max } defs)
 
+export
+setNFThreshold : {auto c : Ref Ctxt Defs} ->
+                 Nat -> Core ()
+setNFThreshold max
+    = do defs <- get Ctxt
+         put Ctxt (record { options->elabDirectives->nfThreshold = max } defs)
+
 export
 isLazyActive : {auto c : Ref Ctxt Defs} ->
                Core Bool

src/Core/Options.idr

@@ -126,6 +126,7 @@ record ElabDirectives where
   totality : TotalReq
   ambigLimit : Nat
   autoImplicitLimit : Nat
+  nfThreshold : Nat
   --
   -- produce traditional (prefix) record projections,
   -- in addition to postfix (dot) projections
@@ -201,7 +202,7 @@ defaultSession = MkSessionOpts False False False Chez [] defaultLogLevel
 
 export
 defaultElab : ElabDirectives
-defaultElab = MkElabDirectives True True CoveringOnly 3 50 True
+defaultElab = MkElabDirectives True True CoveringOnly 3 50 50 True
 
 export
 defaults : Options

src/Core/Unify.idr

@@ -7,6 +7,7 @@ import Core.Core
 import Core.Env
 import Core.GetType
 import Core.Normalise
+import Core.Options
 import Core.TT
 import public Core.UnifyState
 import Core.Value
@@ -626,6 +627,31 @@ isDefInvertible fc i
               | Nothing => throw (UndefinedName fc (Resolved i))
          pure (invertible gdef)
 
+tooBig : (counting : Bool) -> Nat -> List (Term vars) -> Term vars -> Bool
+tooBig _ Z _ _ = True
+tooBig c k stk (App _ f a)
+    = tooBig c k (a :: stk) f
+tooBig c (S k) stk (Bind _ _ _ sc)
+    = tooBig c (S k) [] sc || any (tooBig c k []) stk
+tooBig c (S k) stk (Meta _ _ _ as)
+    = any (tooBig c k []) as || any (tooBig c k []) stk
+tooBig c (S k) stk f
+    = if c || isFn f -- start counting, we're under a function
+         then tooBigArgs True k stk
+         else tooBigArgs c (S k) stk
+  where
+    isFn : Term vs -> Bool
+    isFn (Ref _ Func _) = True
+    isFn _ = False -- Don't count if it's not a function, because normalising
+                   -- won't help
+
+    tooBigArgs : Bool -> Nat -> List (Term vars) -> Bool
+    tooBigArgs c Z _ = True
+    tooBigArgs c k [] = False
+    tooBigArgs c (S k) (a :: as)
+       = tooBig c (if c then k else S k) [] a || tooBigArgs c k as
+tooBig _ _ _ _ = False
+
 mutual
   unifyIfEq : {auto c : Ref Ctxt Defs} ->
               {auto u : Ref UST UState} ->
@@ -865,7 +891,12 @@ mutual
                          | _ => postponeS True swap loc mode "Delayed hole" env
                                           (NApp loc (NMeta mname mref margs) $ map (EmptyFC,) margs')
                                           tmnf
-                     tm <- quote empty env tmnf
+                     tmq <- quote empty env tmnf
+                     tm <- if tooBig False
+                                     defs.options.elabDirectives.nfThreshold
+                                     [] tmq
+                              then quote defs env tmnf
+                              else pure tmq
                      Just tm <- occursCheck loc env mode mname tm
                          | _ => postponeS True swap loc mode "Occurs check failed" env
                                           (NApp loc (NMeta mname mref margs) $ map (EmptyFC,) margs')
@@ -876,7 +907,7 @@ mutual
                                                 margs margs' locs submv
                                                 tm stm tmnf
                           Nothing =>
-                            do tm' <- normalise defs env tm
+                            do tm' <- quote defs env tmnf
                                case shrinkTerm tm' submv of
                                     Nothing => postponeS True swap loc mode "Can't shrink" env
                                                (NApp loc (NMeta mname mref margs) $ map (EmptyFC,) margs')

src/Idris/Desugar.idr

@@ -978,6 +978,7 @@ mutual
                pure [IPragma [] (\nest, env => setPrefixRecordProjections b)]
              AmbigDepth n => pure [IPragma [] (\nest, env => setAmbigLimit n)]
              AutoImplicitDepth n => pure [IPragma [] (\nest, env => setAutoImplicitLimit n)]
+             NFMetavarThreshold n => pure [IPragma [] (\nest, env => setNFThreshold n)]
              PairNames ty f s => pure [IPragma [] (\nest, env => setPair fc ty f s)]
              RewriteName eq rw => pure [IPragma [] (\nest, env => setRewrite fc eq rw)]
              PrimInteger n => pure [IPragma [] (\nest, env => setFromInteger n)]

src/Idris/Parser.idr

@@ -1058,6 +1058,10 @@ directive fname indents
          dpt <- intLit
          atEnd indents
          pure (AutoImplicitDepth (fromInteger dpt))
+  <|> do pragma "nf_metavar_threshold"
+         dpt <- intLit
+         atEnd indents
+         pure (NFMetavarThreshold (fromInteger dpt))
   <|> do pragma "pair"
          ty <- name
          f <- name

src/Idris/Syntax.idr

@@ -253,6 +253,7 @@ mutual
        DefaultTotality : TotalReq -> Directive
        PrefixRecordProjections : Bool -> Directive
        AutoImplicitDepth : Nat -> Directive
+       NFMetavarThreshold : Nat -> Directive
 
   public export
   data PField : Type where