[ fix ] Fix search around %defaulthints (#3258)

* [ cleanup ] Move repeating trying-with-unambiguity pattern to a function

* [ fix #2850 ] Search for dependencies for default hints among all hints

* [ fix #2932 ] Always try defaults in dependencies search

src/Core/AutoSearch.idr

@@ -17,6 +17,27 @@ import Libraries.Data.WithDefault
 
 %default covering
 
+tryUnifyUnambig' : {auto c : Ref Ctxt Defs} ->
+                   {auto u : Ref UST UState} ->
+                   {default False preferLeftError : Bool} ->
+                   Core a -> (Error -> Core a) -> Core a
+tryUnifyUnambig' left right = handleUnify left $ \case
+  e@(AmbiguousSearch {}) => throw e
+  e                      => if preferLeftError
+                              then tryUnify (right e) (throw e)
+                              else right e
+
+tryUnifyUnambig : {auto c : Ref Ctxt Defs} ->
+                  {auto u : Ref UST UState} ->
+                  {default False preferLeftError : Bool} ->
+                  Core a -> Core a -> Core a
+tryUnifyUnambig left right = tryUnifyUnambig' {preferLeftError} left $ const right
+
+tryNoDefaultsFirst : {auto c : Ref Ctxt Defs} ->
+                     {auto u : Ref UST UState} ->
+                     (Bool -> Core a) -> Core a
+tryNoDefaultsFirst f = tryUnifyUnambig {preferLeftError=True} (f False) (f True)
+
 SearchEnv : List Name -> Type
 SearchEnv vars = List (NF vars, Closure vars)
 
@@ -251,10 +272,6 @@ searchLocalWith {vars} fc rigc defaults trying depth def top env (prf, ty) targe
          nty <- nf defs env ty
          findPos defs prf id nty target
   where
-    ambig : Error -> Bool
-    ambig (AmbiguousSearch _ _ _ _) = True
-    ambig _ = False
-
     clearEnvType : {idx : Nat} -> (0 p : IsVar nm idx vs) ->
                    FC -> Env Term vs -> Env Term vs
     clearEnvType First fc (b :: env)
@@ -301,8 +318,7 @@ searchLocalWith {vars} fc rigc defaults trying depth def top env (prf, ty) targe
               (target : NF vars) ->
               Core (Term vars)
     findPos defs p f nty@(NTCon pfc pn _ _ [(_, xty), (_, yty)]) target
-        = handleUnify (findDirect defs prf f nty target) (\e =>
-           if ambig e then throw e else
+        = tryUnifyUnambig (findDirect defs prf f nty target) $
              do fname <- maybe (throw (CantSolveGoal fc (gamma defs) [] top Nothing))
                                pure
                                !fstName
@@ -328,7 +344,7 @@ searchLocalWith {vars} fc rigc defaults trying depth def top env (prf, ty) targe
                                                          ytytm,
                                                          f arg])
                                      ytynf target)]
-                   else throw (CantSolveGoal fc (gamma defs) [] top Nothing))
+                   else throw (CantSolveGoal fc (gamma defs) [] top Nothing)
     findPos defs p f nty target
         = findDirect defs p f nty target
 
@@ -536,35 +552,29 @@ searchType {vars} fc rigc defaults trying depth def checkdets top env target
                                                    (NTCon tfc tyn t a args)
                              if defaults && checkdets
                                 then tryGroups Nothing nty (hintGroups sd)
-                                else handleUnify
+                                else tryUnifyUnambig
                                        (searchLocalVars fc rigc defaults trying' depth def top env nty)
-                                       (\e => if ambig e
-                                                 then throw e
-                                                 else tryGroups Nothing nty (hintGroups sd))
+                                       (tryGroups Nothing nty (hintGroups sd))
                      else throw (CantSolveGoal fc (gamma defs) [] top Nothing)
               _ => do logNF "auto" 10 "Next target: " env nty
                       searchLocalVars fc rigc defaults trying' depth def top env nty
   where
-    ambig : Error -> Bool
-    ambig (AmbiguousSearch _ _ _ _) = True
-    ambig _ = False
-
     -- Take the earliest error message (that's when we look inside pairs,
     -- typically, and it's best to be more precise)
     tryGroups : Maybe Error ->
                 NF vars -> List (Bool, List Name) -> Core (Term vars)
     tryGroups (Just err) nty [] = throw err
     tryGroups Nothing nty [] = throw (CantSolveGoal fc (gamma !(get Ctxt)) [] top Nothing)
     tryGroups merr nty ((ambigok, g) :: gs)
-        = handleUnify
+        = tryUnifyUnambig'
              (do logC "auto" 5
                         (do gn <- traverse getFullName g
                             pure ("Search: Trying " ++ show (length gn) ++
                                            " names " ++ show gn))
                  logNF "auto" 5 "For target" env nty
-                 searchNames fc rigc defaults (target :: trying) depth def top env ambigok g nty)
-             (\err => if ambig err then throw err
-                         else tryGroups (Just $ fromMaybe err merr) nty gs)
+                 tryNoDefaultsFirst $ \d =>
+                   searchNames fc rigc d (target :: trying) depth def top env ambigok g nty)
+             (\err => tryGroups (Just $ fromMaybe err merr) nty gs)
 
 -- Declared in Core.Unify as:
 -- search : {vars : _} ->

tests/idris2/interface/interface031/DefaulthintWithDep.idr

@@ -0,0 +1,67 @@
+interface X where
+  x : Nat
+
+f : X => Nat
+f = x + 1
+
+namespace NoHintArg
+
+  %defaulthint
+  DefaultX : X
+  DefaultX = D where
+    [D] X where x = 5
+
+  fDef : Nat
+  fDef = f
+
+namespace WithDefaultHintArg
+
+  interface Y' where
+    y : Nat
+
+  [YY] Y' where
+    y = 6
+
+  %defaulthint
+  YY' : Y'
+  YY' = YY
+
+  %defaulthint
+  DefaultX : Y' => X
+  DefaultX = D where
+    [D] X where x = 5
+
+  fDef : Nat
+  fDef = f
+
+namespace JustHint
+
+  interface Y'' where
+    y : Nat
+
+  Y'' where
+    y = 6
+
+  %hint
+  DefaultX : Y'' => X
+  DefaultX = D where
+    [D] X where x = 5
+
+  fDef : Nat
+  fDef = f
+
+namespace WithHintArg
+
+  interface Y''' where
+    y : Nat
+
+  Y''' where
+    y = 6
+
+  %defaulthint
+  DefaultX : Y''' => X
+  DefaultX = D where
+    [D] X where x = 5
+
+  fDef : Nat
+  fDef = f

tests/idris2/interface/interface031/expected

@@ -0,0 +1 @@
+1/1: Building DefaulthintWithDep (DefaulthintWithDep.idr)

tests/idris2/interface/interface031/run

@@ -0,0 +1,3 @@
+. ../../../testutils.sh
+
+check DefaulthintWithDep.idr

tests/idris2/interface/interface032/DefaulthintInterfaceBug.idr

@@ -0,0 +1,42 @@
+namespace Data
+
+  interface X where
+    x : Nat
+
+  data Y : Type where
+    MkY : Nat -> Y
+
+  Y => X where
+    x @{MkY y} = y
+
+  %defaulthint
+  DefY : Y
+  DefY = MkY 6
+
+  f : X => IO ()
+  f = printLn x
+
+  main : IO ()
+  main = f
+
+namespace Interface
+
+  interface X' where
+    x' : Nat
+
+  interface Y' where
+    constructor MkY
+    y' : Nat
+
+  Y' => X' where
+    x' = y'
+
+  %defaulthint
+  DefY' : Y'
+  DefY' = MkY 6
+
+  f' : X' => IO ()
+  f' = printLn x'
+
+  main : IO ()
+  main = f'

tests/idris2/interface/interface032/expected

@@ -0,0 +1 @@
+1/1: Building DefaulthintInterfaceBug (DefaulthintInterfaceBug.idr)

tests/idris2/interface/interface032/run

@@ -0,0 +1,3 @@
+. ../../../testutils.sh
+
+check DefaulthintInterfaceBug.idr