f01873f · Idris-dev · git.iko.soy

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

compare with master

unifiedsplit

@@ -687,7 +687,7 @@ 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

692 recoverableErr _ = True

693

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 Name Name (Err' t)

143+ | ElaboratingArg Name Name [(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 f x e) = "Elaborating " ++ show f ++ " arg " ++

199+ show (ElaboratingArg f x prev 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+4−2

@@ -40,8 +40,10 @@ data UResult a = UOK a

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

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

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

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

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

44+ At fc (ElaboratingArg f x

45+ (map (\(FailContext _ f' x') -> (f', x')) prev)

46+ (CantUnify r t1 t2 e ctxt i))

45

47

46-- Solve metavariables by matching terms against each other

48-- Solve metavariables by matching terms against each other

47-- Not really unification, of course!

49-- Not really unification, of course!

src/Idris/Delaborate.hs+1−1

@@ -217,7 +217,7 @@ 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 f x e)

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

221 | isUN x =

222 text "When elaborating argument" <+>

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

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+4−4

@@ -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

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

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

1644 err' <- handle err

1645 return (Elaborating what n err')

1646− handle e@(ElaboratingArg f a err) = do logLvl 3 "Reflecting body of ElaboratingArg"

1646+ handle e@(ElaboratingArg f a prev err) = do logLvl 3 "Reflecting body of ElaboratingArg"

1647− err' <- handle err

1647+ err' <- handle err

1648− return (ElaboratingArg f a err')

1648+ return (ElaboratingArg f a prev err')

1649 -- TODO: argument-specific error handlers go here for ElaboratingArg

1650 handle e = do ist <- getIState

1651 let err = fmap (errReverse ist) e