1cf8fe9 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Context for "Can't find implementation"

Sometimes this is caused by an earlier type error which the elaborator thinks it may be able to resolve later (but then can't), so provide that error as additional context.

commit1cf8fe9a75201d1689bed14afea8f6c22815ac2e authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 11 Feb 2016, 15:06 (11 years ago) parentf2eaf90

11 files changed+33−19

compare with master

unifiedsplit

libs/base/Language/Reflection/Utils.idr+1−1 libs/prelude/Language/Reflection/Errors.idr+1−1 libs/prelude/Prelude.idr+2−2 src/Idris/Core/Binary.hs+4−3 src/Idris/Core/DeepSeq.hs+1−1 src/Idris/Core/TT.hs+3−3 src/Idris/Delaborate.hs+7−1 src/Idris/Elab/Term.hs+2−2 src/Idris/IBC.hs+1−1 src/Idris/ProofSearch.hs+9−3 src/Idris/Reflection.hs+2−1

libs/base/Language/Reflection/Utils.idr+1−1

@@ -303,7 +303,7 @@ implementation Show Err where

303303 showPrec d (CantMatch tm) = showCon d "CantMatch" $ showArg tm

304304 showPrec d (NoTypeDecl n) = showCon d "NoTypeDecl" $ showArg n

305305 showPrec d (NotInjective tm tm' x) = showCon d "NotInjective" $ showArg tm ++ showArg tm'

306− showPrec d (CantResolve tm) = showCon d "CantResolve" $ showArg tm

306+ showPrec d (CantResolve tm e) = showCon d "CantResolve" $ showArg tm ++ showArg e

307307 showPrec d (InvalidTCArg n tm) = showCon d "InvalidTCName" $ showArg n ++ showArg tm

308308 showPrec d (CantResolveAlts xs) = showCon d "CantResolveAlts" $ showArg xs

309309 showPrec d (NoValidAlts xs) = showCon d "NoValidAlts" $ showArg xs

libs/prelude/Language/Reflection/Errors.idr+1−1

@@ -30,7 +30,7 @@ data Err = Msg String

3030 | CantMatch TT

3131 | NoTypeDecl TTName

3232 | NotInjective TT TT TT

33− | CantResolve TT

33+ | CantResolve TT Err

3434 | InvalidTCArg TTName TT

3535 | CantResolveAlts (List TTName)

3636 | NoValidAlts (List TTName)

libs/prelude/Prelude.idr+2−2

@@ -272,7 +272,7 @@ cast_part x = TermPart x

272272

273273%error_handler export

274274cast_error : Err -> Maybe (List ErrorReportPart)

275−cast_error (CantResolve `(Cast ~x ~y))

275+cast_error (CantResolve `(Cast ~x ~y) _)

276276 = Just [TextPart "Can't cast from",

277277 cast_part x,

278278 TextPart "to",

@@ -282,6 +282,6 @@ cast_error _ = Nothing

282282%error_handler

283283export

284284num_error : Err -> Maybe (List ErrorReportPart)

285−num_error (CantResolve `(Num ~x))

285+num_error (CantResolve `(Num ~x) _)

286286 = Just [TermPart x, TextPart "is not a numeric type"]

287287num_error _ = Nothing

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

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

113113 put x

114114 put y

115115 put z

116− put (CantResolve _ t) = do putWord8 15

117− put t

116+ put (CantResolve _ t u) = do putWord8 15

117+ put t

118+ put u

118119 put (CantResolveAlts ns) = do putWord8 16

119120 put ns

120121 put (IncompleteTerm t) = do putWord8 17

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

218219 13 -> fmap NoTypeDecl get

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

220221 return $ NotInjective x y z

221− 15 -> fmap (CantResolve False) get

222+ 15 -> CantResolve False <$> get <*> get

222223 16 -> fmap CantResolveAlts get

223224 17 -> fmap IncompleteTerm get

224225 18 -> UniverseError <$> get <*> get <*> get <*> get <*> get

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

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

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

135135 rnf (NotInjective x1 x2 x3)

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

137− rnf (CantResolve x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

137+ rnf (CantResolve x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

138138 rnf (InvalidTCArg x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

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

140140 rnf (NoValidAlts x1) = rnf x1 `seq` ()

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

@@ -268,7 +268,7 @@ data Err' t

268268 | NoTypeDecl Name

269269 | NotInjective t t t

270270 | CantResolve Bool -- True if postponed, False if fatal

271− t

271+ t (Err' t) -- any further information

272272 | InvalidTCArg Name t

273273 | CantResolveAlts [Name]

274274 | NoValidAlts [Name]

@@ -354,7 +354,7 @@ instance Sized Err where

354354 size (NoSuchVariable name) = size name

355355 size (NoTypeDecl name) = size name

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

357− size (CantResolve _ trm) = size trm

357+ size (CantResolve _ trm _) = size trm

358358 size (NoRewriting trm) = size trm

359359 size (CantResolveAlts _) = 1

360360 size (IncompleteTerm trm) = size trm

@@ -397,7 +397,7 @@ instance Show Err where

397397 show (WithFnType _) = "WithFnType"

398398 show (NoTypeDecl _) = "NoTypeDecl"

399399 show (NotInjective _ _ _) = "NotInjective"

400− show (CantResolve _ _) = "CantResolve"

400+ show (CantResolve _ _ _) = "CantResolve"

401401 show (InvalidTCArg _ _) = "InvalidTCArg"

402402 show (CantResolveAlts _) = "CantResolveAlts"

403403 show (NoValidAlts _) = "NoValidAlts"

src/Idris/Delaborate.hs+7−1

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

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

347347 text " when unifying" <+> annTm x (pprintTerm i (delabSugared i x)) <+> text "and" <+>

348348 annTm y (pprintTerm i (delabSugared i y))

349−pprintErr' i (CantResolve _ c) = text "Can't find implementation for" <+> pprintTerm i (delabSugared i c)

349+pprintErr' i (CantResolve _ c e)

350+ = text "Can't find implementation for" <+> pprintTerm i (delabSugared i c)

351+ <>

352+ case e of

353+ Msg "" -> empty

354+ _ -> line <> line <> text "Possible cause:" <>

355+ indented (pprintErr' i e)

350356pprintErr' i (InvalidTCArg n t)

351357 = annTm t (pprintTerm i (delabSugared i t)) <+> text " cannot be a parameter of "

352358 <> annName n <$>

src/Idris/Elab/Term.hs+2−2

@@ -1704,8 +1704,8 @@ solveAutos ist fn ambigok

17041704-- Return true if the given error suggests a type class failure is

17051705-- recoverable

17061706tcRecoverable :: ElabMode -> Err -> Bool

1707−tcRecoverable ERHS (CantResolve f g) = f

1708−tcRecoverable ETyDecl (CantResolve f g) = f

1707+tcRecoverable ERHS (CantResolve f g _) = f

1708+tcRecoverable ETyDecl (CantResolve f g _) = f

17091709tcRecoverable e (ElaboratingArg _ _ _ err) = tcRecoverable e err

17101710tcRecoverable e (At _ err) = tcRecoverable e err

17111711tcRecoverable _ _ = True

src/Idris/IBC.hs+1−1

@@ -40,7 +40,7 @@ import System.Directory

4040import Codec.Archive.Zip

4141

4242ibcVersion :: Word16

43−ibcVersion = 132

43+ibcVersion = 133

4444

4545-- When IBC is being loaded - we'll load different things (and omit different

4646-- structures/definitions) depending on which phase we're in

src/Idris/ProofSearch.hs+9−3

@@ -383,8 +383,10 @@ resTC' tcs defaultOn topholes depth topg fn elab ist

383383 let (argsok, okholePos) = case tcArgsOK g topholes of

384384 Nothing -> (False, [])

385385 Just hs -> (True, hs)

386+ env <- get_env

387+ probs <- get_probs

386388 if not argsok -- && not mvok)

387− then lift $ tfail $ CantResolve True topg

389+ then lift $ tfail $ CantResolve True topg (probErr probs)

388390 else do

389391 ptm <- get_term

390392 ulog <- getUnifyLog

@@ -431,6 +433,9 @@ resTC' tcs defaultOn topholes depth topg fn elab ist

431433 _ -> Just rs

432434 tcDetArgsOK _ _ _ [] = Just []

433435

436+ probErr [] = Msg ""

437+ probErr ((_,_,_,_,err,_,_) : _) = err

438+

434439 isMeta :: [Name] -> Term -> Bool

435440 isMeta ns (P _ n _) = n `elem` ns

436441 isMeta _ _ = False

@@ -462,12 +467,13 @@ resTC' tcs defaultOn topholes depth topg fn elab ist

462467 boundVar (P Bound _ _) = True

463468 boundVar _ = False

464469

465− blunderbuss t d stk [] = lift $ tfail $ CantResolve False topg

470+ blunderbuss t d stk [] = do ps <- get_probs

471+ lift $ tfail $ CantResolve False topg (probErr ps)

466472 blunderbuss t d stk (n:ns)

467473 | n /= fn -- && (n `elem` stk)

468474 = tryCatch (resolve n d)

469475 (\e -> case e of

470− CantResolve True _ -> lift $ tfail e

476+ CantResolve True _ _ -> lift $ tfail e

471477 _ -> blunderbuss t d stk ns)

472478 | otherwise = blunderbuss t d stk ns

473479

src/Idris/Reflection.hs+2−1

@@ -896,7 +896,8 @@ reflectErr (NotInjective t1 t2 t3) =

896896 , reflect t2

897897 , reflect t3

898898 ]

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

899+reflectErr (CantResolve _ t more)

900+ = raw_apply (Var $ reflErrName "CantResolve") [reflect t, reflectErr more]

900901reflectErr (InvalidTCArg n t) = raw_apply (Var $ reflErrName "InvalidTCArg") [reflectName n, reflect t]

901902reflectErr (CantResolveAlts ss) =

902903 raw_apply (Var $ reflErrName "CantResolveAlts")