From de6cfb48b7ecac034e9182398e5f7128099b29f8 Mon Sep 17 00:00:00 2001
From: Ben Selfridge <benselfridge@galois.com>
Date: Fri, 23 Apr 2021 15:41:52 -0700
Subject: [PATCH 1/4] Replaces ShowF with a type synonym

---
 src/Data/Parameterized/All.hs              |  4 +--
 src/Data/Parameterized/BoolRepr.hs         |  2 --
 src/Data/Parameterized/Classes.hs          | 34 ++++------------------
 src/Data/Parameterized/Context/Safe.hs     | 11 +------
 src/Data/Parameterized/Context/Unsafe.hs   | 14 ++-------
 src/Data/Parameterized/DataKind.hs         |  4 +--
 src/Data/Parameterized/List.hs             |  7 ++---
 src/Data/Parameterized/Map.hs              |  3 +-
 src/Data/Parameterized/NatRepr/Internal.hs |  2 --
 src/Data/Parameterized/Nonce.hs            |  2 --
 src/Data/Parameterized/Nonce/Unsafe.hs     |  2 --
 src/Data/Parameterized/Peano.hs            |  2 --
 src/Data/Parameterized/Some.hs             |  3 --
 src/Data/Parameterized/SymbolRepr.hs       |  2 --
 14 files changed, 17 insertions(+), 75 deletions(-)

diff --git a/src/Data/Parameterized/All.hs b/src/Data/Parameterized/All.hs
index 0c585f0..5fff172 100644
--- a/src/Data/Parameterized/All.hs
+++ b/src/Data/Parameterized/All.hs
@@ -38,6 +38,7 @@
 ------------------------------------------------------------------------
 
 {-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE RankNTypes #-}
 
 module Data.Parameterized.All
@@ -59,9 +60,6 @@ instance FunctorF All where
 instance FoldableF All where
   foldMapF toMonoid (All x) = toMonoid x
 
-instance ShowF f => Show (All f) where
-  show (All fa) = showF fa
-
 instance EqF f => Eq (All f) where
   (All x) == (All y) = eqF x y
 
diff --git a/src/Data/Parameterized/BoolRepr.hs b/src/Data/Parameterized/BoolRepr.hs
index 1534c34..c217e45 100644
--- a/src/Data/Parameterized/BoolRepr.hs
+++ b/src/Data/Parameterized/BoolRepr.hs
@@ -98,8 +98,6 @@ instance Show (BoolRepr m) where
   show FalseRepr = "FalseRepr"
   show TrueRepr  = "TrueRepr"
 
-instance ShowF BoolRepr
-
 instance HashableF BoolRepr where
   hashWithSaltF = hashWithSalt
 
diff --git a/src/Data/Parameterized/Classes.hs b/src/Data/Parameterized/Classes.hs
index dc3b990..56bd0fa 100644
--- a/src/Data/Parameterized/Classes.hs
+++ b/src/Data/Parameterized/Classes.hs
@@ -9,6 +9,7 @@ This module declares classes for working with types with the kind
 not restricted to '*'.
 -}
 {-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE DefaultSignatures #-}
 {-# LANGUAGE FlexibleContexts #-}
@@ -16,6 +17,7 @@ not restricted to '*'.
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE Safe #-}
 {-# LANGUAGE ScopedTypeVariables #-}
@@ -38,8 +40,7 @@ module Data.Parameterized.Classes
   , fromOrdering
   , ordFCompose
     -- * Typeclass generalizations
-  , ShowF(..)
-  , showsF
+  , ShowF
   , HashableF(..)
   , CoercibleF(..)
     -- * Type function application constructor
@@ -62,7 +63,6 @@ import Data.Functor.Compose (Compose(..))
 import Data.Kind
 import Data.Hashable
 import Data.Maybe (isJust)
-import Data.Proxy
 import Data.Type.Equality as Equality
 
 import Data.Parameterized.Compose ()
@@ -247,30 +247,8 @@ instance OrdF f => OrdF (Compose f g) where
 ------------------------------------------------------------------------
 -- ShowF
 
--- | A parameterized type that can be shown on all instances.
---
--- To implement @'ShowF' g@, one should implement an instance @'Show'
--- (g tp)@ for all argument types @tp@, then write an empty instance
--- @instance 'ShowF' g@.
-class ShowF (f :: k -> Type) where
-  -- | Provides a show instance for each type.
-  withShow :: p f -> q tp -> (Show (f tp) => a) -> a
-
-  default withShow :: Show (f tp) => p f -> q tp -> (Show (f tp) => a) -> a
-  withShow _ _ x = x
-
-  showF :: forall tp . f tp -> String
-  showF x = withShow (Proxy :: Proxy f) (Proxy :: Proxy tp) (show x)
-
-  -- | Like 'showsPrec', the precedence argument is /one more/ than the
-  -- precedence of the enclosing context.
-  showsPrecF :: forall tp. Int -> f tp -> String -> String
-  showsPrecF p x = withShow (Proxy :: Proxy f) (Proxy :: Proxy tp) (showsPrec p x)
-
-showsF :: ShowF f => f tp -> String -> String
-showsF x = showsPrecF 0 x
-
-instance Show x => ShowF (Const x)
+-- | A type synonym indicating that a type can be shown on all instances.
+type ShowF f = forall x . Show (f x)
 
 ------------------------------------------------------------------------
 -- IxedF
@@ -343,7 +321,7 @@ instance OrdF f => Ord (TypeAp f tp) where
   compare (TypeAp x) (TypeAp y) = toOrdering (compareF x y)
 
 instance ShowF f => Show (TypeAp f tp) where
-  showsPrec p (TypeAp x) = showsPrecF p x
+  showsPrec p (TypeAp x) = showsPrec p x
 
 instance HashableF f => Hashable (TypeAp f tp) where
   hashWithSalt s (TypeAp x) = hashWithSaltF s x
diff --git a/src/Data/Parameterized/Context/Safe.hs b/src/Data/Parameterized/Context/Safe.hs
index c872a2b..38ef9a3 100644
--- a/src/Data/Parameterized/Context/Safe.hs
+++ b/src/Data/Parameterized/Context/Safe.hs
@@ -37,6 +37,7 @@
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
@@ -137,8 +138,6 @@ data Size (ctx :: Ctx k) where
 instance Show (Size ctx) where
   show = show . sizeInt
 
-instance ShowF Size
-
 -- | Convert a context size to an 'Int'.
 sizeInt :: Size ctx -> Int
 sizeInt SizeZero = 0
@@ -414,8 +413,6 @@ intIndex n sz = listToMaybe $ drop n $ indexList sz
 instance Show (Index ctx tp) where
    show = show . indexVal
 
-instance ShowF (Index ctx)
-
 -- | View of indexes as pointing to the last element in the
 -- index range or pointing to an earlier element in a smaller
 -- range.
@@ -423,7 +420,6 @@ data IndexView ctx tp where
   IndexViewLast :: Size  ctx   -> IndexView (ctx '::> t) t
   IndexViewInit :: Index ctx t -> IndexView (ctx '::> u) t
 
-instance ShowF (IndexView ctx)
 deriving instance Show (IndexView ctx tp)
 
 -- | Project an index
@@ -601,11 +597,6 @@ instance HashableF f => Hashable (Assignment f ctx) where
   hashWithSalt s AssignmentEmpty = s
   hashWithSalt s (AssignmentExtend asgn x) = (s `hashWithSalt` asgn) `hashWithSaltF` x
 
-instance ShowF f => Show (Assignment f ctx) where
-  show a = "[" ++ intercalate ", " (toList showF a) ++ "]"
-
-instance ShowF f => ShowF (Assignment f)
-
 instance FunctorFC Assignment where
   fmapFC = fmapFCDefault
 
diff --git a/src/Data/Parameterized/Context/Unsafe.hs b/src/Data/Parameterized/Context/Unsafe.hs
index f44f521..1e1406b 100644
--- a/src/Data/Parameterized/Context/Unsafe.hs
+++ b/src/Data/Parameterized/Context/Unsafe.hs
@@ -5,6 +5,7 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE RoleAnnotations #-}
 {-# LANGUAGE ScopedTypeVariables #-}
@@ -146,8 +147,6 @@ sizeToNatRepr (Size n) = NatRepr (fromIntegral n)
 instance Show (Size ctx) where
   show (Size i) = show i
 
-instance ShowF Size
-
 -- | A context that can be determined statically at compiler time.
 class KnownContext (ctx :: Ctx k) where
   knownSize :: Size ctx
@@ -335,8 +334,6 @@ intIndex i n | 0 <= i && i < sizeInt n = Just (Some (Index i))
 instance Show (Index ctx tp) where
    show = show . indexVal
 
-instance ShowF (Index ctx)
-
 -- | View of indexes as pointing to the last element in the
 -- index range or pointing to an earlier element in a smaller
 -- range.
@@ -345,7 +342,6 @@ data IndexView ctx tp where
   IndexViewInit :: !(Index ctx t) -> IndexView (ctx '::> u) t
 
 deriving instance Show (IndexView ctx tp)
-instance ShowF (IndexView ctx)
 
 -- | Project an index
 viewIndex :: Size ctx -> Index ctx tp -> IndexView ctx tp
@@ -454,11 +450,9 @@ traverse_bal = go
 {-# INLINABLE traverse_bal #-}
 
 instance ShowF f => Show (BalancedTree h f tp) where
-  show (BalLeaf x) = showF x
+  show (BalLeaf x) = show x
   show (BalPair x y) = "BalPair " Prelude.++ show x Prelude.++ " " Prelude.++ show y
 
-instance ShowF f => ShowF (BalancedTree h f)
-
 unsafe_bal_generate :: forall ctx h f t
                      . Int -- ^ Height of tree to generate
                     -> Int -- ^ Starting offset for entries.
@@ -855,9 +849,7 @@ instance HashableF f => HashableF (Assignment f) where
   hashWithSaltF = hashWithSalt
 
 instance ShowF f => Show (Assignment f ctx) where
-  show a = "[" Prelude.++ intercalate ", " (toListFC showF a) Prelude.++ "]"
-
-instance ShowF f => ShowF (Assignment f)
+  show a = "[" Prelude.++ intercalate ", " (toListFC show a) Prelude.++ "]"
 
 {-# DEPRECATED adjust "Replace 'adjust f i asgn' with 'Lens.over (ixF i) f asgn' instead." #-}
 adjust :: (f tp -> f tp) -> Index ctx tp -> Assignment f ctx -> Assignment f ctx
diff --git a/src/Data/Parameterized/DataKind.hs b/src/Data/Parameterized/DataKind.hs
index b826c33..98afc4a 100644
--- a/src/Data/Parameterized/DataKind.hs
+++ b/src/Data/Parameterized/DataKind.hs
@@ -2,6 +2,7 @@
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE TypeFamilies #-}
@@ -33,8 +34,7 @@ snd (PairRepr _ b) = b
 $(return [])
 
 instance ( ShowF f, ShowF g ) => Show (PairRepr f g p) where
-  show (PairRepr a b) = showChar '(' . showsF a . showChar ',' . showsF b $ ")"
-instance ( ShowF f, ShowF g ) => ShowF (PairRepr f g)
+  show (PairRepr a b) = showChar '(' . shows a . showChar ',' . shows b $ ")"
 
 deriving instance ( Eq (f a), Eq (g b) ) => Eq (PairRepr f g '(a, b))
 instance ( TestEquality f, TestEquality g ) => TestEquality (PairRepr f g) where
diff --git a/src/Data/Parameterized/List.hs b/src/Data/Parameterized/List.hs
index e4a422a..3aa7a2c 100644
--- a/src/Data/Parameterized/List.hs
+++ b/src/Data/Parameterized/List.hs
@@ -126,6 +126,7 @@ use the 'Data.Parameterized.List.List' type for this purpose.
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE StandaloneDeriving #-}
@@ -174,12 +175,10 @@ instance ShowF f => Show (List f sh) where
   showsPrec p (elt :< rest) = showParen (p > precCons) $
     -- Unlike a derived 'Show' instance, we don't print parens implied
     -- by right associativity.
-    showsPrecF (precCons+1) elt . showString " :< " . showsPrec 0 rest
+    showsPrec (precCons+1) elt . showString " :< " . showsPrec 0 rest
     where
       precCons = 5
 
-instance ShowF f => ShowF (List f)
-
 instance FunctorFC List where
   fmapFC _ Nil = Nil
   fmapFC f (x :< xs) = f x :< fmapFC f xs
@@ -251,8 +250,6 @@ data Index :: [k] -> k -> Type  where
 deriving instance Eq (Index l x)
 deriving instance Show  (Index l x)
 
-instance ShowF (Index l)
-
 instance TestEquality (Index l) where
   testEquality IndexHere IndexHere = Just Refl
   testEquality (IndexThere x) (IndexThere y) = testEquality x y
diff --git a/src/Data/Parameterized/Map.hs b/src/Data/Parameterized/Map.hs
index 966df5a..8aabe6e 100644
--- a/src/Data/Parameterized/Map.hs
+++ b/src/Data/Parameterized/Map.hs
@@ -14,6 +14,7 @@ Some code was adapted from containers.
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeOperators #-}
@@ -309,7 +310,7 @@ instance TraversableF (MapF ktp) where
   traverseF = traverse
 
 instance (ShowF ktp, ShowF rtp) => Show (MapF ktp rtp) where
-  show m = showMap showF showF m
+  show m = showMap show show m
 
 -- | Return all keys of the map in ascending order.
 keys :: MapF k a -> [Some k]
diff --git a/src/Data/Parameterized/NatRepr/Internal.hs b/src/Data/Parameterized/NatRepr/Internal.hs
index d916734..e1588e2 100644
--- a/src/Data/Parameterized/NatRepr/Internal.hs
+++ b/src/Data/Parameterized/NatRepr/Internal.hs
@@ -86,8 +86,6 @@ instance PolyEq (NatRepr m) (NatRepr n) where
 instance Show (NatRepr n) where
   show (NatRepr n) = show n
 
-instance ShowF NatRepr
-
 instance HashableF NatRepr where
   hashWithSaltF = hashWithSalt
 
diff --git a/src/Data/Parameterized/Nonce.hs b/src/Data/Parameterized/Nonce.hs
index f605407..159cb08 100644
--- a/src/Data/Parameterized/Nonce.hs
+++ b/src/Data/Parameterized/Nonce.hs
@@ -142,8 +142,6 @@ instance OrdF (Nonce s) where
 instance HashableF (Nonce s) where
   hashWithSaltF s (Nonce x) = hashWithSalt s x
 
-instance ShowF (Nonce s)
-
 ------------------------------------------------------------------------
 -- * GlobalNonceGenerator
 
diff --git a/src/Data/Parameterized/Nonce/Unsafe.hs b/src/Data/Parameterized/Nonce/Unsafe.hs
index 038edf0..3d642c4 100644
--- a/src/Data/Parameterized/Nonce/Unsafe.hs
+++ b/src/Data/Parameterized/Nonce/Unsafe.hs
@@ -77,8 +77,6 @@ instance OrdF Nonce where
 instance HashableF Nonce where
   hashWithSaltF s (Nonce x) = hashWithSalt s x
 
-instance ShowF Nonce
-
 {-# INLINE freshNonce #-}
 -- | Get a fresh index and increment the counter.
 freshNonce :: NonceGenerator s -> ST s (Nonce tp)
diff --git a/src/Data/Parameterized/Peano.hs b/src/Data/Parameterized/Peano.hs
index 55c97ca..3810274 100644
--- a/src/Data/Parameterized/Peano.hs
+++ b/src/Data/Parameterized/Peano.hs
@@ -274,8 +274,6 @@ instance PolyEq (PeanoRepr m) (PeanoRepr n) where
 instance Show (PeanoRepr p) where
   show p = show (peanoValue p)
 
-instance ShowF PeanoRepr
-
 instance HashableF PeanoRepr where
   hashWithSaltF = hashWithSalt
 
diff --git a/src/Data/Parameterized/Some.hs b/src/Data/Parameterized/Some.hs
index 3df9359..68428c3 100644
--- a/src/Data/Parameterized/Some.hs
+++ b/src/Data/Parameterized/Some.hs
@@ -37,9 +37,6 @@ instance HashableF f => Hashable (Some f) where
   hashWithSalt s (Some x) = hashWithSaltF s x
   hash (Some x) = hashF x
 
-instance ShowF f => Show (Some f) where
-  show (Some x) = showF x
-
 -- | Project out of Some.
 viewSome :: (forall tp . f tp -> r) -> Some f -> r
 viewSome f (Some x) = f x
diff --git a/src/Data/Parameterized/SymbolRepr.hs b/src/Data/Parameterized/SymbolRepr.hs
index 749037f..630bbd1 100644
--- a/src/Data/Parameterized/SymbolRepr.hs
+++ b/src/Data/Parameterized/SymbolRepr.hs
@@ -105,8 +105,6 @@ instance Hashable (SymbolRepr nm) where
 instance Show (SymbolRepr nm) where
   show (SymbolRepr nm) = Text.unpack nm
 
-instance ShowF SymbolRepr
-
 
 -- | The SomeSym hides a Symbol parameter but preserves a
 -- KnownSymbol constraint on the hidden parameter.

From 0a1364a5d287e2427360cbdfd75186eb4c64263f Mon Sep 17 00:00:00 2001
From: Ben Selfridge <benselfridge@galois.com>
Date: Sat, 24 Apr 2021 11:06:10 -0700
Subject: [PATCH 2/4] Re-adds Show instance for Some

---
 src/Data/Parameterized/Some.hs | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/Data/Parameterized/Some.hs b/src/Data/Parameterized/Some.hs
index 68428c3..86fc01f 100644
--- a/src/Data/Parameterized/Some.hs
+++ b/src/Data/Parameterized/Some.hs
@@ -10,6 +10,7 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE RankNTypes #-}
 module Data.Parameterized.Some
   ( Some(..)
@@ -37,6 +38,9 @@ instance HashableF f => Hashable (Some f) where
   hashWithSalt s (Some x) = hashWithSaltF s x
   hash (Some x) = hashF x
 
+instance ShowF f => Show (Some f) where
+  show (Some x) = show x
+
 -- | Project out of Some.
 viewSome :: (forall tp . f tp -> r) -> Some f -> r
 viewSome f (Some x) = f x

From fc490a650852cc1bfcfb460cc62d0502e5ddac5c Mon Sep 17 00:00:00 2001
From: Ben Selfridge <benselfridge@galois.com>
Date: Sat, 24 Apr 2021 11:09:09 -0700
Subject: [PATCH 3/4] Re-adds Show instance for Assignment

---
 src/Data/Parameterized/Context/Safe.hs | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/Data/Parameterized/Context/Safe.hs b/src/Data/Parameterized/Context/Safe.hs
index 38ef9a3..81eb6da 100644
--- a/src/Data/Parameterized/Context/Safe.hs
+++ b/src/Data/Parameterized/Context/Safe.hs
@@ -597,6 +597,9 @@ instance HashableF f => Hashable (Assignment f ctx) where
   hashWithSalt s AssignmentEmpty = s
   hashWithSalt s (AssignmentExtend asgn x) = (s `hashWithSalt` asgn) `hashWithSaltF` x
 
+instance ShowF f => Show (Assignment f ctx) where
+  show a = "[" ++ intercalate ", " (toList show a) ++ "]"
+
 instance FunctorFC Assignment where
   fmapFC = fmapFCDefault
 

From dde613ddb474253e978441fced76e418008d3e94 Mon Sep 17 00:00:00 2001
From: Ben Selfridge <benselfridge@galois.com>
Date: Sat, 24 Apr 2021 11:09:23 -0700
Subject: [PATCH 4/4] Fixes tests

---
 test/Test/Context.hs | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/test/Test/Context.hs b/test/Test/Context.hs
index 7a094f3..a8ebe16 100644
--- a/test/Test/Context.hs
+++ b/test/Test/Context.hs
@@ -56,8 +56,6 @@ instance Show (Payload tp) where
   show (StringPayload x) = show x <> " :: String"
   show (BoolPayload x) = show x <> " :: Bool"
 
-instance ShowF Payload
-
 
 twiddle :: Payload a -> Payload a
 twiddle (IntPayload n) = IntPayload (n+1)
@@ -76,7 +74,6 @@ twiddle (BoolPayload b) = BoolPayload (not b)
 -- constraint.
 
 data MyMaybe t = (Show t) => MyJust t | MyNothing
-instance ShowF MyMaybe
 instance Show (MyMaybe t) where
   show (MyJust x) = "MyJust " <> show x
   show MyNothing = "MyNothing"