e1c79ef · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Better error when no alternative is valid

Instead of guessing the error for the thing that's closest to working, better to say that no alternative works. (This makes the bizarre 'score' heuristic for error messages obsolete, so that'll be removed soon too.)

commite1c79ef07df78f7abebe6ba44e4da6eba7f1476f authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 17 Jul 2015, 23:36 (11 years ago) parent452b3c6

9 files changed+25−4

compare with master

unifiedsplit

libs/base/Language/Reflection/Utils.idr+1 libs/prelude/Language/Reflection/Errors.idr+1 src/Idris/Core/Binary.hs+3 src/Idris/Core/DeepSeq.hs+1 src/Idris/Core/Elaborate.hs+5−2 src/Idris/Core/TT.hs+2 src/Idris/Delaborate.hs+2 src/Idris/Elab/Term.hs+8 test/dsl004/Door1.idr+2−2

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

@@ -302,6 +302,7 @@ instance Show Err where

302302 showPrec d (CantResolve tm) = showCon d "CantResolve" $ showArg tm

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

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

305+ showPrec d (NoValidAlts xs) = showCon d "NoValidAlts" $ showArg xs

305306 showPrec d (IncompleteTerm tm) = showCon d "IncompleteTerm" $ showArg tm

306307 showPrec d (NoEliminator s tm) = showCon d "NoEliminator" $ showArg s ++ showArg tm

307308 showPrec d UniverseError = "UniverseError"

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

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

3131 | CantResolve TT

3232 | InvalidTCArg TTName TT

3333 | CantResolveAlts (List TTName)

34+ | NoValidAlts (List TTName)

3435 | IncompleteTerm TT

3536 | NoEliminator String TT

3637 | UniverseError

src/Idris/Core/Binary.hs+3

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

184184 put (UnknownImplicit n f) = do putWord8 40

185185 put n

186186 put f

187+ put (NoValidAlts ns) = do putWord8 41

188+ put ns

187189

188190 get = do i <- getWord8

189191 case i of

@@ -253,6 +255,7 @@ instance Binary a => Binary (Err' a) where

253255 return (ElabScriptStuck x1)

254256 40 -> do x <- get ; y <- get

255257 return $ UnknownImplicit x y

258+ 41 -> fmap NoValidAlts get

256259 _ -> error "Corrupted binary data for Err'"

257260----- Generated by 'derive'

258261

src/Idris/Core/DeepSeq.hs+1

@@ -93,6 +93,7 @@ instance NFData Err where

9393 rnf (CantResolve x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

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

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

96+ rnf (NoValidAlts x1) = rnf x1 `seq` ()

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

9798 rnf (NoEliminator x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

9899 rnf (UniverseError x1 x2 x3 x4 x5) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

src/Idris/Core/Elaborate.hs+5−2

@@ -806,7 +806,7 @@ try' t1 t2 proofSearch

806806 = -- traceWhen r (show err) $

807807 r || proofSearch

808808 recoverableErr (CantSolveGoal _ _) = False

809− recoverableErr (CantResolveAlts _) = False

809+ recoverableErr (CantResolveAlts _) = proofSearch

810810 recoverableErr (ProofSearchFail (Msg _)) = True

811811 recoverableErr (ProofSearchFail _) = False

812812 recoverableErr (ElaboratingArg _ _ _ e) = recoverableErr e

@@ -844,6 +844,9 @@ tryAll xs = tryAll' [] 999999 (cantResolve, 0) xs

844844 cantResolve :: Elab' aux a

845845 cantResolve = lift $ tfail $ CantResolveAlts (map snd xs)

846846

847+ noneValid :: Elab' aux a

848+ noneValid = lift $ tfail $ NoValidAlts (map snd xs)

849+

847850 tryAll' :: [Elab' aux a] -> -- successes

848851 Int -> -- most problems

849852 (Elab' aux a, Int) -> -- smallest failure

@@ -851,7 +854,7 @@ tryAll xs = tryAll' [] 999999 (cantResolve, 0) xs

851854 Elab' aux a

852855 tryAll' [res] pmax _ [] = res

853856 tryAll' (_:_) pmax _ [] = cantResolve

854− tryAll' [] pmax (f, _) [] = f

857+ tryAll' [] pmax (f, _) [] = noneValid

855858 tryAll' cs pmax f ((x, msg):xs)

856859 = do s <- get

857860 ps <- get_probs

src/Idris/Core/TT.hs+2

@@ -266,6 +266,7 @@ data Err' t

266266 t

267267 | InvalidTCArg Name t

268268 | CantResolveAlts [Name]

269+ | NoValidAlts [Name]

269270 | IncompleteTerm t

270271 | NoEliminator String t

271272 | UniverseError FC UExp (Int, Int) (Int, Int) [ConstraintFC]

@@ -360,6 +361,7 @@ instance Sized Err where

360361score :: Err -> Int

361362score (CantUnify _ _ _ m _ s) = 1 + s + score m

362363score (CantResolve _ _) = 20

364+score (NoValidAlts _) = 0

363365score (NoSuchVariable _) = 1000

364366score (ProofSearchFail e) = score e

365367score (CantSolveGoal _ _) = 100000

src/Idris/Delaborate.hs+2

@@ -344,6 +344,8 @@ pprintErr' i (InvalidTCArg n t)

344344 text "(Type class arguments must be injective)"

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

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

347+pprintErr' i (NoValidAlts as) = text "Can't disambiguate since no alternative is valid:" <+>

348+ indented (align (cat (punctuate (comma <> space) (map (fmap (fancifyAnnots i True) . annName) as))))

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

348350pprintErr' i (NoSuchVariable n) = text "No such variable" <+> annName n

349351pprintErr' i (WithFnType ty) =

src/Idris/Elab/Term.hs+8

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

512512 recoverableErr (TooManyArguments _) = False

513513 recoverableErr (CantSolveGoal _ _) = False

514514 recoverableErr (CantResolveAlts _) = False

515+ recoverableErr (NoValidAlts _) = True

515516 recoverableErr (ProofSearchFail (Msg _)) = True

516517 recoverableErr (ProofSearchFail _) = False

517518 recoverableErr (ElaboratingArg _ _ _ e) = recoverableErr e

@@ -526,6 +527,7 @@ elab ist info emode opts fn tm

526527 _ -> filter isLend alts -- special case hack for 'Borrowed'

527528 pruneAlts (ElaboratingArg _ _ _ e) alts env = pruneAlts e alts env

528529 pruneAlts (At _ e) alts env = pruneAlts e alts env

530+ pruneAlts (NoValidAlts _) alts env = alts

529531 pruneAlts _ alts _ = filter isLend alts

530532

531533 hasArg n env ap | isLend ap = True -- special case hack for 'Borrowed'

@@ -1377,6 +1379,12 @@ elab ist info emode opts fn tm

13771379 (t : map (mkCoerce env t) cs)

13781380 return t'

13791381 where

1382+-- mkCoerce env (PAlternative ns aty alts@(a : as)) n

1383+-- = let fc = maybe (fileFC "Coercion") id (highestFC a) in

1384+-- addImplBound ist (map fst env)

1385+-- (PAlternative ns aty

1386+-- (map (\t -> PApp fc (PRef fc n) [pexp (PCoerced t)])

1387+-- alts))

13801388 mkCoerce env t n = let fc = maybe (fileFC "Coercion") id (highestFC t) in

13811389 addImplBound ist (map fst env)

13821390 (PApp fc (PRef fc [] n) [pexp (PCoerced t)])

test/dsl004/Door1.idr+2−2

@@ -30,8 +30,8 @@ action : DoorCmd a -> DoorLang a

3030action = Action

3131

3232testProg : DoorH CLOSED -> DoorLang ()

33−testProg h = do h <- Knock h

33+testProg h = with Main, Show do -- h <- Knock h

3434 h <- Open h

35− h <- Close h

35+ -- h <- Close h

3636 Return ()

3737