06fd947 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add "Can't solve goal" error message

This improves error reporting for arguments which are solved by tactics, printing the proof search that failed rather than the specific part of the search which went wrong.

commit06fd9475fec0bd93cd87f3ecaf2c1e3e6899fc62 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 22 Jan 2014, 15:57 (13 years ago) parentda25e42

5 files changed+36−12

compare with master

unifiedsplit

libs/base/Language/Reflection/Errors.idr+1 src/Idris/Core/Elaborate.hs+19−11 src/Idris/Core/TT.hs+3 src/Idris/Delaborate.hs+5 src/Idris/ElabTerm.hs+8−1

libs/base/Language/Reflection/Errors.idr+1

@@ -15,6 +15,7 @@ data Err = Msg String

1515 -- unification succeed

1616 | InfiniteUnify TTName TT (List (TTName, TT))

1717 | CantConvert TT TT (List (TTName, TT))

18+ | CantSolveGoal TT (List (TTName, TT))

1819 | UnifyScope TTName TTName TT (List (TTName, TT))

1920 | CantInferType String

2021 | NonFunctionType TT TT

src/Idris/Core/Elaborate.hs+19−11

@@ -604,17 +604,24 @@ arg n tyhole = do ty <- unique_hole tyhole

604604 forall n (Var ty)

605605

606606-- try a tactic, if it adds any unification problem, return an error

607−no_errors :: Elab' aux () -> Elab' aux ()

608−no_errors tac

609− = do ps <- get_probs

610− tac

611− ps' <- get_probs

612− if (length ps' > length ps) then

613− case reverse ps' of

614− ((x,y,env,err) : _) ->

615− let env' = map (\(x, b) -> (x, binderTy b)) env in

616− lift $ tfail $ CantUnify False x y err env' 0

617− else return $! ()

607+no_errors :: Elab' aux () -> Maybe Err -> Elab' aux ()

608+no_errors tac err

609+ = do ps <- get_probs

610+ s <- get

611+ case err of

612+ Nothing -> tac

613+ Just e -> -- update the error, if there is one.

614+ case runStateT tac s of

615+ Error _ -> lift $ Error e

616+ OK (a, s') -> do put s'

617+ return a

618+ ps' <- get_probs

619+ if (length ps' > length ps) then

620+ case reverse ps' of

621+ ((x,y,env,err) : _) ->

622+ let env' = map (\(x, b) -> (x, binderTy b)) env in

623+ lift $ tfail $ CantUnify False x y err env' 0

624+ else return $! ()

618625

619626-- Try a tactic, if it fails, try another

620627try :: Elab' aux a -> Elab' aux a -> Elab' aux a

@@ -637,6 +644,7 @@ try' t1 t2 proofSearch

637644 where recoverableErr err@(CantUnify r x y _ _ _)

638645 = -- traceWhen r (show err) $

639646 r || proofSearch

647+ recoverableErr (CantSolveGoal _ _) = False

640648 recoverableErr (ProofSearchFail _) = False

641649 recoverableErr _ = True

642650

src/Idris/Core/TT.hs+3

@@ -98,6 +98,7 @@ data Err = Msg String

9898 -- unification succeed

9999 | InfiniteUnify Name Term [(Name, Type)]

100100 | CantConvert Term Term [(Name, Type)]

101+ | CantSolveGoal Term [(Name, Type)]

101102 | UnifyScope Name Name Term [(Name, Type)]

102103 | CantInferType String

103104 | NonFunctionType Term Term

@@ -155,6 +156,7 @@ score (CantUnify _ _ _ m _ s) = s + score m

155156score (CantResolve _) = 20

156157score (NoSuchVariable _) = 1000

157158score (ProofSearchFail _) = 10000

159+score (CantSolveGoal _ _) = 10000

158160score (InternalMsg _) = -1

159161score _ = 0

160162

@@ -163,6 +165,7 @@ instance Show Err where

163165 show (InternalMsg s) = "Internal error: " ++ show s

164166 show (CantUnify _ l r e sc i) = "CantUnify " ++ show l ++ " " ++ show r ++ " "

165167 ++ show e ++ " in " ++ show sc ++ " " ++ show i

168+ show (CantSolveGoal g _) = "CantSolve " ++ show g

166169 show (Inaccessible n) = show n ++ " is not an accessible pattern variable"

167170 show (ProviderError msg) = "Type provider error: " ++ msg

168171 show (LoadingFailed fn e) = "Loading " ++ fn ++ " failed: (TT) " ++ show e

src/Idris/Delaborate.hs+5

@@ -142,6 +142,11 @@ pshow i (CantConvert x y env)

142142 "Can't convert" ++ indented (showImp (Just i) imps colour (delab i x)) ++ "with"

143143 ++ indented (showImp (Just i) imps colour (delab i y)) ++

144144 if (opt_errContext (idris_options i)) then showSc i env else ""

145+pshow i (CantSolveGoal x env)

146+ = let imps = opt_showimp (idris_options i) in

147+ let colour = idris_colourRepl i in

148+ "Can't solve goal " ++ indented (showImp (Just i) imps colour (delab i x)) ++

149+ if (opt_errContext (idris_options i)) then showSc i env else ""

145150pshow i (UnifyScope n out tm env)

146151 = let imps = opt_showimp (idris_options i) in

147152 let colour = idris_colourRepl i in

src/Idris/ElabTerm.hs+8−1

@@ -810,7 +810,9 @@ collectDeferred top t = return t

810810runTac :: Bool -> IState -> PTactic -> ElabD ()

811811runTac autoSolve ist tac

812812 = do env <- get_env

813− no_errors $ runT (fmap (addImplBound ist (map fst env)) tac)

813+ g <- goal

814+ no_errors (runT (fmap (addImplBound ist (map fst env)) tac))

815+ (Just (CantSolveGoal g (map (\(n, b) -> (n, binderTy b)) env)))

814816 where

815817 runT (Intro []) = do g <- goal

816818 attack; intro (bname g)

@@ -1414,6 +1416,11 @@ reflectErr (CantConvert t t' ctxt) =

14141416 , reflect t'

14151417 , reflectCtxt ctxt

14161418 ]

1419+reflectErr (CantSolveGoal t ctxt) =

1420+ raw_apply (Var $ reflErrName "CantSolveGoal")

1421+ [ reflect t

1422+ , reflectCtxt ctxt

1423+ ]

14171424reflectErr (UnifyScope n n' t ctxt) =

14181425 raw_apply (Var $ reflErrName "UnifyScope")

14191426 [ reflectName n