equational-reasoning 0.6.0.4 → 0.7.0.0
raw patch · 4 files changed
+263/−146 lines, 4 filesdep ~template-haskelldep ~th-desugarPVP ok
version bump matches the API change (PVP)
Dependency ranges changed: template-haskell, th-desugar
API changes (from Hackage documentation)
+ Proof.Equational: coerceInner :: (a :=: b) -> f a -> f b
- Proof.Equational: class Preorder eq => Equality (eq :: k -> k -> *)
+ Proof.Equational: class Preorder eq => Equality (eq :: k -> k -> Type)
- Proof.Equational: class FromBool (c :: *) where {
+ Proof.Equational: class FromBool (c :: Type) where {
- Proof.Equational: class Preorder (eq :: k -> k -> *)
+ Proof.Equational: class Preorder (eq :: k -> k -> Type)
- Proof.Equational: class Proposition (f :: k -> *) where {
+ Proof.Equational: class Proposition (f :: k -> Type) where {
- Proof.Equational: data HVec (xs :: [*])
+ Proof.Equational: data HVec (xs :: [Type])
- Proof.Equational: type family Args c :: [*];
+ Proof.Equational: type family Args c :: [Type];
- Proof.Propositional: withWitness :: IsTrue b -> (b ~ 'True => r) -> r
+ Proof.Propositional: withWitness :: forall b r. IsTrue b -> (b ~ 'True => r) -> r
Files
- Proof/Equational.hs +127/−77
- Proof/Propositional.hs +92/−60
- Proof/Propositional/TH.hs +36/−7
- equational-reasoning.cabal +8/−2
Proof/Equational.hs view
@@ -1,39 +1,86 @@-{-# LANGUAGE CPP, DataKinds, FlexibleContexts, GADTs, KindSignatures #-}-{-# LANGUAGE PolyKinds, RankNTypes, ScopedTypeVariables #-}-{-# LANGUAGE StandaloneDeriving, TypeFamilies, TypeOperators #-}-{-# LANGUAGE TypeSynonymInstances, UndecidableInstances #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeSynonymInstances #-}+{-# LANGUAGE UndecidableInstances #-}+ #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, 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 import Data.Type.Equality hiding (apply) import Unsafe.Coerce infix 4 :=:+ type a :\/: b = Either a b+ infixr 2 :\/: type a :/\: b = (a, b)+ infixr 3 :/\: type (:=:) = (:~:) -data Leibniz a b = Leibniz { apply :: forall f. f a -> f b }+data Leibniz a b = Leibniz {apply :: forall f. f a -> f b} leibnizToRefl :: Leibniz a b -> a :=: b leibnizToRefl eq = apply eq Refl@@ -47,25 +94,25 @@ reflToLeibniz :: a :=: b -> Leibniz a b reflToLeibniz Refl = Leibniz id -class Preorder (eq :: k -> k -> *) where- reflexivity :: proxy a -> eq a a- transitivity :: eq a b -> eq b c -> eq a c+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 -> *) where- symmetry :: eq a b -> eq b a+class Preorder eq => Equality (eq :: k -> k -> Type) where+ symmetry :: eq a b -> eq b a instance Preorder (:=:) where- {-# SPECIALISE instance Preorder (:=:) #-}+ {-# SPECIALIZE instance Preorder (:=:) #-} transitivity Refl Refl = Refl- {-# INLINE[1] transitivity #-}+ {-# INLINE [1] transitivity #-} - reflexivity _ = Refl- {-# INLINE[1] reflexivity #-}+ reflexivity _ = Refl+ {-# INLINE [1] reflexivity #-} instance Equality (:=:) where- {-# SPECIALISE instance Equality (:~:) #-}- symmetry Refl = Refl- {-# INLINE[1] symmetry #-}+ {-# SPECIALIZE instance Equality (:~:) #-}+ symmetry Refl = Refl+ {-# INLINE [1] symmetry #-} instance Preorder (->) where reflexivity _ = id@@ -79,9 +126,9 @@ transitivity (Leibniz aEqb) (Leibniz bEqc) = Leibniz $ bEqc . aEqb instance Equality Leibniz where- symmetry eq = unFlip $ apply eq $ Flip leibniz_refl+ symmetry eq = unFlip $ apply eq $ Flip leibniz_refl -newtype Flip f a b = Flip { unFlip :: f b a }+newtype Flip f a b = Flip {unFlip :: f b a} data Reason eq x y where Because :: proxy y -> eq x y -> Reason eq x y@@ -91,25 +138,25 @@ by, because :: proxy y -> eq x y -> Reason eq x y because = Because-by = Because+by = Because infixl 4 ===, =<=, =~=, =>=+ infix 5 `Because`+ infix 5 `because` (=<=) :: Preorder r => r x y -> Reason r y z -> r x z eq =<= (_ `Because` eq') = transitivity eq eq'--{-# SPECIALISE INLINE[1] (=<=) :: x :~: y -> Reason (:~:) y z -> x :~: z #-}+{-# SPECIALIZE INLINE [1] (=<=) :: x :~: y -> Reason (:~:) y z -> x :~: z #-} (=>=) :: Preorder r => r y z -> Reason r x y -> r x z eq =>= (_ `Because` eq') = transitivity eq' eq--{-# SPECIALISE INLINE[1] (=>=) :: y :~: z -> Reason (:~:) x y -> x :~: z #-}+{-# SPECIALIZE INLINE [1] (=>=) :: y :~: z -> Reason (:~:) x y -> x :~: z #-} (===) :: Equality eq => eq x y -> Reason eq y z -> eq x z (===) = (=<=)-{-# SPECIALISE INLINE[1] (===) :: x :~: y -> Reason (:~:) y z -> x :~: z #-}+{-# SPECIALIZE INLINE [1] (===) :: x :~: y -> Reason (:~:) y z -> x :~: z #-} (=~=) :: r x y -> proxy y -> r x y eq =~= _ = eq@@ -128,63 +175,65 @@ cong Proxy Refl = Refl cong' :: (pxy m -> pxy (f m)) -> a :=: b -> f a :=: f b-cong' _ Refl = Refl+cong' _ Refl = Refl --- | Type coercion. 'coerce' is using @unsafeCoerce a@.--- So, please, please do not provide the @undefined@ as the proof.--- Using this function instead of pattern-matching on equality proof,--- you can reduce the overhead introduced by run-time proof.-coerce :: (a :=: b) -> f a -> f b-coerce _ a = unsafeCoerce a-{-# INLINE[1] coerce #-}+{- | Type coercion. 'coerce' is using @unsafeCoerce a@.+ So, please, please do not provide the @undefined@ as the proof.+ Using this function instead of pattern-matching on equality proof,+ you can reduce the overhead introduced by run-time proof.+-}+coerceInner, coerce :: (a :=: b) -> f a -> f b+{-# DEPRECATED coerce "Use coerceInner instead" #-}+coerce = coerceInner+{-# INLINE coerce #-}+coerceInner _ = unsafeCoerce+{-# INLINE [1] coerceInner #-} -- | Coercion for identity types. coerce' :: a :=: b -> a -> b-coerce' _ a = unsafeCoerce a-{-# INLINE[1] coerce' #-}+coerce' _ = unsafeCoerce+{-# INLINE [1] coerce' #-} {-# RULES "coerce/unsafeCoerce" [~1] forall xs.- coerce xs = unsafeCoerce+ coerceInner xs =+ unsafeCoerce "coerce'/unsafeCoerce" [~1] forall xs.- coerce' xs = unsafeCoerce+ coerce' xs =+ unsafeCoerce #-} --- | Solves equality constraint without explicit coercion.--- It has the same effect as @'Data.Type.Equality.gcastWith'@,--- but some hacks is done to reduce runtime overhead.+{- | Solves equality constraint without explicit coercion.+ 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 _ r = case unsafeCoerce (Refl :: () :~: ()) :: a :~: b of- Refl -> r-{-# NOINLINE withRefl #-}-{-# RULES-"withRefl/unsafeCoerce" [~1] forall x.- withRefl x = unsafeCoerce- #-}+withRefl _ = gcastWith (unsafeCoerce (Refl :: () :~: ()) :: a :~: b) -class Proposition (f :: k -> *) where- type OriginalProp (f :: k -> *) (n :: k) :: *+class Proposition (f :: k -> Type) where+ type OriginalProp (f :: k -> Type) (n :: k) :: Type unWrap :: f n -> OriginalProp f n- wrap :: OriginalProp f n -> f n+ wrap :: OriginalProp f n -> f n -data HVec (xs :: [*]) where+data HVec (xs :: [Type]) where HNil :: HVec '[] (:-) :: x -> HVec xs -> HVec (x ': xs) infixr 9 :--type family (xs :: [*]) :~> (a :: *) :: * where- '[] :~> a = a++type family (xs :: [Type]) :~> (a :: Type) :: Type where+ '[] :~> a = a (x ': xs) :~> a = x -> (xs :~> a) infixr 1 :~> -data HVecView (xs :: [*]) :: * where- HNilView :: HVecView '[]+data HVecView (xs :: [Type]) :: Type where+ HNilView :: HVecView '[] HConsView :: Proxy t -> HVecView ts -> HVecView (t ': ts) deriving instance Show (HVecView xs) -class KnownTypeList (xs :: [*]) where+class KnownTypeList (xs :: [Type]) where viewHVec' :: HVecView xs instance KnownTypeList '[] where@@ -193,15 +242,16 @@ instance KnownTypeList ts => KnownTypeList (t ': ts) where viewHVec' = HConsView Proxy viewHVec' -newtype Magic (xs :: [*]) 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 xs f = (unsafeCoerce (Magic f :: Magic xs a) :: HVecView xs -> a) xs apply' :: HVecView ts -> (HVec ts -> c) -> ts :~> c apply' HNilView f = f HNil-apply' (HConsView Proxy ts) f = \a -> withKnownTypeList ts $- apply' ts (\ts' -> f $ a :- ts')+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 = apply' (viewHVec' :: HVecView ts)@@ -209,10 +259,10 @@ applyNAry' :: KnownTypeList ts => proxy ts -> proxy' c -> (HVec ts -> c) -> ts :~> c applyNAry' _ _ = applyNAry -class FromBool (c :: *) where+class FromBool (c :: Type) where type Predicate c :: Bool- type Args c :: [*]+ type Args c :: [Type] 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' :: 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 view
@@ -1,34 +1,65 @@-{-# LANGUAGE DataKinds, DeriveDataTypeable, EmptyCase, ExplicitForAll #-}-{-# LANGUAGE ExplicitNamespaces, FlexibleInstances, GADTs, KindSignatures #-}-{-# LANGUAGE LambdaCase, PolyKinds, RankNTypes, StandaloneDeriving #-}-{-# LANGUAGE TemplateHaskell, TypeOperators #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE EmptyCase #-}+{-# LANGUAGE ExplicitForAll #-}+{-# LANGUAGE ExplicitNamespaces #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeOperators #-} {-# 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+ ( 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, (:~:) (..))+import Data.Typeable (Typeable)+import Data.Void import Proof.Propositional.Empty import Proof.Propositional.Inhabited import Proof.Propositional.TH--import Data.Data (Data)-import Data.Type.Equality ((:~:))-import Data.Typeable (Typeable)-import Data.Void import Unsafe.Coerce type a /\ b = (a, b)+ type a \/ b = Either a b-type Not a = a -> Void +type Not a = a -> Void+ infixr 2 \/+ infixr 3 /\ exfalso :: a -> Not a -> b@@ -53,69 +84,70 @@ andElimR = snd andAssocL :: a /\ (b /\ c) -> (a /\ b) /\ c-andAssocL (a,(b,c)) = ((a,b), c)+andAssocL (a, (b, c)) = ((a, b), c) andAssocR :: (a /\ b) /\ c -> a /\ (b /\ c)-andAssocR ((a,b),c) = (a,(b,c))+andAssocR ((a, b), c) = (a, (b, c)) orAssocL :: a \/ (b \/ c) -> (a \/ b) \/ c-orAssocL (Left a) = Left (Left a)-orAssocL (Right (Left b)) = Left (Right b)+orAssocL (Left a) = Left (Left a)+orAssocL (Right (Left b)) = Left (Right b) orAssocL (Right (Right c)) = Right c orAssocR :: (a \/ b) \/ c -> a \/ (b \/ c)-orAssocR (Left (Left a)) = Left a+orAssocR (Left (Left a)) = Left a orAssocR (Left (Right b)) = Right (Left b)-orAssocR (Right c) = Right (Right c)-+orAssocR (Right c) = Right (Right c) --- | Utility type to convert type-level (@'Bool'@-valued) predicate function--- into concrete witness data-type.+{- | Utility type to convert type-level (@'Bool'@-valued) predicate function+ into concrete witness data-type.+-} data IsTrue (b :: Bool) where Witness :: IsTrue 'True -withWitness :: IsTrue b -> (b ~ 'True => r) -> r-withWitness Witness r = r+withWitness :: forall b r. IsTrue b -> (b ~ 'True => r) -> r+withWitness _ = gcastWith (unsafeCoerce (Refl :: () :~: ()) :: b :~: 'True) {-# NOINLINE withWitness #-}-{-# RULES-"withWitness/coercion" [~1] forall x.- withWitness x = unsafeCoerce- #-} deriving instance Show (IsTrue b)-deriving instance Eq (IsTrue b)-deriving instance Ord (IsTrue b)++deriving instance Eq (IsTrue b)++deriving instance Ord (IsTrue b)+ deriving instance Read (IsTrue 'True)+ deriving instance Typeable IsTrue+ deriving instance Data (IsTrue 'True) instance {-# OVERLAPPABLE #-} (Inhabited a, Empty b) => Empty (a -> b) where eliminate f = eliminate (f trivial) -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|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|] -prove [t| Bool |]-prove [t| Int |]-prove [t| Integer |]-prove [t| Word |]-prove [t| Double |]-prove [t| Float |]-prove [t| Char |]-prove [t| Ordering |]-prove [t| forall a. [a] |]-prove [t| Rational |]-prove [t| forall a. Maybe a |]-prove [t| forall n. n :~: n |]-prove [t| IsTrue 'True |]+prove [t|Bool|]+prove [t|Int|]+prove [t|Integer|]+prove [t|Word|]+prove [t|Double|]+prove [t|Float|]+prove [t|Char|]+prove [t|Ordering|]+prove [t|forall a. [a]|]+prove [t|Rational|]+prove [t|forall a. Maybe a|]+prove [t|forall n. n :~: n|]+prove [t|IsTrue 'True|] instance Empty (IsTrue 'False) where- eliminate = \ case {}+ eliminate = \case
Proof/Propositional/TH.hs view
@@ -1,5 +1,5 @@ {-# LANGUAGE CPP, ExplicitNamespaces, MultiWayIf, PatternGuards #-}-{-# LANGUAGE TemplateHaskell, TupleSections #-}+{-# LANGUAGE TemplateHaskell, TupleSections, ViewPatterns #-} module Proof.Propositional.TH where import Proof.Propositional.Empty import Proof.Propositional.Inhabited@@ -23,6 +23,10 @@ #else DPat (DConPa, DVarPa), DPred(..), #endif+#if MIN_VERSION_th_desugar(1,12,0)+ DForallTelescope(..),+#endif+ DTyVarBndr (..), DType (..), Overlap (Overlapping), desugar, dsReify, expandType, substTy,@@ -30,7 +34,11 @@ #if !MIN_VERSION_base(4,13,0) import Data.Semigroup (Semigroup (..)) #endif+#if MIN_VERSION_th_desugar(1,12,0)+import Data.Functor (void)+#endif + -- | Macro to automatically derive @'Empty'@ instance for -- concrete (variable-free) types which may contain products. refute :: TypeQ -> DecsQ@@ -181,14 +189,14 @@ substFields subst (DRecC fs) = DRecC <$> forM fs (\(a,b,c) -> (a, b ,) <$> substTy subst c) -dtvbToName :: DTyVarBndr -> Name-dtvbToName (DPlainTV n) = n-dtvbToName (DKindedTV n _) = n- splitType :: DType -> Maybe ([Name], Name, [DType]) #if MIN_VERSION_th_desugar(1,11,0) splitType (DConstrainedT _ t) = splitType t+#if MIN_VERSION_th_desugar(1,12,0)+splitType (DForallT (unTelescope -> vs) t) +#else splitType (DForallT _ vs t) +#endif #else splitType (DForallT vs _ t) #endif@@ -246,7 +254,11 @@ bd <- compareType' t s return (pd <> bd) compareType' DConstrainedT{} _ = return NonEqual+#if MIN_VERSION_th_desugar(1,12,0)+compareType' (DForallT (unTelescope -> tTvBs) t) (DForallT (unTelescope -> sTvBs) s)+#else compareType' (DForallT _ tTvBs t) (DForallT _ sTvBs s)+#endif | length tTvBs == length sTvBs = do let dic = M.fromList $ zip (map dtvbToName sTvBs) (map (DVarT . dtvbToName) tTvBs) s' <- substTy dic s@@ -305,7 +317,11 @@ | l == r = return Equal | otherwise = return NonEqual comparePred (DConT _) _ = return NonEqual+#if MIN_VERSION_th_desugar(1,12,0)+comparePred (DForallT _ _) (DForallT _ _) = return Undecidable+#else comparePred (DForallT _ _ _) (DForallT _ _ _) = return Undecidable+#endif comparePred (DForallT{}) _ = return NonEqual comparePred _ _ = fail "Kind error: Expecting type-level predicate" #else@@ -353,6 +369,19 @@ substPred _ t = return t #endif --+{- FOURMOLU_DISABLE -}+#if MIN_VERSION_th_desugar(1,12,0)+dtvbToName :: DTyVarBndr flag -> Name+dtvbToName (DPlainTV n _) = n+dtvbToName (DKindedTV n _ _) = n+#else+dtvbToName :: DTyVarBndr -> Name+dtvbToName (DPlainTV n) = n+dtvbToName (DKindedTV n _) = n+#endif +#if MIN_VERSION_th_desugar(1,12,0)+unTelescope :: DForallTelescope -> [DTyVarBndr ()]+unTelescope (DForallVis vis) = map void vis+unTelescope (DForallInvis vis) = map void vis+#endif
equational-reasoning.cabal view
@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/ name: equational-reasoning-version: 0.6.0.4+version: 0.7.0.0 synopsis: Proof assistant for Haskell using DataKinds & PolyKinds description: A simple convenient library to write equational / preorder proof as in Agda. Since 0.6.0.0, this no longer depends on @singletons@ package, and the @Proof.Induction@ module goes to @equational-reasoning-induction@ package.@@ -13,7 +13,13 @@ copyright: (c) Hiromi ISHII 2013-2020 category: Math build-type: Simple-tested-with: GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.1, GHC == 8.6.5, GHC == 8.8.2+tested-with: GHC == 8.0.2,+ GHC == 8.2.1,+ GHC == 8.4.1,+ GHC == 8.6.3,+ GHC == 8.8.2,+ GHC == 8.10.3,+ GHC == 9.0.0.20201227 cabal-version: >=1.10 source-repository head type: git