Make NuMatchingAny1Proof an alias for a quantified NuMatching constraint

src/Data/Binding/Hobbits/NuMatching.hs

@@ -4,6 +4,7 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE QuasiQuotes #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
@@ -35,7 +36,7 @@
 module Data.Binding.Hobbits.NuMatching (
   NuMatching(..), mkNuMatching,
   MbTypeRepr(), isoMbTypeRepr, unsafeMbTypeRepr,
-  NuMatchingAny1(..)
+  NuMatchingAny1
 ) where
 
 import Prelude hiding (exp)
@@ -47,11 +48,8 @@ import qualified Language.Haskell.TH as TH
 import Language.Haskell.TH.Datatype.TyVarBndr
 import Control.Monad.State
 import Numeric.Natural
-import Data.Functor.Constant
 import Data.Kind as DK
 import Data.Word
-import Data.Proxy
-import Data.Type.Equality
 --import Control.Monad.Identity
 
 import Data.Type.RList hiding (map)
@@ -231,25 +229,12 @@ instance {-# OVERLAPPABLE #-} (NuMatching1 f, NuMatchingList ctx) =>
                   mapNames r elm
 -}
 
--- | Typeclass for lifting the 'NuMatching' constraint to functors on arbitrary
--- kinds that do not require any constraints on their input types
-class NuMatchingAny1 (f :: k -> Type) where
-  nuMatchingAny1Proof :: MbTypeRepr (f a)
-
-instance {-# INCOHERENT #-} NuMatchingAny1 f => NuMatching (f a) where
-  nuMatchingProof = nuMatchingAny1Proof
-
-instance NuMatchingAny1 Name where
-  nuMatchingAny1Proof = nuMatchingProof
-
-instance NuMatchingAny1 Proxy where
-  nuMatchingAny1Proof = nuMatchingProof
-
-instance NuMatchingAny1 ((:~:) a) where
-  nuMatchingAny1Proof = nuMatchingProof
-
-instance NuMatching a => NuMatchingAny1 (Constant a) where
-  nuMatchingAny1Proof = nuMatchingProof
+-- | An alias for a 'NuMatching' constraint on a functor of arbitrary kind that
+-- does not require any constraints on the input type. We define this as a
+-- class, rather than a type synonym, so that downstream users do not have to
+-- enable @QuantifiedConstraints@ just to be able to use it.
+class    (forall a. NuMatching (f a)) => NuMatchingAny1 (f :: k -> Type)
+instance (forall a. NuMatching (f a)) => NuMatchingAny1 (f :: k -> Type)
 
 instance {-# OVERLAPPABLE #-} NuMatchingAny1 f => NuMatching (RAssign f ctx) where
     nuMatchingProof = MbTypeReprData $ MkMbTypeReprData helper where
@@ -258,9 +243,6 @@ instance {-# OVERLAPPABLE #-} NuMatchingAny1 f => NuMatching (RAssign f ctx) whe
         helper _ MNil = MNil
         helper r (elms :>: elm) = helper r elms :>: mapNames r elm
 
-instance NuMatchingAny1 f => NuMatchingAny1 (RAssign f) where
-  nuMatchingAny1Proof = nuMatchingProof
-
 -- now we define some TH to create NuMatchings
 
 natsFrom :: Integer -> [Integer]

src/Data/Binding/Hobbits/NuMatchingInstances.hs

@@ -44,10 +44,6 @@ $(mkNuMatching [t| forall a b. NuMatching a => Constant a b |])
 $(mkNuMatching [t| forall f g a. (NuMatchingAny1 f,
                                   NuMatchingAny1 g) => Product f g a |])
 
-instance (NuMatchingAny1 f,
-          NuMatchingAny1 g) => NuMatchingAny1 (Product f g) where
-  nuMatchingAny1Proof = nuMatchingProof
-
 instance (Integral a, NuMatching a) => NuMatching (Ratio a) where
   nuMatchingProof =
     isoMbTypeRepr (\r -> (numerator r, denominator r)) (\(n,d) -> n%d)