Annotate functions as %hint for auto search

This allows extra hints, as well as constructors, to guide proof search
for auto implicit arguments.
Added test proof010 which shows how this works to simulate type classes
with overlapping instances (and consequently no injectivity restriction
or assumption)

%hint only works on functions which return an instance of a data type.
Proof search exhaustively searches hints and constructors, so use with
care especially when adding lots of recursive or overlapping hints.

CHANGELOG

@@ -10,6 +10,9 @@ New in 0.9.18:
     '%extern' directive, allowing back ends to define their own special 
     purpose primitives
   + Ptr and ManagedPtr have been removed and replaced with external primitives
+* Add %hint function annotation, which allows functions to be used as
+  hints in proof search for 'auto' arguments. Only functions which return
+  an instance of a data or record type are allowed as hints.
 * Syntax rules no longer perform variable capture. Users of effects will
   need to explicitly name results in dependent effect signatures instead
   of using the default name "result".

idris.cabal

@@ -531,6 +531,9 @@ Extra-source-files:
                        test/proof009/*.idr
                        test/proof009/expected
                        test/proof009/input
+                       test/proof010/run
+                       test/proof010/*.idr
+                       test/proof010/expected
 
                        test/quasiquote001/run
                        test/quasiquote001/*.idr

src/Idris/AbsSyntax.hs

@@ -385,6 +385,23 @@ addClass n i
                       _ -> i
         putIState $ ist { idris_classes = addDef n i' (idris_classes ist) }
 
+addAutoHint :: Name -> Name -> Idris ()
+addAutoHint n hint =
+    do ist <- getIState
+       case lookupCtxtExact n (idris_autohints ist) of
+            Nothing -> 
+                 do let hs = addDef n [hint] (idris_autohints ist)
+                    putIState $ ist { idris_autohints = hs }
+            Just nhints -> 
+                 do let hs = addDef n (hint : nhints) (idris_autohints ist)
+                    putIState $ ist { idris_autohints = hs }
+
+getAutoHints :: Name -> Idris [Name]
+getAutoHints n = do ist <- getIState
+                    case lookupCtxtExact n (idris_autohints ist) of
+                         Nothing -> return []
+                         Just ns -> return ns
+
 addIBC :: IBCWrite -> Idris ()
 addIBC ibc@(IBCDef n)
            = do i <- getIState

src/Idris/AbsSyntaxTree.hs

@@ -179,6 +179,7 @@ data IState = IState {
     idris_tyinfodata :: Ctxt TIData,
     idris_fninfo :: Ctxt FnInfo,
     idris_transforms :: Ctxt [(Term, Term)],
+    idris_autohints :: Ctxt [Name],
     idris_totcheck :: [(FC, Name)], -- names to check totality on
     idris_defertotcheck :: [(FC, Name)], -- names to check at the end
     idris_totcheckfail :: [(FC, String)],
@@ -307,6 +308,7 @@ data IBCWrite = IBCFix FixDecl
               | IBCModDocs Name -- ^ The name is the special name used to track module docs
               | IBCUsage (Name, Int)
               | IBCExport Name
+              | IBCAutoHint Name Name
   deriving Show
 
 -- | The initial state for the compiler
@@ -316,6 +318,7 @@ idrisInit = IState initContext S.empty []
                    emptyContext emptyContext emptyContext emptyContext
                    emptyContext emptyContext emptyContext emptyContext
                    emptyContext emptyContext emptyContext emptyContext
+                   emptyContext
                    [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []
                    [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []
                    (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty
@@ -560,6 +563,7 @@ data FnOpt = Inlinable -- always evaluate when simplifying
            | Reflection -- a reflecting function, compile-time only
            | Specialise [(Name, Maybe Int)] -- specialise it, freeze these names
            | Constructor -- Data constructor type
+           | AutoHint -- use in auto implicit search
     deriving (Show, Eq)
 {-!
 deriving instance Binary FnOpt

src/Idris/Core/Unify.hs

@@ -707,9 +707,11 @@ recoverable (App f a) (App f' a')
 recoverable f (Bind _ (Pi _ _ _) sc)
     | (P (DCon _ _ _) _ _, _) <- unApply f = False
     | (P (TCon _ _) _ _, _) <- unApply f = False
+    | (Constant _) <- f = False
 recoverable (Bind _ (Pi _ _ _) sc) f
     | (P (DCon _ _ _) _ _, _) <- unApply f = False
     | (P (TCon _ _) _ _, _) <- unApply f = False
+    | (Constant _) <- f = False
 recoverable (Bind _ (Lam _) sc) f = recoverable sc f
 recoverable f (Bind _ (Lam _) sc) = recoverable f sc
 recoverable x y = True

src/Idris/DeepSeq.hs

@@ -119,6 +119,7 @@ instance NFData FnOpt where
         rnf Reflection = ()
         rnf (Specialise x1) = rnf x1 `seq` ()
         rnf Constructor = ()
+        rnf AutoHint = ()
 
 instance NFData DataOpt where
         rnf Codata = ()

src/Idris/Elab/Type.hs

@@ -146,8 +146,8 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params
            addInternalApp (fc_fname fc) (fst . fc_start $ fc) ty' -- (mergeTy ty' (delab i nty')) -- TODO: Should use span instead of line and filename?
            addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) ty') -- (mergeTy ty' (delab i nty')))
 
-         let (t, _) = unApply (getRetTy nty')
-         let corec = case t of
+         let (fam, _) = unApply (getRetTy nty')
+         let corec = case fam of
                         P _ rcty _ -> case lookupCtxt rcty (idris_datatypes i) of
                                         [TI _ True _ _ _] -> True
                                         _ -> False
@@ -157,7 +157,7 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params
          let usety = if norm then nty' else nty
          ds <- checkDef fc iderr [(n, (-1, Nothing, usety))]
          addIBC (IBCDef n)
-         let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds
+         let ds' = map (\(n, (i, top, fam)) -> (n, (i, top, fam, True))) ds
          addDeferred ds'
          setFlags n opts'
          checkDocs fc argDocs ty
@@ -171,6 +171,11 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params
          addIBC (IBCOpt n)
          when (Implicit `elem` opts') $ do addCoercion n
                                            addIBC (IBCCoercion n)
+         when (AutoHint `elem` opts') $ 
+             case fam of
+                P _ tyn _ -> do addAutoHint tyn n
+                                addIBC (IBCAutoHint tyn n)
+                t -> ifail $ "Hints must return a data or record type"
 
          -- If the function is declared as an error handler and the language
          -- extension is enabled, then add it to the list of error handlers.

src/Idris/IBC.hs

@@ -37,7 +37,7 @@ import Codec.Compression.Zlib (compress)
 import Util.Zlib (decompressEither)
 
 ibcVersion :: Word8
-ibcVersion = 103
+ibcVersion = 104
 
 data IBCFile = IBCFile { ver :: Word8,
                          sourcefile :: FilePath,
@@ -82,15 +82,16 @@ data IBCFile = IBCFile { ver :: Word8,
                          ibc_externs :: ![(Name, Int)],
                          ibc_parsedSpan :: !(Maybe FC),
                          ibc_usage :: ![(Name, Int)],
-                         ibc_exports :: ![Name]
+                         ibc_exports :: ![Name],
+                         ibc_autohints :: ![(Name, Name)]
                        }
    deriving Show
 {-!
 deriving instance Binary IBCFile
 !-}
 
 initIBC :: IBCFile
-initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] []
+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] []
 
 loadIBC :: Bool -- ^ True = reexport, False = make everything private
         -> FilePath -> Idris ()
@@ -237,6 +238,7 @@ ibc i (IBCModDocs n) f = case lookupCtxtExact n (idris_moduledocs i) of
                            _ -> ifail "IBC write failed"
 ibc i (IBCUsage n) f = return f { ibc_usage = n : ibc_usage f }
 ibc i (IBCExport n) f = return f { ibc_exports = n : ibc_exports f }
+ibc i (IBCAutoHint n h) f = return f { ibc_autohints = (n, h) : ibc_autohints f }
 
 process :: Bool -- ^ Reexporting
            -> IBCFile -> FilePath -> Idris ()
@@ -296,6 +298,7 @@ process reexp i fn
                pParsedSpan $ force (ibc_parsedSpan i)
                pUsage $ force (ibc_usage i)
                pExports $ force (ibc_exports i)
+               pAutoHints $ force (ibc_autohints i)
 
 timestampOlder :: FilePath -> FilePath -> Idris ()
 timestampOlder src ibc = do srct <- runIO $ getModificationTime src
@@ -326,6 +329,9 @@ pExports :: [Name] -> Idris ()
 pExports ns = do ist <- getIState
                  putIState ist { idris_exports = ns ++ idris_exports ist }
 
+pAutoHints :: [(Name, Name)] -> Idris ()
+pAutoHints ns = mapM_ (\(n,h) -> addAutoHint n h) ns
+
 pImportDirs :: [FilePath] -> Idris ()
 pImportDirs fs = mapM_ addImportDir fs
 
@@ -942,7 +948,7 @@ instance Binary MetaInformation where
              _ -> error "Corrupted binary data for MetaInformation"
 
 instance Binary IBCFile where
-        put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40 x41 x42 x43 x44)
+        put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40 x41 x42 x43 x44 x45)
          = {-# SCC "putIBCFile" #-}
             do put x1
                put x2
@@ -988,6 +994,7 @@ instance Binary IBCFile where
                put x42
                put x43
                put x44
+               put x45
 
         get
           = do x1 <- get
@@ -1035,7 +1042,8 @@ instance Binary IBCFile where
                     x42 <- get
                     x43 <- get
                     x44 <- get
-                    return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40 x41 x42 x43 x44)
+                    x45 <- get
+                    return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40 x41 x42 x43 x44 x45)
                   else return (initIBC { ver = x1 })
 
 instance Binary DataOpt where
@@ -1072,6 +1080,7 @@ instance Binary FnOpt where
                 Constructor -> putWord8 13
                 CExport x1 -> do putWord8 14
                                  put x1
+                AutoHint -> putWord8 15
         get
           = do i <- getWord8
                case i of
@@ -1092,6 +1101,7 @@ instance Binary FnOpt where
                    13 -> return Constructor
                    14 -> do x1 <- get
                             return $ CExport x1
+                   15 -> return AutoHint
                    _ -> error "Corrupted binary data for FnOpt"
 
 instance Binary Fixity where

src/Idris/Parser.hs

@@ -479,6 +479,8 @@ fnOpts opts
                  fnOpts (ErrorReverse : opts)
       <|> do try (lchar '%' *> reserved "reflection");
                   fnOpts (Reflection : opts)
+      <|> do try (lchar '%' *> reserved "hint");
+                  fnOpts (AutoHint : opts)
       <|> do lchar '%'; reserved "specialise";
              lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']'
              fnOpts (Specialise ns : opts)

src/Idris/ProofSearch.hs

@@ -91,7 +91,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist
             if ambigok || argsok then
                case lookupCtxt nroot (idris_tyinfodata ist) of
                     [TISolution ts] -> findInferredTy ts
-                    _ -> psRec rec maxDepth
+                    _ -> psRec rec maxDepth []
                else autoArg (sUN "auto") -- not enough info in the type yet
   where
     findInferredTy (t : _) = elab (delab ist (toUN t)) 
@@ -129,12 +129,17 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist
     toUN (App f a) = App (toUN f) (toUN a)
     toUN t = t
 
-    psRec _ 0 | fromProver = cantSolveGoal
-    psRec rec 0 = do attack; defer [] nroot; solve --fail "Maximum depth reached"
-    psRec False d = tryCons d hints 
-    psRec True d = do compute
+    -- psRec counts depth and the local variable applications we're under
+    -- (so we don't try a pointless application of something to itself,
+    -- which obviously won't work anyway but might lead us on a wild
+    -- goose chase...)
+    psRec _ 0 locs | fromProver = cantSolveGoal
+    psRec rec 0 locs = do attack; defer [] nroot; solve --fail "Maximum depth reached"
+    psRec False d locs = tryCons d locs hints 
+    psRec True d locs 
+                 = do compute
                       try' (trivial elab ist)
-                           (try' (try' (resolveByCon (d - 1)) (resolveByLocals (d - 1))
+                           (try' (try' (resolveByCon (d - 1) locs) (resolveByLocals (d - 1) locs)
                                  True)
              -- if all else fails, make a new metavariable
                          (if fromProver 
@@ -145,37 +150,46 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist
     getFn d (Just f) | d < maxDepth-1 = [f]
                      | otherwise = []
 
-    resolveByCon d
+    resolveByCon d locs
         = do t <- goal
              let (f, _) = unApply t
              case f of
-                P _ n _ -> case lookupCtxt n (idris_datatypes ist) of
-                               [t] -> tryCons d (hints ++ con_names t ++
-                                                                getFn d fn)
-                               _ -> fail "Not a data type"
+                P _ n _ -> 
+                   do let autohints = case lookupCtxtExact n (idris_autohints ist) of
+                                           Nothing -> []
+                                           Just hs -> hs
+                      case lookupCtxt n (idris_datatypes ist) of
+                          [t] -> tryCons d locs (hints ++ 
+                                                 con_names t ++ 
+                                                 autohints ++ 
+                                                 getFn d fn)
+                          _ -> fail "Not a data type"
                 _ -> fail "Not a data type"
 
     -- if there are local variables which have a function type, try
     -- applying them too
-    resolveByLocals d
+    resolveByLocals d locs
         = do env <- get_env
-             tryLocals d env
+             tryLocals d locs env
 
-    tryLocals d [] = fail "Locals failed"
-    tryLocals d ((x, t) : xs) = try' (tryLocal d x t) (tryLocals d xs) True
+    tryLocals d locs [] = fail "Locals failed"
+    tryLocals d locs ((x, t) : xs) 
+       | x `elem` locs = tryLocals d locs xs
+       | otherwise = try' (tryLocal d (x : locs) x t) (tryLocals d locs xs) True
 
-    tryCons d [] = fail "Constructors failed"
-    tryCons d (c : cs) = try' (tryCon d c) (tryCons d cs) True
+    tryCons d locs [] = fail "Constructors failed"
+    tryCons d locs (c : cs) = try' (tryCon d locs c) (tryCons d locs cs) True
 
-    tryLocal d n t = do let a = getPArity (delab ist (binderTy t))
-                        tryLocalArg d n a
+    tryLocal d locs n t 
+          = do let a = getPArity (delab ist (binderTy t))
+               tryLocalArg d locs n a
 
-    tryLocalArg d n 0 = elab (PRef (fileFC "prf") n)
-    tryLocalArg d n i = simple_app False (tryLocalArg d n (i - 1))
-                                   (psRec True d) "proof search local apply"
+    tryLocalArg d locs n 0 = elab (PRef (fileFC "prf") n)
+    tryLocalArg d locs n i = simple_app False (tryLocalArg d locs n (i - 1))
+                                   (psRec True d locs) "proof search local apply"
 
     -- Like type class resolution, but searching with constructors
-    tryCon d n = 
+    tryCon d locs n = 
          do ty <- goal
             let imps = case lookupCtxtName n (idris_implicits ist) of
                             [] -> []
@@ -190,7 +204,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist
             when (length ps < length ps') $ fail "Can't apply constructor"
             mapM_ (\ (_, h) -> do focus h
                                   aty <- goal
-                                  psRec True d) 
+                                  psRec True d locs) 
                   (filter (\ (x, y) -> not x) (zip (map fst imps) args))
             solve
 

test/proof010/expected

@@ -0,0 +1,6 @@
+2, << function >>
+3, << function >>
+
+some bools
+some bools
+

test/proof010/proof010.idr

@@ -0,0 +1,39 @@
+data MyShow : Type -> Type where
+     ShowInstance : (show : a -> String) -> MyShow a
+
+myshow : {auto inst : MyShow a} -> a -> String
+myshow {inst = ShowInstance show} x1 = show x1 
+
+%hint
+showNat : MyShow Nat
+showNat = ShowInstance show 
+
+%hint
+showFn : MyShow (a -> b)
+showFn = ShowInstance (\x => "<< function >>")
+
+%hint
+showBools : MyShow (Bool, Bool)
+showBools = ShowInstance (\x => "some bools")
+
+%hint
+showStuff : MyShow a -> MyShow b -> MyShow (a, b)
+showStuff sa sb = ShowInstance showPair
+  where
+    showPair : (a, b) -> String
+    showPair (x, y) = myshow x ++ ", " ++ myshow y
+
+testShow : List (Bool, Bool) -> String
+testShow [] = "" 
+testShow (x :: xs) = myshow x ++ "\n" ++ testShow xs
+
+testShow2 : List (Nat, Int -> Int) -> String
+testShow2 [] = "" 
+testShow2 (x :: xs) = myshow x ++ "\n" ++ testShow2 xs
+
+main : IO ()
+main = do putStrLn $ testShow2 [(2, (+1)), (3, abs)]
+          putStrLn $ testShow [(True, False), (False, True)]
+
+
+

test/proof010/run

@@ -0,0 +1,4 @@
+#!/usr/bin/env bash
+idris $@ proof010.idr -o proof010
+./proof010
+rm -f proof010 *.ibc