.gitattributes

+patches/* -text

README.md

@@ -10,7 +10,7 @@ existing Hackage package(s).
   you submit a PR).
 
 - The patches SHOULD work with at least GHC HEAD and a set of recent stable
-  released GHC versions (currently this means with GHC 9.6, 9.8, 9.10, and 9.11).
+  released GHC versions (currently this means with GHC 9.6, 9.8, 9.10, 9.12 and 9.13).
 
 - The patches SHOULD ideally result in the same code being compiled,
   as one of the main purposes of these patches is to make regression
@@ -22,6 +22,12 @@ existing Hackage package(s).
 This repo contains `<pkg-id>.patch` files in the
 [`patches/`](./patches/) folder (where `<pkg-id>` refers to a specific
 release of a package, e.g. `lens-4.15.3`).
+Adding a patch forces the system to use that specific version,
+so empty patch files may exist to force the system to use that a 
+newer version, instead of a previous patch if available.
+For example consider a patched `th-abstraction-0.5.0`, and an empty patch `th-abstraction-0.6.0`,
+if we were to remove the empty patch, `0.6.0`, certain libraries such
+as `generics-sop` fail to build, because it's forced to use `0.5.0`.
 
 Once merged to `master`, all package releases whose `<pkg-id>` is
 mentioned will enter the *HEAD.hackage* package index; if there is a

ci/config.cabal.project

@@ -3,7 +3,7 @@
 -- ghc/ghc#23048.
 
 index-state:
-    hackage.haskell.org 2024-09-20T11:02:23Z,
+    hackage.haskell.org 2025-05-11T00:00:00Z,
     head.hackage HEAD
 
 constraints: th-abstraction >= 0.4

ci/config.sh

@@ -91,16 +91,32 @@ case $version in
   9.6.*)
     #       package                   ticket
     broken  liquidhaskell-boot        350
+    # singletons-base only supports the latest ghc
+    broken singletons-base            00000
     ;;
 
   9.8.*)
     #       package                   ticket
     broken  liquidhaskell-boot        350
+    # singletons-base only supports the latest ghc
+    broken singletons-base            00000
     ;;
 
   9.10.*)
     #       package                   ticket
     broken  liquidhaskell-boot        350
+    # singletons-base only supports the latest ghc
+    broken singletons-base            00000
+    ;;
+
+  9.12.*)
+    #       package                   ticket
+    broken  liquidhaskell-boot        350
+    ;;
+
+  9.13.*)
+    #       package                   ticket
+    broken  ghcide                    00000 
     ;;
 
   *)
@@ -130,19 +146,20 @@ esac
 #
 # These are packages which we don't have patches for but want to test anyways.
 extra_package lens 5.2.3
+extra_package generic-lens 2.2.2.0
 extra_package optics 0.4.2.1
-extra_package aeson 2.2.1.0
+extra_package aeson 2.2.3.0
 extra_package criterion 1.6.3.0
 extra_package scotty 0.21
 extra_package generic-lens 2.2.2.0
 extra_package microstache 1.0.2.3
-extra_package singletons-base 3.1.1
+extra_package singletons-base 3.5
 extra_package servant 0.20.1
 extra_package hgmp 0.1.2.1
-extra_package Agda 2.6.4.1
+extra_package Agda 2.7.0.1
 extra_package mmark 0.0.7.6
-extra_package doctest 0.22.2
-extra_package tasty 1.5
+extra_package doctest 0.24.0
+extra_package tasty 1.5.3
 extra_package pandoc 3.1.11.1
 extra_package servant-conduit 0.16
 extra_package servant-machines 0.16
@@ -152,7 +169,7 @@ extra_package generic-random 1.5.0.1
 extra_package lame 0.2.2
 extra_package inspection-testing 0.5.0.3
 extra_package ghcide 2.9.0.0
-extra_package ghc-typelits-extra 0.4.6
+extra_package ghc-typelits-extra 0.4.7
 
 # This package is affected by https://gitlab.haskell.org/ghc/ghc/-/issues/22912
 extra_package vector-space 0.16

ci/default.nix

@@ -2,25 +2,7 @@
 
 with nixpkgs;
 let
-  haskellPackages_ = nixpkgs.haskell.packages.ghc963.override {
-       all-cabal-hashes = sources.all-cabal-hashes.outPath;
-       overrides = self: super: {
-         mkDerivation = args: super.mkDerivation (args // {
-           enableLibraryProfiling = false;
-           doCheck = false;
-           doHoogle = false;
-           doHaddock = false;
-         });
-       };
-     };
-
-  haskellPackages = haskellPackages_.extend (self: super: {
-    # This is marked broken in nixpkgs, but seems to work fine.
-    cabal-plan = self.callHackage "cabal-plan" "0.7.3.0" {};
-    # The easiest fix for an incorrect override in nixpkgs (https://github.com/NixOS/nixpkgs/issues/260013)
-    tls        = self.callHackage "tls" "1.6.0" {};
-  });
-
+  haskellPackages = nixpkgs.haskellPackages;
 
   hackage-repo-tool =
     let src = sources.hackage-security.outPath;

ci/pipelines/validation.yml

@@ -14,7 +14,7 @@ stages:
   extends: .run-ci
   parallel:
     matrix:
-      - UPSTREAM_BRANCH_NAME: [ghc-9.6, ghc-9.8, ghc-9.10]
+      - UPSTREAM_BRANCH_NAME: [ghc-9.6, ghc-9.8, ghc-9.10, ghc-9.12]
         ARCH: [aarch64, x86_64]
       - UPSTREAM_BRANCH_NAME: [master]
         ARCH: [aarch64, x86_64]

ci/setup-nix-environment.sh

@@ -3,10 +3,9 @@
 cat >/etc/nix/nix.conf <<EOF
 sandbox = false
 build-users-group =
-trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= loony-tools:pr9m4BkM/5/eSTZlkQyRt57Jz7OMBxNSUiMC4FkcNfk=
-substituters = https://cache.nixos.org https://cache.zw3rk.com
+trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY=
+substituters = https://cache.nixos.org
 experimental-features = nix-command flakes
-cores = 1 # to avoid resource exhaustion. See: <https://gitlab.haskell.org/ghc/head.hackage/-/issues/38>
 EOF
 
 # Equivalent to running `nix develop` but works in CI scripts.

flake.lock

 {
   "nodes": {
-    "all-cabal-hashes": {
-      "flake": false,
-      "locked": {
-        "lastModified": 1696837982,
-        "narHash": "sha256-QebSglEs/Xar/Z/59Fjmv7WDy9Zj1A+7iAJ5yDb7Sjg=",
-        "owner": "commercialhaskell",
-        "repo": "all-cabal-hashes",
-        "rev": "b39aba9b53425d4160667f75b0e1e9ecd3c8bce9",
-        "type": "github"
-      },
-      "original": {
-        "owner": "commercialhaskell",
-        "ref": "hackage",
-        "repo": "all-cabal-hashes",
-        "type": "github"
-      }
-    },
     "flake-compat": {
       "flake": false,
       "locked": {
-        "lastModified": 1673956053,
-        "narHash": "sha256-4gtG9iQuiKITOjNQQeQIpoIB6b16fm+504Ch3sNKLd8=",
+        "lastModified": 1733328505,
+        "narHash": "sha256-NeCCThCEP3eCl2l/+27kNNK7QrwZB1IJCrXfrbv5oqU=",
         "owner": "edolstra",
         "repo": "flake-compat",
-        "rev": "35bb57c0c8d8b62bbfd284272c928ceb64ddbde9",
+        "rev": "ff81ac966bb2cae68946d5ed5fc4994f96d0ffec",
         "type": "github"
       },
       "original": {
@@ -52,11 +35,11 @@
     "hackage-security": {
       "flake": false,
       "locked": {
-        "lastModified": 1696439837,
-        "narHash": "sha256-3/swYPrsBuHl9//S/PwmDqyG2ZIi5c2OCBob3qjkidU=",
+        "lastModified": 1725697204,
+        "narHash": "sha256-zaLDDeKQpBVaSBRKv/X3WTfeu0rLazy5H8AfJQlsVGM=",
         "owner": "haskell",
         "repo": "hackage-security",
-        "rev": "0b501400a4b52593dfab7a1b106fcebdaeba6af7",
+        "rev": "8ada49de74456f3aebd2ae08cf11151acbf8ef05",
         "type": "github"
       },
       "original": {
@@ -67,11 +50,11 @@
     },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1696604326,
-        "narHash": "sha256-YXUNI0kLEcI5g8lqGMb0nh67fY9f2YoJsILafh6zlMo=",
+        "lastModified": 1733392399,
+        "narHash": "sha256-kEsTJTUQfQFIJOcLYFt/RvNxIK653ZkTBIs4DG+cBns=",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "87828a0e03d1418e848d3dd3f3014a632e4a4f64",
+        "rev": "d0797a04b81caeae77bcff10a9dde78bc17f5661",
         "type": "github"
       },
       "original": {
@@ -99,7 +82,6 @@
     },
     "root": {
       "inputs": {
-        "all-cabal-hashes": "all-cabal-hashes",
         "flake-compat": "flake-compat",
         "ghc-artefact-nix": "ghc-artefact-nix",
         "hackage-security": "hackage-security",

flake.nix

@@ -3,8 +3,6 @@
   inputs.nixpkgs.url = "github:NixOS/nixpkgs/nixos-unstable";
   inputs.ghc-artefact-nix.url = "github:mpickering/ghc-artefact-nix";
   inputs.ghc-artefact-nix.flake = false;
-  inputs.all-cabal-hashes.url = "github:commercialhaskell/all-cabal-hashes/hackage";
-  inputs.all-cabal-hashes.flake = false;
   inputs.hackage-security.url = "github:haskell/hackage-security";
   inputs.hackage-security.flake = false;
   inputs.overlay-tool.url = "github:bgamari/hackage-overlay-repo-tool";

patches/Agda-2.7.0.1.patch

+diff --git a/Agda.cabal b/Agda.cabal
+index 9a0863c..cc2f024 100644
+--- a/Agda.cabal
++++ b/Agda.cabal
+@@ -1,7 +1,7 @@
+ cabal-version:   2.4
+ name:            Agda
+ version:         2.7.0.1
+-build-type:      Custom
++build-type:      Simple
+ license:         MIT
+ license-file:    LICENSE
+ copyright:       (c) 2005-2024 The Agda Team.
+diff --git a/Setup.hs b/Setup.hs
+deleted file mode 100644
+index 7064a95..0000000
+--- a/Setup.hs
++++ /dev/null
+@@ -1,235 +0,0 @@
+-{-# LANGUAGE BlockArguments #-}
+-{-# LANGUAGE CPP #-}
+-{-# LANGUAGE LambdaCase #-}
+-{-# LANGUAGE ScopedTypeVariables #-}
+-
+-import Data.Functor ( (<&>) )
+-import Data.List    ( intercalate )
+-import Data.Maybe   ( catMaybes )
+-
+-import Distribution.Simple
+-import Distribution.Simple.LocalBuildInfo
+-import Distribution.Simple.Setup
+-import Distribution.Simple.BuildPaths (exeExtension)
+-import Distribution.PackageDescription
+-import Distribution.System ( buildPlatform )
+-
+-import System.FilePath
+-import System.Directory (doesFileExist, makeAbsolute, removeFile)
+-import System.Environment (getEnvironment)
+-import System.Process
+-import System.Exit
+-import System.IO
+-import System.IO.Error (isDoesNotExistError)
+-
+-import Control.Monad
+-import Control.Exception
+-
+-main :: IO ()
+-main = defaultMainWithHooks userhooks
+-
+-userhooks :: UserHooks
+-userhooks = simpleUserHooks
+-  { copyHook  = copyHook'
+-  , instHook  = instHook'
+-  }
+-
+--- Install and copy hooks are default, but amended with .agdai files in data-files.
+-instHook' :: PackageDescription -> LocalBuildInfo -> UserHooks -> InstallFlags -> IO ()
+-instHook' pd lbi hooks flags = instHook simpleUserHooks pd' lbi hooks flags where
+-  pd' = pd { dataFiles = concatMap (expandAgdaExt pd) $ dataFiles pd }
+-
+--- Andreas, 2020-04-25, issue #4569: defer 'generateInterface' until after
+--- the library has been copied to a destination where it can be found.
+--- @cabal build@ will likely no longer produce the .agdai files, but @cabal install@ does.
+-copyHook' :: PackageDescription -> LocalBuildInfo -> UserHooks -> CopyFlags -> IO ()
+-copyHook' pd lbi hooks flags = do
+-  -- Copy library and executable etc.
+-  copyHook simpleUserHooks pd lbi hooks flags
+-  if wantInterfaces flags && not (skipInterfaces lbi) then do
+-    -- Generate .agdai files.
+-    success <- generateInterfaces pd lbi
+-    -- Copy again, now including the .agdai files.
+-    when success $ copyHook simpleUserHooks pd' lbi hooks flags
+-  else
+-    putStrLn "Skipping generation of Agda core library interface files"
+-  where
+-  pd' = pd
+-    { dataFiles = concatMap (expandAgdaExt pd) $ dataFiles pd
+-      -- Andreas, 2020-04-25, issue #4569:
+-      -- I tried clearing some fields to avoid copying again.
+-      -- However, cabal does not like me messing with the PackageDescription.
+-      -- Clearing @library@ or @executables@ leads to internal errors.
+-      -- Thus, we just copy things again.  Not a terrible problem.
+-    -- , library       = Nothing
+-    -- , executables   = []
+-    -- , subLibraries  = []
+-    -- , foreignLibs   = []
+-    -- , testSuites    = []
+-    -- , benchmarks    = []
+-    -- , extraSrcFiles = []
+-    -- , extraTmpFiles = []
+-    -- , extraDocFiles = []
+-    }
+-
+--- We only want to write interfaces if installing the executable.
+--- If we're installing *just* the library, the interface files are not needed
+--- and, most importantly, the executable will not be available to be run (cabal#10235)
+-wantInterfaces :: CopyFlags -> Bool
+-wantInterfaces _flags = do
+-#if MIN_VERSION_Cabal(3,11,0)
+-    any isAgdaExe (copyArgs _flags)
+-      where
+-        isAgdaExe "exe:agda" = True
+-        isAgdaExe _ = False
+-#else
+-  True
+-#endif
+-
+--- Used to add .agdai files to data-files
+-expandAgdaExt :: PackageDescription -> FilePath -> [FilePath]
+-expandAgdaExt pd = \ fp ->
+-    -- N.B. using lambda here so that @expandAgdaExt pd@ can be partially evaluated.
+-    if takeExtension fp == ".agda" then [ fp, iFile fp ] else [ fp ]
+-  where
+-  iFile = toIFile pd
+-
+-version :: PackageDescription -> String
+-version = intercalate "." . map show . versionNumbers . pkgVersion . package
+-
+--- | This returns @lib/prim@.
+---
+-projectRoot :: PackageDescription -> FilePath
+-projectRoot pd = takeDirectory agdaLibFile
+-  where
+-  [agdaLibFile] = filter ((".agda-lib" ==) . takeExtension) $ dataFiles pd
+-
+--- | Turns e.g. @lib/prim/Agda/Primitive.agda@
+---   into @lib/prim/_build/2.7.0/agda/Agda/Primitive.agdai@.
+---
+---   An absolute path will be returned unchanged.
+-toIFile ::
+-     PackageDescription
+-  -> FilePath            -- ^ Should be a relative path.
+-  -> FilePath            -- ^ Then this is also a relative path.
+-toIFile pd = (buildDir </>) . fileName
+-  where
+-  root = projectRoot pd
+-    -- e.g. root     = "lib/prim"
+-  buildDir = root </> "_build" </> version pd </> "agda"
+-    -- e.g. buildDir = "lib/prim/_build/2.7.0/agda"
+-  fileName file = makeRelative root $ replaceExtension file ".agdai"
+-    -- e.g. fileName "lib/prim/Agda/Primitive.agda" = "Agda/Primitive.agdai"
+-
+--- Andreas, 2019-10-21, issue #4151:
+--- skip the generation of interface files with program suffix "-quicker"
+-skipInterfaces :: LocalBuildInfo -> Bool
+-skipInterfaces lbi = fromPathTemplate (progSuffix lbi) == "-quicker"
+-
+--- | Returns 'True' if call to Agda executes without error.
+---
+-generateInterfaces :: PackageDescription -> LocalBuildInfo -> IO Bool
+-generateInterfaces pd lbi = do
+-
+-  putStrLn "Generating Agda core library interface files..."
+-
+-  -- for debugging, these are examples how you can inspect the flags...
+-  -- print $ flagAssignment lbi
+-  -- print $ fromPathTemplate $ progSuffix lbi
+-
+-  -- then...
+-  let bdir = buildDir lbi
+-      agda = bdir </> "agda" </> "agda" <.> agdaExeExtension
+-
+-  -- We should be in the current directory root of the cabal package
+-  -- and data-files reside in src/data relative to this.
+-  --
+-  ddir <- makeAbsolute $ "src" </> "data"
+-
+-  -- The Agda.Primitive* and Agda.Builtin* modules.
+-  let builtins = filter ((== ".agda") . takeExtension) (dataFiles pd)
+-
+-  -- The absolute filenames of their interfaces.
+-  let interfaces = map ((ddir </>) . toIFile pd) builtins
+-
+-  -- Remove all existing .agdai files.
+-  forM_ interfaces $ \ fp -> removeFile fp `catch` \ e ->
+-    unless (isDoesNotExistError e) $ throwIO e
+-
+-  -- Type-check all builtin modules (in a single Agda session to take
+-  -- advantage of caching).
+-  let agdaDirEnvVar = "Agda_datadir"
+-  let agdaArgs =
+-        [ "--interaction"
+-        , "--interaction-exit-on-error"
+-        , "-Werror"
+-        , "-v0"
+-        ]
+-  let loadBuiltinCmds = concat
+-        [ [ cmd ("Cmd_load " ++ f ++ " []")
+-          , cmd "Cmd_no_metas"
+-            -- Fail if any meta-variable is unsolved.
+-          ]
+-        | b <- builtins
+-        , let f     = show (ddir </> b)
+-              cmd c = "IOTCM " ++ f ++ " None Indirect (" ++ c ++ ")"
+-        ]
+-  let callLines = concat
+-        [ [ unwords $ concat
+-            [ [ concat [ agdaDirEnvVar, "=", ddir ] ]
+-            , [ agda ]
+-            , agdaArgs
+-            , [ "<<EOF" ]
+-            ]
+-          ]
+-        , loadBuiltinCmds
+-        , [ "EOF" ]
+-        ]
+-  let onIOError (e :: IOException) = False <$ do
+-        warn $ concat
+-          [ [ "*** Could not generate Agda library interface files."
+-            , "*** Reason:"
+-            , show e
+-            , "*** The attempted call to Agda was:"
+-            ]
+-          , callLines
+-          ]
+-  env <- getEnvironment
+-  handle onIOError $ do
+-
+-    -- Generate interface files via a call to Agda.
+-    readCreateProcess
+-      (proc agda agdaArgs)
+-        { delegate_ctlc = True
+-                          -- Make Agda look for data files in a
+-                          -- certain place.
+-        , env           = Just ((agdaDirEnvVar, ddir) : env)
+-        }
+-      (unlines loadBuiltinCmds)
+-
+-    -- Check whether all interface files have been generated.
+-    missing <- catMaybes <$> forM interfaces \ f ->
+-      doesFileExist f <&> \case
+-        True  -> Nothing
+-        False -> Just f
+-
+-    -- Warn if not all interface files have been generated, but don't crash.
+-    -- This might help with issue #7455.
+-    let success = null missing
+-    unless success $ warn $ concat
+-      [ [ "*** Agda failed to generate the following library interface files:" ]
+-      , missing
+-      ]
+-    return success
+-
+-warn :: [String] -> IO ()
+-warn msgs = putStr $ unlines $ concat
+-    [ [ "*** Warning!" ]
+-    , msgs
+-    , [ "*** Ignoring error, continuing installation..." ]
+-    ]
+-
+-
+-
+-agdaExeExtension :: String
+-agdaExeExtension = exeExtension buildPlatform

patches/bv-sized-1.0.5.patch

+diff --git a/bv-sized.cabal b/bv-sized.cabal
+index 5ff840f..9a6222c 100644
+--- a/bv-sized.cabal
++++ b/bv-sized.cabal
+@@ -32,7 +32,7 @@ library
+                        deepseq >= 1.4.0 && < 1.5.0,
+                        panic >= 0.4.0 && < 0.5,
+                        parameterized-utils >= 2.0.2 && < 2.2,
+-                       random >= 1.2.0 && < 1.3,
++                       random >= 1.3.0 && < 1.4,
+                        th-lift >= 0.8.1 && < 0.9
+   hs-source-dirs:      src
+   default-language:    Haskell2010
+diff --git a/src/Data/BitVector/Sized/Signed.hs b/src/Data/BitVector/Sized/Signed.hs
+index 691d248..05c8ade 100644
+--- a/src/Data/BitVector/Sized/Signed.hs
++++ b/src/Data/BitVector/Sized/Signed.hs
+@@ -1,3 +1,4 @@
++{-# LANGUAGE CPP #-}
+ {-# LANGUAGE DataKinds #-}
+ {-# LANGUAGE DeriveAnyClass #-}
+ {-# LANGUAGE DeriveGeneric #-}
+@@ -141,6 +142,10 @@ instance KnownNat w => Uniform (SignedBV w) where
+ instance (KnownNat w, 1 <= w) => UniformRange (SignedBV w) where
+   uniformRM (SignedBV lo, SignedBV hi) g =
+     SignedBV <$> BV.sUniformRM knownNat (lo, hi) g
++#if MIN_VERSION_random(1,3,0)
++  isInRange (lo, hi) x =
++    lo <= x && x <= hi
++#endif
+ 
+ instance (KnownNat w, 1 <= w) => Random (SignedBV w)
+ 
+diff --git a/src/Data/BitVector/Sized/Unsigned.hs b/src/Data/BitVector/Sized/Unsigned.hs
+index 65f3ece..f9cb94f 100644
+--- a/src/Data/BitVector/Sized/Unsigned.hs
++++ b/src/Data/BitVector/Sized/Unsigned.hs
+@@ -1,3 +1,4 @@
++{-# LANGUAGE CPP #-}
+ {-# LANGUAGE DataKinds #-}
+ {-# LANGUAGE DeriveAnyClass #-}
+ {-# LANGUAGE DeriveGeneric #-}
+@@ -132,6 +133,10 @@ instance KnownNat w => Uniform (UnsignedBV w) where
+ instance UniformRange (UnsignedBV w) where
+   uniformRM (UnsignedBV lo, UnsignedBV hi) g =
+     UnsignedBV <$> BV.uUniformRM (lo, hi) g
++#if MIN_VERSION_random(1,3,0)
++  isInRange (lo, hi) x =
++    lo <= x && x <= hi
++#endif
+ 
+ instance KnownNat w => Random (UnsignedBV w)
+ 

patches/cabal-doctest-1.0.9.patch

-diff --git a/cabal-doctest.cabal b/cabal-doctest.cabal
-index 30aeb12..2fef71f 100644
---- a/cabal-doctest.cabal
-+++ b/cabal-doctest.cabal
-@@ -1,5 +1,6 @@
- name:               cabal-doctest
- version:            1.0.9
-+x-revision:         2
- synopsis:           A Setup.hs helper for running doctests
- description:
-   As of now (end of 2021), there isn't @cabal doctest@
-@@ -20,20 +21,21 @@ extra-source-files:
-   README.md
- 
- tested-with:
--  GHC == 7.0.4
--  GHC == 7.2.2
--  GHC == 7.4.2
--  GHC == 7.6.3
--  GHC == 7.8.4
--  GHC == 7.10.3
--  GHC == 8.0.2
--  GHC == 8.2.2
--  GHC == 8.4.4
--  GHC == 8.6.5
--  GHC == 8.8.4
-+  GHC == 9.4.1
-+  GHC == 9.2.4
-+  GHC == 9.0.2
-   GHC == 8.10.7
--  GHC == 9.0.1
--  GHC == 9.2.1
-+  GHC == 8.8.4
-+  GHC == 8.6.5
-+  GHC == 8.4.4
-+  GHC == 8.2.2
-+  GHC == 8.0.2
-+  GHC == 7.10.3
-+  GHC == 7.8.4
-+  GHC == 7.6.3
-+  GHC == 7.4.2
-+  GHC == 7.2.2
-+  GHC == 7.0.4
- 
- source-repository head
-   type:     git
-@@ -44,8 +46,8 @@ library
-   other-modules:
-   other-extensions:
-   build-depends:
--      base       >=4.3  && <4.17
--    , Cabal      >=1.10 && <3.8
-+      base       >=4.3  && <5
-+    , Cabal      >=1.10 && <3.10
-     , directory
-     , filepath
- 
-diff --git a/src/Distribution/Extra/Doctest.hs b/src/Distribution/Extra/Doctest.hs
-index ac5d07d..17b3d0d 100644
---- a/src/Distribution/Extra/Doctest.hs
-+++ b/src/Distribution/Extra/Doctest.hs
-@@ -125,7 +125,7 @@ import Distribution.Types.LibraryName
-        (libraryNameString)
- #endif
- 
--#if MIN_VERSION_Cabal(3,6,0)
-+#if MIN_VERSION_Cabal(3,5,0)
- import Distribution.Utils.Path
-        (getSymbolicPath)
- #endif
-@@ -331,7 +331,7 @@ generateBuildModule testSuiteName flags pkg lbi = do
-               <- mapM makeAbsolute
-                $ compAutogenDir           -- autogenerated files
-                : (distPref ++ "/build")   -- preprocessed files (.hsc -> .hs); "build" is hardcoded in Cabal.
--#if MIN_VERSION_Cabal(3,6,0)
-+#if MIN_VERSION_Cabal(3,5,0)
-                : map getSymbolicPath (hsSourceDirs compBI)
- #else
-                : hsSourceDirs compBI

patches/doctest-0.24.0.patch

+diff --git a/src/Extract.hs b/src/Extract.hs
+index f8237de..4ca77cc 100644
+--- a/src/Extract.hs
++++ b/src/Extract.hs
+@@ -1,4 +1,5 @@
+ {-# LANGUAGE CPP #-}
++{-# LANGUAGE LambdaCase #-}
+ module Extract (Module(..), extract) where
+ 
+ import           Imports hiding (mod, concat)
+@@ -115,7 +116,11 @@ parse args = withGhc args $ \modules_ -> withTempOutputDir $ do
+                      $ filterToposortToModules
+ #endif
+                      $ topSortModuleGraph False mods Nothing
++#if __GLASGOW_HASKELL__ >= 913
++  reverse <$> (mapM (loadModPlugins >=> parseModule) $ mapMaybe (\case ModuleNodeCompile mod -> Just mod; _ -> Nothing) sortedMods)
++#else
+   reverse <$> mapM (loadModPlugins >=> parseModule) sortedMods
++#endif
+   where
+ 
+     -- copied from Haddock/GhcUtils.hs

patches/extra-1.7.14.patch

-diff --git a/src/Data/List/Extra.hs b/src/Data/List/Extra.hs
-index 076a682..db3ed52 100644
---- a/src/Data/List/Extra.hs
-+++ b/src/Data/List/Extra.hs
-@@ -39,7 +39,7 @@ module Data.List.Extra(
-     ) where
- 
- import Partial
--import Data.List
-+import Data.List hiding (compareLength)
- import Data.Maybe
- import Data.Function
- import Data.Char
-diff --git a/src/Data/List/NonEmpty/Extra.hs b/src/Data/List/NonEmpty/Extra.hs
-index 1ac16cc..66c2b59 100644
---- a/src/Data/List/NonEmpty/Extra.hs
-+++ b/src/Data/List/NonEmpty/Extra.hs
-@@ -62,11 +62,14 @@ appendl (x :| xs) l = x :| (xs ++ l)
- appendr :: [a] -> NonEmpty a -> NonEmpty a
- appendr l nel = foldr cons nel l
- 
-+-- replace with !MIN_VERSION_base(4,20,0) later
-+#if __GLASGOW_HASKELL__ < 909
- -- | Sort by comparing the results of a function applied to each element.
- --   The sort is stable, and the function is evaluated only once for
- --   each element.
- sortOn :: Ord b => (a -> b) -> NonEmpty a -> NonEmpty a
- sortOn f = fromList . List.sortOn f . toList
-+#endif
- 
- -- | Return the union of two non-empty lists. Duplicates, and elements of the
- --   first list, are removed from the the second list, but if the first list
-diff --git a/src/Extra.hs b/src/Extra.hs
-index cd729aa..a7e7bc8 100644
---- a/src/Extra.hs
-+++ b/src/Extra.hs
-@@ -62,7 +62,7 @@ import Control.Monad.Extra
- import Data.Either.Extra
- import Data.IORef.Extra
- import Data.List.Extra
--import Data.List.NonEmpty.Extra hiding (cons, snoc, sortOn, union, unionBy, nubOrd, nubOrdBy, nubOrdOn, (!?), foldl1', repeatedly)
-+import Data.List.NonEmpty.Extra hiding (cons, snoc, sortOn, union, unionBy, nubOrd, nubOrdBy, nubOrdOn, (!?), foldl1', repeatedly, compareLength)
- import Data.Monoid.Extra
- import Data.Tuple.Extra
- import Data.Version.Extra

patches/ghc-lib-parser-9.8.1.20231121.patch → patches/ghc-lib-parser-9.8.4.20241130.patch

@@ -14,50 +14,6 @@ index b3b52bd..5f78678 100644
        (PsErrExplicitForall (isUnicode tok))
  
  -- Hint about qualified-do
-diff --git a/compiler/cbits/genSym.c b/compiler/cbits/genSym.c
-index 0897547..03c6870 100644
---- a/compiler/cbits/genSym.c
-+++ b/compiler/cbits/genSym.c
-@@ -9,17 +9,35 @@
- //
- // The CPP is thus about the RTS version GHC is linked against, and not the
- // version of the GHC being built.
-+#if !MIN_VERSION_GLASGOW_HASKELL(9,9,0,0)
-+HsWord64 ghc_unique_counter64 = 0;
-+#endif
- #if !MIN_VERSION_GLASGOW_HASKELL(9,3,0,0)
--HsInt ghc_unique_counter = 0;
- HsInt ghc_unique_inc     = 1;
- #endif
- 
--#define UNIQUE_BITS (sizeof (HsInt) * 8 - UNIQUE_TAG_BITS)
-+
-+// This function has been added to the RTS. Here we pessimistically assume
-+// that a threaded RTS is used. This function is only used for bootstrapping.
-+#if !MIN_VERSION_GLASGOW_HASKELL(9,9,0,0)
-+EXTERN_INLINE StgWord64
-+atomic_inc64(StgWord64 volatile* p, StgWord64 incr)
-+{
-+#if defined(HAVE_C11_ATOMICS)
-+    return __atomic_add_fetch(p, incr, __ATOMIC_SEQ_CST);
-+#else
-+    return __sync_add_and_fetch(p, incr);
-+#endif
-+}
-+#endif
-+
-+#define UNIQUE_BITS (sizeof (HsWord64) * 8 - UNIQUE_TAG_BITS)
- #define UNIQUE_MASK ((1ULL << UNIQUE_BITS) - 1)
- 
--HsInt ghc_lib_parser_genSym(void) {
--    HsInt u = atomic_inc((StgWord *)&ghc_unique_counter, ghc_unique_inc) & UNIQUE_MASK;
-+HsWord64 genSym(void) {
-+    HsWord64 u = atomic_inc64((StgWord64 *)&ghc_unique_counter64, ghc_unique_inc) & UNIQUE_MASK;
-     // Uh oh! We will overflow next time a unique is requested.
-     ASSERT(u != UNIQUE_MASK);
-     return u;
- }
-+
 diff --git a/libraries/template-haskell/Language/Haskell/TH/Syntax.hs b/libraries/template-haskell/Language/Haskell/TH/Syntax.hs
 index fccdbd3..aa131ae 100644
 --- a/libraries/template-haskell/Language/Haskell/TH/Syntax.hs

patches/ghc-typelits-extra-0.4.6.patch → patches/ghc-typelits-extra-0.4.7.patch

-diff --git a/CHANGELOG.md b/CHANGELOG.md
-index c87495b..4007a62 100644
---- a/CHANGELOG.md
-+++ b/CHANGELOG.md
-@@ -1,5 +1,13 @@
- # Changelog for the [`ghc-typelits-extra`](http://hackage.haskell.org/package/ghc-typelits-extra) package
- 
-+# 0.4.8
-+* Add support for GHC 9.11.20240522
-+
-+# 0.4.7 *May 22nd, 2024*
-+* Add support for GHC 9.10.1
-+* Fix Plugin silently fails when normalizing <= in GHC 9.4+ [#50](https://github.com/clash-lang/ghc-typelits-extra/issues/50)
-+* Fix faulty lookup for `Mod` and `Div` in GHC >= 9.2
-+
- # 0.4.6 *October 10th 2023*
- * Support for GHC-9.8.1
- 
-diff --git a/HACKING.md b/HACKING.md
-new file mode 100644
-index 0000000..3fe0cd3
---- /dev/null
-+++ b/HACKING.md
-@@ -0,0 +1,31 @@
-+#Hacking
-+Download sources:
-+```
-+git clone https://github.com/christiaanb/ghc-typelits-extra.git
-+git clone https://github.com/clash-lang/ghc-tcplugins-extra.git
-+git clone https://github.com/clash-lang/ghc-typelits-natnormalise.git
-+```
-+
-+Go to ghc-typelits-extra dir:
-+```
-+cd ghc-typelits-extra
-+```
-+
-+Run:
-+```
-+cabal sandbox init
-+cabal sandbox add-source ../ghc-typelits-extra
-+cabal sandbox add-source ../ghc-typelits-natnormalise
-+cabal install --dependencies-only --enable-tests
-+```
-+
-+Configure the package with testing enabled:
-+```
-+cabal configure --enable-tests
-+```
-+
-+Once you've finished hacking, build and test:
-+```
-+cabal build
-+cabal test
-+```
 diff --git a/ghc-typelits-extra.cabal b/ghc-typelits-extra.cabal
-index 77851bd..27ba1ba 100644
+index 115201e..5b11838 100644
 --- a/ghc-typelits-extra.cabal
 +++ b/ghc-typelits-extra.cabal
-@@ -1,5 +1,5 @@
- name:                ghc-typelits-extra
--version:             0.4.6
-+version:             0.4.8
- synopsis:            Additional type-level operations on GHC.TypeLits.Nat
- description:
-   Additional type-level operations on @GHC.TypeLits.Nat@:
-@@ -49,7 +49,7 @@ extra-source-files:  README.md
- cabal-version:       >=1.10
- tested-with:         GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.4, GHC == 8.6.5,
-                      GHC == 8.8.4, GHC == 8.10.7, GHC == 9.0.2, GHC == 9.2.8,
--                     GHC == 9.4.7, GHC == 9.6.3, GHC == 9.8.1
-+                     GHC == 9.4.7, GHC == 9.6.3, GHC == 9.8.2, GHC == 9.10.1
- 
- 
- source-repository head
-@@ -68,8 +68,8 @@ library
-   other-modules:       GHC.TypeLits.Extra.Solver.Unify
-                        GHC.TypeLits.Extra.Solver.Operations
-   build-depends:       base                      >= 4.8     && <5,
--                       containers                >= 0.5.7.1 && <0.7,
--                       ghc                       >= 7.10    && <9.10,
-+                       containers                >= 0.5.7.1 && <0.8,
-+                       ghc                       >= 7.10    && <9.12,
-                        ghc-prim                  >= 0.5     && <1.0,
-                        ghc-tcplugins-extra       >= 0.3.1,
-                        ghc-typelits-knownnat     >= 0.7.2   && <0.8,
-@@ -82,8 +82,12 @@ library
-   hs-source-dirs:      src
-   if impl(ghc >= 8.0) && impl(ghc < 9.4)
-     hs-source-dirs:    src-pre-ghc-9.4
--  if impl(ghc >= 9.4) && impl(ghc < 9.10)
-+  if impl(ghc >= 9.4) && impl(ghc < 9.11)
-     hs-source-dirs:    src-ghc-9.4
-+    build-depends:     template-haskell          >= 2.17    && <2.23
-+  if impl(ghc >= 9.11) && impl(ghc < 9.13)
-+    hs-source-dirs:    src-ghc-9.12
-+    build-depends:     template-haskell          >= 2.17    && <2.23
-   default-language:    Haskell2010
-   other-extensions:    DataKinds
-                        FlexibleInstances
-@@ -115,7 +119,7 @@ test-suite test-ghc-typelits-extra
-   hs-source-dirs:      tests
-   if impl(ghc >= 8.0) && impl(ghc < 9.4)
-     hs-source-dirs:    tests-pre-ghc-9.4
--  if impl(ghc >= 9.4) && impl(ghc < 9.10)
-+  if impl(ghc >= 9.4) && impl(ghc < 9.12)
-     hs-source-dirs:    tests-ghc-9.4
-   default-language:    Haskell2010
-   other-extensions:    DataKinds
+@@ -69,7 +69,7 @@ library
+                        GHC.TypeLits.Extra.Solver.Operations
+   build-depends:       base                      >= 4.8     && <5,
+                        containers                >= 0.5.7.1 && <0.8,
+-                       ghc                       >= 7.10    && <9.12,
++                       ghc                       >= 7.10    && <9.14,
+                        ghc-prim                  >= 0.5     && <1.0,
+                        ghc-tcplugins-extra       >= 0.3.1,
+                        ghc-typelits-knownnat     >= 0.7.2   && <0.8,
+@@ -82,9 +82,12 @@ library
+   hs-source-dirs:      src
+   if impl(ghc >= 8.0) && impl(ghc < 9.4)
+     hs-source-dirs:    src-pre-ghc-9.4
+-  if impl(ghc >= 9.4) && impl(ghc < 9.12)
++  if impl(ghc >= 9.4) && impl(ghc < 9.11)
+     hs-source-dirs:    src-ghc-9.4
+     build-depends:     template-haskell          >= 2.17    && <2.23
++  if impl(ghc >= 9.11) && impl(ghc < 9.14)
++    hs-source-dirs:    src-ghc-9.12
++    build-depends:     template-haskell          >= 2.17    && <2.23
+   default-language:    Haskell2010
+   other-extensions:    DataKinds
+                        FlexibleInstances
+@@ -116,7 +119,7 @@ test-suite test-ghc-typelits-extra
+   hs-source-dirs:      tests
+   if impl(ghc >= 8.0) && impl(ghc < 9.4)
+     hs-source-dirs:    tests-pre-ghc-9.4
+-  if impl(ghc >= 9.4) && impl(ghc < 9.12)
++  if impl(ghc >= 9.4) && impl(ghc < 9.14)
+     hs-source-dirs:    tests-ghc-9.4
+   default-language:    Haskell2010
+   other-extensions:    DataKinds
 diff --git a/src-ghc-9.12/GHC/TypeLits/Extra/Solver.hs b/src-ghc-9.12/GHC/TypeLits/Extra/Solver.hs
 new file mode 100644
-index 0000000..eb5dcd5
+index 0000000..4f64869
 --- /dev/null
 +++ b/src-ghc-9.12/GHC/TypeLits/Extra/Solver.hs
-@@ -0,0 +1,349 @@
+@@ -0,0 +1,347 @@
 +{-|
 +Copyright  :  (C) 2015-2016, University of Twente
 +License    :  BSD2 (see the file LICENSE)
 +Maintainer :  Christiaan Baaij <christiaan.baaij@gmail.com>
-+
 +To use the plugin, add the
-+
 +@
 +{\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver \#-\}
 +@
-+
 +pragma to the header of your file
-+
 +-}
 +
 +{-# LANGUAGE TupleSections #-}
@@ -149,7 +72,7 @@ index 0000000..eb5dcd5
 +import GHC.Builtin.Types (promotedTrueDataCon, promotedFalseDataCon)
 +import GHC.Builtin.Types (boolTy, naturalTy, cTupleDataCon, cTupleTyCon)
 +import GHC.Builtin.Types.Literals (typeNatDivTyCon, typeNatModTyCon, typeNatCmpTyCon)
-+import GHC.Core.Coercion (mkUnivCo)
++import GHC.Core.Coercion (Coercion, mkUnivCo)
 +import GHC.Core.DataCon (dataConWrapId)
 +import GHC.Core.Predicate (EqRel (NomEq), Pred (EqPred, IrredPred), classifyPredType)
 +import GHC.Core.Reduction (Reduction(..))
@@ -160,15 +83,17 @@ index 0000000..eb5dcd5
 +import GHC.Data.IOEnv (getEnv)
 +import GHC.Driver.Env (hsc_NC)
 +import GHC.Driver.Plugins (Plugin (..), defaultPlugin, purePlugin)
-+import GHC.Plugins (DCoVarSet, Var, emptyDVarSet, extendDVarSet, thNameToGhcNameIO)
++import GHC.Plugins (thNameToGhcNameIO)
 +import GHC.Tc.Plugin
 +  (TcPluginM, tcLookupTyCon, tcPluginTrace, tcPluginIO, unsafeTcPluginTcM)
 +import GHC.Tc.Types
 +  (TcPlugin(..), TcPluginSolveResult (..), TcPluginRewriter, TcPluginRewriteResult (..),
 +   Env (env_top))
 +import GHC.Tc.Types.Constraint
-+  (Ct, ctEvidence, ctEvId, ctEvPred, ctLoc, isWantedCt)
-+import GHC.Tc.Types.Constraint (Ct (..), DictCt(..), EqCt(..), IrredCt(..), qci_ev)
++  (Ct, ctEvidence, ctEvPred, ctLoc, isWantedCt)
++import GHC.Tc.Types.Constraint
++  (Ct (..), DictCt(..), EqCt(..), IrredCt(..),
++   qci_ev, ctEvCoercion)
 +import GHC.Tc.Types.Evidence (EvTerm, EvBindsVar, Role(..), evCast, evId)
 +import GHC.Types.Unique.FM (UniqFM, listToUFM)
 +import GHC.Utils.Outputable (Outputable (..), (<+>), ($$), text)
@@ -239,7 +164,7 @@ index 0000000..eb5dcd5
 +
 +    reduce tc args res = Reduction co res
 +     where
-+      co = mkUnivCo (PluginProv "ghc-typelits-extra" emptyDVarSet) Nominal
++      co = mkUnivCo (PluginProv "ghc-typelits-extra") [] Nominal
 +             (mkTyConApp tc args) res
 +
 +
@@ -259,7 +184,7 @@ index 0000000..eb5dcd5
 +
 +data SolverConstraint
 +   = NatEquality Ct ExtraOp ExtraOp Normalised
-+   | NatInequality Ct DCoVarSet ExtraOp ExtraOp Bool Normalised
++   | NatInequality Ct [Coercion] ExtraOp ExtraOp Bool Normalised
 +
 +instance Outputable SolverConstraint where
 +  ppr (NatEquality ct op1 op2 norm) =
@@ -286,11 +211,11 @@ index 0000000..eb5dcd5
 +      ur <- unifyExtra ct u v
 +      tcPluginTrace "unifyExtra result" (ppr ur)
 +      case ur of
-+        Win -> simples (((,) <$> evMagic ct emptyDVarSet <*> pure ct):evs) news eqs'
++        Win -> simples (((,) <$> evMagic ct [] <*> pure ct):evs) news eqs'
 +        Lose | null evs && null eqs' -> return (Impossible eq)
 +        _ | norm == Normalised && isWantedCt ct -> do
 +          newCt <- createWantedFromNormalised defs eq
-+          simples (((,) <$> evMagic ct emptyDVarSet <*> pure ct):evs) (newCt:news) eqs'
++          simples (((,) <$> evMagic ct [] <*> pure ct):evs) (newCt:news) eqs'
 +        Lose -> simples evs news eqs'
 +        Draw -> simples evs news eqs'
 +    simples evs news (eq@(NatInequality ct deps u v b norm):eqs') = do
@@ -310,7 +235,7 @@ index 0000000..eb5dcd5
 +          | b -> case findMax q eqs of
 +                   Just (i,m) ->
 +                      simples evs news
-+                        (NatInequality ct (extendDVarSet deps i) p m b norm:eqs')
++                        (NatInequality ct (i:deps) p m b norm:eqs')
 +                   Nothing -> simples evs news eqs'
 +        _ | norm == Normalised && isWantedCt ct -> do
 +          newCt <- createWantedFromNormalised defs eq
@@ -318,16 +243,16 @@ index 0000000..eb5dcd5
 +        _ -> simples evs news eqs'
 +
 +    -- look for given constraint with the form: c ~ Max x y
-+    findMax :: ExtraOp -> [SolverConstraint] -> Maybe (Var, ExtraOp)
++    findMax :: ExtraOp -> [SolverConstraint] -> Maybe (Coercion, ExtraOp)
 +    findMax c = go
 +      where
 +        go [] = Nothing
 +        go ((NatEquality ct a b@(Max _ _) _) :_)
 +          | c == a && not (isWantedCt ct)
-+            = Just (ctEvId ct, b)
++            = Just (ctEvCoercion (ctEvidence ct), b)
 +        go ((NatEquality ct a@(Max _ _) b _) :_)
 +          | c == b && not (isWantedCt ct)
-+            = Just (ctEvId ct, a)
++            = Just (ctEvCoercion (ctEvidence ct), a)
 +        go (_:rest) = go rest
 +
 +
@@ -352,10 +277,10 @@ index 0000000..eb5dcd5
 +          (x', n1) <- normaliseNat defs x
 +          (y', n2) <- normaliseNat defs y
 +          let res | tc' == promotedTrueDataCon
-+                  = pure (NatInequality ct emptyDVarSet x' y' True
++                  = pure (NatInequality ct [] x' y' True
 +                            (mergeNormalised n1 n2))
 +                  | tc' == promotedFalseDataCon
-+                  = pure (NatInequality ct emptyDVarSet x' y' False
++                  = pure (NatInequality ct [] x' y' False
 +                            (mergeNormalised n1 n2))
 +                  | otherwise                   = fail "Nothing"
 +          res
@@ -376,7 +301,7 @@ index 0000000..eb5dcd5
 +      -> do
 +          (x', n1) <- normaliseNat defs x
 +          (y', n2) <- normaliseNat defs y
-+          pure (NatInequality ct emptyDVarSet x' y' True  (mergeNormalised n1 n2))
++          pure (NatInequality ct [] x' y' True  (mergeNormalised n1 n2))
 +    IrredPred (TyConApp tc [TyConApp ordCondTc zs, _])
 +      | tc == assertTC defs
 +      , ordCondTc == ordTyCon defs
@@ -392,7 +317,7 @@ index 0000000..eb5dcd5
 +      -> do
 +          (x', n1) <- normaliseNat defs x
 +          (y', n2) <- normaliseNat defs y
-+          pure (NatInequality ct emptyDVarSet x' y' True  (mergeNormalised n1 n2))
++          pure (NatInequality ct [] x' y' True  (mergeNormalised n1 n2))
 +    _ -> fail "Nothing"
 +  where
 +    isNatKind :: Kind -> Bool
@@ -453,223 +378,12 @@ index 0000000..eb5dcd5
 +    maybe (fail $ "Failed to lookup " ++ show th) return res
 +
 +-- Utils
-+evMagic :: Ct -> DCoVarSet -> Maybe EvTerm
++evMagic :: Ct -> [Coercion] -> Maybe EvTerm
 +evMagic ct deps = case classifyPredType $ ctEvPred $ ctEvidence ct of
 +    EqPred NomEq t1 t2 -> Just (evByFiatWithDependencies "ghc-typelits-extra" deps t1 t2)
 +    IrredPred p ->
 +      let t1 = mkTyConApp (cTupleTyCon 0) []
-+          co = mkUnivCo (PluginProv "ghc-typelits-extra" deps) Representational t1 p
++          co = mkUnivCo (PluginProv "ghc-typelits-extra") deps Representational t1 p
 +          dcApp = evId (dataConWrapId (cTupleDataCon 0))
 +       in Just (evCast dcApp co)
 +    _ -> Nothing
-diff --git a/src-ghc-9.4/GHC/TypeLits/Extra/Solver.hs b/src-ghc-9.4/GHC/TypeLits/Extra/Solver.hs
-index 809d3e2..8d2ed0e 100644
---- a/src-ghc-9.4/GHC/TypeLits/Extra/Solver.hs
-+++ b/src-ghc-9.4/GHC/TypeLits/Extra/Solver.hs
-@@ -15,6 +15,7 @@ pragma to the header of your file
- 
- {-# LANGUAGE CPP #-}
- {-# LANGUAGE TupleSections #-}
-+{-# LANGUAGE TemplateHaskellQuotes #-}
- 
- {-# OPTIONS_HADDOCK show-extensions #-}
- 
-@@ -25,15 +26,15 @@ where
- -- external
- import Control.Monad.Trans.Maybe (MaybeT (..))
- import Data.Maybe (catMaybes)
--import GHC.TcPluginM.Extra
--  (evByFiat, lookupModule, lookupName, tracePlugin, newWanted)
-+import GHC.TcPluginM.Extra (evByFiat, tracePlugin, newWanted)
-+import qualified Data.Type.Ord
-+import qualified GHC.TypeError
- 
- -- GHC API
--import GHC.Builtin.Names (eqPrimTyConKey, hasKey)
-+import GHC.Builtin.Names (eqPrimTyConKey, hasKey, getUnique)
- import GHC.Builtin.Types (promotedTrueDataCon, promotedFalseDataCon)
- import GHC.Builtin.Types (boolTy, naturalTy, cTupleDataCon, cTupleTyCon)
--import GHC.Builtin.Types.Literals (typeNatTyCons)
--import GHC.Builtin.Types.Literals (typeNatCmpTyCon)
-+import GHC.Builtin.Types.Literals (typeNatDivTyCon, typeNatModTyCon, typeNatCmpTyCon)
- import GHC.Core.Coercion (mkUnivCo)
- import GHC.Core.DataCon (dataConWrapId)
- import GHC.Core.Predicate (EqRel (NomEq), Pred (EqPred, IrredPred), classifyPredType)
-@@ -46,10 +47,12 @@ import GHC.Core.TyCo.Compare (eqType)
- #else
- import GHC.Core.Type (eqType)
- #endif
--import GHC.Data.FastString (fsLit)
-+import GHC.Data.IOEnv (getEnv)
-+import GHC.Driver.Env (hsc_NC)
- import GHC.Driver.Plugins (Plugin (..), defaultPlugin, purePlugin)
--import GHC.Tc.Plugin (TcPluginM, tcLookupTyCon, tcPluginTrace)
--import GHC.Tc.Types (TcPlugin(..), TcPluginSolveResult (..), TcPluginRewriter, TcPluginRewriteResult (..))
-+import GHC.Plugins (thNameToGhcNameIO)
-+import GHC.Tc.Plugin (TcPluginM, tcLookupTyCon, tcPluginTrace, tcPluginIO, unsafeTcPluginTcM)
-+import GHC.Tc.Types (TcPlugin(..), TcPluginSolveResult (..), TcPluginRewriter, TcPluginRewriteResult (..), Env (env_top))
- import GHC.Tc.Types.Constraint
-   (Ct, ctEvidence, ctEvPred, ctLoc, isWantedCt)
- #if MIN_VERSION_ghc(9,8,0)
-@@ -58,14 +61,17 @@ import GHC.Tc.Types.Constraint (Ct (..), DictCt(..), EqCt(..), IrredCt(..), qci_
- import GHC.Tc.Types.Constraint (Ct (CQuantCan), qci_ev, cc_ev)
- #endif
- import GHC.Tc.Types.Evidence (EvTerm, EvBindsVar, Role(..), evCast, evId)
--import GHC.Types.Name.Occurrence (mkTcOcc)
- import GHC.Types.Unique.FM (UniqFM, listToUFM)
--import GHC.Unit.Module (mkModuleName)
- import GHC.Utils.Outputable (Outputable (..), (<+>), ($$), text)
-+import GHC (Name)
-+
-+-- template-haskell
-+import qualified Language.Haskell.TH as TH
- 
- -- internal
- import GHC.TypeLits.Extra.Solver.Operations
- import GHC.TypeLits.Extra.Solver.Unify
-+import GHC.TypeLits.Extra
- 
- -- | A solver implement as a type-checker plugin for:
- --
-@@ -289,7 +295,8 @@ createWantedFromNormalised defs sct = do
-   let (ct, t1, t2) = extractCtSides sct
-   newPredTy <- case splitTyConApp_maybe $ ctEvPred $ ctEvidence ct of
-     Just (tc, [a, b, _, _]) | tc `hasKey` eqPrimTyConKey -> pure (mkTyConApp tc [a, b, t1, t2])
--    _ -> fail "Nothing"
-+    Just (tc, [_, b]) | tc `hasKey` getUnique (assertTC defs) -> pure (mkTyConApp tc [t1,b])
-+    _ -> error "Impossible: neither (<=?) nor Assert"
-   ev <- newWanted (ctLoc ct) newPredTy
-   let ctN = case ct of
-               CQuantCan qc -> CQuantCan (qc { qci_ev = ev})
-@@ -309,27 +316,25 @@ fromSolverConstraint (NatInequality ct _ _ _ _) = ct
- 
- lookupExtraDefs :: TcPluginM ExtraDefs
- lookupExtraDefs = do
--    md <- lookupModule myModule myPackage
--    md1 <- lookupModule ordModule basePackage
--    md2 <- lookupModule typeErrModule basePackage
--    ExtraDefs <$> look md "Max"
--              <*> look md "Min"
--              <*> pure (typeNatTyCons !! 5)
--              <*> pure (typeNatTyCons !! 6)
--              <*> look md "FLog"
--              <*> look md "CLog"
--              <*> look md "Log"
--              <*> look md "GCD"
--              <*> look md "LCM"
--              <*> look md1 "OrdCond"
--              <*> look md2 "Assert"
-+    ExtraDefs <$> look ''GHC.TypeLits.Extra.Max
-+              <*> look ''GHC.TypeLits.Extra.Min
-+              <*> pure typeNatDivTyCon
-+              <*> pure typeNatModTyCon
-+              <*> look ''GHC.TypeLits.Extra.FLog
-+              <*> look ''GHC.TypeLits.Extra.CLog
-+              <*> look ''GHC.TypeLits.Extra.Log
-+              <*> look ''GHC.TypeLits.Extra.GCD
-+              <*> look ''GHC.TypeLits.Extra.LCM
-+              <*> look ''Data.Type.Ord.OrdCond
-+              <*> look ''GHC.TypeError.Assert
-   where
--    look md s = tcLookupTyCon =<< lookupName md (mkTcOcc s)
--    myModule  = mkModuleName "GHC.TypeLits.Extra"
--    myPackage = fsLit "ghc-typelits-extra"
--    ordModule   = mkModuleName "Data.Type.Ord"
--    basePackage = fsLit "base"
--    typeErrModule = mkModuleName "GHC.TypeError"
-+    look nm = tcLookupTyCon =<< lookupTHName nm
-+
-+lookupTHName :: TH.Name -> TcPluginM Name
-+lookupTHName th = do
-+    nc <- unsafeTcPluginTcM (hsc_NC . env_top <$> getEnv)
-+    res <- tcPluginIO $ thNameToGhcNameIO nc th
-+    maybe (fail $ "Failed to lookup " ++ show th) return res
- 
- -- Utils
- evMagic :: Ct -> Maybe EvTerm
-diff --git a/src-pre-ghc-9.4/GHC/TypeLits/Extra/Solver.hs b/src-pre-ghc-9.4/GHC/TypeLits/Extra/Solver.hs
-index 1ad5d3b..3d9a9d3 100644
---- a/src-pre-ghc-9.4/GHC/TypeLits/Extra/Solver.hs
-+++ b/src-pre-ghc-9.4/GHC/TypeLits/Extra/Solver.hs
-@@ -42,7 +42,7 @@ import GHC.Builtin.Types (boolTy, naturalTy)
- #else
- import GHC.Builtin.Types (typeNatKind)
- #endif
--import GHC.Builtin.Types.Literals (typeNatTyCons)
-+import GHC.Builtin.Types.Literals (typeNatDivTyCon, typeNatModTyCon)
- #if MIN_VERSION_ghc(9,2,0)
- import GHC.Builtin.Types.Literals (typeNatCmpTyCon)
- #else
-@@ -82,7 +82,7 @@ import TyCoRep    (Type (..))
- import TysWiredIn (typeNatKind, promotedTrueDataCon, promotedFalseDataCon)
- import TcTypeNats (typeNatLeqTyCon)
- #if MIN_VERSION_ghc(8,4,0)
--import TcTypeNats (typeNatTyCons)
-+import TcTypeNats (typeNatDivTyCon, typeNatModTyCon)
- #else
- import TcPluginM  (zonkCt)
- #endif
-@@ -313,8 +313,8 @@ lookupExtraDefs = do
-     ExtraDefs <$> look md "Max"
-               <*> look md "Min"
- #if MIN_VERSION_ghc(8,4,0)
--              <*> pure (typeNatTyCons !! 5)
--              <*> pure (typeNatTyCons !! 6)
-+              <*> pure typeNatDivTyCon
-+              <*> pure typeNatModTyCon
- #else
-               <*> look md "Div"
-               <*> look md "Mod"
-diff --git a/tests-ghc-9.4/ErrorTests.hs b/tests-ghc-9.4/ErrorTests.hs
-index 4cc5fbe..2bed8e3 100644
---- a/tests-ghc-9.4/ErrorTests.hs
-+++ b/tests-ghc-9.4/ErrorTests.hs
-@@ -212,14 +212,26 @@ testFail23Errors =
-   ["Couldn't match type ‘'True’ with ‘'False’"]
- 
- testFail24Errors =
-+#if __GLASGOW_HASKELL__ >= 910
-+  ["Couldn't match type ‘ghc-internal-9.1001.0:GHC.Internal.Data.Type.Ord.OrdCond"
-+  ,"(CmpNat z (Max x y)) 'True 'True 'False’"
-+  ,"with ‘'True’"]
-+#else
-   ["Couldn't match type ‘Data.Type.Ord.OrdCond"
-   ,"(CmpNat z (Max x y)) 'True 'True 'False’"
-   ,"with ‘'True’"]
-+#endif
- 
- testFail25Errors =
-+#if __GLASGOW_HASKELL__ >= 910
-+  ["Couldn't match type ‘ghc-internal-9.1001.0:GHC.Internal.Data.Type.Ord.OrdCond"
-+  ,"(CmpNat (x + 1) (Max x y)) 'True 'True 'False’"
-+  ,"with ‘'True’"]
-+#else
-   ["Couldn't match type ‘Data.Type.Ord.OrdCond"
-   ,"(CmpNat (x + 1) (Max x y)) 'True 'True 'False’"
-   ,"with ‘'True’"]
-+#endif
- 
- testFail26Errors =
- #if __GLASGOW_HASKELL__ >= 906
-diff --git a/tests/Main.hs b/tests/Main.hs
-index 4fa8382..d260275 100644
---- a/tests/Main.hs
-+++ b/tests/Main.hs
-@@ -223,6 +223,17 @@ test57
-   -> Proxy True
- test57 _ _ = id
- 
-+test58a
-+  :: 1 <= n
-+  => Proxy n
-+  -> Proxy n
-+test58a = id
-+
-+test58b
-+  :: Proxy (Max (n+2) 1)
-+  -> Proxy (Max (n+2) 1)
-+test58b = test58a
-+
- main :: IO ()
- main = defaultMain tests
- 

patches/ghc-typelits-knownnat-0.7.10.patch

-diff --git a/CHANGELOG.md b/CHANGELOG.md
-index 24c66bf..d03f767 100644
---- a/CHANGELOG.md
-+++ b/CHANGELOG.md
-@@ -1,5 +1,14 @@
- # Changelog for the [`ghc-typelits-knownnat`](http://hackage.haskell.org/package/ghc-typelits-knownnat) package
- 
-+## 0.7.13
-+* Support for GHC 9.11.20220522
-+
-+## 0.7.12 *May 22nd, 2024*
-+* Support for GHC 9.10.1
-+
-+## 0.7.11
-+* Fix infinite loop between plugin and solver pipeline
-+
- ## 0.7.10 *November 14th 2023*
- * Work around [GHC issue 23109](https://gitlab.haskell.org/ghc/ghc/-/issues/23109)
- 
-diff --git a/ghc-typelits-knownnat.cabal b/ghc-typelits-knownnat.cabal
-index c8254fb..0f4833d 100644
---- a/ghc-typelits-knownnat.cabal
-+++ b/ghc-typelits-knownnat.cabal
-@@ -1,5 +1,5 @@
- name:                ghc-typelits-knownnat
--version:             0.7.10
-+version:             0.7.13
- synopsis:            Derive KnownNat constraints from other KnownNat constraints
- description:
-   A type checker plugin for GHC that can derive \"complex\" @KnownNat@
-@@ -55,7 +55,7 @@ extra-source-files:  README.md
- cabal-version:       >=1.10
- tested-with:         GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.4, GHC == 8.6.5,
-                      GHC == 8.8.4, GHC == 8.10.7, GHC == 9.0.2, GHC == 9.2.8,
--                     GHC == 9.4.7, GHC == 9.6.3, GHC == 9.8.1
-+                     GHC == 9.4.7, GHC == 9.6.3, GHC == 9.8.2, GHC == 9.10.1
- 
- source-repository head
-   type: git
-@@ -87,12 +87,12 @@ library
-                        UndecidableInstances
-                        ViewPatterns
-   build-depends:       base                      >= 4.9      && <5,
--                       ghc                       >= 8.0.1    && <9.10,
-+                       ghc                       >= 8.0.1    && <9.12,
-                        ghc-prim                  >= 0.4.0.0  && <0.12,
-                        ghc-tcplugins-extra       >= 0.3.1,
-                        ghc-typelits-natnormalise >= 0.7.1    && <0.8,
-                        transformers              >= 0.5.2.0  && <0.7,
--                       template-haskell          >= 2.11.0.0 && <2.22
-+                       template-haskell          >= 2.11.0.0 && <2.23
-   hs-source-dirs:      src
-   default-language:    Haskell2010
-   if flag(deverror)
-@@ -101,7 +101,7 @@ library
-     ghc-options:       -Wall
-   if impl(ghc >= 8.0) && impl(ghc < 9.4)
-     hs-source-dirs:    src-pre-ghc-9.4
--  if impl(ghc >= 9.4) && impl(ghc < 9.10)
-+  if impl(ghc >= 9.4) && impl(ghc < 9.12)
-     hs-source-dirs:    src-ghc-9.4
-   if impl(ghc < 8.2)
-     build-depends:     integer-gmp               >= 0.5.1.0
-diff --git a/src-ghc-9.4/GHC/TypeLits/KnownNat/Solver.hs b/src-ghc-9.4/GHC/TypeLits/KnownNat/Solver.hs
-index 299030c..f51523c 100644
---- a/src-ghc-9.4/GHC/TypeLits/KnownNat/Solver.hs
-+++ b/src-ghc-9.4/GHC/TypeLits/KnownNat/Solver.hs
-@@ -88,7 +88,7 @@ Pragma to the header of your file.
- {-# LANGUAGE LambdaCase    #-}
- {-# LANGUAGE TupleSections #-}
- {-# LANGUAGE ViewPatterns  #-}
--
-+{-# LANGUAGE TemplateHaskellQuotes #-}
- {-# LANGUAGE Trustworthy   #-}
- 
- {-# OPTIONS_HADDOCK show-extensions #-}
-@@ -102,7 +102,9 @@ import Control.Arrow ((&&&), first)
- import Control.Monad.Trans.Maybe (MaybeT (..))
- import Control.Monad.Trans.Writer.Strict
- import Data.Maybe (catMaybes, fromMaybe, mapMaybe)
--import GHC.TcPluginM.Extra (lookupModule, lookupName, newWanted, tracePlugin)
-+import Data.Type.Ord (OrdCond)
-+import Data.Type.Bool (If)
-+import GHC.TcPluginM.Extra (newWanted, tracePlugin)
- import GHC.TypeLits.Normalise.SOP (SOP (..), Product (..), Symbol (..))
- import GHC.TypeLits.Normalise.Unify (CType (..),normaliseNat,reifySOP)
- 
-@@ -138,8 +140,8 @@ import GHC.Core.Type
- import GHC.Data.FastString (fsLit)
- import GHC.Driver.Plugins (Plugin (..), defaultPlugin, purePlugin)
- import GHC.Tc.Instance.Family (tcInstNewTyCon_maybe)
--import GHC.Tc.Plugin (TcPluginM, tcLookupClass, getInstEnvs, unsafeTcPluginTcM)
--import GHC.Tc.Types (TcPlugin(..), TcPluginSolveResult (..), getPlatform)
-+import GHC.Tc.Plugin (TcPluginM, tcLookupClass, getInstEnvs, unsafeTcPluginTcM, tcPluginIO, tcLookupTyCon)
-+import GHC.Tc.Types (TcPlugin(..), TcPluginSolveResult (..), getPlatform, env_top)
- import GHC.Tc.Types.Constraint
-   (Ct, ctEvExpr, ctEvidence, ctEvPred, ctLoc, mkNonCanonical)
- #if MIN_VERSION_ghc(9,6,0)
-@@ -152,12 +154,20 @@ import GHC.Tc.Types.Evidence
-   (EvTerm (..), EvExpr, EvBindsVar, evDFunApp, mkEvCast, mkTcSymCo, mkTcTransCo,
-    evTermCoercion_maybe)
- #endif
-+#if MIN_VERSION_ghc(9,11,0)
-+import GHC.Plugins (emptyDVarSet)
-+#endif
- import GHC.Types.Id (idType)
--import GHC.Types.Name (nameModule_maybe, nameOccName)
--import GHC.Types.Name.Occurrence (mkTcOcc, occNameString)
-+import GHC.Types.Name (nameModule_maybe, nameOccName, Name)
-+import GHC.Types.Name.Occurrence (occNameString)
- import GHC.Types.Unique.FM (emptyUFM)
- import GHC.Types.Var (DFunId)
--import GHC.Unit.Module (mkModuleName, moduleName, moduleNameString)
-+import GHC.Unit.Module (moduleName, moduleNameString)
-+import qualified Language.Haskell.TH as TH
-+import GHC.Plugins (thNameToGhcNameIO, TyCon)
-+import GHC.Driver.Env (hsc_NC)
-+import GHC.Data.IOEnv (getEnv)
-+import GHC.TypeLits.KnownNat
- 
- #if MIN_VERSION_ghc(9,6,0)
- mkTcSymCo :: Coercion -> Coercion
-@@ -174,6 +184,8 @@ data KnownNatDefs
-   , knownBoolNat2 :: Class
-   , knownNat2Bool :: Class
-   , knownNatN     :: Int -> Maybe Class -- ^ KnownNat{N}
-+  , ordCondTyCon  :: TyCon
-+  , ifTyCon       :: TyCon
-   }
- 
- -- | Simple newtype wrapper to distinguish the original (flattened) argument of
-@@ -322,13 +334,14 @@ toGivenEntry ct = let ct_ev = ctEvidence ct
- -- | Find the \"magic\" classes and instances in "GHC.TypeLits.KnownNat"
- lookupKnownNatDefs :: TcPluginM KnownNatDefs
- lookupKnownNatDefs = do
--    md     <- lookupModule myModule myPackage
--    kbC    <- look md "KnownBool"
--    kbn2C  <- look md "KnownBoolNat2"
--    kn2bC  <- look md "KnownNat2Bool"
--    kn1C   <- look md "KnownNat1"
--    kn2C   <- look md "KnownNat2"
--    kn3C   <- look md "KnownNat3"
-+    kbC    <- look ''KnownBool
-+    kbn2C  <- look ''KnownBoolNat2
-+    kn2bC  <- look ''KnownNat2Bool
-+    kn1C   <- look ''KnownNat1
-+    kn2C   <- look ''KnownNat2
-+    kn3C   <- look ''KnownNat3
-+    ordcond <- lookupTHName ''OrdCond >>= tcLookupTyCon
-+    ifTc <- lookupTHName ''If >>= tcLookupTyCon
-     return KnownNatDefs
-            { knownBool     = kbC
-            , knownBoolNat2 = kbn2C
-@@ -338,14 +351,17 @@ lookupKnownNatDefs = do
-                                    ; 3 -> Just kn3C
-                                    ; _ -> Nothing
-                                    }
-+           , ordCondTyCon  = ordcond
-+           , ifTyCon       = ifTc
-            }
-   where
--    look md s = do
--      nm   <- lookupName md (mkTcOcc s)
--      tcLookupClass nm
-+    look nm = lookupTHName nm >>= tcLookupClass
- 
--    myModule  = mkModuleName "GHC.TypeLits.KnownNat"
--    myPackage = fsLit "ghc-typelits-knownnat"
-+lookupTHName :: TH.Name -> TcPluginM Name
-+lookupTHName th = do
-+    nc <- unsafeTcPluginTcM (hsc_NC . env_top <$> getEnv)
-+    res <- tcPluginIO $ thNameToGhcNameIO nc th
-+    maybe (fail $ "Failed to lookup " ++ show th) return res
- 
- -- | Try to create evidence for a wanted constraint
- constraintToEvTerm
-@@ -385,7 +401,7 @@ constraintToEvTerm defs givens (ct,cls,op,orig) = do
-               () | Just knN_cls    <- knownNatN defs (length args0)
-                  , Right (inst, _) <- lookupUniqueInstEnv ienv knN_cls args1
-                  -> Just (inst,knN_cls,args0,args1)
--                 | fn0 == "Data.Type.Ord.OrdCond"
-+                 | tc == ordCondTyCon defs
-                  , [_,cmpNat,TyConApp t1 [],TyConApp t2 [],TyConApp f1 []] <- args0
-                  , TyConApp cmpNatTc args2@(arg2:_) <- cmpNat
-                  , cmpNatTc == typeNatCmpTyCon
-@@ -405,7 +421,7 @@ constraintToEvTerm defs givens (ct,cls,op,orig) = do
-                  -> Just (inst,knN_cls,args0,args1N)
-                  | (arg0:args0Rest) <- args0
-                  , length args0Rest == 3
--                 , fn0 == "Data.Type.Bool.If"
-+                 , tc == ifTyCon defs
-                  , let args1N = arg0:fn1:args0Rest
-                        knN_cls = knownNat2Bool defs
-                  , Right (inst, _) <- lookupUniqueInstEnv ienv knN_cls args1N
-@@ -493,6 +509,7 @@ constraintToEvTerm defs givens (ct,cls,op,orig) = do
-     -- Find a known constraint for a wanted, so that (modulo normalization)
-     -- the two are a constant offset apart.
-     offset :: Type -> TcPluginM (Maybe (EvTerm,[Ct]))
-+    offset LitTy{} = pure Nothing
-     offset want = runMaybeT $ do
-       let -- Get the knownnat contraints
-           unKn ty' = case classifyPredType ty' of
-@@ -662,7 +679,11 @@ makeOpDict (opCls,dfid) knCls tyArgsC tyArgsI z evArgs sM
-           Nothing -> op_to_kn
-           Just (_,rw) ->
-             let kn_co_rw = mkTyConAppCo Representational (classTyCon knCls) [rw]
-+#if MIN_VERSION_ghc(9,11,0)
-+                kn_co_co = mkUnivCo (PluginProv "ghc-typelits-knownnat" emptyDVarSet)
-+#else
-                 kn_co_co = mkUnivCo (PluginProv "ghc-typelits-knownnat")
-+#endif
-                             Representational
-                               (coercionRKind kn_co_rw)
-                               (mkTyConApp (classTyCon knCls) [z])
-@@ -778,7 +799,11 @@ makeOpDictByFiat (opCls,dfid) knCls tyArgsC tyArgsI z evArgs
-                        $ dropForAlls     -- KnownBool b => SBool b
-                        $ idType kn_meth  -- forall b. KnownBool b => SBool b
-     -- SBool b R~ Bool (The "Lie")
-+#if MIN_VERSION_ghc(9,11,0)
-+  , let kn_co_rep = mkUnivCo (PluginProv "ghc-typelits-knownnat" emptyDVarSet)
-+#else
-   , let kn_co_rep = mkUnivCo (PluginProv "ghc-typelits-knownnat")
-+#endif
-                              Representational
-                              (mkTyConApp kn_tcRep [z]) boolTy
-     -- KnownBoolNat2 f a b ~ SBool f
-diff --git a/src-pre-ghc-9.4/GHC/TypeLits/KnownNat/Solver.hs b/src-pre-ghc-9.4/GHC/TypeLits/KnownNat/Solver.hs
-index e07c2e8..ebc3a35 100644
---- a/src-pre-ghc-9.4/GHC/TypeLits/KnownNat/Solver.hs
-+++ b/src-pre-ghc-9.4/GHC/TypeLits/KnownNat/Solver.hs
-@@ -579,6 +579,7 @@ constraintToEvTerm defs givens (ct,cls,op,orig) = do
-     -- Find a known constraint for a wanted, so that (modulo normalization)
-     -- the two are a constant offset apart.
-     offset :: Type -> TcPluginM (Maybe (EvTerm,[Ct]))
-+    offset LitTy{} = pure Nothing
-     offset want = runMaybeT $ do
-       let -- Get the knownnat contraints
-           unKn ty' = case classifyPredType ty' of

patches/ghc-typelits-knownnat-0.7.12.patch

+diff --git a/ghc-typelits-knownnat.cabal b/ghc-typelits-knownnat.cabal
+index 079f520..780ac0b 100644
+--- a/ghc-typelits-knownnat.cabal
++++ b/ghc-typelits-knownnat.cabal
+@@ -87,7 +87,7 @@ library
+                        UndecidableInstances
+                        ViewPatterns
+   build-depends:       base                      >= 4.9      && <5,
+-                       ghc                       >= 8.0.1    && <9.12,
++                       ghc                       >= 8.0.1    && <9.14,
+                        ghc-prim                  >= 0.4.0.0  && <0.12,
+                        ghc-tcplugins-extra       >= 0.3.1,
+                        ghc-typelits-natnormalise >= 0.7.1    && <0.8,
+@@ -101,7 +101,7 @@ library
+     ghc-options:       -Wall
+   if impl(ghc >= 8.0) && impl(ghc < 9.4)
+     hs-source-dirs:    src-pre-ghc-9.4
+-  if impl(ghc >= 9.4) && impl(ghc < 9.12)
++  if impl(ghc >= 9.4) && impl(ghc < 9.14)
+     hs-source-dirs:    src-ghc-9.4
+   if impl(ghc < 8.2)
+     build-depends:     integer-gmp               >= 0.5.1.0
+diff --git a/src-ghc-9.4/GHC/TypeLits/KnownNat/Solver.hs b/src-ghc-9.4/GHC/TypeLits/KnownNat/Solver.hs
+index 7e8dadd..08ad863 100644
+--- a/src-ghc-9.4/GHC/TypeLits/KnownNat/Solver.hs
++++ b/src-ghc-9.4/GHC/TypeLits/KnownNat/Solver.hs
+@@ -677,6 +677,9 @@ makeOpDict (opCls,dfid) knCls tyArgsC tyArgsI z evArgs sM
+           Just (_,rw) ->
+             let kn_co_rw = mkTyConAppCo Representational (classTyCon knCls) [rw]
+                 kn_co_co = mkUnivCo (PluginProv "ghc-typelits-knownnat")
++#if MIN_VERSION_ghc(9,11,0)
++                            []
++#endif
+                             Representational
+                               (coercionRKind kn_co_rw)
+                               (mkTyConApp (classTyCon knCls) [z])
+@@ -793,6 +796,9 @@ makeOpDictByFiat (opCls,dfid) knCls tyArgsC tyArgsI z evArgs
+                        $ idType kn_meth  -- forall b. KnownBool b => SBool b
+     -- SBool b R~ Bool (The "Lie")
+   , let kn_co_rep = mkUnivCo (PluginProv "ghc-typelits-knownnat")
++#if MIN_VERSION_ghc(9,11,0)
++                             []
++#endif
+                              Representational
+                              (mkTyConApp kn_tcRep [z]) boolTy
+     -- KnownBoolNat2 f a b ~ SBool f

patches/ghc-typelits-natnormalise-0.7.9.patch → patches/ghc-typelits-natnormalise-0.7.10.patch

-diff --git a/CHANGELOG.md b/CHANGELOG.md
-index b46b16e..5d150b4 100644
---- a/CHANGELOG.md
-+++ b/CHANGELOG.md
-@@ -1,5 +1,11 @@
- # Changelog for the [`ghc-typelits-natnormalise`](http://hackage.haskell.org/package/ghc-typelits-natnormalise) package
- 
-+## 0.7.11
-+* Support for GHC 9.11.20240522
-+
-+## 0.7.10 *May 22nd 2024*
-+* Support for GHC 9.10.1
-+
- ## 0.7.9 *October 10th 2023*
- * Support for GHC 9.8.1
- 
-diff --git a/doc/ghc-typelits-natnormalise-hcar.tex b/doc/ghc-typelits-natnormalise-hcar.tex
-new file mode 100644
-index 0000000..1607f11
---- /dev/null
-+++ b/doc/ghc-typelits-natnormalise-hcar.tex
-@@ -0,0 +1,64 @@
-+\documentclass[DIV16,twocolumn,10pt]{scrreprt}
-+\usepackage{paralist}
-+\usepackage{graphicx}
-+\usepackage[final]{hcar}
-+
-+%include polycode.fmt
-+
-+\begin{document}
-+
-+\begin{hcarentry}{GHC type-checker plugin for kind Nat}
-+\report{Christiaan Baaij}
-+\status{actively developed}
-+% \participants{(PARTICIPANTS OTHER THAN MYSELF)}% optional
-+\makeheader
-+
-+% (WHAT IS IT?)
-+As of GHC version 7.10, GHC's type checking and inference mechanisms can be enriched by plugins.
-+This particular plugin enriches GHC's knowledge of arithmetic on the type-level.
-+Specifically it allows the compiler to reason about \emph{equalities} of types of kind \verb!GHC.TypeLits.Nat!.
-+
-+GHC's type-checker's knowledge of arithmetic is virtually non-existent: it doesn't know addition is associative and commutative, that multiplication distributes over addition, etc.
-+In a dependently-typed language, or in Haskell using singleton types, one can provide proofs for these properties and use them to type-check programs that depend on these properties in order to be (type-)correct.
-+However, most of these properties of arithmetic over natural number are elementary school level knowledge, and it is cumbersome and tiresome to keep on providing and proving them manually.
-+This type-checker plugin adds the knowledge of these properties to GHC's type-checker.
-+
-+For example, using this plugin, GHC now knows that:
-+\begin{verbatim}
-+(x + 2)^(y + 2)
-+\end{verbatim}
-+is equal to:
-+\begin{verbatim}
-+4*x*(2 + x)^y + 4*(2 + x)^y + (2 + x)^y*x^2
-+\end{verbatim}
-+
-+The way that the plugin works, is that it normalises arithmetic expressions to a normal form that very much resembles \emph{Cantor normal form for ordinals}(\url{http://en.wikipedia.org/wiki/Ordinal_arithmetic#Cantor_normal_form}).
-+Subsequently, it perform a simple syntactic equality of the two expressions.
-+Indeed, in the example above, the latter expression is the normal form of the former expression.
-+
-+% (WHAT IS ITS STATUS? / WHAT HAS HAPPENED SINCE LAST TIME?)
-+The main test suite for the plugin can be found at: \url{https://github.com/christiaanb/ghc-typelits-natnormalise/blob/master/tests/Tests.hs}.
-+It demonstrates what kind of \emph{correct} code can be written without type equality annotations, or the use of \verb!unsafeCoerce!.
-+
-+One important aspect of this plugin is that it only enriches the type checkers knowledge of equalities, but \underline{not} \emph{in}equalities.
-+That is, it does not allow GHC to solve constraints such as:
-+\begin{verbatim}
-+CmpNat (x + 2) (x + 3) ~ 'LT
-+\end{verbatim}
-+
-+% (CAN OTHERS GET IT?)
-+The plugin is available on hackage, for GHC version 7.10 and higher:
-+\begin{verbatim}
-+$ cabal update
-+$ cabal install ghc-typelits-natnormalise
-+\end{verbatim}
-+
-+% (WHAT ARE THE IMMEDIATE PLANS?)
-+Development focus for the plugin is on further testing and improving its testsuite.
-+
-+\FurtherReading
-+  \url{http://hackage.haskell.org/package/ghc-typelits-natnormalise} \\
-+  \url{http://hackage.haskell.org/package/base/docs/GHC-TypeLits.html}
-+\end{hcarentry}
-+
-+\end{document}
 diff --git a/ghc-typelits-natnormalise.cabal b/ghc-typelits-natnormalise.cabal
-index 1295e0c..57e9964 100644
+index 347de8c..b5149f2 100644
 --- a/ghc-typelits-natnormalise.cabal
 +++ b/ghc-typelits-natnormalise.cabal
-@@ -1,5 +1,5 @@
- name:                ghc-typelits-natnormalise
--version:             0.7.9
-+version:             0.7.11
- synopsis:            GHC typechecker plugin for types of kind GHC.TypeLits.Nat
- description:
-   A type checker plugin for GHC that can solve /equalities/ and /inequalities/
-@@ -50,7 +50,7 @@ extra-source-files:  README.md
- cabal-version:       >=1.10
- tested-with:         GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.4, GHC == 8.6.5,
-                      GHC == 8.8.4, GHC == 8.10.7, GHC == 9.0.2, GHC == 9.2.8,
--                     GHC == 9.4.7, GHC == 9.6.3, GHC == 9.8.1
-+                     GHC == 9.4.7, GHC == 9.6.3, GHC == 9.8.2, GHC == 9.10.1
- 
- source-repository head
-   type: git
-@@ -67,8 +67,8 @@ library
-                        GHC.TypeLits.Normalise.SOP,
-                        GHC.TypeLits.Normalise.Unify
-   build-depends:       base                >=4.9   && <5,
--                       containers          >=0.5.7.1 && <0.7,
--                       ghc                 >=8.0.1 && <9.10,
-+                       containers          >=0.5.7.1 && <0.8,
-+                       ghc                 >=8.0.1 && <9.12,
-                        ghc-tcplugins-extra >=0.3.1,
-                        transformers        >=0.5.2.0 && < 0.7
-   if impl(ghc >= 9.0.0)
-@@ -78,8 +78,12 @@ library
-   hs-source-dirs:      src
-   if impl(ghc >= 8.0) && impl(ghc < 9.4)
-     hs-source-dirs:    src-pre-ghc-9.4
--  if impl(ghc >= 9.4) && impl(ghc < 9.10)
-+  if impl(ghc >= 9.4) && impl(ghc < 9.11)
-     hs-source-dirs:    src-ghc-9.4
-+    build-depends:     template-haskell    >=2.17 && <2.23
-+  if impl(ghc >= 9.11) && impl(ghc < 9.13)
-+    hs-source-dirs:    src-ghc-9.12
-+    build-depends:     template-haskell    >=2.17 && <2.23
-   default-language:    Haskell2010
-   other-extensions:    CPP
-                        LambdaCase
+@@ -68,7 +68,7 @@ library
+                        GHC.TypeLits.Normalise.Unify
+   build-depends:       base                >=4.9   && <5,
+                        containers          >=0.5.7.1 && <0.8,
+-                       ghc                 >=8.0.1 && <9.12,
++                       ghc                 >=8.0.1 && <9.14,
+                        ghc-tcplugins-extra >=0.3.1,
+                        transformers        >=0.5.2.0 && < 0.7
+   if impl(ghc >= 9.0.0)
+@@ -78,9 +78,12 @@ library
+   hs-source-dirs:      src
+   if impl(ghc >= 8.0) && impl(ghc < 9.4)
+     hs-source-dirs:    src-pre-ghc-9.4
+-  if impl(ghc >= 9.4) && impl(ghc < 9.12)
++  if impl(ghc >= 9.4) && impl(ghc < 9.11)
+     hs-source-dirs:    src-ghc-9.4
+     build-depends:     template-haskell    >=2.17 && <2.23
++  if impl(ghc >= 9.11) && impl(ghc < 9.14)
++    hs-source-dirs:    src-ghc-9.12
++    build-depends:     template-haskell    >=2.17 && <2.23
+   default-language:    Haskell2010
+   other-extensions:    CPP
+                        LambdaCase
 diff --git a/src-ghc-9.12/GHC/TypeLits/Normalise.hs b/src-ghc-9.12/GHC/TypeLits/Normalise.hs
 new file mode 100644
-index 0000000..ace9891
+index 0000000..41faa7e
 --- /dev/null
 +++ b/src-ghc-9.12/GHC/TypeLits/Normalise.hs
-@@ -0,0 +1,740 @@
+@@ -0,0 +1,734 @@
 +{-|
 +Copyright  :  (C) 2015-2016, University of Twente,
 +                  2017     , QBayLogic B.V.
 +License    :  BSD2 (see the file LICENSE)
 +Maintainer :  Christiaan Baaij <christiaan.baaij@gmail.com>
-+
 +A type checker plugin for GHC that can solve /equalities/ of types of kind
 +'GHC.TypeLits.Nat', where these types are either:
-+
 +* Type-level naturals
 +* Type variables
 +* Applications of the arithmetic expressions @(+,-,*,^)@.
-+
 +It solves these equalities by normalising them to /sort-of/
 +'GHC.TypeLits.Normalise.SOP.SOP' (Sum-of-Products) form, and then perform a
 +simple syntactic equality.
-+
 +For example, this solver can prove the equality between:
-+
 +@
 +(x + 2)^(y + 2)
 +@
-+
 +and
-+
 +@
 +4*x*(2 + x)^y + 4*(2 + x)^y + (2 + x)^y*x^2
 +@
-+
 +Because the latter is actually the 'GHC.TypeLits.Normalise.SOP.SOP' normal form
 +of the former.
-+
 +To use the plugin, add
-+
 +@
 +{\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise \#-\}
 +@
-+
 +To the header of your file.
-+
 +== Treating subtraction as addition with a negated number
-+
 +If you are absolutely sure that your subtractions can /never/ lead to (a locally)
 +negative number, you can ask the plugin to treat subtraction as addition with
 +a negated operand by additionally adding:
-+
 +@
 +{\-\# OPTIONS_GHC -fplugin-opt GHC.TypeLits.Normalise:allow-negated-numbers \#-\}
 +@
-+
 +to the header of your file, thereby allowing to use associativity and
 +commutativity rules when proving constraints involving subtractions. Note that
 +this option can lead to unsound behaviour and should be handled with extreme
 +care.
-+
 +=== When it leads to unsound behaviour
-+
 +For example, enabling the /allow-negated-numbers/ feature would allow
 +you to prove:
-+
 +@
 +(n - 1) + 1 ~ n
 +@
-+
 +/without/ a @(1 <= n)@ constraint, even though when /n/ is set to /0/ the
 +subtraction @n-1@ would be locally negative and hence not be a natural number.
-+
 +This would allow the following erroneous definition:
-+
 +@
 +data Fin (n :: Nat) where
 +  FZ :: Fin (n + 1)
 +  FS :: Fin n -> Fin (n + 1)
-+
 +f :: forall n . Natural -> Fin n
 +f n = case of
 +  0 -> FZ
 +  x -> FS (f \@(n-1) (x - 1))
-+
 +fs :: [Fin 0]
 +fs = f \<$\> [0..]
 +@
-+
 +=== When it might be Okay
-+
 +This example is taken from the <http://hackage.haskell.org/package/mezzo mezzo>
 +library.
-+
 +When you have:
-+
 +@
 +-- | Singleton type for the number of repetitions of an element.
 +data Times (n :: Nat) where
 +    T :: Times n
-+
 +-- | An element of a "run-length encoded" vector, containing the value and
 +-- the number of repetitions
 +data Elem :: Type -> Nat -> Type where
 +    (:*) :: t -> Times n -> Elem t n
-+
 +-- | A length-indexed vector, optimised for repetitions.
 +data OptVector :: Type -> Nat -> Type where
 +    End  :: OptVector t 0
 +    (:-) :: Elem t l -> OptVector t (n - l) -> OptVector t n
 +@
-+
 +And you want to define:
-+
 +@
 +-- | Append two optimised vectors.
 +type family (x :: OptVector t n) ++ (y :: OptVector t m) :: OptVector t (n + m) where
@@ -250,36 +115,28 @@ index 0000000..ace9891
 +    End       ++ ys = ys
 +    (x :- xs) ++ ys = x :- (xs ++ ys)
 +@
-+
 +then the last line will give rise to the constraint:
-+
 +@
 +(n-l)+m ~ (n+m)-l
 +@
-+
 +because:
-+
 +@
 +x  :: Elem t l
 +xs :: OptVector t (n-l)
 +ys :: OptVector t m
 +@
-+
 +In this case it's okay to add
-+
 +@
 +{\-\# OPTIONS_GHC -fplugin-opt GHC.TypeLits.Normalise:allow-negated-numbers \#-\}
 +@
-+
 +if you can convince yourself you will never be able to construct a:
-+
 +@
 +xs :: OptVector t (n-l)
 +@
-+
 +where /n-l/ is a negative number.
 +-}
 +
++{-# LANGUAGE CPP             #-}
 +{-# LANGUAGE LambdaCase      #-}
 +{-# LANGUAGE NamedFieldPuns  #-}
 +{-# LANGUAGE RecordWildCards #-}
@@ -317,11 +174,16 @@ index 0000000..ace9891
 +import GHC.Builtin.Types.Literals (typeNatCmpTyCon)
 +import GHC.Core (Expr (..))
 +import GHC.Core.Class (className)
-+import GHC.Core.Coercion (Role (..), mkUnivCo)
++import GHC.Core.Coercion (Coercion, Role (..), mkUnivCo)
 +import GHC.Core.DataCon (dataConWrapId)
 +import GHC.Core.Predicate
 +  (EqRel (NomEq), Pred (EqPred, IrredPred), classifyPredType, mkClassPred,
-+   mkPrimEqPred, isEqPred, isEqPrimPred, getClassPredTys_maybe)
++#if MIN_VERSION_ghc(9,13,0)
++   mkNomEqPred, isEqClassPred,
++#else
++   mkPrimEqPred, isEqPrimPred,
++#endif
++   isEqPred, getClassPredTys_maybe)
 +import GHC.Core.TyCo.Rep (Type (..), UnivCoProvenance (..))
 +import GHC.Core.TyCon (TyCon)
 +import GHC.Core.Type
@@ -331,15 +193,21 @@ index 0000000..ace9891
 +import GHC.Data.IOEnv (getEnv)
 +import GHC.Driver.Plugins (Plugin (..), defaultPlugin, purePlugin)
 +import GHC.Plugins
-+  (thNameToGhcNameIO, HscEnv (hsc_NC), DCoVarSet, emptyDVarSet, extendDVarSet)
++  (thNameToGhcNameIO, HscEnv (hsc_NC))
 +import GHC.Tc.Plugin
 +  (TcPluginM, tcLookupClass, tcPluginTrace, tcPluginIO, newEvVar)
 +import GHC.Tc.Plugin (tcLookupTyCon, unsafeTcPluginTcM)
 +import GHC.Tc.Types (TcPlugin (..), TcPluginSolveResult(..), Env (env_top))
 +import GHC.Tc.Types.Constraint
-+  (Ct, CtEvidence (..), CtLoc, TcEvDest (..), ctEvidence,
-+   ctLoc, ctLocSpan, isGiven, isWanted, mkNonCanonical, setCtLocSpan,
-+   isWantedCt, ctEvId, ctEvLoc, ctEvPred, ctEvExpr, emptyRewriterSet, setCtEvLoc)
++  (Ct, CtEvidence (..), TcEvDest (..), ctEvidence,
++   ctLoc, isGiven, isWanted, mkNonCanonical,
++   isWantedCt, ctEvLoc, ctEvPred, ctEvExpr,
++   ctEvCoercion, emptyRewriterSet, setCtEvLoc)
++#if MIN_VERSION_ghc(9,13,0)
++import GHC.Tc.Types.Constraint (WantedCtEvidence(..))
++#endif
++import GHC.Tc.Types.CtLoc
++  (CtLoc, ctLocSpan, setCtLocSpan)
 +import GHC.Tc.Types.Evidence (EvBindsVar, EvTerm (..), evCast, evId)
 +import GHC.Types.Unique.FM (emptyUFM)
 +import GHC.Utils.Outputable (Outputable (..), (<+>), ($$), text)
@@ -352,11 +220,25 @@ index 0000000..ace9891
 +import GHC.TypeLits.Normalise.SOP
 +import GHC.TypeLits.Normalise.Unify hiding (subtractionToPred)
 +
++#if MIN_VERSION_ghc(9,13,0)
++mkCtWanted x y z w = CtWanted (WantedCt x y z w)
++#else
++mkCtWanted x y z w = CtWanted x y z w
++#endif
++
 +isEqPredClass :: PredType -> Bool
 +isEqPredClass ty = case tyConAppTyCon_maybe ty of
 +  Just tc -> tc `hasKey` eqTyConKey || tc `hasKey` heqTyConKey
 +  _ -> False
 +
++isEq :: PredType -> Bool
++isEq pty =
++#if MIN_VERSION_ghc(9,13,0)
++  isEqPred pty || isEqClassPred pty
++#else
++  isEqPrimPred pty || isEqPred pty
++#endif
++
 +-- | To use the plugin, add
 +--
 +-- @
@@ -443,11 +325,7 @@ index 0000000..ace9891
 +-- containing naturals.
 +decideEqualSOP opts (gen'd,tcs@(leqT,_,_)) ev givens wanteds = do
 +    let unit_wanteds = mapMaybe (toNatEquality tcs) wanteds
-+        nonEqs = filter ( not
-+                        . (\p -> isEqPred p || isEqPrimPred p)
-+                        . ctEvPred
-+                        . ctEvidence )
-+                 wanteds
++        nonEqs = filter (not . isEq . ctEvPred . ctEvidence) wanteds
 +    done <- tcPluginIO $ readIORef gen'd
 +    let redGs = reduceGivens opts leqT done givens
 +        newlyDone = map (\(_,(prd, _,_)) -> CType prd) redGs
@@ -498,7 +376,7 @@ index 0000000..ace9891
 +        , let ev = ctEvidence ct
 +              prd = ctEvPred ev
 +        , isGiven ev
-+        , not $ (\p -> isEqPred p || isEqPrimPred p || isEqPredClass p) prd
++        , not $ (\p -> isEq p || isEqPredClass p) prd
 +        ]
 +  in filter
 +      (\(_, (prd, _, _)) ->
@@ -543,10 +421,10 @@ index 0000000..ace9891
 +            evVar <- newEvVar pred'
 +            -- Bind the evidence to a new wanted normalized class constraint
 +            let wDict = mkNonCanonical
-+                          (CtWanted pred' (EvVarDest evVar) (ctLoc ct) emptyRewriterSet)
++                          (mkCtWanted pred' (EvVarDest evVar) (ctLoc ct) emptyRewriterSet)
 +            -- Evidence for current wanted is simply the coerced binding for
 +            -- the new binding
-+                evCo = mkUnivCo (PluginProv "ghc-typelits-natnormalise" emptyDVarSet)
++                evCo = mkUnivCo (PluginProv "ghc-typelits-natnormalise") []
 +                         Representational
 +                         pred' pred0
 +                ev = evId evVar `evCast` evCo
@@ -560,7 +438,7 @@ index 0000000..ace9891
 +toReducedDict :: CtEvidence -> PredType -> EvTerm
 +toReducedDict ct pred' =
 +  let pred0 = ctEvPred ct
-+      evCo = mkUnivCo (PluginProv "ghc-typelits-natnormalise" emptyDVarSet)
++      evCo = mkUnivCo (PluginProv "ghc-typelits-natnormalise") []
 +              Representational
 +              pred0 pred'
 +      ev = ctEvExpr ct
@@ -593,7 +471,7 @@ index 0000000..ace9891
 +      [] -> do
 +        let eqs = otherEqs ++ eqsW
 +        tcPluginTrace "simplifyNats" (ppr eqs)
-+        simples emptyDVarSet [] [] [] [] eqs
++        simples [] [] [] [] [] eqs
 +      _  -> do
 +        tcPluginTrace ("simplifyNats(backtrack: " ++ show (length fancyGivens) ++ ")")
 +                      (ppr varEqs)
@@ -601,11 +479,11 @@ index 0000000..ace9891
 +        allSimplified <- forM fancyGivens $ \v -> do
 +          let eqs = v ++ eqsW
 +          tcPluginTrace "simplifyNats" (ppr eqs)
-+          simples emptyDVarSet [] [] [] [] eqs
++          simples [] [] [] [] [] eqs
 +
 +        pure (foldr findFirstSimpliedWanted (Simplified []) allSimplified)
 +  where
-+    simples :: DCoVarSet
++    simples :: [Coercion]
 +            -> [CoreUnify]
 +            -> [((EvTerm, Ct), [Ct])]
 +            -> [(CoreSOP,CoreSOP,Bool)]
@@ -631,12 +509,12 @@ index 0000000..ace9891
 +                                        subToPred opts leqT k)
 +          let (leqsG1, deps1)
 +                | isGiven (ctEvidence ct) = ( eqToLeq u' v' ++ leqsG
-+                                            , extendDVarSet deps (ctEvId ct))
++                                            , ctEvCoercion (ctEvidence ct) : deps )
 +                | otherwise               = (leqsG, deps)
 +          case evM of
 +            Nothing -> simples deps1 subst evs leqsG1 xs eqs'
 +            Just ev ->
-+              simples (extendDVarSet deps (ctEvId ct))
++              simples (ctEvCoercion (ctEvidence ct) : deps)
 +                      (substsSubst subst' subst ++ subst')
 +                      (ev:evs) leqsG1 [] (xs ++ eqs')
 +    simples deps subst evs leqsG xs (eq@(Right (ct,u@(x,y,b)),k):eqs') = do
@@ -737,7 +615,13 @@ index 0000000..ace9891
 +    leq (a,b) =
 +      let lhs = TyConApp leqT [naturalTy,b,a]
 +          rhs = TyConApp (cTupleTyCon 0) []
-+       in mkPrimEqPred lhs rhs
++       in
++#if MIN_VERSION_ghc(9,13,0)
++          mkNomEqPred
++#else
++          mkPrimEqPred
++#endif
++            lhs rhs
 +
 +-- Extract the Nat equality constraints
 +toNatEquality :: (TyCon,TyCon,TyCon) -> Ct -> Maybe (Either NatEquality NatInEquality,[(Type,Type)])
@@ -831,7 +715,13 @@ index 0000000..ace9891
 +    isNatKind = (`eqType` naturalTy)
 +
 +unifyItemToPredType :: CoreUnify -> PredType
-+unifyItemToPredType ui = mkPrimEqPred ty1 ty2
++unifyItemToPredType ui =
++#if MIN_VERSION_ghc(9,13,0)
++  mkNomEqPred
++#else
++  mkPrimEqPred
++#endif
++    ty1 ty2
 +  where
 +    ty1 = case ui of
 +            SubstItem {..} -> mkTyVarTy siVar
@@ -843,18 +733,18 @@ index 0000000..ace9891
 +evSubtPreds :: CtLoc -> [PredType] -> TcPluginM [Ct]
 +evSubtPreds loc = mapM (fmap mkNonCanonical . newWanted loc)
 +
-+evMagic :: Ct -> DCoVarSet -> Set CType -> [PredType] -> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))
++evMagic :: Ct -> [Coercion] -> Set CType -> [PredType] -> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))
 +evMagic ct deps knW preds = do
 +  holeWanteds <- evSubtPreds (ctLoc ct) preds
 +  knWanted <- mapM (mkKnWanted (ctLoc ct)) (toList knW)
 +  let newWant = knWanted ++ holeWanteds
 +  case classifyPredType $ ctEvPred $ ctEvidence ct of
 +    EqPred NomEq t1 t2 ->
-+      let ctEv = mkUnivCo (PluginProv "ghc-typelits-natnormalise" deps) Nominal t1 t2
++      let ctEv = mkUnivCo (PluginProv "ghc-typelits-natnormalise") deps Nominal t1 t2
 +      in return (Just ((EvExpr (Coercion ctEv), ct),newWant))
 +    IrredPred p ->
 +      let t1 = mkTyConApp (cTupleTyCon 0) []
-+          co = mkUnivCo (PluginProv "ghc-typelits-natnormalise" deps) Representational t1 p
++          co = mkUnivCo (PluginProv "ghc-typelits-natnormalise") deps Representational t1 p
 +          dcApp = evId (dataConWrapId (cTupleDataCon 0))
 +       in return (Just ((evCast dcApp co, ct),newWant))
 +    _ -> return Nothing
@@ -875,153 +765,38 @@ index 0000000..ace9891
 +  wantedCtEv <- newWanted loc kn_pred
 +  let wanted' = mkNonCanonical' loc wantedCtEv
 +  return wanted'
-diff --git a/src-ghc-9.4/GHC/TypeLits/Normalise.hs b/src-ghc-9.4/GHC/TypeLits/Normalise.hs
-index 052bb29..5f1bbe2 100644
---- a/src-ghc-9.4/GHC/TypeLits/Normalise.hs
-+++ b/src-ghc-9.4/GHC/TypeLits/Normalise.hs
-@@ -149,6 +149,7 @@ where /n-l/ is a negative number.
- {-# LANGUAGE RecordWildCards #-}
- {-# LANGUAGE TupleSections   #-}
- {-# LANGUAGE ViewPatterns    #-}
-+{-# LANGUAGE TemplateHaskellQuotes #-}
- 
- {-# OPTIONS_HADDOCK show-extensions #-}
- 
-@@ -166,9 +167,10 @@ import Data.List (intersect, partition, stripPrefix, find)
- import Data.Maybe (mapMaybe, catMaybes)
- import Data.Set (Set, empty, toList, notMember, fromList, union)
- import Text.Read (readMaybe)
-+import qualified Data.Type.Ord
-+import qualified GHC.TypeError
- 
--import GHC.TcPluginM.Extra
--  (tracePlugin, lookupModule, lookupName, newGiven, newWanted)
-+import GHC.TcPluginM.Extra (tracePlugin, newGiven, newWanted)
- 
- -- GHC API
- import GHC.Builtin.Names (knownNatClassName, eqTyConKey, heqTyConKey, hasKey)
-@@ -195,21 +197,24 @@ import GHC.Core.TyCo.Compare
- import GHC.Core.Type
-   (Kind, PredType, eqType, mkTyVarTy, tyConAppTyCon_maybe, typeKind, mkTyConApp)
- #endif
-+import GHC.Data.IOEnv (getEnv)
- import GHC.Driver.Plugins (Plugin (..), defaultPlugin, purePlugin)
-+import GHC.Plugins (thNameToGhcNameIO, HscEnv (hsc_NC))
- import GHC.Tc.Plugin
-   (TcPluginM, tcLookupClass, tcPluginTrace, tcPluginIO, newEvVar)
--import GHC.Tc.Plugin (tcLookupTyCon)
--import GHC.Tc.Types (TcPlugin (..), TcPluginSolveResult(..))
-+import GHC.Tc.Plugin (tcLookupTyCon, unsafeTcPluginTcM)
-+import GHC.Tc.Types (TcPlugin (..), TcPluginSolveResult(..), Env (env_top))
- import GHC.Tc.Types.Constraint
-   (Ct, CtEvidence (..), CtLoc, TcEvDest (..), ctEvidence,
-    ctLoc, ctLocSpan, isGiven, isWanted, mkNonCanonical, setCtLocSpan,
-    isWantedCt, ctEvLoc, ctEvPred, ctEvExpr, emptyRewriterSet, setCtEvLoc)
- import GHC.Tc.Types.Evidence (EvBindsVar, EvTerm (..), evCast, evId)
--import GHC.Data.FastString (fsLit)
--import GHC.Types.Name.Occurrence (mkTcOcc)
- import GHC.Types.Unique.FM (emptyUFM)
--import GHC.Unit.Module (mkModuleName)
- import GHC.Utils.Outputable (Outputable (..), (<+>), ($$), text)
-+import GHC (Name)
-+
-+-- template-haskell
-+import qualified Language.Haskell.TH as TH
- 
- -- internal
- import GHC.TypeLits.Normalise.SOP
-@@ -254,17 +259,16 @@ type ExtraDefs = (IORef (Set CType), (TyCon,TyCon,TyCon))
- lookupExtraDefs :: TcPluginM ExtraDefs
- lookupExtraDefs = do
-     ref <- tcPluginIO (newIORef empty)
--    md <- lookupModule ordModule basePackage
--    ordCond <- look md "OrdCond"
--    leqT <- look md "<="
--    md1 <- lookupModule typeErrModule basePackage
--    assertT <- look md1 "Assert"
-+    ordCond <- lookupTHName ''Data.Type.Ord.OrdCond >>= tcLookupTyCon
-+    leqT <- lookupTHName ''(Data.Type.Ord.<=) >>= tcLookupTyCon
-+    assertT <- lookupTHName ''GHC.TypeError.Assert >>= tcLookupTyCon
-     return (ref, (leqT,assertT,ordCond))
--  where
--    look md s = tcLookupTyCon =<< lookupName md (mkTcOcc s)
--    ordModule = mkModuleName "Data.Type.Ord"
--    typeErrModule = mkModuleName "GHC.TypeError"
--    basePackage = fsLit "base"
-+
-+lookupTHName :: TH.Name -> TcPluginM Name
-+lookupTHName th = do
-+    nc <- unsafeTcPluginTcM (hsc_NC . env_top <$> getEnv)
-+    res <- tcPluginIO $ thNameToGhcNameIO nc th
-+    maybe (fail $ "Failed to lookup " ++ show th) return res
- 
- decideEqualSOP
-   :: Opts
-diff --git a/tests/ErrorTests.hs b/tests/ErrorTests.hs
-index 6a0cca4..cf6237f 100644
---- a/tests/ErrorTests.hs
-+++ b/tests/ErrorTests.hs
-@@ -191,7 +191,24 @@ testProxy10 :: Proxy (a :: Nat) -> Proxy (a + 2) -> ()
- testProxy10 = proxyInEq'
- 
- testProxy10Errors =
--#if __GLASGOW_HASKELL__ >= 906
-+#if __GLASGOW_HASKELL__ >= 910
-+  [$(do localeEncoding <- runIO (getLocaleEncoding)
-+        if textEncodingName localeEncoding == textEncodingName utf8
-+          then litE $ stringL "Couldn't match type ‘ghc-internal-9.1001.0:GHC.Internal.Data.Type.Ord.OrdCond"
-+          else litE $ stringL "Couldn't match type `ghc-internal-9.1001.0:GHC.Internal.Data.Type.Ord.OrdCond"
-+    )
-+  ,$(do localeEncoding <- runIO (getLocaleEncoding)
-+        if textEncodingName localeEncoding == textEncodingName utf8
-+          then litE $ stringL "(CmpNat a (a + 2)) True True False’"
-+          else litE $ stringL "(CmpNat a (a + 2)) True True False'"
-+    )
-+  ,$(do localeEncoding <- runIO (getLocaleEncoding)
-+        if textEncodingName localeEncoding == textEncodingName utf8
-+          then litE $ stringL "with ‘False"
-+          else litE $ stringL "with `False"
-+    )
-+  ]
-+#elif __GLASGOW_HASKELL__ >= 906
-   [$(do localeEncoding <- runIO (getLocaleEncoding)
-         if textEncodingName localeEncoding == textEncodingName utf8
-           then litE $ stringL "Couldn't match type ‘Data.Type.Ord.OrdCond"
-@@ -239,7 +256,10 @@ testProxy11 = proxyInEq'
- testProxy11Errors =
-   [$(do localeEncoding <- runIO (getLocaleEncoding)
-         if textEncodingName localeEncoding == textEncodingName utf8
--#if __GLASGOW_HASKELL__ >= 906
-+#if __GLASGOW_HASKELL__ >= 910
-+          then litE $ stringL "Couldn't match type ‘True’ with ‘False’"
-+          else litE $ stringL "Couldn't match type `True' with `False'"
-+#elif __GLASGOW_HASKELL__ >= 906
-           then litE $ stringL "Couldn't match type ‘True’ with ‘False’"
-           else litE $ stringL "Couldn't match type True with False"
- #else
-@@ -314,7 +334,24 @@ testProxy14 :: Proxy (2*a) -> Proxy (4*a) -> ()
- testProxy14 = proxyInEq'
- 
- testProxy14Errors =
--#if __GLASGOW_HASKELL__ >= 906
-+#if __GLASGOW_HASKELL__ >= 910
-+  [$(do localeEncoding <- runIO (getLocaleEncoding)
-+        if textEncodingName localeEncoding == textEncodingName utf8
-+          then litE $ stringL "Couldn't match type ‘ghc-internal-9.1001.0:GHC.Internal.Data.Type.Ord.OrdCond"
-+          else litE $ stringL "Couldn't match type `ghc-internal-9.1001.0:GHC.Internal.Data.Type.Ord.OrdCond"
-+    )
-+  ,$(do localeEncoding <- runIO (getLocaleEncoding)
-+        if textEncodingName localeEncoding == textEncodingName utf8
-+          then litE $ stringL "(CmpNat (2 * a) (4 * a)) True True False’"
-+          else litE $ stringL "(CmpNat (2 * a) (4 * a)) True True False'"
-+    )
-+  ,$(do localeEncoding <- runIO (getLocaleEncoding)
-+        if textEncodingName localeEncoding == textEncodingName utf8
-+          then litE $ stringL "with ‘False"
-+          else litE $ stringL "with `False"
-+    )
-+  ]
-+#elif __GLASGOW_HASKELL__ >= 906
-   [$(do localeEncoding <- runIO (getLocaleEncoding)
-         if textEncodingName localeEncoding == textEncodingName utf8
-           then litE $ stringL "Couldn't match type ‘Data.Type.Ord.OrdCond"
+diff --git a/src/GHC/TypeLits/Normalise/Unify.hs b/src/GHC/TypeLits/Normalise/Unify.hs
+index e31c658..2bd47ff 100644
+--- a/src/GHC/TypeLits/Normalise/Unify.hs
++++ b/src/GHC/TypeLits/Normalise/Unify.hs
+@@ -71,7 +71,14 @@ import GHC.Builtin.Types.Literals (typeNatCmpTyCon)
+ import GHC.Builtin.Types (typeNatKind)
+ import GHC.Builtin.Types.Literals (typeNatLeqTyCon)
+ #endif
+-import GHC.Core.Predicate (EqRel (NomEq), Pred (EqPred), classifyPredType, mkPrimEqPred)
++import GHC.Core.Predicate
++  ( EqRel (NomEq), Pred (EqPred), classifyPredType
++#if MIN_VERSION_ghc(9,13,0)
++  , mkNomEqPred
++#else
++  , mkPrimEqPred
++#endif
++  )
+ import GHC.Core.TyCon (TyCon)
+ #if MIN_VERSION_ghc(9,6,0)
+ import GHC.Core.Type
+@@ -333,7 +340,13 @@ subtractionToPred ordCond (x,y) =
+       falseTc = mkTyConApp promotedFalseDataCon []
+       ordCmp = mkTyConApp ordCond
+                 [boolTy,cmpNat,trueTc,trueTc,falseTc]
+-      predTy = mkPrimEqPred ordCmp trueTc
++      predTy =
++#if MIN_VERSION_ghc(9,13,0)
++        mkNomEqPred
++#else
++        mkPrimEqPred
++#endif
++          ordCmp trueTc
+    in (predTy,boolTy)
+ #else
+   (mkPrimEqPred (mkTyConApp ordCond [y,x])