Get GlobalHint flag right

'True' means a default hint, which is only used if all else fails (and
is only really intended to get default Integer)

libs/base/Control/WellFounded.idr

@@ -40,7 +40,7 @@ Smaller x y = size x `LT` size y
 
 SizeAccessible : Sized a => a -> Type
 SizeAccessible = Accessible Smaller
-    
+
 sizeAccessible : Sized a => (x : a) -> SizeAccessible x
 sizeAccessible x = Access (acc $ size x)
   where

src/Core/AutoSearch.idr

@@ -412,7 +412,9 @@ searchType {vars} fc rigc defaults depth def top env target
     tryGroups nty [] = throw (CantSolveGoal fc [] top)
     tryGroups nty (g :: gs)
         = handleUnify
-             (searchNames fc rigc defaults depth def top env g nty)
+             (do logC 5 (do gn <- traverse getFullName g
+                            pure ("Search: Trying names " ++ show gn))
+                 searchNames fc rigc defaults depth def top env g nty)
              (\err => if ambig err || isNil gs
                          then throw err
                          else tryGroups nty gs)
@@ -427,7 +429,8 @@ searchType {vars} fc rigc defaults depth def top env target
 Core.Unify.search fc rigc defaults depth def top_in env
     = do defs <- get Ctxt
          top <- normaliseScope defs env top_in
-         logTerm 10 "Initial target: " top
+         logTerm 2 "Initial target: " top
+         log 2 $ "Running search with defaults " ++ show defaults
          tm <- searchType fc rigc defaults depth def 
                           (abstractEnvType fc env top) env 
                           top

src/Core/Context.idr

@@ -945,9 +945,9 @@ getSearchData fc defaults target
                        Just hs => hs
                        Nothing => []
          if defaults
-            then let defaults = map fst (filter isDefault
+            then let defns = map fst (filter isDefault
                                              (toList (autoHints defs))) in
-                     pure (MkSearchData [] [defaults])
+                     pure (MkSearchData [] [defns])
             else let opens = map fst (toList (openHints defs))
                      autos = map fst (filter (not . isDefault) 
                                              (toList (autoHints defs)))

src/Core/Unify.idr

@@ -1013,25 +1013,30 @@ retryGuess mode smode (hid, (loc, hname))
            Just def =>
              case definition def of
                BySearch rig depth defining =>
-                 handleUnify
+                 case smode of
-                   (do tm <- search loc rig (smode == Defaults) depth defining
+                      LastChance =>
-                                    (type def) []
+                          do log 5 $ "Last chance at " ++ show hname
-                       let gdef = record { definition = PMDef [] (STerm tm) (STerm tm) [] } def
+                             search loc rig False depth defining (type def) []
-                       logTerm 5 ("Solved " ++ show hname) tm
+                             pure True
-                       addDef (Resolved hid) gdef
+                      _ => handleUnify
-                       removeGuess hid
+                             (do tm <- search loc rig (smode == Defaults) depth defining
-                       pure True)
+                                              (type def) []
-                   (\err => case err of
+                                 let gdef = record { definition = PMDef [] (STerm tm) (STerm tm) [] } def
-                              DeterminingArg _ n i _ _ => 
+                                 logTerm 5 ("Solved " ++ show hname) tm
-                                  do logTerm 5 ("Failed (det " ++ show hname ++ ")")
+                                 addDef (Resolved hid) gdef
-                                               (type def)
+                                 removeGuess hid
-                                     setInvertible loc i
+                                 pure True)
-                                     pure False -- progress made!
+                             (\err => case err of
-                              _ => do logTerm 5 ("Search failed for " ++ show hname) 
+                                        DeterminingArg _ n i _ _ => 
-                                                (type def)
+                                            do logTerm 5 ("Failed (det " ++ show hname ++ ")")
-                                      case smode of
+                                                         (type def)
-                                           LastChance => throw err
+                                               setInvertible loc i
-                                           _ => pure False) -- Postpone again
+                                               pure False -- progress made!
+                                        _ => do logTerm 5 ("Search failed for " ++ show hname) 
+                                                          (type def)
+                                                case smode of
+                                                     LastChance => throw err
+                                                     _ => pure False) -- Postpone again
                Guess tm constrs => 
                  do cs' <- traverse (retry mode) constrs
                     let csAll = unionAll cs'

src/Idris/Parser.idr

@@ -968,9 +968,9 @@ fnDirectOpt
     = do exactIdent "hint"
          pure (Hint True)
   <|> do exactIdent "globalhint"
-         pure (GlobalHint True)
-  <|> do exactIdent "defaulthint"
          pure (GlobalHint False)
+  <|> do exactIdent "defaulthint"
+         pure (GlobalHint True)
   <|> do exactIdent "inline"
          pure Inline
   <|> do exactIdent "extern"
@@ -1381,6 +1381,9 @@ command
   <|> do symbol ":"; keyword "total"
          n <- name
          pure (Total n)
+  <|> do symbol ":"; replCmd ["log", "logging"]
+         i <- intLit
+         pure (SetLog (fromInteger i))
   <|> do symbol ":"; cmd <- editCmd
          pure (Editing cmd)
   <|> do tm <- expr EqOK "(interactive)" init

src/Idris/REPL.idr

@@ -521,6 +521,10 @@ process (DebugInfo n)
 process (SetOpt opt)
     = do setOpt opt
          pure True
+process (SetLog lvl)
+    = do setLogLevel lvl
+         iputStrLn $ "Log level to set " ++ show lvl
+         pure True
 process (Editing cmd)
     = do ppopts <- getPPrint
          -- Since we're working in a local environment, don't do the usual

src/Idris/Syntax.idr

@@ -271,6 +271,7 @@ data REPLCmd : Type where
      CD : String -> REPLCmd
      Missing : Name -> REPLCmd
      Total : Name -> REPLCmd
+     SetLog : Nat -> REPLCmd
      Editing : EditCmd -> REPLCmd
      Quit : REPLCmd
 

src/TTImp/TTImp.idr

@@ -156,8 +156,7 @@ mutual
        -- Flag means the hint is a direct hint, not a function which might
        -- find the result (e.g. chasing parent interface dictionaries)
        Hint : Bool -> FnOpt
-       -- flag means always use this in search. If not set, it is only
+       -- Flag means to use as a default if all else fails
-       -- used as a hint if all else fails (i.e. a default)
        GlobalHint : Bool -> FnOpt
        ExternFn : FnOpt
        -- assume safe to cancel arguments in unification