[ #4547 ] use List1/2 in Concrete.Definition.Errors.ShadowingInTelescope

src/full/Agda/Interaction/Highlighting/Generate.hs

@@ -71,6 +71,8 @@ import Agda.Syntax.Abstract.Views ( KName, declaredNames )
 
 import Agda.Utils.FileName
 import Agda.Utils.List            ( caseList, initWithDefault, last1 )
+import Agda.Utils.List2           ( List2 )
+import qualified Agda.Utils.List2 as List2
 import Agda.Utils.Maybe
 import qualified Agda.Utils.Maybe.Strict as Strict
 import Agda.Utils.Null
@@ -548,11 +550,11 @@ coverageErrorHighlighting :: Range -> HighlightingInfoBuilder
 coverageErrorHighlighting r = H.singleton (rToR $ P.continuousPerLine r) m
   where m = parserBased { otherAspects = Set.singleton CoverageProblem }
 
-shadowingTelHighlighting :: [Range] -> HighlightingInfoBuilder
+shadowingTelHighlighting :: List2 Range -> HighlightingInfoBuilder
 shadowingTelHighlighting =
   -- we do not want to highlight the one variable in scope so we take
   -- the @init@ segment of the ranges in question
-  foldMap (\r -> H.singleton (rToR $ P.continuous r) m) . initWithDefault __IMPOSSIBLE__
+  foldMap (\r -> H.singleton (rToR $ P.continuous r) m) . List2.init
   where
   m = parserBased { otherAspects =
                       Set.singleton H.ShadowingInTelescope }

src/full/Agda/Syntax/Concrete/Definitions/Errors.hs

@@ -15,6 +15,7 @@ import Agda.Interaction.Options.Warnings
 
 import Agda.Utils.CallStack ( CallStack )
 import Agda.Utils.List1 (List1, pattern (:|))
+import Agda.Utils.List2 (List2, pattern List2)
 import qualified Agda.Utils.List1 as List1
 import Agda.Utils.Pretty
 
@@ -102,7 +103,7 @@ data DeclarationWarning'
   --   by @{-\# TERMINATING \#-}@ and @{-\# NON_TERMINATING \#-}@.
   | PragmaCompiled Range
   -- ^ @COMPILE@ pragmas are not allowed in safe mode
-  | ShadowingInTelescope [(Name, [Range])]
+  | ShadowingInTelescope (List1 (Name, List2 Range))
   | UnknownFixityInMixfixDecl [Name]
   | UnknownNamesInFixityDecl [Name]
   | UnknownNamesInPolarityPragmas [Name]
@@ -357,7 +358,7 @@ instance Pretty DeclarationWarning' where
     pwords "public does not have any effect in a private block."
   pretty (ShadowingInTelescope nrs) = fsep $
     pwords "Shadowing in telescope, repeated variable names:"
-    ++ punctuate comma (map (pretty . fst) nrs)
+    ++ punctuate comma (fmap (pretty . fst) nrs)
 
 instance NFData DeclarationWarning
 instance NFData DeclarationWarning'

src/full/Agda/Syntax/Scope/Monad.hs

@@ -53,7 +53,9 @@ import Agda.Utils.Functor
 import Agda.Utils.Lens
 import Agda.Utils.List
 import Agda.Utils.List1 (List1, pattern (:|), nonEmpty)
+import Agda.Utils.List2 (List2(List2))
 import qualified Agda.Utils.List1 as List1
+import qualified Agda.Utils.List2 as List2
 import Agda.Utils.Maybe
 import Agda.Utils.Monad
 import Agda.Utils.Null
@@ -225,17 +227,16 @@ checkNoShadowing old new = do
     -- Filter out the underscores.
     let newNames = filter (not . isNoName) $ AssocList.keys diff
     -- Associate each name to its occurrences.
-    let nameOccs = Map.toList $ Map.fromListWith (++) $ map pairWithRange newNames
+    let nameOccs1 :: [(C.Name, List1 Range)]
+        nameOccs1 = Map.toList $ Map.fromListWith (<>) $ map pairWithRange newNames
     -- Warn if we have two or more occurrences of the same name.
-    unlessNull (filter (atLeastTwo . snd) nameOccs) $ \ conflicts -> do
-      scopeWarning $ ShadowingInTelescope conflicts
+    let nameOccs2 :: [(C.Name, List2 Range)]
+        nameOccs2 = mapMaybe (traverseF List2.fromList1Maybe) nameOccs1
+    caseList nameOccs2 (return ()) $ \ c conflicts -> do
+      scopeWarning $ ShadowingInTelescope $ c :| conflicts
   where
-    pairWithRange :: C.Name -> (C.Name, [Range])
-    pairWithRange n = (n, [getRange n])
-
-    atLeastTwo :: [a] -> Bool
-    atLeastTwo (_ : _ : _) = True
-    atLeastTwo _ = False
+    pairWithRange :: C.Name -> (C.Name, List1 Range)
+    pairWithRange n = (n, singleton $ getRange n)
 
 getVarsToBind :: ScopeM LocalVars
 getVarsToBind = useScope scopeVarsToBind

src/full/Agda/TypeChecking/Serialise/Instances/Common.hs

@@ -48,6 +48,8 @@ import Agda.Utils.BiMap (BiMap)
 import qualified Agda.Utils.BiMap as BiMap
 import qualified Agda.Utils.Empty as Empty
 import Agda.Utils.FileName
+import Agda.Utils.List2 (List2(List2))
+import qualified Agda.Utils.List2 as List2
 import Agda.Utils.Maybe
 import qualified Agda.Utils.Maybe.Strict as Strict
 import Agda.Utils.Trie (Trie(..))
@@ -234,6 +236,10 @@ instance EmbPrj a => EmbPrj (NonEmpty a) where
   icod_ = icod_ . NonEmpty.toList
   value = maybe malformed return . nonEmpty <=< value
 
+instance EmbPrj a => EmbPrj (List2 a) where
+  icod_ = icod_ . List2.toList
+  value = maybe malformed return . List2.fromListMaybe <=< value
+
 instance (EmbPrj k, EmbPrj v, EmbPrj (BiMap.Tag v)) =>
          EmbPrj (BiMap k v) where
   icod_ m = icode (BiMap.toDistinctAscendingLists m)

src/full/Agda/Utils/List2.hs

@@ -13,6 +13,7 @@ module Agda.Utils.List2
   ) where
 
 import Control.DeepSeq
+import Control.Monad                   ( (<=<) )
 
 import Data.Data                       ( Data )
 import qualified Data.List as List
@@ -21,36 +22,48 @@ import GHC.Exts                        ( IsList(..) )
 import qualified GHC.Exts  as Reexport ( toList )
 
 import Agda.Utils.List1                ( List1, pattern (:|) )
+import qualified Agda.Utils.List1 as List1
 
 import Agda.Utils.Impossible
 
 -- | Lists of length ≥2.
 data List2 a = List2 a a [a]
   deriving (Eq, Ord, Show, Data, Functor, Foldable, Traversable)
 
--- | Safe.
+-- | Safe. O(1).
 head :: List2 a -> a
 head (List2 a _ _) = a
 
--- | Safe.
-tail :: List2 a -> [a]
-tail (List2 a b cs) = b : cs
+-- | Safe. O(1).
+tail :: List2 a -> List1 a
+tail (List2 a b cs) = b :| cs
 
--- | Safe.
-tail1 :: List2 a -> List1 a
-tail1 (List2 a b cs) = b :| cs
+-- | Safe. O(n).
+init :: List2 a -> List1 a
+init (List2 a b cs) = a :| List1.init (b :| cs)
+
+-- | Safe. O(1).
+fromListMaybe :: [a] -> Maybe (List2 a)
+fromListMaybe = fromList1Maybe <=< List1.nonEmpty
+
+-- | Safe. O(1).
+fromList1Maybe :: List1 a -> Maybe (List2 a)
+fromList1Maybe = \case
+  (a :| b : cs) -> Just (List2 a b cs)
+  _ -> Nothing
 
 instance IsList (List2 a) where
   type Item (List2 a) = a
 
-  -- | Unsafe!
+  -- | Unsafe! O(1).
   fromList :: [a] -> List2 a
   fromList (a : b : cs) = List2 a b cs
   fromList _            = __IMPOSSIBLE__
 
   toList :: List2 a -> [a]
   toList (List2 a b cs) = a : b : cs
 
+-- | Safe. O(1).
 toList1 :: List2 a -> List1 a
 toList1 (List2 a b cs) = a :| b : cs