git.iko.soy/Idris-dev
on master help sign in
Highlight differing implicits in errors
9af885aEdwin Brady
src/Idris/AbsSyntaxTree.hs+9−3
compare with master
unifiedsplit
@@ -836,7 +836,7 @@ data PArg' t = PImp { priority :: Int,
836 getTm :: t }
836 getTm :: t }
837 deriving (Show, Eq, Functor)
837 deriving (Show, Eq, Functor)
838
838
839−data ArgOpt = HideDisplay | InaccessibleArg
839+data ArgOpt = AlwaysShow | HideDisplay | InaccessibleArg
840 deriving (Show, Eq)
840 deriving (Show, Eq)
841
841
842instance Sized a => Sized (PArg' a) where
842instance Sized a => Sized (PArg' a) where
@@ -1275,7 +1275,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd
1275 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $
1275 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $
1276 char '\'' <> prettySe 10 bnd (PRef fc (sUN str))
1276 char '\'' <> prettySe 10 bnd (PRef fc (sUN str))
1277 prettySe p bnd (PApp _ f as) = -- Normal prefix applications
1277 prettySe p bnd (PApp _ f as) = -- Normal prefix applications
1278− let args = getExps as
1278+ let args = getShowArgs as
1279 fp = prettySe 1 bnd f
1279 fp = prettySe 1 bnd f
1280 in
1280 in
1281 bracket p 1 . group $
1281 bracket p 1 . group $
@@ -1285,7 +1285,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd
1285 else fp <+> align (vsep (map (prettyArgS bnd) as))
1285 else fp <+> align (vsep (map (prettyArgS bnd) as))
1286 else if null args
1286 else if null args
1287 then fp
1287 then fp
1288− else fp <+> align (vsep (map (prettyArgSe bnd) args))
1288+ else fp <+> align (vsep (map (prettyArgS bnd) args))
1289 prettySe p bnd (PCase _ scr opts) =
1289 prettySe p bnd (PCase _ scr opts) =
1290 kwd "case" <+> prettySe 10 bnd scr <+> kwd "of" <> prettyBody
1290 kwd "case" <+> prettySe 10 bnd scr <+> kwd "of" <> prettyBody
1291 where
1291 where
@@ -1525,6 +1525,12 @@ getExps [] = []
1525getExps (PExp _ _ _ tm : xs) = tm : getExps xs
1525getExps (PExp _ _ _ tm : xs) = tm : getExps xs
1526getExps (_ : xs) = getExps xs
1526getExps (_ : xs) = getExps xs
1527
1527
1528+getShowArgs :: [PArg] -> [PArg]
1529+getShowArgs [] = []
1530+getShowArgs (e@(PExp _ _ _ tm) : xs) = e : getShowArgs xs
1531+getShowArgs (e : xs) | AlwaysShow `elem` argopts e = e : getShowArgs xs
1532+getShowArgs (_ : xs) = getShowArgs xs
1533+
1528getConsts :: [PArg] -> [PTerm]
1534getConsts :: [PArg] -> [PTerm]
1529getConsts [] = []
1535getConsts [] = []
1530getConsts (PConstraint _ _ _ tm : xs) = tm : getConsts xs
1536getConsts (PConstraint _ _ _ tm : xs) = tm : getConsts xs
src/Idris/Delaborate.hs+71−8
@@ -164,14 +164,15 @@ pprintErr' i (InternalMsg s) =
164 text "This is probably a bug, or a missing error message.",
164 text "This is probably a bug, or a missing error message.",
165 text ("Please consider reporting at " ++ bugaddr)
165 text ("Please consider reporting at " ++ bugaddr)
166 ]
166 ]
167−pprintErr' i (CantUnify _ x y e sc s) =
167+pprintErr' i (CantUnify _ x_in y_in e sc s) =
168+ let (x, y) = addImplicitDiffs (delab i x_in) (delab i y_in) in
168− text "Can't unify" <> indented (annTm x (pprintTerm' i (map (\ (n, b) -> (n, False)) sc) (delab i x))) <$>
169+ text "Can't unify" <> indented (annTm x_in (pprintTerm' i (map (\ (n, b) -> (n, False)) sc) x)) <$>
169− text "with" <> indented (annTm y (pprintTerm' i (map (\ (n, b) -> (n, False)) sc) (delab i y))) <>
170+ text "with" <> indented (annTm y_in (pprintTerm' i (map (\ (n, b) -> (n, False)) sc) y)) <>
170− case e of
171+ case e of
171− Msg "" -> empty
172+ Msg "" -> empty
172− _ -> line <> line <> text "Specifically:" <>
173+ _ -> line <> line <> text "Specifically:" <>
173− indented (pprintErr' i e) <>
174+ indented (pprintErr' i e) <>
174− if (opt_errContext (idris_options i)) then showSc i sc else empty
175+ if (opt_errContext (idris_options i)) then showSc i sc else empty
175pprintErr' i (CantConvert x y env) =
176pprintErr' i (CantConvert x y env) =
176 text "Can't convert" <>
177 text "Can't convert" <>
177 indented (annTm x (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i x))) <$>
178 indented (annTm x (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i x))) <$>
@@ -262,6 +263,68 @@ pprintErr' i (ReflectionFailed msg err) =
262 indented (pprintErr' i err) <>
263 indented (pprintErr' i err) <>
263 text ("This is probably a bug. Please consider reporting it at " ++ bugaddr)
264 text ("This is probably a bug. Please consider reporting it at " ++ bugaddr)
264
265
266+-- If the two terms only differ in their implicits, mark the implicits which
267+-- differ as AlwaysShow so that they appear in errors
268+addImplicitDiffs :: PTerm -> PTerm -> (PTerm, PTerm)
269+addImplicitDiffs x y
270+ = if (x `expLike` y) then addI x y else (x, y)
271+ where
272+ addI :: PTerm -> PTerm -> (PTerm, PTerm)
273+ addI (PApp fc f as) (PApp gc g bs)
274+ = let (as', bs') = addShows as bs in
275+ (PApp fc f as', PApp gc g bs')
276+ where addShows [] [] = ([], [])
277+ addShows (a:as) (b:bs)
278+ = let (as', bs') = addShows as bs
279+ (a', b') = addI (getTm a) (getTm b) in
280+ if (not (a' `expLike` b'))
281+ then (a { argopts = AlwaysShow : argopts a,
282+ getTm = a' } : as',
283+ b { argopts = AlwaysShow : argopts b,
284+ getTm = b' } : bs')
285+ else (a { getTm = a' } : as',
286+ b { getTm = b' } : bs')
287+ addI (PLam n a b) (PLam n' c d)
288+ = let (a', c') = addI a c
289+ (b', d') = addI b d in
290+ (PLam n a' b', PLam n' c' d')
291+ addI (PPi p n a b) (PPi p' n' c d)
292+ = let (a', c') = addI a c
293+ (b', d') = addI b d in
294+ (PPi p n a' b', PPi p' n' c' d')
295+ addI (PRefl fc a) (PRefl fc' b)
296+ = let (a', b') = addI a b in
297+ (PRefl fc a', PRefl fc' b')
298+ addI (PEq fc a b) (PEq fc' c d)
299+ = let (a', c') = addI a c
300+ (b', d') = addI b d in
301+ (PEq fc a' b', PEq fc' c' d')
302+ addI (PPair fc pi a b) (PPair fc' pi' c d)
303+ = let (a', c') = addI a c
304+ (b', d') = addI b d in
305+ (PPair fc pi a' b', PPair fc' pi' c' d')
306+ addI (PDPair fc pi a t b) (PDPair fc' pi' c u d)
307+ = let (a', c') = addI a c
308+ (t', u') = addI t u
309+ (b', d') = addI b d in
310+ (PDPair fc pi a' t' b', PDPair fc' pi' c' u' d')
311+ addI x y = (x, y)
312+
313+ -- Just the ones which appear desugared in errors
314+ expLike (PRef _ n) (PRef _ n') = n == n'
315+ expLike (PApp _ f as) (PApp _ f' as')
316+ = expLike f f' && length as == length as' &&
317+ and (zipWith expLike (getExps as) (getExps as'))
318+ expLike (PPi _ n s t) (PPi _ n' s' t')
319+ = n == n' && expLike s s' && expLike t t'
320+ expLike (PLam n s t) (PLam n' s' t')
321+ = n == n' && expLike s s' && expLike t t'
322+ expLike (PPair _ _ x y) (PPair _ _ x' y') = expLike x x' && expLike y y'
323+ expLike (PDPair _ _ x _ y) (PDPair _ _ x' _ y') = expLike x x' && expLike y y'
324+ expLike (PEq _ x y) (PEq _ x' y') = expLike x x' && expLike y y'
325+ expLike (PRefl _ x) (PRefl _ x') = expLike x x'
326+ expLike x y = x == y
327+
265isUN :: Name -> Bool
328isUN :: Name -> Bool
266isUN (UN n) = not $ T.isPrefixOf (T.pack "__") n -- TODO figure out why MNs are getting rewritte to UNs for top-level pattern-matching functions
329isUN (UN n) = not $ T.isPrefixOf (T.pack "__") n -- TODO figure out why MNs are getting rewritte to UNs for top-level pattern-matching functions
267isUN (NS n _) = isUN n
330isUN (NS n _) = isUN n
src/Idris/IBC.hs+2
@@ -1001,11 +1001,13 @@ instance Binary ArgOpt where
1001 = case x of
1001 = case x of
1002 HideDisplay -> putWord8 0
1002 HideDisplay -> putWord8 0
1003 InaccessibleArg -> putWord8 1
1003 InaccessibleArg -> putWord8 1
1004+ AlwaysShow -> putWord8 2
1004 get
1005 get
1005 = do i <- getWord8
1006 = do i <- getWord8
1006 case i of
1007 case i of
1007 0 -> return HideDisplay
1008 0 -> return HideDisplay
1008 1 -> return InaccessibleArg
1009 1 -> return InaccessibleArg
1010+ 2 -> return AlwaysShow
1009 _ -> error "Corrupted binary data for Static"
1011 _ -> error "Corrupted binary data for Static"
1010
1012
1011instance Binary Static where
1013instance Binary Static where