th-desugar 1.18 support

.vscode/settings.json

@@ -0,0 +1,3 @@
+{
+  "haskell.formattingProvider": "fourmolu"
+}

Changelog.md

@@ -1,6 +1,11 @@
 Changelog
 ==========
 
+## 0.7.1.0
+
+- Supports GHC 9.10 and 9.12
+- Drops support for GHC <9.2
+
 ## 0.7.0.2
 
 - Supports GHC 9.8

Proof/Equational.hs

@@ -15,53 +15,52 @@
 #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800
 {-# LANGUAGE ConstrainedClassMethods, TypeFamilyDependencies #-}
 #endif
-module Proof.Equational
-  ( (:~:) (..),
-    (:=:),
-    sym,
-    trans,
-    Equality (..),
-    Preorder (..),
-    reflexivity',
-    (:\/:),
-    (:/\:),
-    (=<=),
-    (=>=),
-    (=~=),
-    Leibniz (..),
-    Reason (..),
-    because,
-    by,
-    (===),
-    start,
-    byDefinition,
-    admitted,
-    Proxy (..),
-    cong,
-    cong',
-    Proposition (..),
-    HVec (..),
-    FromBool (..),
-    applyNAry,
-    applyNAry',
-    fromBool',
-
-    -- * Conversion between equalities
-    fromRefl,
-    fromLeibniz,
-    reflToLeibniz,
-    leibnizToRefl,
-
-    -- * Coercion
-    coerce,
-    coerceInner,
-    coerce',
-    withRefl,
-
-    -- * Re-exported modules
-    module Data.Proxy,
-  )
-where
+module Proof.Equational (
+  (:~:) (..),
+  (:=:),
+  sym,
+  trans,
+  Equality (..),
+  Preorder (..),
+  reflexivity',
+  (:\/:),
+  (:/\:),
+  (=<=),
+  (=>=),
+  (=~=),
+  Leibniz (..),
+  Reason (..),
+  because,
+  by,
+  (===),
+  start,
+  byDefinition,
+  admitted,
+  Proxy (..),
+  cong,
+  cong',
+  Proposition (..),
+  HVec (..),
+  FromBool (..),
+  applyNAry,
+  applyNAry',
+  fromBool',
+
+  -- * Conversion between equalities
+  fromRefl,
+  fromLeibniz,
+  reflToLeibniz,
+  leibnizToRefl,
+
+  -- * Coercion
+  coerce,
+  coerceInner,
+  coerce',
+  withRefl,
+
+  -- * Re-exported modules
+  module Data.Proxy,
+) where
 
 import Data.Kind (Type)
 import Data.Proxy
@@ -98,7 +97,7 @@ class Preorder (eq :: k -> k -> Type) where
   reflexivity :: proxy a -> eq a a
   transitivity :: eq a b -> eq b c -> eq a c
 
-class Preorder eq => Equality (eq :: k -> k -> Type) where
+class (Preorder eq) => Equality (eq :: k -> k -> Type) where
   symmetry :: eq a b -> eq b a
 
 instance Preorder (:=:) where
@@ -146,22 +145,22 @@ infix 5 `Because`
 
 infix 5 `because`
 
-(=<=) :: Preorder r => r x y -> Reason r y z -> r x z
+(=<=) :: (Preorder r) => r x y -> Reason r y z -> r x z
 eq =<= (_ `Because` eq') = transitivity eq eq'
 {-# SPECIALIZE INLINE [1] (=<=) :: x :~: y -> Reason (:~:) y z -> x :~: z #-}
 
-(=>=) :: Preorder r => r y z -> Reason r x y -> r x z
+(=>=) :: (Preorder r) => r y z -> Reason r x y -> r x z
 eq =>= (_ `Because` eq') = transitivity eq' eq
 {-# SPECIALIZE INLINE [1] (=>=) :: y :~: z -> Reason (:~:) x y -> x :~: z #-}
 
-(===) :: Equality eq => eq x y -> Reason eq y z -> eq x z
+(===) :: (Equality eq) => eq x y -> Reason eq y z -> eq x z
 (===) = (=<=)
 {-# SPECIALIZE INLINE [1] (===) :: x :~: y -> Reason (:~:) y z -> x :~: z #-}
 
 (=~=) :: r x y -> proxy y -> r x y
 eq =~= _ = eq
 
-start :: Preorder eq => proxy a -> eq a a
+start :: (Preorder eq) => proxy a -> eq a a
 start = reflexivity
 
 byDefinition :: (Preorder eq) => eq a a
@@ -207,7 +206,7 @@ coerce' _ = unsafeCoerce
    It has the same effect as @'Data.Type.Equality.gcastWith'@,
    but some hacks is done to reduce runtime overhead.
 -}
-withRefl :: forall a b r. a :~: b -> (a ~ b => r) -> r
+withRefl :: forall a b r. a :~: b -> ((a ~ b) => r) -> r
 withRefl _ = gcastWith (unsafeCoerce (Refl :: () :~: ()) :: a :~: b)
 
 class Proposition (f :: k -> Type) where
@@ -239,12 +238,12 @@ class KnownTypeList (xs :: [Type]) where
 instance KnownTypeList '[] where
   viewHVec' = HNilView
 
-instance KnownTypeList ts => KnownTypeList (t ': ts) where
+instance (KnownTypeList ts) => KnownTypeList (t ': ts) where
   viewHVec' = HConsView Proxy viewHVec'
 
-newtype Magic (xs :: [Type]) a = Magic {_viewHVec' :: KnownTypeList xs => a}
+newtype Magic (xs :: [Type]) a = Magic {_viewHVec' :: (KnownTypeList xs) => a}
 
-withKnownTypeList :: forall a xs. HVecView xs -> (KnownTypeList xs => a) -> a
+withKnownTypeList :: forall a xs. HVecView xs -> ((KnownTypeList xs) => a) -> a
 withKnownTypeList xs f = (unsafeCoerce (Magic f :: Magic xs a) :: HVecView xs -> a) xs
 
 apply' :: HVecView ts -> (HVec ts -> c) -> ts :~> c
@@ -253,16 +252,16 @@ apply' (HConsView Proxy ts) f = \a ->
   withKnownTypeList ts $
     apply' ts (\ts' -> f $ a :- ts')
 
-applyNAry :: forall ts c. KnownTypeList ts => (HVec ts -> c) -> ts :~> c
+applyNAry :: forall ts c. (KnownTypeList ts) => (HVec ts -> c) -> ts :~> c
 applyNAry = apply' (viewHVec' :: HVecView ts)
 
-applyNAry' :: KnownTypeList ts => proxy ts -> proxy' c -> (HVec ts -> c) -> ts :~> c
+applyNAry' :: (KnownTypeList ts) => proxy ts -> proxy' c -> (HVec ts -> c) -> ts :~> c
 applyNAry' _ _ = applyNAry
 
 class FromBool (c :: Type) where
   type Predicate c :: Bool
   type Args c :: [Type]
-  fromBool :: Predicate c ~ 'True => HVec (Args c) -> c
+  fromBool :: (Predicate c ~ 'True) => HVec (Args c) -> c
 
 fromBool' :: forall proxy c. (KnownTypeList (Args c), FromBool c, Predicate c ~ 'True) => proxy c -> Args c :~> c
 fromBool' pxyc = applyNAry' (Proxy :: Proxy (Args c)) pxyc fromBool

Proof/Propositional.hs

@@ -16,32 +16,31 @@
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 
 -- | Provides type synonyms for logical connectives.
-module Proof.Propositional
-  ( type (/\),
-    type (\/),
-    Not,
-    exfalso,
-    orIntroL,
-    orIntroR,
-    orElim,
-    andIntro,
-    andElimL,
-    andElimR,
-    orAssocL,
-    orAssocR,
-    andAssocL,
-    andAssocR,
-    IsTrue (..),
-    withWitness,
-    Empty (..),
-    withEmpty,
-    withEmpty',
-    refute,
-    Inhabited (..),
-    withInhabited,
-    prove,
-  )
-where
+module Proof.Propositional (
+  type (/\),
+  type (\/),
+  Not,
+  exfalso,
+  orIntroL,
+  orIntroR,
+  orElim,
+  andIntro,
+  andElimL,
+  andElimR,
+  orAssocL,
+  orAssocR,
+  andAssocL,
+  andAssocR,
+  IsTrue (..),
+  withWitness,
+  Empty (..),
+  withEmpty,
+  withEmpty',
+  refute,
+  Inhabited (..),
+  withInhabited,
+  prove,
+) where
 
 import Data.Data (Data)
 import Data.Type.Equality (gcastWith, (:~:) (..))
@@ -105,7 +104,7 @@ orAssocR (Right c) = Right (Right c)
 data IsTrue (b :: Bool) where
   Witness :: IsTrue 'True
 
-withWitness :: forall b r. IsTrue b -> (b ~ 'True => r) -> r
+withWitness :: forall b r. IsTrue b -> ((b ~ 'True) => r) -> r
 withWitness _ = gcastWith (unsafeCoerce (Refl :: () :~: ()) :: b :~: 'True)
 {-# NOINLINE withWitness #-}
 
@@ -126,14 +125,14 @@ instance {-# OVERLAPPABLE #-} (Inhabited a, Empty b) => Empty (a -> b) where
 
 refute [t|0 :~: 1|]
 refute [t|() :~: Int|]
-refute [t| 'True :~: 'False|]
-refute [t| 'False :~: 'True|]
-refute [t| 'LT :~: 'GT|]
-refute [t| 'LT :~: 'EQ|]
-refute [t| 'EQ :~: 'LT|]
-refute [t| 'EQ :~: 'GT|]
-refute [t| 'GT :~: 'LT|]
-refute [t| 'GT :~: 'EQ|]
+refute [t|'True :~: 'False|]
+refute [t|'False :~: 'True|]
+refute [t|'LT :~: 'GT|]
+refute [t|'LT :~: 'EQ|]
+refute [t|'EQ :~: 'LT|]
+refute [t|'EQ :~: 'GT|]
+refute [t|'GT :~: 'LT|]
+refute [t|'GT :~: 'EQ|]
 
 prove [t|Bool|]
 prove [t|Int|]
@@ -150,4 +149,4 @@ prove [t|forall n. n :~: n|]
 prove [t|IsTrue 'True|]
 
 instance Empty (IsTrue 'False) where
-  eliminate = \case
+  eliminate = \case {}