Do not display global bindings with -fno-max-relevant-binds
Presently, "Relevant bindings" messages (e.g., from holes) will attempt to report all local bindings, and relevant global bindings (by some heuristic), up to the number of bindings specified by -fmax-relevant-binds=N. For example, here is an error I recently had with a small number of relevant bindings:
Productive.hs:162:16: error:
• Found hole: _ :: Par (D k0 (Stream k0 b))
Where: ‘k0’ is an ambiguous type variable
‘b’ is a rigid type variable bound by
the type signature for:
maapM :: forall a b.
(a -> Par b)
-> (forall (k :: Clock). Stream k a) -> Par (Forall1 Stream b)
at Productive.hs:155:10
• In the second argument of ‘(<$>)’, namely ‘_’
In a stmt of a 'do' block: Cons b <$> _
In the expression:
do { (a, s') <- deStreamCons s;
b <- f a;
b' <- f (scar (unForall1 s'));
Cons b <$> _ }
• Relevant bindings include
b' :: b (bound at Productive.hs:159:5)
b :: b (bound at Productive.hs:158:5)
s' :: Forall1 Stream a (bound at Productive.hs:157:9)
(Some bindings suppressed; use -fmax-relevant-binds=N or -fno-max-relevant-binds)When I set -fno-max-relevant-binds), this extends with:
a :: a (bound at Productive.hs:157:6)
s :: forall (k :: Clock). Stream k a (bound at Productive.hs:156:9)
f :: a -> Par b (bound at Productive.hs:156:7)
maapM :: (a -> Par b)
-> (forall (k :: Clock). Stream k a) -> Par (Forall1 Stream b)
(bound at Productive.hs:156:1)
take :: forall a.
Int -> (forall (k :: Clock). Stream k a) -> Par [a]
(bound at Productive.hs:143:1)
...and a pile more global binds...I think this is not really the behavior we want. If I'm doing an Agda/Coq development, what I want is for the compiler to tell me all LOCAL bindings. Heuristically picked global bindings might be nice, but it's not a priority (after all, I probably have explicit type signatures for all of these anyway.) So really, to see all local bindings I just want to set -fmax-relevant-binds=100000 (i.e., to a large number.)
So, I think there should be another flag -frelevant-global-binds which triggers display of global relevant bindings, making -fno-max-relevant-binds equivalent to -fmax-relevant-binds=BIGNUM; i.e., it does NOT report global bindings. I don't know if the error message should mention -frelevant-global-binds by default, but for now I would say it shouldn't.
As a minor addendum, I don't find the context information In the second argument of ‘(<$>)’, namely ‘_’, etc. very useful. Just makes the message longer and harder to view.
Activity
added Tfeature request Trac import typechecker labels
Related #10411
added Pnormal label
