Replace Proxy3 with something more appropriate

Author: Ericson2314

src/Data/Functor/Misc.hs

@@ -21,7 +21,6 @@ are relevant to the use of 'Functor'-based datastructures like
 module Data.Functor.Misc
   ( -- * Const2
     Const2 (..)
-  , Proxy3 (..)
   , First2 (..)
   , unConst2
   , dmapToMap
@@ -43,7 +42,6 @@ module Data.Functor.Misc
   , ComposeMaybe (..)
   ) where
 
-import qualified Control.Category as Cat
 import Data.Dependent.Map (DMap)
 import qualified Data.Dependent.Map as DMap
 import Data.Dependent.Sum
@@ -96,17 +94,6 @@ instance Ord k => GCompare (Const2 k v) where
     EQ -> GEQ
     GT -> GGT
 
-data Proxy3 :: x -> y -> z -> Type where
-  Proxy3 :: Proxy3 vx vy vz
-  deriving ( Show, Read, Eq, Ord
-           , Functor, Foldable, Traversable
-           , Typeable
-           )
-
-instance Cat.Category (Proxy3 x) where
-  id = Proxy3
-  ~Proxy3 . ~Proxy3 = Proxy3
-
 newtype First2 (t :: k -> Type) (a :: k) (b :: k) = First2 (t b)
   deriving ( Show, Read, Eq, Ord
            , Functor, Foldable, Traversable

src/Data/Patch/Class.hs

@@ -3,11 +3,13 @@
 {-# LANGUAGE DerivingStrategies #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE StandaloneDeriving #-}
 
 {-|
 Description: The module provides the 'Patch' class.
@@ -17,6 +19,7 @@ This is a class for types which represent changes made to other types
 module Data.Patch.Class where
 
 import qualified Data.Semigroupoid as Cat
+import qualified Control.Category as Cat
 import Data.Functor.Identity
 import Data.Functor.Misc
 import Data.Kind (Type)
@@ -25,7 +28,7 @@ import Data.Maybe
 import Data.Semigroup (Semigroup(..))
 #endif
 import Data.Proxy
-import Data.Type.Equality ((:~:) (..))
+import Data.Typeable
 
 class PatchHet p where
   type PatchSource p :: Type
@@ -165,12 +168,25 @@ instance PatchHet (First2 (t :: k -> Type) (from :: k) (to :: k)) where
   type PatchTarget (First2 t from to) = t to
   applyHet (First2 val) _ = Right val
 
--- | 'Proxy3' can be used as a 'Patch' that always does nothing
-instance PatchHet (Proxy3 (t :: k -> Type) (a :: k) (a :: k)) where
-  type PatchSource (Proxy3 t a a) = t a
-  type PatchTarget (Proxy3 t a a) = t a
-  applyHet ~Proxy3 _ = Left Refl
+data IndexedEq :: (k -> Type) -> k -> k -> Type where
+  IndexedRefl :: IndexedEq k x x
+  deriving (Typeable)
 
-instance PatchHet2Base (Proxy3 (t :: k -> Type) :: k -> k -> Type) where
-  type PatchSource1 (Proxy3 t) = t
-  type PatchTarget1 (Proxy3 t) = t
+deriving instance Eq (IndexedEq k x y)
+deriving instance Ord (IndexedEq k x y)
+deriving instance Show (IndexedEq k x y)
+deriving instance Read (IndexedEq k x x)
+
+instance Cat.Category (IndexedEq x) where
+  id = IndexedRefl
+  IndexedRefl . IndexedRefl = IndexedRefl
+
+-- | 'IndexedEq' can be used as a 'Patch' that always does nothing
+instance PatchHet (IndexedEq (t :: k -> Type) (a :: k) (b :: k)) where
+  type PatchSource (IndexedEq t a b) = t a
+  type PatchTarget (IndexedEq t a b) = t b
+  applyHet IndexedRefl _ = Left Refl
+
+instance PatchHet2Base (IndexedEq (t :: k -> Type) :: k -> k -> Type) where
+  type PatchSource1 (IndexedEq t) = t
+  type PatchTarget1 (IndexedEq t) = t

src/Data/Patch/DMapWithPatchingMove.hs

@@ -28,7 +28,7 @@ import Data.Dependent.Sum (DSum (..))
 import qualified Data.Dependent.Map as DMap
 import Data.Functor.Constant (Constant (..))
 import Data.Functor.Misc
-  ( Const2 (..), Proxy3 (..)
+  ( Const2 (..)
   , weakenDMapWith
   , dmapToMapWith
   )
@@ -53,6 +53,7 @@ import Data.Patch.Class
   ( Patch (..), PatchHet (..)
   , PatchHet2 (..), PatchSource1, PatchTarget1
   , applyAlwaysHet2
+  , IndexedEq (..)
   )
 import Data.Patch.MapWithPatchingMove (PatchMapWithPatchingMove (..))
 import qualified Data.Patch.MapWithPatchingMove as MapWithPatchingMove
@@ -359,10 +360,10 @@ insertDMapKey k v =
 -- @
 moveDMapKey
   :: GCompare k
-  => k a -> k a -> PatchDMapWithPatchingMove k (Proxy3 v)
+  => k a -> k a -> PatchDMapWithPatchingMove k (IndexedEq v)
 moveDMapKey src dst = case src `geq` dst of
   Nothing -> PatchDMapWithPatchingMove $ DMap.fromList
-    [ dst :=> NodeInfo (From_Move (src :=> Flip Proxy3)) To_NonMove
+    [ dst :=> NodeInfo (From_Move (src :=> Flip IndexedRefl)) To_NonMove
     , src :=> NodeInfo From_Delete (To_Move $ Some dst)
     ]
   Just _ -> PatchDMapWithPatchingMove DMap.empty
@@ -377,11 +378,11 @@ moveDMapKey src dst = case src `geq` dst of
 --      . maybe id (DMap.insert b) (aMay <> bMay)
 --      . DMap.delete a . DMap.delete b $ dmap
 -- @
-swapDMapKey :: GCompare k => k a -> k a -> PatchDMapWithPatchingMove k (Proxy3 v)
+swapDMapKey :: GCompare k => k a -> k a -> PatchDMapWithPatchingMove k (IndexedEq v)
 swapDMapKey src dst = case src `geq` dst of
   Nothing -> PatchDMapWithPatchingMove $ DMap.fromList
-    [ dst :=> NodeInfo (From_Move (src :=> Flip Proxy3)) (To_Move $ Some src)
-    , src :=> NodeInfo (From_Move (dst :=> Flip Proxy3)) (To_Move $ Some dst)
+    [ dst :=> NodeInfo (From_Move (src :=> Flip IndexedRefl)) (To_Move $ Some src)
+    , src :=> NodeInfo (From_Move (dst :=> Flip IndexedRefl)) (To_Move $ Some dst)
     ]
   Just _ -> PatchDMapWithPatchingMove DMap.empty
 
@@ -566,16 +567,16 @@ const2PatchDMapWithPatchingMoveWith
   :: forall k v v' a
   .  (v -> v' a)
   -> PatchMapWithPatchingMove k (Proxy v)
-  -> PatchDMapWithPatchingMove (Const2 k a) (Proxy3 v')
+  -> PatchDMapWithPatchingMove (Const2 k a) (IndexedEq v')
 const2PatchDMapWithPatchingMoveWith f (PatchMapWithPatchingMove p) =
   PatchDMapWithPatchingMove $ DMap.fromDistinctAscList $ g <$> Map.toAscList p
   where g :: (k, MapWithPatchingMove.NodeInfo k (Proxy v))
-          -> DSum (Const2 k a) (NodeInfo (Const2 k a) (Proxy3 v'))
+          -> DSum (Const2 k a) (NodeInfo (Const2 k a) (IndexedEq v'))
         g (k, ni) = Const2 k :=> NodeInfo
           { _nodeInfo_from = case MapWithPatchingMove._nodeInfo_from ni of
               MapWithPatchingMove.From_Insert v -> From_Insert $ f v
               MapWithPatchingMove.From_Delete -> From_Delete
-              MapWithPatchingMove.From_Move fromKey Proxy -> From_Move $ Const2 fromKey :=> Flip Proxy3
+              MapWithPatchingMove.From_Move fromKey Proxy -> From_Move $ Const2 fromKey :=> Flip IndexedRefl
           , _nodeInfo_to = case MapWithPatchingMove._nodeInfo_to ni of
               Nothing -> To_NonMove
               Just toKey -> To_Move $ Some (Const2 toKey)