[Import] Data.List.*
#2625
[Import] Data.List.*
#2625
Conversation
|
Something's broken concerning (missing import?) |
src/Data/List/Relation/Binary/Disjoint/Propositional/Properties.agda
Outdated
Show resolved
Hide resolved
| @@ -8,14 +8,14 @@ | |||
|
|
|||
| module Data.List.NonEmpty.Effectful where | |||
|
|
|||
| open import Agda.Builtin.List | |||
| open import Agda.Builtin.List using (List; _∷_; []) | |||
There was a problem hiding this comment.
Going directly into Data.Builtin.List is not a good idea here, it should use Data.List.Core instead.
There was a problem hiding this comment.
@JacquesCarette you meant Agda.Builtin.List and Data.List.Base, I think?
Not quite sure why this module seemed to be originally based off Agda.Builtin.List, there are usually only two (acceptable!?) reasons for that:
- breaking a dependency cycle (occasionally)
- a MWE mindest of using only 'minimal commitments' to dependency (almost never now)
In any case, @jmougeot : please do not touch any imports from Agda.Builtin.* (nor from modules marked altogether as DEPRECATED...)
There was a problem hiding this comment.
Yes, typo in both cases!!! Serves me right for doing this fairly late after a long day.
I'm pretty sure this use of Agda.Builtin.List is a mistake - but you're right that it likely should be cleaned up in a separate PR.
There was a problem hiding this comment.
Actually, I took the executive decision to resolve this as part of your 'cleanup': precisely because the overall strategy of narrowing imports via using directives actually resolves a non-trivial dependency/ambiguity issue which AFAICT was responsible for the original appeal to Agda.Builtin. A separate PR would have been excessive, I think.
src/Data/List/Relation/Binary/Disjoint/Propositional/Properties.agda
Outdated
Show resolved
Hide resolved
There was a problem hiding this comment.
Removed the appeal to Agda.Builtin, otherwise all looks fine.
@JacquesCarette are you happy too?
Resolves question about use of `Agda.Builtin` here. Originally it solved a dependency/ambiguity conflict, but the generally strategy of localising imports pays off in this case!
src/Data/List/Relation/Binary/Disjoint/Propositional/Properties.agda
Outdated
Show resolved
Hide resolved
src/Data/List/Relation/Binary/Disjoint/Propositional/Properties.agda
Outdated
Show resolved
Hide resolved
…s.agda Reorder to reflect conventions on dependency.
No description provided.