ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-09-19 13:07:15 +03:00
Code Issues Projects Releases Wiki Activity

Better disambiguation with type class methods

Browse Source 
If a type class resolution fails in an unrecoverable way (i.e., it
hasn't been postponed due to missing arguments) then it won't be one of
the things we're choosing between in type-based disambiguation, so rule
it out.

Fixes #2701
This commit is contained in:
Edwin Brady 2015-10-18 00:39:19 +01:00
parent c6a8862798
commit c7bed76d1f
2 changed files with 15 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
src/Idris/Elab/Term.hs
View File

@ -714,8 +714,9 @@ elab ist info emode opts fn tm
g <- goal g <- goal
hs <- get_holes hs <- get_holes
if all (\n -> n == tyn || not (n `elem` hs)) (freeNames g) if all (\n -> n == tyn || not (n `elem` hs)) (freeNames g)
then try (resolveTC' True False 10 g fn ist) then handleError (tcRecoverable emode)
(movelast n) (resolveTC' True False 10 g fn ist)
(movelast n)
else movelast n) else movelast n)
(ivs' \\ ivs) (ivs' \\ ivs)
-- HACK: If the name leaks into its type, it may leak out of -- HACK: If the name leaks into its type, it may leak out of
@ -886,7 +887,8 @@ elab ist info emode opts fn tm
env <- get_env env <- get_env
hs <- get_holes hs <- get_holes
if all (\n -> not (n `elem` hs)) (freeNames g) if all (\n -> not (n `elem` hs)) (freeNames g)
then try (resolveTC' False False 10 g fn ist) then handleError (tcRecoverable emode)
(resolveTC' False False 10 g fn ist)
(movelast n) (movelast n)
else movelast n) else movelast n)
(ivs' \\ ivs) (ivs' \\ ivs)
@ -1672,6 +1674,15 @@ solveAutos ist fn ambigok
= do autos <- get_autos = do autos <- get_autos
mapM_ (solveAuto ist fn ambigok) (map (\(n, (fc, _)) -> (n, fc)) autos) mapM_ (solveAuto ist fn ambigok) (map (\(n, (fc, _)) -> (n, fc)) autos)
-- Return true if the given error suggests a type class failure is
-- recoverable
tcRecoverable :: ElabMode -> Err -> Bool
tcRecoverable ERHS (CantResolve f g) = f
tcRecoverable ETyDecl (CantResolve f g) = f
tcRecoverable e (ElaboratingArg _ _ _ err) = tcRecoverable e err
tcRecoverable e (At _ err) = tcRecoverable e err
tcRecoverable _ _ = True
trivial' ist trivial' ist
= trivial (elab ist toplevel ERHS [] (sMN 0 "tac")) ist = trivial (elab ist toplevel ERHS [] (sMN 0 "tac")) ist
trivialHoles' psn h ist trivialHoles' psn h ist

4
src/Idris/ProofSearch.hs
View File

@ -462,9 +462,7 @@ resTC' tcs defaultOn topholes depth topg fn elab ist
boundVar (P Bound _ _) = True boundVar (P Bound _ _) = True
boundVar _ = False boundVar _ = False
blunderbuss t d stk [] = do -- c <- get_env blunderbuss t d stk [] = lift $ tfail $ CantResolve False topg
-- ps <- get_probs
lift $ tfail $ CantResolve False topg
blunderbuss t d stk (n:ns) blunderbuss t d stk (n:ns)
| n /= fn -- && (n `elem` stk) | n /= fn -- && (n `elem` stk)
= tryCatch (resolve n d) = tryCatch (resolve n d)