Skip to content

Remove malfunctioning hint "Avoid NonEmpty.unzip" #1657

@andreasabel

Description

@andreasabel

The hint "Avoid NonEmpty.unzip" can and should be removed as there is now a custom warning x-data-list-nonempty-unzip in base for this function, see:

The hint malfunctions in my setting. In VSCode, with the HLS and GHC 9.12 (base 4.21), the hint shows up, even though I import unzip from Data.Functor rather than Data.List.NonEmpty for this base version.
https://github.com/agda/agda/blob/670777792fb9ccdece123f782ef9ca5f0251f06b/src/full/Agda/Utils/List1.hs#L42-L46

-- Prevent warning -Wx-data-list-nonempty-unzip
#if MIN_VERSION_base(4,19,0)
import Data.Functor as Unzip (unzip)
#else
import Data.List.NonEmpty as Unzip (unzip)
#end

https://github.com/agda/agda/blob/670777792fb9ccdece123f782ef9ca5f0251f06b/src/full/Agda/Utils/List1.hs#L252-L253

unzipWith :: (a -> (b, c)) -> List1 a -> (List1 b, List1 c)
unzipWith f = unzip . fmap f
Image

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions