Make it work on ghc 9.8.2

src/Agda2Hs/Compile/Data.hs

@@ -23,8 +23,9 @@ import Agda2Hs.HsUtils
 checkNewtype :: Hs.Name () -> [Hs.QualConDecl ()] -> C ()
 checkNewtype name cs = do
   checkSingleElement name cs "Newtype must have exactly one constructor in definition"
-  case head cs of
-    Hs.QualConDecl () _ _ (Hs.ConDecl () cName types) -> checkNewtypeCon cName types
+  case cs of
+    (Hs.QualConDecl () _ _ (Hs.ConDecl () cName types):_) -> checkNewtypeCon cName types
+    _ -> __IMPOSSIBLE__
 
 compileData :: AsNewType -> [Hs.Deriving ()] -> Definition -> C [Hs.Decl ()]
 compileData newtyp ds def = do

src/Agda2Hs/Compile/Function.hs

@@ -110,7 +110,7 @@ compileFun, compileFun'
   -> Definition -> C [Hs.Decl ()]
 
 compileFun withSig def@Defn{..} =
-  setCurrentRangeQ defName 
+  setCurrentRangeQ defName
     $ maybePrependFixity defName (defName ^. lensFixity)
     -- initialize locals when first stepping into a function
     $ withFunctionLocals defName
@@ -125,7 +125,7 @@ compileFun' withSig def@Defn{..} = inTopContext $ withCurrentModule m $ do
 
   ifM (endsInSort defType)
     -- if the function type ends in Sort, it's a type alias!
-    (ensureNoLocals err >> compileTypeDef x def) 
+    (ensureNoLocals err >> compileTypeDef x def)
     -- otherwise, we have to compile clauses.
     $ do
     tel <- lookupSection m
@@ -140,18 +140,18 @@ compileFun' withSig def@Defn{..} = inTopContext $ withCurrentModule m $ do
       -- the canonicity check for typeclass instances picks up the
       -- module parameters (see https://github.com/agda/agda2hs/issues/305).
       liftTCM $ setModuleCheckpoint m
-          
+
       pars <- getContextArgs
       reportSDoc "agda2hs.compile.type" 8 $ "Function module parameters: " <+> prettyTCM pars
 
       reportSDoc "agda2hs.compile.type" 8 $ "Function type (before instantiation): " <+> inTopContext (prettyTCM defType)
       typ <- piApplyM defType pars
-      reportSDoc "agda2hs.compile.type" 8 $ "Function type (after instantiation): " <+> prettyTCM typ 
+      reportSDoc "agda2hs.compile.type" 8 $ "Function type (after instantiation): " <+> prettyTCM typ
 
       sig <- if not withSig then return [] else do
         checkValidFunName x
         ty <- paramTy <$> compileType (unEl typ)
-        reportSDoc "agda2hs.compile.type" 8 $ "Compiled function type: " <+> text (Hs.prettyPrint ty) 
+        reportSDoc "agda2hs.compile.type" 8 $ "Compiled function type: " <+> text (Hs.prettyPrint ty)
         return [Hs.TypeSig () [x] ty]
 
       let clauses = funClauses `apply` pars
@@ -366,7 +366,9 @@ withClauseLocals curModule c@Clause{..} k = do
     nonExtLamUses = qnameModule <$> filter (not . isExtendedLambdaName) uses
     whereModuleName
       | null uses = Nothing
-      | otherwise = Just $ head (nonExtLamUses ++ [curModule])
+      | otherwise = Just $ case nonExtLamUses ++ [curModule] of
+          (x:_) -> x
+          _ -> __IMPOSSIBLE__
     ls' = case whereModuleName of
       Nothing -> []
       Just m  -> zoomLocals m ls

src/Agda2Hs/Compile/Imports.hs

@@ -18,6 +18,7 @@ import Agda2Hs.Compile.Name
 import Agda2Hs.Compile.Types
 import Agda2Hs.Compile.Utils
 import Agda2Hs.HsUtils
+import qualified Data.List as L
 
 type ImportSpecMap = Map NamespacedName (Set NamespacedName)
 type ImportDeclMap = Map (Hs.ModuleName (), Qualifier) ImportSpecMap
@@ -54,10 +55,10 @@ compileImports top is0 = do
     -- Name in the Import datatype
     makeCName :: Hs.Name () -> Hs.CName ()
     makeCName n@(Hs.Ident _ s)
-      | isUpper (head s) = Hs.ConName () n
+      | Just True == (isUpper . fst <$> L.uncons s) = Hs.ConName () n
       | otherwise        = Hs.VarName () n
     makeCName n@(Hs.Symbol _ s)
-      | head s == ':' = Hs.ConName () n
+      | (fst <$> L.uncons s) == Just ':' = Hs.ConName () n
       | otherwise     = Hs.VarName () n
 
     makeImportSpec :: NamespacedName -> Set NamespacedName -> Hs.ImportSpec ()

src/Agda2Hs/Compile/Term.hs

@@ -43,6 +43,7 @@ import Agda2Hs.Compile.Var ( compileDBVar )
 import Agda2Hs.HsUtils
 
 import {-# SOURCE #-} Agda2Hs.Compile.Function ( compileClause' )
+import qualified Data.List as L
 
 
 -- * Compilation of special definitions
@@ -407,7 +408,7 @@ compileTerm ty v = do
     Lit l   -> compileLiteral l
 
     Lam v b -> compileLam ty v b
-      
+
     v@Pi{} -> bad "function type" v
     v@Sort{} -> bad "sort type" v
     v@Level{} -> bad "level term" v
@@ -486,7 +487,7 @@ compileInlineFunctionApp f ty args = do
     extractPatName :: DeBruijnPattern -> ArgName
     extractPatName (VarP _ v) = dbPatVarName v
     extractPatName (ConP _ _ args) =
-      let arg = namedThing $ unArg $ head $ filter (usableModality `and2M` visible) args
+      let arg = namedThing $ unArg $ maybe __IMPOSSIBLE__ fst $ L.uncons $ filter (usableModality `and2M` visible) args
       in extractPatName arg
     extractPatName _ = __IMPOSSIBLE__
 
@@ -497,7 +498,7 @@ compileInlineFunctionApp f ty args = do
 
     etaExpand :: NAPs -> Type -> [Term] -> C Term
     etaExpand [] ty args = do
-      r <- liftReduce 
+      r <- liftReduce
             $ locallyReduceDefs (OnlyReduceDefs $ Set.singleton f)
             $ unfoldDefinitionStep (Def f [] `applys` args) f (Apply . defaultArg <$> args)
       case r of

src/Agda2Hs/Compile/Utils.hs

@@ -46,6 +46,8 @@ import Agda2Hs.AgdaUtils ( (~~) )
 import Agda2Hs.Compile.Types
 import Agda2Hs.HsUtils
 import Agda2Hs.Pragma
+import qualified Data.List as L
+import Agda.Utils.Impossible ( __IMPOSSIBLE__ )
 
 
 -- | Primitive modules provided by the agda2hs library.
@@ -82,12 +84,13 @@ freshString :: String -> C String
 freshString s = liftTCM $ do
   scope <- getScope
   ctxNames <- map (prettyShow . nameConcrete) <$> getContextNames
-  return $ head $ filter (isFresh scope ctxNames) $ s : map (\i -> s ++ show i) [0..]
+  let freshName = L.uncons $ filter (isFresh scope ctxNames) $ s : map (\i -> s ++ show i) [0..]
+  return (maybe __IMPOSSIBLE__ fst freshName)
   where
     dummyName s = C.QName $ C.Name noRange C.NotInScope $ singleton $ C.Id s
     isFresh scope ctxNames s =
       null (scopeLookup (dummyName s) scope :: [AbstractName]) &&
-      not (s `elem` ctxNames)
+      notElem s ctxNames
 
 makeList :: C Doc -> Term -> C [Term]
 makeList = makeList' "Agda.Builtin.List.List.[]" "Agda.Builtin.List.List._∷_"
@@ -130,7 +133,7 @@ isPropSort :: Sort -> C Bool
 isPropSort s = reduce s <&> \case
   Prop _ -> True
   _      -> False
-  
+
 
 -- Determine whether it is ok to erase arguments of this type,
 -- even in the absence of an erasure annotation.