content: {-# LANGUAGE AllowAmbiguousTypes #-} -- joinA
  {-# LANGUAGE InstanceSigs #-}
  {-# LANGUAGE TypeApplications #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE FlexibleInstances #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE TypeFamilies #-}
  {-# LANGUAGE MultiParamTypeClasses #-}
  {-# LANGUAGE ImpredicativeTypes #-}
  {-|
  
  Like 'Data.Equality.Analysis' but for 'Analysis' that are only well-defined
  within an (effectful) context. Mostly used with the monadic operations
  'representM', 'addM', 'mergeM', and 'rebuildM'.
  
  This effectful 'Analysis' could almost be trivially defined in terms of the
  other, through a "contextful" domain and by means of the '_classes' 'Traversal'.
  
  However, that would require an instance of 'Eq' for the monadic domain, which
  is usually unnattainable.
  
  Therefore, we do need this class for monadic 'Analysis'.
  
  -}
  module Data.Equality.Analysis.Monadic where
  
  
  import Data.Kind (Type)
  
  import Data.Equality.Graph.Internal (EGraph)
  import Data.Equality.Graph.Classes
  
  -- | An e-class analysis with domain @domain@ defined for a language @l@, whose operations are only well-defined within some effectful context.
  --
  -- The @domain@ is the type of the domain of the e-class analysis, that is, the
  -- type of the data stored in an e-class according to this e-class analysis
  class (Monad m, Eq domain) => AnalysisM m domain (l :: Type -> Type) where
  
      -- | When a new e-node is added into a new, singleton e-class, construct a
      -- new value of the domain to be associated with the new e-class, by
      -- accessing the associated data of the node's children
      --
      -- The argument is the e-node term populated with its children data
      makeA :: l domain -> m domain
  
      -- | When e-classes c1 c2 are being merged into c, join d_c1 and
      -- d_c2 into a new value d_c to be associated with the new
      -- e-class c
      joinA :: domain -> domain -> m domain
  
      -- | Optionally modify the e-class c (based on d_c), typically by adding an
      -- e-node to c. Modify should be idempotent if no other changes occur to
      -- the e-class, i.e., modify(modify(c)) = modify(c)
      modifyA :: ClassId
              -- ^ Id of class @c@ whose new data @d_c@ triggered the modify call
              -> EGraph domain l
              -- ^ E-graph where class @c@ being modified exists
              -> m (EGraph domain l)
              -- ^ E-graph resulting from the modification
      modifyA _ = pure
      {-# INLINE modifyA #-}
  
  
  -- | The simplest analysis that defines the domain to be () and does nothing otherwise
  instance Monad m => AnalysisM m () l where
    makeA _ = pure ()
    joinA _ _ = pure ()
  
  