5ce7362 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Type class resolution fix

Type class resolution should not proceed if there are metavariables in a goal at any stage, because (with the exception of 'Num') type class resolution should never be resolving metavariables. Fixes #1986

commit5ce73622ae3eb6a6fbef9da3714ad52cec4719ca authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 17 Mar 2015, 11:41 (12 years ago) parentb493858

6 files changed+84−37

compare with master

unifiedsplit

src/Idris/Core/Binary.hs+3−3 src/Idris/Core/DeepSeq.hs+1−1 src/Idris/Core/Elaborate.hs+30−14 src/Idris/Core/TT.hs+4−3 src/Idris/Delaborate.hs+1−1 src/Idris/ElabTerm.hs+45−15

src/Idris/Core/Binary.hs+3−3

@@ -91,8 +91,8 @@ instance Binary a => Binary (Err' a) where

9191 put x

9292 put y

9393 put z

94− put (CantResolve t) = do putWord8 15

95− put t

94+ put (CantResolve _ t) = do putWord8 15

95+ put t

9696 put (CantResolveAlts ns) = do putWord8 16

9797 put ns

9898 put (IncompleteTerm t) = do putWord8 17

@@ -172,7 +172,7 @@ instance Binary a => Binary (Err' a) where

172172 13 -> fmap NoTypeDecl get

173173 14 -> do x <- get ; y <- get ; z <- get

174174 return $ NotInjective x y z

175− 15 -> fmap CantResolve get

175+ 15 -> fmap (CantResolve False) get

176176 16 -> fmap CantResolveAlts get

177177 17 -> fmap IncompleteTerm get

178178 18 -> return UniverseError

src/Idris/Core/DeepSeq.hs+1−1

@@ -80,7 +80,7 @@ instance NFData Err where

8080 rnf (NoTypeDecl x1) = rnf x1 `seq` ()

8181 rnf (NotInjective x1 x2 x3)

8282 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

83− rnf (CantResolve x1) = rnf x1 `seq` ()

83+ rnf (CantResolve x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

8484 rnf (CantResolveAlts x1) = rnf x1 `seq` ()

8585 rnf (IncompleteTerm x1) = rnf x1 `seq` ()

8686 rnf UniverseError = ()

src/Idris/Core/Elaborate.hs+30−14

@@ -756,20 +756,20 @@ handleError p t1 t2 proofSearch

756756

757757try' :: Elab' aux a -> Elab' aux a -> Bool -> Elab' aux a

758758try' t1 t2 proofSearch

759− = do s <- get

760− ps <- get_probs

761− ulog <- getUnifyLog

762− case prunStateT 999999 False ps t1 s of

763− OK ((v, _, _), s') -> do put s'

764− return $! v

765− Error e1 -> traceWhen ulog ("try failed " ++ show e1) $

766− if recoverableErr e1 then

767− do case runStateT t2 s of

768− OK (v, s') -> do put s'; return $! v

769− Error e2 -> if score e1 >= score e2

770− then lift (tfail e1)

771− else lift (tfail e2)

772− else lift (tfail e1)

759+ = do s <- get

760+ ps <- get_probs

761+ ulog <- getUnifyLog

762+ case prunStateT 999999 False ps t1 s of

763+ OK ((v, _, _), s') -> do put s'

764+ return $! v

765+ Error e1 -> traceWhen ulog ("try failed " ++ show e1) $

766+ if recoverableErr e1 then

767+ do case runStateT t2 s of

768+ OK (v, s') -> do put s'; return $! v

769+ Error e2 -> if score e1 >= score e2

770+ then lift (tfail e1)

771+ else lift (tfail e2)

772+ else lift (tfail e1)

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

774774 = -- traceWhen r (show err) $

775775 r || proofSearch

@@ -782,6 +782,22 @@ try' t1 t2 proofSearch

782782 recoverableErr (ElabDebug _ _ _) = False

783783 recoverableErr _ = True

784784

785+tryCatch :: Elab' aux a -> (Err -> Elab' aux a) -> Elab' aux a

786+tryCatch t1 t2

787+ = do s <- get

788+ ps <- get_probs

789+ ulog <- getUnifyLog

790+ case prunStateT 999999 False ps t1 s of

791+ OK ((v, _, _), s') -> do put s'

792+ return $! v

793+ Error e1 -> traceWhen ulog ("tryCatch failed " ++ show e1) $

794+ case runStateT (t2 e1) s of

795+ OK (v, s') -> do put s'

796+ return $! v

797+ Error e2 -> if score e1 >= score e2

798+ then lift (tfail e1)

799+ else lift (tfail e2)

800+

785801tryWhen :: Bool -> Elab' aux a -> Elab' aux a -> Elab' aux a

786802tryWhen True a b = try a b

787803tryWhen False a b = a

src/Idris/Core/TT.hs+4−3

@@ -155,7 +155,8 @@ data Err' t

155155 | WithFnType t

156156 | NoTypeDecl Name

157157 | NotInjective t t t

158− | CantResolve t

158+ | CantResolve Bool -- ^ True if postponed, False if fatal

159+ t

159160 | CantResolveAlts [Name]

160161 | IncompleteTerm t

161162 | UniverseError

@@ -231,7 +232,7 @@ instance Sized Err where

231232 size (NoSuchVariable name) = size name

232233 size (NoTypeDecl name) = size name

233234 size (NotInjective l c r) = size l + size c + size r

234− size (CantResolve trm) = size trm

235+ size (CantResolve _ trm) = size trm

235236 size (NoRewriting trm) = size trm

236237 size (CantResolveAlts _) = 1

237238 size (IncompleteTerm trm) = size trm

@@ -246,7 +247,7 @@ instance Sized Err where

246247

247248score :: Err -> Int

248249score (CantUnify _ _ _ m _ s) = s + score m

249−score (CantResolve _) = 20

250+score (CantResolve _ _) = 20

250251score (NoSuchVariable _) = 1000

251252score (ProofSearchFail e) = score e

252253score (CantSolveGoal _ _) = 100000

src/Idris/Delaborate.hs+1−1

@@ -289,7 +289,7 @@ pprintErr' i (NotInjective p x y) =

289289 text "Can't verify injectivity of" <+> annTm p (pprintTerm i (delab i p)) <+>

290290 text " when unifying" <+> annTm x (pprintTerm i (delab i x)) <+> text "and" <+>

291291 annTm y (pprintTerm i (delab i y))

292−pprintErr' i (CantResolve c) = text "Can't resolve type class" <+> pprintTerm i (delab i c)

292+pprintErr' i (CantResolve _ c) = text "Can't resolve type class" <+> pprintTerm i (delab i c)

293293pprintErr' i (CantResolveAlts as) = text "Can't disambiguate name:" <+>

294294 align (cat (punctuate (comma <> space) (map (fmap (fancifyAnnots i) . annName) as)))

295295pprintErr' i (NoTypeDecl n) = text "No type declaration for" <+> annName n

src/Idris/ElabTerm.hs+45−15

@@ -64,7 +64,7 @@ build ist info emode opts fn tm

6464 mapM_ (\n -> when (n `elem` hs) $

6565 do focus n

6666 g <- goal

67− try (resolveTC True 7 g fn ist)

67+ try (resolveTC True False 7 g fn ist)

6868 (movelast n)) ivs

6969 ivs <- get_instances

7070 hs <- get_holes

@@ -72,7 +72,7 @@ build ist info emode opts fn tm

7272 mapM_ (\n -> when (n `elem` hs) $

7373 do focus n

7474 g <- goal

75− resolveTC True 7 g fn ist) ivs

75+ resolveTC True True 7 g fn ist) ivs

7676 tm <- get_term

7777 ctxt <- get_context

7878 probs <- get_probs

@@ -321,7 +321,7 @@ elab ist info emode opts fn tm

321321 UType _ -> elab' ina (Just fc) (PRef fc unitTy)

322322 _ -> elab' ina (Just fc) (PRef fc unitCon)

323323 elab' ina fc (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes

324− = do g <- goal; resolveTC False 5 g fn ist

324+ = do g <- goal; resolveTC False False 5 g fn ist

325325 elab' ina fc (PResolveTC fc')

326326 = do c <- getNameFrom (sMN 0 "class")

327327 instanceArg c

@@ -540,7 +540,7 @@ elab ist info emode opts fn tm

540540 g <- goal

541541 hs <- get_holes

542542 if all (\n -> n == tyn || not (n `elem` hs)) (freeNames g)

543− then try (resolveTC True 7 g fn ist)

543+ then try (resolveTC True False 7 g fn ist)

544544 (movelast n)

545545 else movelast n)

546546 (ivs' \\ ivs)

@@ -700,7 +700,7 @@ elab ist info emode opts fn tm

700700 env <- get_env

701701 hs <- get_holes

702702 if all (\n -> not (n `elem` hs)) (freeNames g)

703− then try (resolveTC False 7 g fn ist)

703+ then try (resolveTC False False 7 g fn ist)

704704 (movelast n)

705705 else movelast n)

706706 (ivs' \\ ivs)

@@ -1376,14 +1376,25 @@ proofSearch' ist rec ambigok depth prv top n hints

13761376-- Resolve type classes. This will only pick up 'normal' instances, never

13771377-- named instances (hence using 'tcname' to check it's a generated instance

13781378-- name).

1379−resolveTC :: Bool -> Int -> Term -> Name -> IState -> ElabD ()

1379+resolveTC :: Bool -- using default Int

1380+ -> Bool -- allow metavariables in the goal

1381+ -> Int -- depth

1382+ -> Term -- top level goal

1383+ -> Name -- top level function name

1384+ -> IState -> ElabD ()

13801385resolveTC = resTC' []

13811386

1382−resTC' tcs def 0 topg fn ist = fail $ "Can't resolve type class"

1383−resTC' tcs def 1 topg fn ist = try' (trivial' ist) (resolveTC def 0 topg fn ist) True

1384−resTC' tcs defaultOn depth topg fn ist

1385− = do compute

1386− g <- goal

1387+resTC' tcs def mvok 0 topg fn ist = fail $ "Can't resolve type class"

1388+resTC' tcs def mvok 1 topg fn ist = try' (trivial' ist) (resolveTC def mvok 0 topg fn ist) True

1389+resTC' tcs defaultOn mvok depth topg fn ist

1390+ = do compute

1391+ g <- goal

1392+ hs <- get_holes

1393+ let argsok = tcArgsOK g hs

1394+-- trace (show (g,hs,argsok,mvok)) $

1395+ if (not argsok && not mvok)

1396+ then lift $ tfail $ CantResolve True topg

1397+ else do

13871398 ptm <- get_term

13881399 ulog <- getUnifyLog

13891400 hs <- get_holes

@@ -1400,6 +1411,22 @@ resTC' tcs defaultOn depth topg fn ist

14001411 let depth' = if scopeOnly then 2 else depth

14011412 blunderbuss t depth' stk (stk ++ insts)) True

14021413 where

1414+ tcArgsOK ty hs | (P _ nc _, as) <- unApply ty, nc == numclass && defaultOn

1415+ = True

1416+ tcArgsOK ty hs -- if any arguments are metavariables, postpone

1417+ = let (f, as) = unApply ty in

1418+ not $ any (isMeta hs) as

1419+

1420+ isMeta :: [Name] -> Term -> Bool

1421+ isMeta ns (P _ n _) = n `elem` ns

1422+ isMeta _ _ = False

1423+

1424+ notHole hs (P _ n _, c)

1425+ | (P _ cn _, _) <- unApply c,

1426+ n `elem` hs && isConName cn (tt_ctxt ist) = False

1427+ | Constant _ <- c = not (n `elem` hs)

1428+ notHole _ _ = True

1429+

14031430 elabTC n | n /= fn && tcname n = (resolve n depth, show n)

14041431 | otherwise = (fail "Can't resolve", show n)

14051432

@@ -1427,10 +1454,13 @@ resTC' tcs defaultOn depth topg fn ist

14271454

14281455 blunderbuss t d stk [] = do -- c <- get_env

14291456 -- ps <- get_probs

1430− lift $ tfail $ CantResolve topg

1457+ lift $ tfail $ CantResolve False topg

14311458 blunderbuss t d stk (n:ns)

14321459 | n /= fn && (n `elem` stk || tcname n)

1433− = try' (resolve n d) (blunderbuss t d stk ns) True

1460+ = tryCatch (resolve n d)

1461+ (\e -> case e of

1462+ CantResolve True _ -> lift $ tfail e

1463+ _ -> blunderbuss t d stk ns)

14341464 | otherwise = blunderbuss t d stk ns

14351465

14361466 resolve n depth

@@ -1459,7 +1489,7 @@ resTC' tcs defaultOn depth topg fn ist

14591489 let got = fst (unApply t)

14601490 let depth' = if tc' `elem` tcs

14611491 then depth - 1 else depth

1462− resTC' (got : tcs) defaultOn depth' topg fn ist)

1492+ resTC' (got : tcs) defaultOn mvok depth' topg fn ist)

14631493 (filter (\ (x, y) -> not x) (zip (map fst imps) args))

14641494 -- if there's any arguments left, we've failed to resolve

14651495 hs <- get_holes

@@ -2604,7 +2634,7 @@ reflectErr (NotInjective t1 t2 t3) =

26042634 , reflect t2

26052635 , reflect t3

26062636 ]

2607−reflectErr (CantResolve t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]

2637+reflectErr (CantResolve _ t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]

26082638reflectErr (CantResolveAlts ss) =

26092639 raw_apply (Var $ reflErrName "CantResolveAlts")

26102640 [rawList (Var $ reflm "TTName") (map reflectName ss)]