fb3f7f0 · Idris-dev · git.iko.soy

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

compare with master

unifiedsplit

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

687 r || proofSearch

688 recoverableErr (CantSolveGoal _ _) = False

689 recoverableErr (ProofSearchFail _) = False

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

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

691+ recoverableErr (At _ e) = recoverableErr e

691 recoverableErr _ = True

692 recoverableErr _ = True

692

693

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

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

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

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

140 | NoRewriting t

141 | At FC (Err' t)

142 | Elaborating String Name (Err' t)

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

143+ | ElaboratingArg Name Name (Err' t)

144 | ProviderError String

145 | LoadingFailed String (Err' t)

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

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

171 size ProgramLineComment = 1

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

173 size (Elaborating _ n err) = size err

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

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

175 size (ProviderError msg) = length msg

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

177 size _ = 1

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

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

197 show ProgramLineComment = "Program line next to comment"

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

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

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

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

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

201 show _ = "Error"

202

203instance Pretty Err OutputAnnotation where

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

@@ -41,7 +41,7 @@ data UResult a = UOK a

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

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

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

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

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

45

46-- Solve metavariables by matching terms against each other

47-- Not really unification, of course!

src/Idris/Delaborate.hs+1−3

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

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

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

219 pprintErr' i e

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

220+pprintErr' i (ElaboratingArg f x e)

221 | isUN x =

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

223 text "When elaborating argument" <+>

222 text "When elaborating argument" <+>

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

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

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

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

226 indented (pprintErr' i e)

225 indented (pprintErr' i e)

227 | otherwise =

226 | otherwise =

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

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

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

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

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

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

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

src/Idris/ElabDecls.hs+1−1

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

1279 impossibleError (CantConvert _ _ _) = False

1280 impossibleError (At _ e) = impossibleError e

1281 impossibleError (Elaborating _ _ e) = impossibleError e

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

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

1283 impossibleError _ = True

1284

1285 sameFam topx topy

src/Idris/ElabTerm.hs+1−1

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

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

190 ht == txt "Lazy" = True

191 forceErr (Elaborating _ _ t) = forceErr t

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

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

193 forceErr (At _ t) = forceErr t

194 forceErr t = False

195

src/Idris/Error.hs−3

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

57tclift :: TC a -> Idris a

58tclift (OK v) = return v

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

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

61− throwError err

62tclift (Error err) = throwError err

60tclift (Error err) = throwError err

63

61

64tctry :: TC a -> TC a -> Idris a

62tctry :: TC a -> TC a -> Idris a

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

69

67

70getErrSpan :: Err -> FC

68getErrSpan :: Err -> FC

71getErrSpan (At fc _) = fc

69getErrSpan (At fc _) = fc

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

73getErrSpan _ = emptyFC

70getErrSpan _ = emptyFC