@@ -104,10 +104,10 @@ delabTy' ist imps tm fullname mvs = de [] imps tm
104104 (de env [] l) (de env [] r)
105105 | n == sUN "Sg_intro" = PDPair un IsTerm (de env [] l) Placeholder
106106 (de env [] r)
107− deFn env f@(P _ n _) args
108− | n `elem` map snd env
107+ deFn env f@(P _ n _) args
108+ | n `elem` map snd env
109109 = PApp un (de env [] f) (map pexp (map (de env []) args))
110− deFn env (P _ n _) args
110+ deFn env (P _ n _) args
111111 | not mvs = case lookup n (idris_metavars ist) of
112112 Just (Just _, mi, _) ->
113113 mkMVApp n (drop mi (map (de env []) args))
@@ -170,10 +170,10 @@ pprintErr' i (InternalMsg s) =
170170pprintErr' i (CantUnify _ x_in y_in e sc s) =
171171 let (x_ns, y_ns, nms) = renameMNs x_in y_in
172172 (x, y) = addImplicitDiffs (delab i x_ns) (delab i y_ns) in
173− text "Can't unify" <> indented (annTm x_ns
173+ text "Can't unify" <> indented (annTm x_ns
174174 (pprintTerm' i (map (\ (n, b) -> (n, False)) sc
175175 ++ zip nms (repeat False)) x)) <$>
176− text "with" <> indented (annTm y_ns
176+ text "with" <> indented (annTm y_ns
177177 (pprintTerm' i (map (\ (n, b) -> (n, False)) sc
178178 ++ zip nms (repeat False)) y)) <>
179179 case e of
@@ -183,10 +183,10 @@ pprintErr' i (CantUnify _ x_in y_in e sc s) =
183183 if (opt_errContext (idris_options i)) then showSc i sc else empty
184184pprintErr' i (CantConvert x y env) =
185185 text "Can't convert" <>
186− indented (annTm x (pprintTerm' i (map (\ (n, b) -> (n, False)) env)
186+ indented (annTm x (pprintTerm' i (map (\ (n, b) -> (n, False)) env)
187187 (delab i (flagUnique x)))) <$>
188188 text "with" <>
189− indented (annTm y (pprintTerm' i (map (\ (n, b) -> (n, False)) env)
189+ indented (annTm y (pprintTerm' i (map (\ (n, b) -> (n, False)) env)
190190 (delab i (flagUnique y)))) <>
191191 if (opt_errContext (idris_options i)) then line <> showSc i env else empty
192192 where flagUnique (Bind n (Pi t k@(UType u)) sc)
@@ -232,7 +232,7 @@ pprintErr' i (NoTypeDecl n) = text "No type declaration for" <+> annName n
232232pprintErr' i (NoSuchVariable n) = text "No such variable" <+> annName n
233233pprintErr' i (IncompleteTerm t) = text "Incomplete term" <+> annTm t (pprintTerm i (delab i t))
234234pprintErr' i UniverseError = text "Universe inconsistency"
235−pprintErr' i (UniqueError NullType n)
235+pprintErr' i (UniqueError NullType n)
236236 = text "Borrowed name" <+> annName' n (showbasic n)
237237 <+> text "must not be used on RHS"
238238pprintErr' i (UniqueError _ n) = text "Unique name" <+> annName' n (showbasic n)
@@ -255,7 +255,8 @@ pprintErr' i (Elaborating s n e) = text "When elaborating" <+> text s <>
255255pprintErr' i (ElaboratingArg f x _ e)
256256 | isUN x =
257257 text "When elaborating argument" <+>
258− annotate (AnnBoundName x False) (text (showbasic x)) <+> --TODO check plicity
258+ annotate (AnnBoundName x False) (text (showbasic x)) <+> -- TODO check plicity
259+ -- Issue #1591 on the issue tracker: https://github.com/idris-lang/Idris-dev/issues/1591
259260 text "to" <+> whatIsName <> annName f <> colon <>
260261 indented (pprintErr' i e)
261262 | otherwise =
@@ -289,7 +290,11 @@ pprintErr' i (ReflectionFailed msg err) =
289290
290291-- Make sure the machine invented names are shown helpfully to the user, so
291292-- that any names which differ internally also differ visibly
293+
292294-- FIXME: I can't actually contrive an error to test this! Will revisit later...
295+--
296+-- Issue #1590 in the Issue tracker.
297+-- https://github.com/idris-lang/Idris-dev/issues/1590
293298renameMNs :: Term -> Term -> (Term, Term, [Name])
294299renameMNs x y = let ns = nub $ allTTNames x ++ allTTNames y
295300 newnames = evalState (getRenames [] ns) 1 in
@@ -307,7 +312,7 @@ renameMNs x y = let ns = nub $ allTTNames x ++ allTTNames y
307312 rename :: [(Name, Name)] -> Term -> Term
308313 rename ns (P nt x t) | Just x' <- lookup x ns = P nt x' t
309314 rename ns (App f a) = App (rename ns f) (rename ns a)
310− rename ns (Bind x b sc)
315+ rename ns (Bind x b sc)
311316 = let b' = fmap (rename ns) b
312317 sc' = rename ns sc in
313318 case lookup x ns of
@@ -318,15 +323,15 @@ renameMNs x y = let ns = nub $ allTTNames x ++ allTTNames y
318323-- If the two terms only differ in their implicits, mark the implicits which
319324-- differ as AlwaysShow so that they appear in errors
320325addImplicitDiffs :: PTerm -> PTerm -> (PTerm, PTerm)
321−addImplicitDiffs x y
326+addImplicitDiffs x y
322327 = if (x `expLike` y) then addI x y else (x, y)
323328 where
324329 addI :: PTerm -> PTerm -> (PTerm, PTerm)
325− addI (PApp fc f as) (PApp gc g bs)
330+ addI (PApp fc f as) (PApp gc g bs)
326331 = let (as', bs') = addShows as bs in
327332 (PApp fc f as', PApp gc g bs')
328333 where addShows [] [] = ([], [])
329− addShows (a:as) (b:bs)
334+ addShows (a:as) (b:bs)
330335 = let (as', bs') = addShows as bs
331336 (a', b') = addI (getTm a) (getTm b) in
332337 if (not (a' `expLike` b'))
@@ -334,20 +339,20 @@ addImplicitDiffs x y
334339 getTm = a' } : as',
335340 b { argopts = AlwaysShow : argopts b,
336341 getTm = b' } : bs')
337− else (a { getTm = a' } : as',
342+ else (a { getTm = a' } : as',
338343 b { getTm = b' } : bs')
339− addI (PLam n a b) (PLam n' c d)
344+ addI (PLam n a b) (PLam n' c d)
340345 = let (a', c') = addI a c
341346 (b', d') = addI b d in
342347 (PLam n a' b', PLam n' c' d')
343− addI (PPi p n a b) (PPi p' n' c d)
348+ addI (PPi p n a b) (PPi p' n' c d)
344349 = let (a', c') = addI a c
345350 (b', d') = addI b d in
346351 (PPi p n a' b', PPi p' n' c' d')
347− addI (PRefl fc a) (PRefl fc' b)
352+ addI (PRefl fc a) (PRefl fc' b)
348353 = let (a', b') = addI a b in
349354 (PRefl fc a', PRefl fc' b')
350− addI (PEq fc at bt a b) (PEq fc' ct dt c d)
355+ addI (PEq fc at bt a b) (PEq fc' ct dt c d)
351356 | trace (show (at,bt)) False = undefined
352357 | at `expLike` ct && bt `expLike` dt
353358 = let (a', c') = addI a c
@@ -357,8 +362,8 @@ addImplicitDiffs x y
357362 = let (at', ct') = addI at ct
358363 (bt', dt') = addI bt dt
359364 (a', c') = addI a c
360− (b', d') = addI b d
361− showa = if at `expLike` ct then [] else [AlwaysShow]
365+ (b', d') = addI b d
366+ showa = if at `expLike` ct then [] else [AlwaysShow]
362367 showb = if bt `expLike` dt then [] else [AlwaysShow] in
363368 (PApp fc (PRef fc eqTy) [(pimp (sUN "A") at' True)
364369 { argopts = showa },
@@ -370,12 +375,12 @@ addImplicitDiffs x y
370375 (pimp (sUN "B") dt' True)
371376 { argopts = showb },
372377 pexp c', pexp d'])
373−
374− addI (PPair fc pi a b) (PPair fc' pi' c d)
378+
379+ addI (PPair fc pi a b) (PPair fc' pi' c d)
375380 = let (a', c') = addI a c
376381 (b', d') = addI b d in
377382 (PPair fc pi a' b', PPair fc' pi' c' d')
378− addI (PDPair fc pi a t b) (PDPair fc' pi' c u d)
383+ addI (PDPair fc pi a t b) (PDPair fc' pi' c u d)
379384 = let (a', c') = addI a c
380385 (t', u') = addI t u
381386 (b', d') = addI b d in
@@ -387,19 +392,24 @@ addImplicitDiffs x y
387392 expLike (PApp _ f as) (PApp _ f' as')
388393 = expLike f f' && length as == length as' &&
389394 and (zipWith expLike (getExps as) (getExps as'))
390− expLike (PPi _ n s t) (PPi _ n' s' t')
395+ expLike (PPi _ n s t) (PPi _ n' s' t')
391396 = n == n' && expLike s s' && expLike t t'
392− expLike (PLam n s t) (PLam n' s' t')
397+ expLike (PLam n s t) (PLam n' s' t')
393398 = n == n' && expLike s s' && expLike t t'
394399 expLike (PPair _ _ x y) (PPair _ _ x' y') = expLike x x' && expLike y y'
395400 expLike (PDPair _ _ x _ y) (PDPair _ _ x' _ y') = expLike x x' && expLike y y'
396− expLike (PEq _ xt yt x y) (PEq _ xt' yt' x' y')
401+ expLike (PEq _ xt yt x y) (PEq _ xt' yt' x' y')
397402 = expLike x x' && expLike y y'
398403 expLike (PRefl _ x) (PRefl _ x') = expLike x x'
399404 expLike x y = x == y
400405
406+-- Issue #1589 on the issue tracker
407+-- https://github.com/idris-lang/Idris-dev/issues/1589
408+--
409+-- Figure out why MNs are getting rewritte to UNs for top-level
410+-- pattern-matching functions
401411isUN :: Name -> Bool
402−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
412+isUN (UN n) = not $ T.isPrefixOf (T.pack "__") n -- TODO
403413isUN (NS n _) = isUN n
404414isUN _ = False
405415
@@ -428,6 +438,8 @@ fancifyAnnots ist annot@(AnnName n _ _ _) =
428438 docOverview ist n = do docs <- lookupCtxtExact n (idris_docstrings ist)
429439 let o = overview (fst docs)
430440 -- TODO make width configurable
441+ -- Issue #1588 on the Issue Tracker
442+ -- https://github.com/idris-lang/Idris-dev/issues/1588
431443 out = displayS . renderPretty 1.0 50 $
432444 renderDocstring (pprintDelab ist) o
433445 return (out "")
@@ -460,5 +472,3 @@ showbasic n@(UN _) = show n
460472showbasic (MN _ s) = str s
461473showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n
462474showbasic (SN s) = show s
463−
464−