Skip to content
Snippets Groups Projects
Commit 2becd80c authored by sheaf's avatar sheaf
Browse files

Update sbv & singletons for GHC MR !11112

GHC MR !11112 makes it so that one needs to enable the (new)
TypeAbstractions extension in order to use type applications in
constructor patterns. The old behaviour (ScopedTypeVariables + TypeApplications)
is still supported, but it emits a warning, which causes sbv to fail
to build due to -Werror.

In addition, the changes in GHC MR !11112 mean that the use of invisible
binders in type declarations requires the TypeAbstractions extension
to be enabled.
parent cca143be
No related branches found
No related tags found
No related merge requests found
......@@ -252,6 +252,24 @@ index 416f8e2..c4b719b 100644
module Documentation.SBV.Examples.Existentials.Diophantine where
diff --git a/Documentation/SBV/Examples/Misc/FirstOrderLogic.hs b/Documentation/SBV/Examples/Misc/FirstOrderLogic.hs
index 29576d4..7bc4e97 100644
--- a/Documentation/SBV/Examples/Misc/FirstOrderLogic.hs
+++ b/Documentation/SBV/Examples/Misc/FirstOrderLogic.hs
@@ -17,6 +17,13 @@
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE CPP #-}
+
+-- Type applications in patterns require the TypeAbstractions
+-- extension starting in GHC 9.8.
+#if __GLASGOW_HASKELL__ >= 907
+{-# LANGUAGE TypeAbstractions #-}
+#endif
{-# OPTIONS_GHC -Wall -Werror #-}
diff --git a/Documentation/SBV/Examples/Puzzles/Coins.hs b/Documentation/SBV/Examples/Puzzles/Coins.hs
index 1c1eaee..594d1ab 100644
--- a/Documentation/SBV/Examples/Puzzles/Coins.hs
......
diff --git a/src/Data/Singletons.hs b/src/Data/Singletons.hs
index 67e0a63..6154010 100644
index 67e0a63..b95bfe5 100644
--- a/src/Data/Singletons.hs
+++ b/src/Data/Singletons.hs
@@ -149,7 +149,11 @@ type SameKind (a :: k) (b :: k) = (() :: Constraint)
@@ -27,6 +27,15 @@
{-# LANGUAGE StandaloneKindSignatures #-}
#endif
+-- Invisible type binders in type declarations, such as
+--
+-- type family Sing @k
+--
+-- require the TypeAbstractions extension.
+#if GLASGOW_HASKELL >= 909
+{-# LANGUAGE TypeAbstractions #-}
+#endif
+
-----------------------------------------------------------------------------
-- |
-- Module : Data.Singletons
@@ -149,7 +158,11 @@ type SameKind (a :: k) (b :: k) = (() :: Constraint)
#if __GLASGOW_HASKELL__ >= 810
type Sing :: k -> Type
#endif
......@@ -14,7 +30,7 @@ index 67e0a63..6154010 100644
{-
Note [The kind of Sing]
@@ -512,7 +516,11 @@ data family TyCon :: (k1 -> k2) -> unmatchable_fun
@@ -512,7 +525,11 @@ data family TyCon :: (k1 -> k2) -> unmatchable_fun
#if __GLASGOW_HASKELL__ >= 810
type ApplyTyCon :: (k1 -> k2) -> (k1 ~> unmatchable_fun)
#endif
......@@ -26,7 +42,7 @@ index 67e0a63..6154010 100644
#if __GLASGOW_HASKELL__ >= 808
ApplyTyCon @k1 @(k2 -> k3) @unmatchable_fun = ApplyTyConAux2
ApplyTyCon @k1 @k2 @k2 = ApplyTyConAux1
@@ -589,6 +597,29 @@ type TyCon8 :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7 -> k8 -> k9)
@@ -589,6 +606,29 @@ type TyCon8 :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7 -> k8 -> k9)
-- We can write:
--
-- > Map (TyCon1 Succ) [Zero, Succ Zero]
......@@ -56,7 +72,7 @@ index 67e0a63..6154010 100644
type TyCon1 = (TyCon :: (k1 -> k2) -> (k1 ~> k2))
-- | Similar to 'TyCon1', but for two-parameter type constructors.
@@ -603,6 +634,7 @@ type TyCon7 = (TyCon :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7 -> k8)
@@ -603,6 +643,7 @@ type TyCon7 = (TyCon :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7 -> k8)
-> (k1 ~> k2 ~> k3 ~> k4 ~> k5 ~> k6 ~> k7 ~> k8))
type TyCon8 = (TyCon :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7 -> k8 -> k9)
-> (k1 ~> k2 ~> k3 ~> k4 ~> k5 ~> k6 ~> k7 ~> k8 ~> k9))
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment