Only normalise a search goal if it's fast (#2109)

While we do end up normalising it anyway on success, there might be
things blocking it that make the intermediate terms very big, so only do
it speculatively to see if it's quick.

src/Core/Normalise.idr

@@ -83,8 +83,6 @@ normaliseLHS defs env (Bind fc n b sc)
 normaliseLHS defs env tm
     = quote defs env !(nfOpts onLHS defs env tm)
 
--- The size limit here is the depth of stuck applications. If it gets past
--- that size, return the original
 export
 tryNormaliseSizeLimit : {auto c : Ref Ctxt Defs} ->
                      {free : _} ->
@@ -94,6 +92,8 @@ tryNormaliseSizeLimit defs limit env tm
     = do tm' <- nf defs env tm
          quoteOpts (MkQuoteOpts False False (Just limit)) defs env tm'
 
+-- The size limit here is the depth of stuck applications. If it gets past
+-- that size, return the original
 export
 normaliseSizeLimit : {auto c : Ref Ctxt Defs} ->
                      {free : _} ->

src/TTImp/Elab/App.idr

@@ -212,9 +212,14 @@ mutual
                                 fntm fnty (n, 1 + argpos) expargs autoargs namedargs kr expty
            else do defs <- get Ctxt
                    nm <- genMVName x
-                   -- We need the full normal form to check determining arguments
-                   -- so we might as well calculate the whole thing now
-                   metaty <- quote defs env aty
+                   empty <- clearDefs defs
+                   -- Normalise fully, but only if it's cheap enough.
+                   -- We have to get the normal form eventually anyway, but
+                   -- it might be too early to do it now if something is
+                   -- blocking it and we're not yet ready to search.
+                   metaty <- catch (quoteOpts (MkQuoteOpts False False (Just 10))
+                                              defs env aty)
+                                   (\err => quote empty env aty)
                    est <- get EST
                    lim <- getAutoImplicitLimit
                    metaval <- searchVar fc argRig lim (Resolved (defining est))