Auto implicit search fix

Can't use a local which has 'erased' as its type, since that's just been
substituted in while working out how many arguments a local function
needs to have. Also need to ensure we've searched for default hints when
encountering IBindImplicits rather than after because otherwise it might
find the wrong instance.

Both these problems result it terms which don't type check getting past
the elaborator! So, also added a --debug-elab-check flag to check the
result of elaboration. It's not on by default because there are cases
where it really hurts performance, typically when inferring implicits
with lots of sharing. So we'll keep it as a debug flag, for now at
least.

src/Core/AutoSearch.idr

@@ -199,6 +199,7 @@ usableLocal loc defaults env (NBind fc x (Pi _ _ _) sc)
     = do defs <- get Ctxt
          usableLocal loc defaults env 
                 !(sc defs (toClosure defaultOpts env (Erased fc)))
+usableLocal loc defaults env (NErased _) = pure False
 usableLocal loc _ _ _ = pure True
 
 searchLocalWith : {auto c : Ref Ctxt Defs} ->
@@ -514,6 +515,6 @@ Core.Unify.search fc rigc defaults depth def top env
          tm <- searchType fc rigc defaults [] depth def 
                           True (abstractEnvType fc env top) env 
                           top
-         logTerm 2 "Result" tm
+         logTermNF 2 "Result" env tm
          defs <- get Ctxt
          pure tm

src/Core/Context.idr

@@ -1811,6 +1811,13 @@ setLogTimings b
     = do defs <- get Ctxt
          put Ctxt (record { options->session->logTimings = b } defs)
 
+export
+setDebugElabCheck : {auto c : Ref Ctxt Defs} ->
+                    Bool -> Core ()
+setDebugElabCheck b
+    = do defs <- get Ctxt
+         put Ctxt (record { options->session->debugElabCheck = b } defs)
+
 export
 getSession : {auto c : Ref Ctxt Defs} ->
              Core Session

src/Core/LinearCheck.idr

@@ -279,11 +279,13 @@ mutual
                       -- it makes the check very slow (id id id id ... id id etc
                       -- for example) and there may be similar realistic cases.
                       -- If elaboration is correct, this should never fail!
---                       aty <- getNF gaty
---                       when (not !(convert defs env aty ty)) $
---                          do ty' <- quote defs env ty
---                             aty' <- quote defs env aty
---                             throw (CantConvert fc env ty' aty') 
+                      opts <- getSession
+                      when (debugElabCheck opts) $ do
+                        aty <- getNF gaty
+                        when (not !(convert defs env aty ty)) $
+                           do ty' <- quote defs env ty
+                              aty' <- quote defs env aty
+                              throw (CantConvert fc env ty' aty') 
                       pure (App fc f' aerased, 
                             glueBack defs env sc', 
                             fused ++ aused)

src/Core/Options.idr

@@ -87,6 +87,7 @@ record Session where
   codegen : CG
   logLevel : Nat
   logTimings : Bool
+  debugElabCheck : Bool -- do conversion check to verify results of elaborator
 
 public export
 record PPrinter where
@@ -114,7 +115,7 @@ defaultPPrint : PPrinter
 defaultPPrint = MkPPOpts False True False
 
 defaultSession : Session
-defaultSession = MkSessionOpts False False Chez 0 False
+defaultSession = MkSessionOpts False False Chez 0 False False
 
 defaultElab : ElabDirectives
 defaultElab = MkElabDirectives True True

src/Idris/CommandLine.idr

@@ -68,6 +68,7 @@ data CLOpt
    ||| Run as a checker for the core language TTImp
   Yaffle String |
   Timing |
+  DebugElabCheck |
   BlodwenPaths
 
 
@@ -126,17 +127,21 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly]
               (Just "Display version string"),
            MkOpt ["--help", "-h", "-?"] [] [Help]
               (Just "Display help text"),
-           MkOpt ["--yaffle", "--ttimp"] ["ttimp file"] (\f => [Yaffle f])
-              Nothing,
            MkOpt ["--timing"] [] [Timing]
-              (Just "Display timing logs")
+              (Just "Display timing logs"),
+
+           -- Internal debugging options
+           MkOpt ["--yaffle", "--ttimp"] ["ttimp file"] (\f => [Yaffle f])
+              Nothing, -- run ttimp REPL rather than full Idris
+           MkOpt ["--debug-elab-check"] [] [DebugElabCheck]
+              Nothing -- do more elaborator checks (currently conversion in LinearCheck)
            ]
 
 optUsage : OptDesc -> String
 optUsage d
     = maybe "" -- Don't show anything if there's no help string (that means
                -- it's an internal option)
-        (\h =>
+        (\h => "  " ++
             let optshow = showSep "," (flags d) ++ " " ++
                     showSep " " (map (\x => "<" ++ x ++ ">") (argdescs d)) in
                 optshow ++ pack (List.replicate (minus 26 (length optshow)) ' ')
@@ -156,7 +161,7 @@ usage : String
 usage = versionMsg ++ "\n" ++
         "Usage: idris2 [options] [input file]\n\n" ++
         "Available options:\n" ++
-        concatMap (\u => "  " ++ optUsage u) options
+        concatMap optUsage options
 
 processArgs : String -> (args : List String) -> List String -> ActType args ->
               Either String (List CLOpt, List String)

src/Idris/SetOptions.idr

@@ -63,6 +63,9 @@ preOptions (Directory d :: opts)
 preOptions (Timing :: opts)
     = do setLogTimings True
          preOptions opts
+preOptions (DebugElabCheck :: opts)
+    = do setDebugElabCheck True
+         preOptions opts
 preOptions (_ :: opts) = preOptions opts
 
 -- Options to be processed after type checking. Returns whether execution

src/TTImp/Elab/ImplicitBind.idr

@@ -500,6 +500,9 @@ checkBindHere rig elabinfo nest env fc bindmode tm exp
          solveConstraints (case elabMode elabinfo of
                                 InLHS c => InLHS
                                 _ => InTerm) Normal
+         solveConstraints (case elabMode elabinfo of
+                                InLHS c => InLHS
+                                _ => InTerm) Defaults
          ust <- get UST
          catch (retryDelayed (delayedElab ust))
                (\err =>

tests/idris2/basic017/CaseInf.idr

@@ -1,5 +1,5 @@
 test3ok : Nat
-test3ok = case (the Nat 1, 2) of
+test3ok = case (the Nat 1, the Nat 2) of
                (x, y) => x + y
 
 test3bad : Nat

tests/idris2/interactive009/expected

@@ -5,14 +5,14 @@ Main>               (True @@ d) => ?now_4
               (False @@ d) => ?now_5
 
 Main>  0 m : Type -> Type
- 1 d : Door Open
    x : Integer
+ 1 d : Door Open
  0 r : Res Bool (\r => (Door (if r then Open else Closed)))
 -------------------------------------
 now_2 : Use Many m ()
 Main>  0 m : Type -> Type
- 1 d : Door Closed
    x : Integer
+ 1 d : Door Closed
  0 r : Res Bool (\r => (Door (if r then Open else Closed)))
 -------------------------------------
 now_3 : Use Many m ()

tests/idris2/interface007/run

@@ -1,3 +1,3 @@
-$1 --check A.idr
+$1 --debug-elab-check --check A.idr
 
 rm -rf build