Build with GHC-9.8: no more head, tail, init, last (x-partial warning)

src/full/Agda/Termination/TypeBased/Definitions.hs

@@ -59,6 +59,7 @@ import qualified Agda.Termination.Order as Order
 import Data.List (unfoldr)
 import qualified Agda.Benchmarking as Benchmark
 import Agda.TypeChecking.Monad.Benchmark (billTo)
+import qualified Agda.Utils.List1 as List1
 
 
 -- | 'initSizeTypeEncoding names' computes size types for every definition in 'names'
@@ -377,8 +378,8 @@ encodeDatatypeDomain :: Bool -> Bool -> [Bool] -> Tele (Dom Type) -> SizeType
 encodeDatatypeDomain isRecursive _ params EmptyTel =
   let size = if isRecursive then SDefined 0 else SUndefined
       -- tail because scanl inserts the given starting element in the beginning
-      treeArgs = tail $
-        scanl (\(ind, t) isGeneric -> if isGeneric then (ind + 1, SizeGenericVar 0 ind) else (ind, UndefinedSizeType))
+      treeArgs = List1.tail $ List1.scanl
+              (\(ind, t) isGeneric -> if isGeneric then (ind + 1, SizeGenericVar 0 ind) else (ind, UndefinedSizeType))
               (0, UndefinedSizeType)
               params
       actualArgs = reverse (map snd treeArgs)

src/full/Agda/Termination/TypeBased/Graph.hs

@@ -42,6 +42,7 @@ import qualified Agda.Benchmarking as Benchmark
 import qualified Agda.Utils.Graph.AdjacencyMap.Unidirectional as DGraph
 import Agda.TypeChecking.Monad.Benchmark (billTo)
 import Data.Either
+import Agda.Utils.List (headWithDefault)
 
 -- A size expression is represented as a minimum of a set of rigid size variables,
 -- where the length of the set is equal to the number of clusters.
@@ -81,7 +82,7 @@ simplifySizeGraph rigidContext graph = billTo [Benchmark.TypeBasedTermination, B
 
   -- Lazy map representing an approximate cluster of each variable
   let rigidClusters = (mapMaybe (\(i, b) -> (i,) <$> findCluster rigidContext i) rigidContext)
-  let rememberNeighbor v1 v2 = IntMap.insertWith (\n old -> head n : old) v1 [v2]
+  let rememberNeighbor v1 v2 = IntMap.insertWith (\n old -> headWithDefault __IMPOSSIBLE__ n : old) v1 [v2]
   let neighbourMap = foldr (\(SConstraint _ from to) -> rememberNeighbor to from . rememberNeighbor from to) IntMap.empty enrichedGraph
   let clusterMapping = gatherClusters rigidClusters neighbourMap (IntMap.fromList rigidClusters)
 
@@ -146,15 +147,15 @@ instantiateComponents baseSize rigids clusterMapping graph subst (comp : is) = d
            -- Some element in the component has is bigger or equal than infinity,
            -- which means that the component should be assigned to infinity
            baseSize
-        | head comp `IntSet.member` bottomVars =
+        | headWithDefault __IMPOSSIBLE__ comp `IntSet.member` bottomVars =
           -- The component corresponds to a non-recursive constructor,
           -- which means that it should be assigned to the least available size expression,
           -- which is a meet of certain rigids
           SEMeet globalMinimum
         | null lowerBoundSizes =
           -- There are no lower bounds for the component, which means that we can try to do some witchcraft
           -- It won't be worse than infinity, right?
-          case (IntMap.lookup (head comp) fallback, ((head comp) `IntMap.lookup` clusterMapping)) of
+          case (IntMap.lookup (headWithDefault __IMPOSSIBLE__ comp) fallback, ((headWithDefault __IMPOSSIBLE__ comp) `IntMap.lookup` clusterMapping)) of
             (Just r, _) ->
               -- The component corresponds to a freshened variable of some recursive call, we can try to assign it to the original variable
               fromMaybe baseSize (subst IntMap.!? r)
@@ -210,7 +211,7 @@ findLowestClusterVariable bounds target = fst $ go 0 target
             l -> let inner = map (go (depth + 1)) l
                      maxLevel = maximum (map snd inner)
                      maxLevelVars = filter (\(a, d) -> d == maxLevel) inner
-                 in head maxLevelVars
+                 in headWithDefault __IMPOSSIBLE__ maxLevelVars
 
 collectIncoherentRigids :: IntMap SizeExpression -> [SConstraint] -> TCM IntSet
 collectIncoherentRigids m g = billTo [Benchmark.TypeBasedTermination, Benchmark.SizeGraphSolving] $ collectIncoherentRigids' m g

src/full/Agda/Termination/TypeBased/Monad.hs

@@ -25,6 +25,8 @@ import Control.Arrow ( first )
 import Control.Monad
 import Data.Maybe
 import Data.Set (Set )
+
+import Agda.Utils.List (headWithDefault)
 import Agda.Utils.Impossible
 
 import qualified Agda.Utils.Benchmark as B
@@ -113,18 +115,21 @@ getConstraints :: MonadSizeChecker [[SConstraint]]
 getConstraints = MSC $ gets scsConstraints
 
 getCurrentConstraints :: MonadSizeChecker [SConstraint]
-getCurrentConstraints = MSC $ head <$> gets scsConstraints
+getCurrentConstraints = MSC $ headWithDefault __IMPOSSIBLE__ <$> gets scsConstraints
 
 getCurrentRigids :: MonadSizeChecker [(Int, SizeBound)]
-getCurrentRigids = MSC $ head <$> gets scsRigidSizeVars
+getCurrentRigids = MSC $ headWithDefault __IMPOSSIBLE__ <$> gets scsRigidSizeVars
 
 -- | Adds a new rigid variable. This function is fragile, since bound might not be expressed in terms of current rigids.
 --   Unfortunately we have to live with it if we want to support record projections in arbitrary places.
 addNewRigid :: Int -> SizeBound -> MonadSizeChecker ()
-addNewRigid x bound = MSC $ modify (\s -> let rigids = scsRigidSizeVars s in s { scsRigidSizeVars = ((x, bound) : head rigids) : tail rigids })
+addNewRigid x bound = MSC $ modify \s ->
+  case scsRigidSizeVars s of
+    rs:rss -> s { scsRigidSizeVars = ((x, bound) : rs) : rss }
+    _ -> __IMPOSSIBLE__
 
 getCurrentCoreContext :: MonadSizeChecker [SizeContextEntry]
-getCurrentCoreContext = MSC $ head <$> gets scsCoreContext
+getCurrentCoreContext = MSC $ headWithDefault __IMPOSSIBLE__ <$> gets scsCoreContext
 
 -- | Initializes internal data strustures that will be filled by the processing of a clause
 initNewClause :: [SizeBound] -> MonadSizeChecker ()
@@ -150,7 +155,10 @@ getArity :: QName -> MonadSizeChecker Int
 getArity qn = sizeSigArity . fromJust . defSizedType <$> getConstInfo qn
 
 storeConstraint :: SConstraint -> MonadSizeChecker ()
-storeConstraint c = MSC $ modify (\s -> s { scsConstraints = let constraints = scsConstraints s in ((c : head constraints) : tail constraints) })
+storeConstraint c = MSC $ modify \ s ->
+  case scsConstraints s of
+    cs:css -> s { scsConstraints = (c:cs):css }
+    [] -> __IMPOSSIBLE__
 
 reportCall :: QName -> QName -> [Int] -> [Int] -> Closure Term -> MonadSizeChecker ()
 reportCall q1 q2 sizes1 sizes2 place = MSC $ modify (\s -> s { scsRecCalls = (q1, q2, sizes1, sizes2, place) : scsRecCalls s })
@@ -189,10 +197,13 @@ getUndefinedSizes = MSC $ gets scsUndefinedVariables
 abstractCoreContext :: Int -> Either FreeGeneric SizeType -> MonadSizeChecker a -> MonadSizeChecker a
 abstractCoreContext i tele action = do
   contexts <- MSC $ gets scsCoreContext
-  MSC $ modify (\s -> s { scsCoreContext = ((i, tele) : (map (incrementDeBruijnEntry tele) (head contexts))) : tail contexts })
-  res <- action
-  MSC $ modify (\s -> s { scsCoreContext = contexts })
-  pure res
+  case contexts of
+    cs:css -> do
+      MSC $ modify \s -> s { scsCoreContext = ((i, tele) : map (incrementDeBruijnEntry tele) cs) : css }
+      res <- action
+      MSC $ modify \s -> s { scsCoreContext = contexts }
+      pure res
+    [] -> __IMPOSSIBLE__
 
 incrementDeBruijnEntry :: Either FreeGeneric SizeType -> (Int, Either FreeGeneric SizeType) -> (Int, Either FreeGeneric SizeType)
 incrementDeBruijnEntry (Left _) (x, Left fg) = (x + 1, Left $ fg { fgIndex = fgIndex fg + 1 })
@@ -240,12 +251,17 @@ requestNewRigidVariables bound pack = do
         SizeBounded i -> newBound) pack
 
   currentRigids <- gets scsRigidSizeVars
-
-  modify (\s -> s { scsRigidSizeVars = ((zip newVarIdxs newBounds) ++ (head currentRigids)) : tail currentRigids })
-  return $ newVarIdxs
+  case currentRigids of
+    rs:rss -> do
+      modify \s -> s { scsRigidSizeVars = (zip newVarIdxs newBounds ++ rs) : rss }
+      return newVarIdxs
+    [] -> __IMPOSSIBLE__
 
 appendCoreVariable :: Int -> Either FreeGeneric SizeType -> MonadSizeChecker ()
-appendCoreVariable i tele = MSC $ modify (\s -> s { scsCoreContext = let cc = (scsCoreContext s) in ((i, tele) : head cc) : tail cc })
+appendCoreVariable i tele = MSC $ modify \s ->
+  case scsCoreContext s of
+    c:cc -> s { scsCoreContext = ((i, tele) : c) : cc }
+    [] -> __IMPOSSIBLE__
 
 runSizeChecker :: QName -> Set QName -> MonadSizeChecker a -> TCM (a, SizeCheckerState)
 runSizeChecker rootName mutualNames (MSC action) = do

src/full/Agda/Termination/TypeBased/Patterns.hs

@@ -53,7 +53,7 @@ import Agda.Termination.CallGraph
 import Agda.Termination.Monad
 import Agda.Termination.TypeBased.Graph
 import Data.Foldable (traverse_)
-import Agda.Utils.List ((!!!))
+import Agda.Utils.List ((!!!), initWithDefault, headWithDefault, lastWithDefault, tailWithDefault)
 import Data.Functor ((<&>))
 import Agda.Termination.CallMatrix
 import qualified Agda.Termination.CallMatrix
@@ -109,7 +109,7 @@ matchPatterns tele patterns = do
   currentRootArity <- getArity currentRoot
   let finalLeaves = peDepthStack modifiedState
   let leafVariables = map (\i -> case IntMap.lookup i finalLeaves of
-        Just l@(_ : _) -> last l
+        Just l@(_ : _) -> lastWithDefault __IMPOSSIBLE__ l
         _ -> -1
         ) [0..currentRootArity - 1]
   pure (leafVariables, sizeTypeOfClause)
@@ -302,7 +302,7 @@ getOrRequestDepthVar cluster level = do
         pure $ currentLeaves List.!! level
       else do
         -- We need to populate a depth stack with a new level
-        let actualBound = if (head currentLeaves == -1) then SUndefined else SDefined (last currentLeaves)
+        let actualBound = if (headWithDefault __IMPOSSIBLE__ currentLeaves == -1) then SUndefined else SDefined (lastWithDefault __IMPOSSIBLE__ currentLeaves)
         [var] <- lift $ requestNewRigidVariables actualBound [SizeBounded (-1)]
         modify (\s -> s { peDepthStack = IntMap.insert cluster (currentLeaves ++ [var]) (peDepthStack s) })
         pure var
@@ -330,12 +330,12 @@ freshenPatternConstructor conName codomainDataVar domainDataVar expectedCodomain
   let (SizeTree topSize datatypeParameters) = expectedCodomain
   let shouldBeUnbounded b = b == SizeUnbounded || codomainDataVar == (-1)
   -- We need to strip the codomain size from the constructor here.
-  let modifier = if codomainDataVar /= -1 then init else id
+  let modifier = if codomainDataVar /= -1 then initWithDefault __IMPOSSIBLE__ else id
   newVarsRaw <- lift $ requestNewRigidVariables topSize (modifier (filter shouldBeUnbounded bounds)) -- tail for stripping codomain TODO
   -- It is important to call `domainDataVar` lazily,
   -- because otherwise leaf variables would gain access to a cluster var with lower level than expected
   domainVar <- if length newVarsRaw + 1 == length bounds then pure (-1) else domainDataVar
-  let newVars = snd $ List.mapAccumL (\nv bound -> if shouldBeUnbounded bound then (tail nv, head nv) else (nv, domainVar)) newVarsRaw (modifier bounds)
+  let newVars = snd $ List.mapAccumL (\nv bound -> if shouldBeUnbounded bound then (tailWithDefault __IMPOSSIBLE__ nv, headWithDefault __IMPOSSIBLE__ nv) else (nv, domainVar)) newVarsRaw (modifier bounds)
   reportSDoc "term.tbt" 70 $ vcat
     [ "New variables for instantiation: " <+> text (show newVars)
     , "Raw variables: " <+> text (show newVarsRaw)
@@ -353,7 +353,7 @@ freshenCopatternProjection :: Int -> [SizeBound] -> SizeType -> PatternEncoder S
 freshenCopatternProjection newCoDepthVar bounds tele = do
   let isNewPatternSizeVar b = b == SizeUnbounded || newCoDepthVar == (-1)
   newVarsRaw <- lift $ requestNewRigidVariables SUndefined (filter isNewPatternSizeVar bounds)
-  let newVars = snd $ List.mapAccumL (\nv bound -> if isNewPatternSizeVar bound then (tail nv, head nv) else (nv, newCoDepthVar)) newVarsRaw bounds
+  let newVars = snd $ List.mapAccumL (\nv bound -> if isNewPatternSizeVar bound then (tailWithDefault __IMPOSSIBLE__ nv, headWithDefault __IMPOSSIBLE__ nv) else (nv, newCoDepthVar)) newVarsRaw bounds
   reportSDoc "term.tbt" 70 $ "Raw size type of copattern projection: " <+> pretty tele <+> "With new variabless:" <+> text (show newVars)
   let instantiatedSig = instantiateSizeType tele newVars
   pure instantiatedSig