Add uniqueSearch data type option

This changes the behaviour of 'auto' implicits so that by default they
return the first result, rather than checking for unique results. This
is consistent with Idris 1. However, we still want to check for
uniqueness somtimes (for example, with interface search, which should
reject overlapping results) so the 'uniqueSearch' option means that any
auto implicit search for the type should check uniqueness of results.

Fixes #169

libs/base/Language/Reflection/TTImp.idr

@@ -102,6 +102,7 @@ mutual
   data DataOpt : Type where
        SearchBy : List Name -> DataOpt -- determining arguments
        NoHints : DataOpt -- Don't generate search hints for constructors
+       UniqueSearch : DataOpt
 
   public export
   data Data : Type where

src/Compiler/Common.idr

@@ -61,7 +61,7 @@ mkNameTags : Defs -> NameTags -> Int -> List Name -> Core NameTags
 mkNameTags defs tags t [] = pure tags
 mkNameTags defs tags t (n :: ns)
     = case !(lookupDefExact n (gamma defs)) of
-           Just (TCon _ _ _ _ _ _)
+           Just (TCon _ _ _ _ _ _ _)
               => mkNameTags defs (insert n t tags) (t + 1) ns
            _ => mkNameTags defs tags t ns
 

src/Compiler/CompileExpr.idr

@@ -359,7 +359,7 @@ toCDef tags n ty (Builtin {arity} op)
     getVars (ConsArg a rest) = MkVar First :: map weakenVar (getVars rest)
 toCDef tags n _ (DCon tag arity)
     = pure $ MkCon (fromMaybe tag $ lookup n tags) arity
-toCDef tags n _ (TCon tag arity _ _ _ _)
+toCDef tags n _ (TCon tag arity _ _ _ _ _)
     = pure $ MkCon (fromMaybe tag $ lookup n tags) arity
 -- We do want to be able to compile these, but also report an error at run time
 -- (and, TODO: warn at compile time)

src/Core/AutoSearch.idr

@@ -113,6 +113,11 @@ anyOne : {vars : _} ->
          List (Core (Term vars)) ->
          Core (Term vars)
 anyOne fc env top [] = throw (CantSolveGoal fc [] top)
+anyOne fc env top [elab]
+    = catch elab
+         (\err => case err of
+                       CantSolveGoal _ _ _ => throw err
+                       _ => throw (CantSolveGoal fc [] top))
 anyOne fc env top (elab :: elabs)
     = tryUnify elab (anyOne fc env top elabs)
 
@@ -335,7 +340,7 @@ searchName fc rigc defaults trying depth def top env target (n, ndef)
          let namety : NameType
                  = case definition ndef of
                         DCon tag arity => DataCon tag arity
-                        TCon tag arity _ _ _ _ => TyCon tag arity
+                        TCon tag arity _ _ _ _ _ => TyCon tag arity
                         _ => Func
          nty <- nf defs env (embed ty)
          logNF 10 ("Searching Name " ++ show n) env nty

src/Core/Binary.idr

@@ -27,7 +27,7 @@ import Data.Buffer
 -- TTC files can only be compatible if the version number is the same
 export
 ttcVersion : Int
-ttcVersion = 12
+ttcVersion = 13
 
 export
 checkTTCVersion : Int -> Int -> Core ()

src/Core/Context.idr

@@ -43,6 +43,8 @@ data Def : Type where
     TCon : (tag : Int) -> (arity : Nat) ->
            (parampos : List Nat) -> -- parameters
            (detpos : List Nat) -> -- determining arguments
+           (uniqueAuto : Bool) -> -- should 'auto' implicits check
+                                  -- for uniqueness
            (mutwith : List Name) ->
            (datacons : List Name) ->
            Def
@@ -68,7 +70,7 @@ Show Def where
   show (PMDef _ args ct rt pats)
       = show args ++ "; " ++ show ct
   show (DCon t a) = "DataCon " ++ show t ++ " " ++ show a
-  show (TCon t a ps ds ms cons)
+  show (TCon t a ps ds u ms cons)
       = "TyCon " ++ show t ++ " " ++ show a ++ " params: " ++ show ps ++
         " constructors: " ++ show cons ++
         " mutual with: " ++ show ms
@@ -577,9 +579,9 @@ HasNames Def where
       fullNamesPat (_ ** (env, lhs, rhs))
           = pure $ (_ ** (!(full gam env),
                           !(full gam lhs), !(full gam rhs)))
-  full gam (TCon t a ps ds ms cs)
-      = pure $ TCon t a ps ds !(traverse (full gam) ms)
-                              !(traverse (full gam) cs)
+  full gam (TCon t a ps ds u ms cs)
+      = pure $ TCon t a ps ds u !(traverse (full gam) ms)
+                                !(traverse (full gam) cs)
   full gam (BySearch c d def)
       = pure $ BySearch c d !(full gam def)
   full gam (Guess tm b cs)
@@ -595,9 +597,9 @@ HasNames Def where
       resolvedNamesPat (_ ** (env, lhs, rhs))
           = pure $ (_ ** (!(resolved gam env),
                           !(resolved gam lhs), !(resolved gam rhs)))
-  resolved gam (TCon t a ps ds ms cs)
-      = pure $ TCon t a ps ds !(traverse (resolved gam) ms)
-                              !(traverse (resolved gam) cs)
+  resolved gam (TCon t a ps ds u ms cs)
+      = pure $ TCon t a ps ds u !(traverse (resolved gam) ms)
+                                !(traverse (resolved gam) cs)
   resolved gam (BySearch c d def)
       = pure $ BySearch c d !(resolved gam def)
   resolved gam (Guess tm b cs)
@@ -1201,7 +1203,7 @@ getSearchData : {auto c : Ref Ctxt Defs} ->
                 Core SearchData
 getSearchData fc defaults target
     = do defs <- get Ctxt
-         Just (TCon _ _ _ dets _ _) <- lookupDefExact target (gamma defs)
+         Just (TCon _ _ _ dets u _ _) <- lookupDefExact target (gamma defs)
               | _ => throw (UndefinedName fc target)
          let hs = case lookup !(toFullNames target) (typeHints defs) of
                        Just hs => hs
@@ -1218,7 +1220,7 @@ getSearchData fc defaults target
                      pure (MkSearchData dets (filter (isCons . snd)
                                [(False, opens),
                                 (False, autos),
-                                (False, tyhs),
+                                (not u, tyhs),
                                 (True, chasers)]))
   where
     isDefault : (Name, Bool) -> Bool
@@ -1234,9 +1236,9 @@ setMutWith fc tn tns
     = do defs <- get Ctxt
          Just g <- lookupCtxtExact tn (gamma defs)
               | _ => throw (UndefinedName fc tn)
-         let TCon t a ps dets _ cons = definition g
+         let TCon t a ps dets u _ cons = definition g
               | _ => throw (GenericMsg fc (show (fullname g) ++ " is not a type constructor [setMutWith]"))
-         updateDef tn (const (Just (TCon t a ps dets tns cons)))
+         updateDef tn (const (Just (TCon t a ps dets u tns cons)))
 
 export
 addMutData : {auto c : Ref Ctxt Defs} ->
@@ -1259,10 +1261,10 @@ setDetermining fc tyn args
     = do defs <- get Ctxt
          Just g <- lookupCtxtExact tyn (gamma defs)
               | _ => throw (UndefinedName fc tyn)
-         let TCon t a ps _ cons ms = definition g
+         let TCon t a ps _ u cons ms = definition g
               | _ => throw (GenericMsg fc (show (fullname g) ++ " is not a type constructor [setDetermining]"))
          apos <- getPos 0 args (type g)
-         updateDef tyn (const (Just (TCon t a ps apos cons ms)))
+         updateDef tyn (const (Just (TCon t a ps apos u cons ms)))
   where
     -- Type isn't normalised, but the argument names refer to those given
     -- explicitly in the type, so there's no need.
@@ -1276,6 +1278,16 @@ setDetermining fc tyn args
     getPos _ ns ty = throw (GenericMsg fc ("Unknown determining arguments: "
                            ++ showSep ", " (map show ns)))
 
+export
+setUniqueSearch : {auto c : Ref Ctxt Defs} ->
+                  FC -> Name -> Bool -> Core ()
+setUniqueSearch fc tyn u
+    = do defs <- get Ctxt
+         Just g <- lookupCtxtExact tyn (gamma defs)
+              | _ => throw (UndefinedName fc tyn)
+         let TCon t a ps ds _ cons ms = definition g
+              | _ => throw (GenericMsg fc (show (fullname g) ++ " is not a type constructor [setDetermining]"))
+         updateDef tyn (const (Just (TCon t a ps ds u cons ms)))
 
 export
 addHintFor : {auto c : Ref Ctxt Defs} ->
@@ -1509,7 +1521,7 @@ addData vars vis tidx (MkData (MkCon dfc tyn arity tycon) datacons)
                             (TCon tag arity
                                   (paramPos (Resolved tidx) (map type datacons))
                                   (allDet arity)
-                                  [] (map name datacons))
+                                  False [] (map name datacons))
          (idx, gam') <- addCtxt tyn tydef (gamma defs)
          gam'' <- addDataConstructors 0 datacons gam'
          put Ctxt (record { gamma = gam'' } defs)

src/Core/Coverage.idr

@@ -51,7 +51,7 @@ export
 isEmpty : Defs -> NF vars -> Core Bool
 isEmpty defs (NTCon fc n t a args)
      = case !(lookupDefExact n (gamma defs)) of
-            Just (TCon _ _ _ _ _ cons)
+            Just (TCon _ _ _ _ _ _ cons)
                  => allM (conflict defs (NTCon fc n t a args)) cons
             _ => pure False
 isEmpty defs _ = pure False
@@ -66,7 +66,7 @@ freeEnv fc (n :: ns) = PVar RigW Explicit (Erased fc) :: freeEnv fc ns
 getCons : Defs -> NF vars -> Core (List (NF [], Name, Int, Nat))
 getCons defs (NTCon _ tn _ _ _)
     = case !(lookupDefExact tn (gamma defs)) of
-           Just (TCon _ _ _ _ _ cons) =>
+           Just (TCon _ _ _ _ _ _ cons) =>
                 do cs' <- traverse addTy cons
                    pure (mapMaybe id cs')
            _ => pure []

src/Core/Reflect.idr

@@ -21,7 +21,7 @@ getCon : FC -> Defs -> Name -> Core (Term vars)
 getCon fc defs n
     = case !(lookupDefExact n (gamma defs)) of
            Just (DCon t a) => resolved (gamma defs) (Ref fc (DataCon t a) n)
-           Just (TCon t a _ _ _ _) => resolved (gamma defs) (Ref fc (TyCon t a) n)
+           Just (TCon t a _ _ _ _ _) => resolved (gamma defs) (Ref fc (TyCon t a) n)
            Just _ => resolved (gamma defs) (Ref fc Func n)
            _ => throw (UndefinedName fc n)
 

src/Core/TTC.idr

@@ -743,9 +743,9 @@ TTC Def where
   toBuf b (Builtin a)
       = throw (InternalError "Trying to serialise a Builtin")
   toBuf b (DCon t arity) = do tag 4; toBuf b t; toBuf b arity
-  toBuf b (TCon t arity parampos detpos ms datacons)
+  toBuf b (TCon t arity parampos detpos u ms datacons)
       = do tag 5; toBuf b t; toBuf b arity; toBuf b parampos
-           toBuf b detpos; toBuf b ms; toBuf b datacons
+           toBuf b detpos; toBuf b u; toBuf b ms; toBuf b datacons
   toBuf b (Hole locs p)
       = do tag 6; toBuf b locs; toBuf b p
   toBuf b (BySearch c depth def)
@@ -772,8 +772,9 @@ TTC Def where
                      pure (DCon t a)
              5 => do t <- fromBuf b; a <- fromBuf b
                      ps <- fromBuf b; dets <- fromBuf b;
+                     u <- fromBuf b
                      ms <- fromBuf b; cs <- fromBuf b
-                     pure (TCon t a ps dets ms cs)
+                     pure (TCon t a ps dets u ms cs)
              6 => do l <- fromBuf b
                      p <- fromBuf b
                      pure (Hole l p)

src/Core/Termination.idr

@@ -492,7 +492,7 @@ posArg : Defs -> List Name -> NF [] -> Core Terminating
 posArg defs tyns (NTCon _ tc _ _ args)
     = let testargs : List (Closure [])
              = case !(lookupDefExact tc (gamma defs)) of
-                    Just (TCon _ _ params _ _ _) =>
+                    Just (TCon _ _ params _ _ _ _) =>
                          dropParams 0 params args
                     _ => args in
           if !(anyM (nameIn defs tyns)
@@ -548,7 +548,7 @@ calcPositive : {auto c : Ref Ctxt Defs} ->
 calcPositive loc n
     = do defs <- get Ctxt
          case !(lookupDefTyExact n (gamma defs)) of
-              Just (TCon _ _ _ _ tns dcons, ty) =>
+              Just (TCon _ _ _ _ _ tns dcons, ty) =>
                   case !(totRefsIn defs ty) of
                        IsTerminating =>
                             do t <- checkData defs (n :: tns) dcons
@@ -588,7 +588,7 @@ checkTotal loc n_in
          case isTerminating tot of
               Unchecked =>
                   case !(lookupDefExact n (gamma defs)) of
-                       Just (TCon _ _ _ _ _ _)
+                       Just (TCon _ _ _ _ _ _ _)
                            => checkPositive loc n
                        _ => checkTerminating loc n
               t => pure t

src/Idris/Elab/Interface.idr

@@ -36,8 +36,8 @@ mkIfaceData : {auto c : Ref Ctxt Defs} ->
               List Name -> List (Name, RigCount, RawImp) -> Core ImpDecl
 mkIfaceData {vars} fc vis env constraints n conName ps dets meths
     = let opts = if isNil dets
-                    then [NoHints]
-                    else [NoHints, SearchBy dets]
+                    then [NoHints, UniqueSearch]
+                    else [NoHints, UniqueSearch, SearchBy dets]
           retty = apply (IVar fc n) (map (IVar fc) (map fst ps))
           conty = mkTy Implicit (map jname ps) $
                   mkTy Explicit (map bhere constraints ++ map bname meths) retty

src/Idris/Parser.idr

@@ -836,6 +836,8 @@ dataOpt : Rule DataOpt
 dataOpt
     = do exactIdent "noHints"
          pure NoHints
+  <|> do exactIdent "uniqueSearch"
+         pure UniqueSearch
   <|> do exactIdent "search"
          ns <- some name
          pure (SearchBy ns)

src/TTImp/Elab/Ambiguity.idr

@@ -78,7 +78,7 @@ expandAmbigName mode nest env orig args (IVar fc x) exp
     wrapDot : Bool -> EState vars ->
               ElabMode -> Name -> List RawImp -> Def -> RawImp -> RawImp
     wrapDot _ _ _ _ _ (DCon _ _) tm = tm
-    wrapDot _ _ _ _ _ (TCon _ _ _ _ _ _) tm = tm
+    wrapDot _ _ _ _ _ (TCon _ _ _ _ _ _ _) tm = tm
     -- Leave primitive applications alone, because they'll be inlined
     -- before compiling the case tree
     wrapDot prim est (InLHS _) n' [arg] _ tm

src/TTImp/Elab/App.idr

@@ -56,7 +56,7 @@ getNameType rigc env fc x
                  let nt = case definition def of
                                PMDef _ _ _ _ _ => Func
                                DCon t a => DataCon t a
-                               TCon t a _ _ _ _ => TyCon t a
+                               TCon t a _ _ _ _ _ => TyCon t a
                                _ => Func
                  pure (Ref fc nt (Resolved i), gnf env (embed (type def)))
   where
@@ -90,7 +90,7 @@ getVarType rigc nest env fc x
                          let nt = case definition ndef of
                                        PMDef _ _ _ _ _ => Func
                                        DCon t a => DataCon t a
-                                       TCon t a _ _ _ _ => TyCon t a
+                                       TCon t a _ _ _ _ _ => TyCon t a
                                        _ => Func
                              tm = tmf fc nt
                              tyenv = useVars (getArgs tm)

src/TTImp/Elab/Record.idr

@@ -37,7 +37,7 @@ toRHS loc (Constr con args)
 findConName : Defs -> Name -> Core (Maybe Name)
 findConName defs tyn
     = case !(lookupDefExact tyn (gamma defs)) of
-           Just (TCon _ _ _ _ _ [con]) => pure (Just con)
+           Just (TCon _ _ _ _ _ _ [con]) => pure (Just con)
            _ => pure Nothing
 
 findFields : Defs -> Name -> Core (Maybe (List (String, Maybe Name)))

src/TTImp/Interactive/CaseSplit.idr

@@ -92,7 +92,7 @@ findCons n lhs
                       Nothing => pure (SplitFail (CantSplitThis n
                                          ("Can't find type of " ++ show n ++ " in LHS")))
                       Just tyn =>
-                          do Just (TCon _ _ _ _ _ cons) <-
+                          do Just (TCon _ _ _ _ _ _ cons) <-
                                       lookupDefExact tyn (gamma defs)
                                 | res => pure (SplitFail
                                             (CantSplitThis n

src/TTImp/Interactive/ExprSearch.idr

@@ -114,7 +114,7 @@ searchName fc rigc opts env target topty defining (n, ndef)
          let namety : NameType
                  = case definition ndef of
                         DCon tag arity => DataCon tag arity
-                        TCon tag arity _ _ _ _ => TyCon tag arity
+                        TCon tag arity _ _ _ _ _ => TyCon tag arity
                         _ => Func
          log 5 $ "Trying " ++ show (fullname ndef)
          nty <- nf defs env (embed ty)

src/TTImp/Parser.idr

@@ -524,6 +524,8 @@ dataOpt : Rule DataOpt
 dataOpt
     = do exactIdent "noHints"
          pure NoHints
+  <|> do exactIdent "uniqueSearch"
+         pure UniqueSearch
   <|> do exactIdent "search"
          ns <- some name
          pure (SearchBy ns)

src/TTImp/ProcessData.idr

@@ -23,6 +23,8 @@ processDataOpt fc n NoHints
     = pure ()
 processDataOpt fc ndef (SearchBy dets)
     = setDetermining fc ndef dets
+processDataOpt fc ndef UniqueSearch
+    = setUniqueSearch fc ndef True
 
 checkRetType : {auto c : Ref Ctxt Defs} ->
                Env Term vars -> NF vars ->
@@ -121,7 +123,7 @@ processData {vars} eopts nest env fc vis (MkImpLater dfc n_in ty_raw)
 
          -- Add the type constructor as a placeholder
          tidx <- addDef n (newDef fc n Rig1 vars fullty vis
-                          (TCon 0 arity [] [] [] []))
+                          (TCon 0 arity [] [] False [] []))
          addMutData (Resolved tidx)
          defs <- get Ctxt
          traverse_ (\n => setMutWith fc n (mutData defs)) (mutData defs)
@@ -158,7 +160,7 @@ processData {vars} eopts nest env fc vis (MkImpData dfc n_in ty_raw opts cons_ra
                   Nothing => pure []
                   Just ndef =>
                     case definition ndef of
-                         TCon _ _ _ _ mw _ =>
+                         TCon _ _ _ _ _ mw _ =>
                             do ok <- convert defs [] fullty (type ndef)
                                if ok then pure mw
                                      else do logTermNF 1 "Previous" [] (type ndef)
@@ -174,7 +176,7 @@ processData {vars} eopts nest env fc vis (MkImpData dfc n_in ty_raw opts cons_ra
          -- Add the type constructor as a placeholder while checking
          -- data constructors
          tidx <- addDef n (newDef fc n Rig1 vars fullty vis
-                          (TCon 0 arity [] [] [] []))
+                          (TCon 0 arity [] [] False [] []))
          case vis of
               Private => pure ()
               _ => do addHash n

src/TTImp/Reflect.idr

@@ -252,6 +252,8 @@ mutual
              pure (SearchBy x')
     reify defs (NDCon _ (NS _ (UN "NoHints")) _ _ _)
         = pure NoHints
+    reify defs (NDCon _ (NS _ (UN "UniqueSearch")) _ _ _)
+        = pure UniqueSearch
     reify defs val = cantReify val "DataOpt"
 
   export
@@ -549,6 +551,7 @@ mutual
         = do x' <- reflect fc defs env x
              appCon fc defs (reflectionttimp "SearchBy") [x']
     reflect fc defs env NoHints = getCon fc defs (reflectionttimp "NoHints")
+    reflect fc defs env UniqueSearch = getCon fc defs (reflectionttimp "UniqueSearch")
 
   export
   Reflect ImpData where

src/TTImp/TTImp.idr

@@ -221,11 +221,13 @@ mutual
   data DataOpt : Type where
        SearchBy : List Name -> DataOpt -- determining arguments
        NoHints : DataOpt -- Don't generate search hints for constructors
+       UniqueSearch : DataOpt -- auto implicit search must check result is unique
 
   export
   Eq DataOpt where
     (==) (SearchBy xs) (SearchBy ys) = xs == ys
     (==) NoHints NoHints = True
+    (==) UniqueSearch UniqueSearch = True
     (==) _ _ = False
 
   public export
@@ -794,12 +796,14 @@ mutual
     toBuf b (SearchBy ns)
         = do tag 0; toBuf b ns
     toBuf b NoHints = tag 1
+    toBuf b UniqueSearch = tag 2
 
     fromBuf b
         = case !getTag of
                0 => do ns <- fromBuf b
                        pure (SearchBy ns)
                1 => pure NoHints
+               2 => pure UniqueSearch
                _ => corrupt "DataOpt"
 
   export

tests/Main.idr

@@ -44,7 +44,7 @@ idrisTests
        "linear001", "linear002", "linear003", "linear004", "linear005",
        "linear006", "linear007",
        "params001",
-       "perf001", "perf002",
+       "perf001", "perf002", "perf003",
        "perror001", "perror002", "perror003", "perror004", "perror005",
        "perror006",
        "pkg001",

tests/idris2/perf003/Auto.idr

@@ -0,0 +1,18 @@
+public export
+data Phase = Gas | Liquid | Solid
+
+public export
+data ChangePhase : Phase -> Phase -> Type where
+	Sequence : ChangePhase a b -> ChangePhase b c -> ChangePhase a c
+	Condense : ChangePhase Gas Liquid
+	Freeze : ChangePhase Liquid Solid
+	Melt : ChangePhase Solid Liquid
+	Vaporize : ChangePhase Liquid Gas
+	Sublimate : ChangePhase Solid Gas
+
+public export
+inferred : { auto transition : ChangePhase l r } -> ChangePhase l r
+inferred { transition } = transition
+
+test : ChangePhase Gas Solid
+test = inferred

tests/idris2/perf003/expected

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

tests/idris2/perf003/run

@@ -0,0 +1,3 @@
+$1 --check Auto.idr
+
+rm -rf build