Friendlier error on proof search failure

Now, proof search doesn't throw an INTERNAL ERROR when called on a goal
that isn't a datatype. Instead, it provides the following message:

    Prover error: Attempted to find an element of type Nat -> Bool using
    proof search, but proof search only works on datatypes with
    constructors.

When the goal is a function type, which seems to be a likely reason why
it would fail, it adds the sentence:

    In particular, function types are not supported.

Additionally, a variant of the Msg constructor for errors, called
FancyMsg, was introduced. This allows the use of the ErrorReportPart
type to define custom messages.

Fixes #2713.

src/Idris/Core/Binary.hs

@@ -190,7 +190,8 @@ instance Binary a => Binary (Err' a) where
                                  put e
   put (ElabScriptStaging n) = do putWord8 43
                                  put n
-
+  put (FancyMsg xs) = do putWord8 44
+                         put xs
   get = do i <- getWord8
            case i of
              0 -> fmap Msg get
@@ -262,6 +263,7 @@ instance Binary a => Binary (Err' a) where
              41 -> fmap NoValidAlts get
              42 -> fmap RunningElabScript get
              43 -> fmap ElabScriptStaging get
+             44 -> fmap FancyMsg get
              _ -> error "Corrupted binary data for Err'"
 ----- Generated by 'derive'
 

src/Idris/Core/DeepSeq.hs

@@ -157,6 +157,7 @@ instance NFData Err where
         rnf (ElabScriptStuck x1) = rnf x1 `seq` ()
         rnf (RunningElabScript x1) = rnf x1 `seq` ()
         rnf (ElabScriptStaging x1) = rnf x1 `seq` ()
+        rnf (FancyMsg x1) = rnf x1 `seq` ()
 
 instance NFData ErrorReportPart where
   rnf (TextPart x1) = rnf x1 `seq` ()

src/Idris/Core/TT.hs

@@ -298,6 +298,7 @@ data Err' t
           | ElabScriptStuck t
           | RunningElabScript (Err' t) -- ^ The error occurred during a top-level elaboration script
           | ElabScriptStaging Name
+          | FancyMsg [ErrorReportPart]
   deriving (Eq, Functor, Data, Typeable)
 
 type Err = Err' Term

src/Idris/Delaborate.hs

@@ -507,6 +507,8 @@ pprintErr' i (ElabScriptStaging n) =
   text "Can't run elaboration script because it contains pattern matching that has not yet been elaborated." <$>
   text "Try lifting the script to a top-level definition." <$>
   text "In particular, the problem is caused by:" <+> annName n
+pprintErr' i (FancyMsg parts) =
+  fillSep (map (showPart i) parts)
 
 showPart :: IState -> ErrorReportPart -> Doc OutputAnnotation
 showPart ist (TextPart str) = fillSep . map text . words $ str

src/Idris/IBC.hs

@@ -40,7 +40,7 @@ import System.Directory
 import Codec.Archive.Zip
 
 ibcVersion :: Word16
-ibcVersion = 123
+ibcVersion = 124
 
 data IBCFile = IBCFile { ver :: Word16,
                          sourcefile :: FilePath,

src/Idris/ProofSearch.hs

@@ -196,7 +196,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi
                               Nothing -> -- local variable, go for it
                                     return True
               TType _ -> return True
-              _ -> fail "Not a data type"
+              _ -> typeNotSearchable ty
 
     conReady :: [Term] -> Name -> ElabD Bool
     conReady as n 
@@ -282,8 +282,8 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi
                                    -- since that's part of the point...)
                                    $ checkConstructor ist others
                              tryCons d locs tys (others ++ getFn d fn)
-                          Nothing -> fail "Not a data type"
-                _ -> fail "Not a data type"
+                          Nothing -> typeNotSearchable t
+                _ -> typeNotSearchable t
 
     -- if there are local variables which have a function type, try
     -- applying them too
@@ -326,11 +326,20 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi
             let newhs = filter (\ (x, y) -> not x) (zip (map fst imps) args)
             mapM_ (\ (_, h) -> do focus h
                                   aty <- goal
-                                  psRec True d locs tys) newhs      
+                                  psRec True d locs tys) newhs
             solve
 
     isImp (PImp p _ _ _ _) = (True, p)
-    isImp arg = (False, priority arg) 
+    isImp arg = (False, priority arg)
+
+    typeNotSearchable ty =
+       lift $ tfail $ FancyMsg $
+       [TextPart "Attempted to find an element of type",
+        TermPart ty,
+        TextPart "using proof search, but proof search only works on datatypes with constructors."] ++
+       case ty of
+         (Bind _ (Pi _ _ _) _) -> [TextPart "In particular, function types are not supported."]
+         _ -> []
 
 -- In interactive mode, only search for things if there is some 
 -- index to help pick a relevant constructor