Update in response to changes to how the GHC backend compiles ∞/♯_/♭.

See Issue 2909 on the Agda bug tracker.

CHANGELOG.md

@@ -123,6 +123,10 @@ Non-backwards compatible changes
 * Names in Data.Nat.Divisibility now use the divides symbol `|` (typed \|) consistently.
   Previously a mixture of `|` and `|` was used.
 
+* Starting from Agda 2.5.4 the GHC backend compiles `Coinduction.∞` in
+  a different way, and for this reason the GHC backend pragmas for
+  `Data.Colist.Colist` and `Data.Stream.Stream` have been modified.
+
 Deprecated features
 -------------------
 

src/Data/Colist.agda

@@ -43,8 +43,11 @@ data Colist {a} (A : Set a) : Set a where
   []  : Colist A
   _∷_ : (x : A) (xs : ∞ (Colist A)) → Colist A
 
-{-# FOREIGN GHC type AgdaColist a b = [b] #-}
-{-# COMPILE GHC Colist = data MAlonzo.Code.Data.Colist.AgdaColist ([] | (:)) #-}
+{-# FOREIGN GHC
+  data AgdaColist a    = Nil | Cons a (MAlonzo.RTE.Inf (AgdaColist a))
+  type AgdaColist' l a = AgdaColist a
+  #-}
+{-# COMPILE GHC Colist = data AgdaColist' (Nil | Cons) #-}
 {-# COMPILE UHC Colist = data __LIST__ (__NIL__ | __CONS__) #-}
 
 module Colist-injective {a} {A : Set a} where

src/Data/Stream.agda

@@ -21,8 +21,10 @@ infixr 5 _∷_
 data Stream {a} (A : Set a) : Set a where
   _∷_ : (x : A) (xs : ∞ (Stream A)) → Stream A
 
-{-# FOREIGN GHC data AgdaStream a = Cons a (AgdaStream a) #-}
-{-# COMPILE GHC Stream = data MAlonzo.Code.Data.Stream.AgdaStream (MAlonzo.Code.Data.Stream.Cons) #-}
+{-# FOREIGN GHC
+  data AgdaStream a = Cons a (MAlonzo.RTE.Inf (AgdaStream a))
+  #-}
+{-# COMPILE GHC Stream = data AgdaStream (Cons) #-}
 
 ------------------------------------------------------------------------
 -- Some operations

src/IO.agda

@@ -120,3 +120,7 @@ putStrLn∞ s =
 
 putStrLn : String → IO ⊤
 putStrLn s = putStrLn∞ (toCostring s)
+
+-- Note that the commands writeFile, appendFile, putStr and putStrLn
+-- perform two conversions (string → costring → Haskell list). It may
+-- be preferable to only perform one conversion.

src/IO/Primitive.agda

@@ -63,14 +63,24 @@ postulate
     Control.Exception.bracketOnError (return ()) (\_ -> System.IO.hClose h)
                                                  (\_ -> System.IO.hFileSize h)
     Data.Text.IO.hGetContents h
+
+  fromColist :: MAlonzo.Code.Data.Colist.AgdaColist a -> [a]
+  fromColist MAlonzo.Code.Data.Colist.Nil         = []
+  fromColist (MAlonzo.Code.Data.Colist.Cons x xs) =
+    x : fromColist (MAlonzo.RTE.flat xs)
+
+  toColist :: [a] -> MAlonzo.Code.Data.Colist.AgdaColist a
+  toColist []       = MAlonzo.Code.Data.Colist.Nil
+  toColist (x : xs) =
+    MAlonzo.Code.Data.Colist.Cons x (MAlonzo.RTE.Sharp (toColist xs))
 #-}
 
-{-# COMPILE GHC getContents    = getContents                           #-}
-{-# COMPILE GHC readFile       = readFile . Data.Text.unpack           #-}
-{-# COMPILE GHC writeFile      = \x -> writeFile (Data.Text.unpack x)  #-}
-{-# COMPILE GHC appendFile     = \x -> appendFile (Data.Text.unpack x) #-}
-{-# COMPILE GHC putStr         = putStr                                #-}
-{-# COMPILE GHC putStrLn       = putStrLn                              #-}
+{-# COMPILE GHC getContents    = fmap toColist getContents                          #-}
+{-# COMPILE GHC readFile       = fmap toColist . readFile . Data.Text.unpack        #-}
+{-# COMPILE GHC writeFile      = \x -> writeFile (Data.Text.unpack x) . fromColist  #-}
+{-# COMPILE GHC appendFile     = \x -> appendFile (Data.Text.unpack x) . fromColist #-}
+{-# COMPILE GHC putStr         = putStr . fromColist                                #-}
+{-# COMPILE GHC putStrLn       = putStrLn . fromColist                              #-}
 {-# COMPILE GHC readFiniteFile = readFiniteFile                        #-}
 {-# COMPILE UHC getContents    = UHC.Agda.Builtins.primGetContents     #-}
 {-# COMPILE UHC readFile       = UHC.Agda.Builtins.primReadFile        #-}