Require building with singletons-base-3.5/GHC 9.12

RyanGlScott · Dec 30, 2024 · d1e4f6e · d1e4f6e
1 parent cdd3e3a
commit d1e4f6e
Show file tree

Hide file tree

Showing 4 changed files with 49 additions and 27 deletions.
diff --git a/.github/workflows/haskell-ci.yml b/.github/workflows/haskell-ci.yml
@@ -8,9 +8,9 @@
 #
 # For more information, see https://github.com/haskell-CI/haskell-ci
 #
-# version: 0.19.20240514
+# version: 0.19.20241222
 #
-# REGENDATA ("0.19.20240514",["github","cabal.project"])
+# REGENDATA ("0.19.20241222",["github","cabal.project"])
 #
 name: Haskell-CI
 on:
@@ -28,22 +28,37 @@ jobs:
     strategy:
       matrix:
         include:
-          - compiler: ghc-9.10.1
+          - compiler: ghc-9.12.1
             compilerKind: ghc
-            compilerVersion: 9.10.1
+            compilerVersion: 9.12.1
             setup-method: ghcup
             allow-failure: false
       fail-fast: false
     steps:
-      - name: apt
+      - name: apt-get install
         run: |
           apt-get update
           apt-get install -y --no-install-recommends gnupg ca-certificates dirmngr curl git software-properties-common libtinfo5
+      - name: Install GHCup
+        run: |
           mkdir -p "$HOME/.ghcup/bin"
-          curl -sL https://downloads.haskell.org/ghcup/0.1.20.0/x86_64-linux-ghcup-0.1.20.0 > "$HOME/.ghcup/bin/ghcup"
+          curl -sL https://downloads.haskell.org/ghcup/0.1.30.0/x86_64-linux-ghcup-0.1.30.0 > "$HOME/.ghcup/bin/ghcup"
           chmod a+x "$HOME/.ghcup/bin/ghcup"
+      - name: Install cabal-install (prerelease)
+        run: |
+          "$HOME/.ghcup/bin/ghcup" config add-release-channel https://raw.githubusercontent.com/haskell/ghcup-metadata/master/ghcup-prereleases-0.0.8.yaml;
+          "$HOME/.ghcup/bin/ghcup" install cabal 3.15.0.0.2024.10.3 || (cat "$HOME"/.ghcup/logs/*.* && false)
+          echo "CABAL=$HOME/.ghcup/bin/cabal-3.15.0.0.2024.10.3 -vnormal+nowrap" >> "$GITHUB_ENV"
+      - name: Install GHC (GHCup)
+        if: matrix.setup-method == 'ghcup'
+        run: |
           "$HOME/.ghcup/bin/ghcup" install ghc "$HCVER" || (cat "$HOME"/.ghcup/logs/*.* && false)
-          "$HOME/.ghcup/bin/ghcup" install cabal 3.10.2.0 || (cat "$HOME"/.ghcup/logs/*.* && false)
+          HC=$("$HOME/.ghcup/bin/ghcup" whereis ghc "$HCVER")
+          HCPKG=$(echo "$HC" | sed 's#ghc$#ghc-pkg#')
+          HADDOCK=$(echo "$HC" | sed 's#ghc$#haddock#')
+          echo "HC=$HC" >> "$GITHUB_ENV"
+          echo "HCPKG=$HCPKG" >> "$GITHUB_ENV"
+          echo "HADDOCK=$HADDOCK" >> "$GITHUB_ENV"
         env:
           HCKIND: ${{ matrix.compilerKind }}
           HCNAME: ${{ matrix.compiler }}
@@ -54,21 +69,12 @@ jobs:
           echo "LANG=C.UTF-8" >> "$GITHUB_ENV"
           echo "CABAL_DIR=$HOME/.cabal" >> "$GITHUB_ENV"
           echo "CABAL_CONFIG=$HOME/.cabal/config" >> "$GITHUB_ENV"
-          HCDIR=/opt/$HCKIND/$HCVER
-          HC=$("$HOME/.ghcup/bin/ghcup" whereis ghc "$HCVER")
-          HCPKG=$(echo "$HC" | sed 's#ghc$#ghc-pkg#')
-          HADDOCK=$(echo "$HC" | sed 's#ghc$#haddock#')
-          echo "HC=$HC" >> "$GITHUB_ENV"
-          echo "HCPKG=$HCPKG" >> "$GITHUB_ENV"
-          echo "HADDOCK=$HADDOCK" >> "$GITHUB_ENV"
-          echo "CABAL=$HOME/.ghcup/bin/cabal-3.10.2.0 -vnormal+nowrap" >> "$GITHUB_ENV"
           HCNUMVER=$(${HC} --numeric-version|perl -ne '/^(\d+)\.(\d+)\.(\d+)(\.(\d+))?$/; print(10000 * $1 + 100 * $2 + ($3 == 0 ? $5 != 1 : $3))')
           echo "HCNUMVER=$HCNUMVER" >> "$GITHUB_ENV"
           echo "ARG_TESTS=--enable-tests" >> "$GITHUB_ENV"
           echo "ARG_BENCH=--enable-benchmarks" >> "$GITHUB_ENV"
           echo "HEADHACKAGE=false" >> "$GITHUB_ENV"
           echo "ARG_COMPILER=--$HCKIND --with-compiler=$HC" >> "$GITHUB_ENV"
-          echo "GHCJSARITH=0" >> "$GITHUB_ENV"
         env:
           HCKIND: ${{ matrix.compilerKind }}
           HCNAME: ${{ matrix.compiler }}
@@ -187,8 +193,8 @@ jobs:
         run: |
           $CABAL v2-haddock --disable-documentation --haddock-all $ARG_COMPILER --with-haddock $HADDOCK $ARG_TESTS $ARG_BENCH all
       - name: save cache
-        uses: actions/cache/save@v4
         if: always()
+        uses: actions/cache/save@v4
         with:
           key: ${{ runner.os }}-${{ matrix.compiler }}-${{ github.sha }}
           path: ~/.cabal/store
diff --git a/logical-foundations/logical-foundations.cabal b/logical-foundations/logical-foundations.cabal
@@ -14,7 +14,7 @@ category:            Dependent Types
 build-type:          Simple
 extra-source-files:  README.md
 cabal-version:       >=1.10
-tested-with:         GHC == 9.10.1
+tested-with:         GHC == 9.12.1
 
 source-repository head
   type:     git
@@ -37,9 +37,9 @@ library
                        SF.LF.ImpC
   other-modules:       SF.LF.Axiom
                        SF.LF.FunExt
-  build-depends:       base            >= 4.20  && < 4.21
+  build-depends:       base            >= 4.21  && < 4.22
                      , eliminators     >= 0.9   && < 0.10
-                     , singletons-base >= 3.4   && < 3.5
+                     , singletons-base >= 3.5   && < 3.6
                      , singleton-nats  >= 0.4.2 && < 0.5
                      , text
   hs-source-dirs:      src

diff --git a/logical-foundations/src/SF/LF/Maps.hs b/logical-foundations/src/SF/LF/Maps.hs
@@ -6,7 +6,6 @@
 {-# LANGUAGE UndecidableInstances #-}
 module SF.LF.Maps where
 
-import Data.Kind
 import Data.Singletons.TH
 import Data.Text (Text)
 import Data.Tuple
@@ -18,9 +17,26 @@ import SF.LF.FunExt
 import SF.LF.IndProp
 import SF.LF.Logic
 
-type TotalMap' (p :: Type ~> Type ~> Type) sym a = p @@ sym @@ a
-type TotalMap  a = TotalMap' (TyCon2 (->)) Text   a
-type PTotalMap a = TotalMap' (~>@#@$)      Symbol a
+{-
+It would be cool if we could define TotalMap and PTotalMap in terms of a common
+definition, i.e.,
+
+  type TotalMap' (p :: Type ~> Type ~> Type) sym a = p @@ sym @@ a
+  type TotalMap  a = TotalMap' (TyCon2 (->)) Text   a
+  type PTotalMap a = TotalMap' (~>@#@$)      Symbol a
+
+Sadly, this won't work. If you attempt to defunctionalize TEmpty below,
+singletons-th will generate an Apply instance that looks like this:
+
+  type instance Apply @a @(PTotalMap a) TEmptySym0 x = TEmpty x
+
+GHC will reject this type family instance because the left-hand side of the
+instance contains a nested type family application (PTotalMap, which in turn
+expands to applications of the Apply type family). For this reason, we define
+TotalMap and PTotalMap separately, without any nested type families.
+-}
+type TotalMap  a = Text   -> a
+type PTotalMap a = Symbol ~> a
 
 tEmpty :: a -> TotalMap a
 tEmpty v _ = v

diff --git a/verified-functional-algorithms/verified-functional-algorithms.cabal b/verified-functional-algorithms/verified-functional-algorithms.cabal
@@ -14,7 +14,7 @@ category:            Dependent Types
 build-type:          Simple
 extra-source-files:  README.md
 cabal-version:       >=1.10
-tested-with:         GHC == 9.10.1
+tested-with:         GHC == 9.12.1
 
 source-repository head
   type:     git
@@ -23,9 +23,9 @@ source-repository head
 
 library
   exposed-modules:     SF.VFA.Perm
-  build-depends:       base                >= 4.20 && < 4.21
+  build-depends:       base                >= 4.21 && < 4.22
                      , logical-foundations >= 0.1  && < 0.2
-                     , singletons-base     >= 3.4  && < 3.5
+                     , singletons-base     >= 3.5  && < 3.6
   hs-source-dirs:      src
   default-language:    GHC2021
   ghc-options:         -Wall -Wcompat -Wno-unticked-promoted-constructors -fenable-th-splice-warnings