aed179c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Track the providence of unification errors

Unification errors can now be wrapped in a constructor specifying what function was being applied when they were generated, where it was in the source, and which argument of the function had a problem.

commitaed179ced806ea10edbe32c19ff25ce4a520230f authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateThu 20 Mar 2014, 17:04 (13 years ago) parentff742fe

8 files changed+51−18

compare with master

unifiedsplit

src/Idris/Core/Elaborate.hs+1 src/Idris/Core/TT.hs+4−1 src/Idris/Core/Unify.hs+17−11 src/Idris/Delaborate.hs+19−2 src/Idris/ElabDecls.hs+1−1 src/Idris/ElabTerm.hs+5−2 src/Idris/Error.hs+3 src/Idris/ParseOps.hs+1−1

src/Idris/Core/Elaborate.hs+1

@@ -687,6 +687,7 @@ try' t1 t2 proofSearch

687687 r || proofSearch

688688 recoverableErr (CantSolveGoal _ _) = False

689689 recoverableErr (ProofSearchFail _) = False

690+ recoverableErr (ElaboratingArg _ _ _ e) = recoverableErr e

690691 recoverableErr _ = True

691692

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

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

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

140140 | NoRewriting t

141141 | At FC (Err' t)

142142 | Elaborating String Name (Err' t)

143− | ElaboratingArg Name Name (Err' t)

143+ | ElaboratingArg FC Name Name (Err' t)

144144 | ProviderError String

145145 | LoadingFailed String (Err' t)

146146 | ReflectionError [[ErrorReportPart]] (Err' t)

@@ -171,6 +171,7 @@ instance Sized Err where

171171 size ProgramLineComment = 1

172172 size (At fc err) = size fc + size err

173173 size (Elaborating _ n err) = size err

174+ size (ElaboratingArg _ _ _ err) = size err

174175 size (ProviderError msg) = length msg

175176 size (LoadingFailed fn e) = 1 + length fn + size e

176177 size _ = 1

@@ -195,6 +196,8 @@ instance Show Err where

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

196197 show ProgramLineComment = "Program line next to comment"

197198 show (At f e) = show f ++ ":" ++ show e

199+ show (ElaboratingArg fc f x e) = show fc ++ ": Elaborating " ++ show f ++ " arg " ++

200+ show x ++ ": " ++ show e

198201 show _ = "Error"

199202

200203instance Pretty Err OutputAnnotation where

src/Idris/Core/Unify.hs+17−11

@@ -37,6 +37,12 @@ data UResult a = UOK a

3737 | UPartOK a

3838 | UFail Err

3939

40+-- | Smart constructor for unification errors that takes into account the FailContext

41+cantUnify :: [FailContext] -> Bool -> t -> t -> (Err' t) -> [(Name, t)] -> Int -> Err' t

42+cantUnify [] r t1 t2 e ctxt i = CantUnify r t1 t2 e ctxt i

43+cantUnify (FailContext fc f x : _) r t1 t2 e ctxt i =

44+ ElaboratingArg fc f x (CantUnify r t1 t2 e ctxt i)

45+

4046-- Solve metavariables by matching terms against each other

4147-- Not really unification, of course!

4248

@@ -89,7 +95,7 @@ match_unify ctxt env topx topy inj holes from =

8995 | OK True <- convEq' ctxt holes x y = do sc 1; return []

9096 | otherwise = do UI s f <- get

9197 let r = recoverable x y

92− let err = CantUnify r

98+ let err = cantUnify from r

9399 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

94100 if (not r) then lift $ tfail err

95101 else do put (UI s ((x, y, env, err, from, Match) : f))

@@ -103,9 +109,9 @@ match_unify ctxt env topx topy inj holes from =

103109 uB bnames (Pi tx) (Pi ty) = un bnames tx ty

104110 uB bnames x y = do UI s f <- get

105111 let r = recoverable (binderTy x) (binderTy y)

106− let err = CantUnify r topx topy

107− (CantUnify r (binderTy x) (binderTy y) (Msg "") (errEnv env) s)

108− (errEnv env) s

112+ let err = cantUnify from r topx topy

113+ (CantUnify r (binderTy x) (binderTy y) (Msg "") (errEnv env) s)

114+ (errEnv env) s

109115 put (UI s ((binderTy x, binderTy y, env, err, from, Match) : f))

110116 return []

111117

@@ -117,7 +123,7 @@ match_unify ctxt env topx topy inj holes from =

117123

118124 unifyFail x y = do UI s f <- get

119125 let r = recoverable x y

120− let err = CantUnify r

126+ let err = cantUnify from r

121127 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

122128 put (UI s ((x, y, env, err, from, Match) : f))

123129 lift $ tfail err

@@ -370,7 +376,7 @@ unify ctxt env topx topy inj holes from =

370376 | OK True <- convEq' ctxt holes x y = do sc 1; return []

371377 | otherwise = do UI s f <- get

372378 let r = recoverable x y

373− let err = CantUnify r

379+ let err = cantUnify from r

374380 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

375381 if (not r) then lift $ tfail err

376382 else do put (UI s ((x, y, env, err, from, Unify) : f))

@@ -470,7 +476,7 @@ unify ctxt env topx topy inj holes from =

470476 unifyTmpFail x y

471477 = do UI s f <- get

472478 let r = recoverable x y

473− let err = CantUnify r

479+ let err = cantUnify from r

474480 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

475481 put (UI s ((topx, topy, env, err, from, Unify) : f))

476482 return []

@@ -478,7 +484,7 @@ unify ctxt env topx topy inj holes from =

478484 -- shortcut failure, if we *know* nothing can fix it

479485 unifyFail x y = do UI s f <- get

480486 let r = recoverable x y

481− let err = CantUnify r

487+ let err = cantUnify from r

482488 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

483489 put (UI s ((topx, topy, env, err, from, Unify) : f))

484490 lift $ tfail err

@@ -500,9 +506,9 @@ unify ctxt env topx topy inj holes from =

500506 uB bnames (PVar tx) (PVar ty) = un' False bnames tx ty

501507 uB bnames x y = do UI s f <- get

502508 let r = recoverable (binderTy x) (binderTy y)

503− let err = CantUnify r topx topy

504− (CantUnify r (binderTy x) (binderTy y) (Msg "") (errEnv env) s)

505− (errEnv env) s

509+ let err = cantUnify from r topx topy

510+ (CantUnify r (binderTy x) (binderTy y) (Msg "") (errEnv env) s)

511+ (errEnv env) s

506512 put (UI s ((binderTy x, binderTy y, env, err, from, Unify) : f))

507513 return [] -- lift $ tfail err

508514

src/Idris/Delaborate.hs+19−2

@@ -1,5 +1,4 @@

11{-# LANGUAGE PatternGuards #-}

2−

32module Idris.Delaborate (bugaddr, delab, delab', delabMV, delabTy, delabTy', pshow, pprintErr) where

54-- Convert core TT back into high level syntax, primarily for display

@@ -13,6 +12,7 @@ import Idris.Core.Evaluate

1312import Idris.ErrReverse

1413

1514import Data.List (intersperse)

15+import qualified Data.Text as T

1616

1717import Debug.Trace

1818

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

200200 pprintTerm i (delab i y)

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

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

203− cat (punctuate (comma <> space) (map text as))

203+ align (cat (punctuate (comma <> space) (map text as)))

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

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

206206pprintErr' i (IncompleteTerm t) = text "Incomplete term" <+> pprintTerm i (delab i t)

@@ -217,6 +217,17 @@ pprintErr' i (At f e) = annotate (AnnFC f) (text (show f)) <> colon <> pprintErr

217217pprintErr' i (Elaborating s n e) = text "When elaborating" <+> text s <>

218218 annName' n (showqual i n) <> colon <$>

219219 pprintErr' i e

220+pprintErr' i (ElaboratingArg fc f x e)

221+ | isUN x =

222+ annotate (AnnFC fc) (text (show fc)) <> colon <+>

223+ text "When elaborating argument" <+>

224+ annotate (AnnBoundName x False) (text (showbasic x)) <+> --TODO check plicity

225+ text "to function" <+> annName f <> colon <>

226+ indented (pprintErr' i e)

227+ | otherwise =

228+ annotate (AnnFC fc) (text (show fc)) <> colon <+>

229+ text "When elaborating an application of function" <+>

230+ annName f <> colon <> indented (pprintErr' i e)

220231pprintErr' i (ProviderError msg) = text ("Type provider error: " ++ msg)

221232pprintErr' i (LoadingFailed fn e) = text "Loading" <+> text fn <+> text "failed:" <+> pprintErr' i e

222233pprintErr' i (ReflectionError parts orig) =

@@ -235,6 +246,11 @@ pprintErr' i (ReflectionFailed msg err) =

235246 indented (pprintErr' i err) <>

236247 text ("This is probably a bug. Please consider reporting it at " ++ bugaddr)

237248

249+isUN :: Name -> Bool

250+isUN (UN n) = not $ T.isPrefixOf (T.pack "__") n -- TODO figure out why MNs are getting rewritte to UNs for top-level pattern-matching functions

251+isUN (NS n _) = isUN n

252+isUN _ = False

253+

238254annName :: Name -> Doc OutputAnnotation

239255annName n = annName' n (showbasic n)

240256

@@ -259,6 +275,7 @@ showqual i n = showName (Just i) [] False False (dens n)

259275 _ -> ns

260276 dens n = n

261277

278+showbasic :: Name -> String

262279showbasic n@(UN _) = show n

263280showbasic (MN _ s) = str s

264281showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n

src/Idris/ElabDecls.hs+1−1

@@ -693,7 +693,6 @@ elabProvider info syn fc what n ty tm

693693 , prov == txt "Provider" && provs == txt "Providers" = True

694694 isProviderOf _ _ = False

695695

696−-- | Elaborate a type provider

697696elabTransform :: ElabInfo -> FC -> Bool -> PTerm -> PTerm -> Idris ()

698697elabTransform info fc safe lhs_in rhs_in

699698 = do ctxt <- getContext

@@ -1280,6 +1279,7 @@ checkPossible info fc tcgen fname lhs_in

12801279 impossibleError (CantConvert _ _ _) = False

12811280 impossibleError (At _ e) = impossibleError e

12821281 impossibleError (Elaborating _ _ e) = impossibleError e

1282+ impossibleError (ElaboratingArg _ _ _ e) = impossibleError e

12831283 impossibleError _ = True

12841284

12851285 sameFam topx topy

src/Idris/ElabTerm.hs+5−2

@@ -189,6 +189,7 @@ elab ist info pattern opts fn tm

189189 | (P _ (UN ht) _, _) <- unApply t,

190190 ht == txt "Lazy" = True

191191 forceErr (Elaborating _ _ t) = forceErr t

192+ forceErr (ElaboratingArg _ _ _ t) = forceErr t

192193 forceErr (At _ t) = forceErr t

193194 forceErr t = False

194195

@@ -802,6 +803,7 @@ pruneAlt xs = map prune xs

802803 case fs of

803804 [a] -> a

804805 _ -> PAlternative a as'

806+

805807 choose f (PApp fc f' as) = PApp fc (choose f f') (fmap (fmap (choose f)) as)

806808 choose f t = t

807809

@@ -1113,9 +1115,9 @@ runTac autoSolve ist fn tac

11131115 runReflected tactic

11141116 where tacticTy = Var (reflm "Tactic")

11151117 listTy = Var (sNS (sUN "List") ["List", "Prelude"])

1116− scriptTy = (RBind (sUN "__pi_arg")

1118+ scriptTy = (RBind (sMN 0 "__pi_arg")

11171119 (Pi (RApp listTy envTupleType))

1118− (RBind (sUN "__pi_arg1")

1120+ (RBind (sMN 1 "__pi_arg")

11191121 (Pi (Var $ reflm "TT")) tacticTy))

11201122 runT (ByReflection tm) -- run the reflection function 'tm' on the

11211123 -- goal, then apply the resulting reflected Tactic

@@ -1641,6 +1643,7 @@ withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)

16411643 handle e@(Elaborating what n err) = do logLvl 3 "Reflecting body of Elaborating"

16421644 err' <- handle err

16431645 return (Elaborating what n err')

1646+ -- TODO: argument-specific error handlers go here for ElaboratingArg

16441647 handle e = do ist <- getIState

16451648 let err = fmap (errReverse ist) e

16461649 logLvl 2 "Starting error reflection"

src/Idris/Error.hs+3

@@ -57,6 +57,8 @@ ierror = throwError

5757tclift :: TC a -> Idris a

5858tclift (OK v) = return v

5959tclift (Error err@(At fc e)) = do setErrSpan fc; throwError err

60+tclift (Error err@(ElaboratingArg fc _ _ e)) = do setErrSpan fc

61+ throwError err

6062tclift (Error err) = throwError err

6163

6264tctry :: TC a -> TC a -> Idris a

@@ -67,4 +69,5 @@ tctry tc1 tc2

6769

6870getErrSpan :: Err -> FC

6971getErrSpan (At fc _) = fc

72+getErrSpan (ElaboratingArg fc _ _ e) = fc

7073getErrSpan _ = emptyFC

src/Idris/ParseOps.hs+1−1

@@ -39,7 +39,7 @@ table fixes

3939 [[backtick],

4040 [binary "$" (\fc x y -> PApp fc x [pexp y]) AssocRight],

4141 [binary "=" PEq AssocLeft],

42− [binary "->" (\fc x y -> PPi expl (sUN "__pi_arg") x y) AssocRight]]

42+ [binary "->" (\fc x y -> PPi expl (sMN 0 "__pi_arg") x y) AssocRight]]

4343

4444-- | Calculates table for fixtiy declarations

4545toTable :: [FixDecl] -> OperatorTable IdrisParser PTerm