Represent term/value types with type families.

src/Analysis/Abstract/Caching.hs

@@ -1,4 +1,4 @@
-{-# LANGUAGE DataKinds, GeneralizedNewtypeDeriving, MultiParamTypeClasses, ScopedTypeVariables, StandaloneDeriving, TypeApplications, TypeOperators, UndecidableInstances #-}
+{-# LANGUAGE DataKinds, GeneralizedNewtypeDeriving, MultiParamTypeClasses, ScopedTypeVariables, StandaloneDeriving, TypeApplications, TypeFamilies, TypeOperators, UndecidableInstances #-}
 module Analysis.Abstract.Caching
   ( evaluateCache )
   where
@@ -29,7 +29,7 @@ type CacheFor term value = Cache (LocationFor value) term value
 newtype CachingAnalysis term value a = CachingAnalysis { runCachingAnalysis :: Evaluator term value (CachingEffects term value) a }
   deriving (Alternative, Applicative, Functor, Monad, MonadFail, MonadFresh, MonadNonDet)
 
-deriving instance MonadEvaluator term value (CachingAnalysis term value)
+deriving instance Ord (LocationFor value) => MonadEvaluator (CachingAnalysis term value)
 
 -- TODO: reabstract these later on
 
@@ -62,12 +62,12 @@ instance ( Corecursive t
          , Evaluatable (Base t)
          , Foldable (Cell (LocationFor v))
          , FreeVariables t
-         , MonadAddressable (LocationFor v) v (CachingAnalysis t v)
+         , MonadAddressable (LocationFor v) (CachingAnalysis t v)
-         , MonadValue t v (CachingAnalysis t v)
+         , MonadValue v (CachingAnalysis t v)
          , Recursive t
          , Semigroup (CellFor v)
          )
-         => MonadAnalysis t v (CachingAnalysis t v) where
+         => MonadAnalysis (CachingAnalysis t v) where
   analyzeTerm e = do
     c <- getConfiguration (embedSubterm e)
     -- Convergence here is predicated upon an Eq instance, not α-equivalence
@@ -85,6 +85,9 @@ instance ( Corecursive t
       getCache) mempty
     maybe empty scatter (cacheLookup c cache)
 
+type instance AnalysisTerm (CachingAnalysis term value) = term
+type instance AnalysisValue (CachingAnalysis term value) = value
+
 
 -- | Coinductively-cached evaluation.
 evaluateCache :: forall v term
@@ -98,8 +101,8 @@ evaluateCache :: forall v term
                 , Foldable (Cell (LocationFor v))
                 , Functor (Base term)
                 , Recursive term
-                , MonadAddressable (LocationFor v) v (CachingAnalysis term v)
+                , MonadAddressable (LocationFor v) (CachingAnalysis term v)
-                , MonadValue term v (CachingAnalysis term v)
+                , MonadValue v (CachingAnalysis term v)
                 , Semigroup (CellFor v)
                 , ValueRoots (LocationFor v) v
                 )
@@ -123,7 +126,7 @@ converge f = loop
             loop x'
 
 -- | Nondeterministically write each of a collection of stores & return their associated results.
-scatter :: (Alternative m, Foldable t, MonadEvaluator term v m) => t (a, Store (LocationFor v) v) -> m a
+scatter :: (Alternative m, Foldable t, MonadEvaluator m) => t (a, Store (LocationFor (AnalysisValue m)) (AnalysisValue m)) -> m a
 scatter = getAlt . foldMap (\ (value, store') -> Alt (putStore store' *> pure value))
 
 -- | Evaluation of a single iteration of an analysis, given an in-cache as an oracle for results and an out-cache to record computed results in.
@@ -138,8 +141,8 @@ memoizeEval :: forall v term
               , Foldable (Cell (LocationFor v))
               , Functor (Base term)
               , Recursive term
-              , MonadAddressable (LocationFor v) v (CachingAnalysis term v)
+              , MonadAddressable (LocationFor v) (CachingAnalysis term v)
-              , MonadValue term v (CachingAnalysis term v)
+              , MonadValue v (CachingAnalysis term v)
               , Semigroup (CellFor v)
               )
             => SubtermAlgebra (Base term) term (CachingAnalysis term v v)

src/Analysis/Abstract/Dead.hs

@@ -1,4 +1,4 @@
-{-# LANGUAGE DataKinds, GeneralizedNewtypeDeriving, MultiParamTypeClasses, ScopedTypeVariables, StandaloneDeriving, TypeApplications, TypeOperators, UndecidableInstances #-}
+{-# LANGUAGE DataKinds, GeneralizedNewtypeDeriving, MultiParamTypeClasses, ScopedTypeVariables, StandaloneDeriving, TypeApplications, TypeFamilies, TypeOperators, UndecidableInstances #-}
 module Analysis.Abstract.Dead where
 
 import Control.Abstract.Addressable
@@ -19,8 +19,8 @@ evaluateDead :: forall term value
                 , Evaluatable (Base term)
                 , Foldable (Base term)
                 , FreeVariables term
-                , MonadAddressable (LocationFor value) value (DeadCodeAnalysis term value)
+                , MonadAddressable (LocationFor value) (DeadCodeAnalysis term value)
-                , MonadValue term value (DeadCodeAnalysis term value)
+                , MonadValue value (DeadCodeAnalysis term value)
                 , Ord (LocationFor value)
                 , Ord term
                 , Recursive term
@@ -39,7 +39,7 @@ evaluateDead term = run @(DeadCodeEffects term value) . runEvaluator . runDeadCo
 newtype DeadCodeAnalysis term value a = DeadCodeAnalysis { runDeadCodeAnalysis :: Evaluator term value (DeadCodeEffects term value) a }
   deriving (Applicative, Functor, Monad, MonadFail)
 
-deriving instance MonadEvaluator term value (DeadCodeAnalysis term value)
+deriving instance Ord (LocationFor value) => MonadEvaluator (DeadCodeAnalysis term value)
 
 
 -- | A set of “dead” (unreachable) terms.
@@ -60,13 +60,16 @@ revive t = DeadCodeAnalysis (Evaluator (modify (Dead . delete t . unDead)))
 instance ( Corecursive t
          , Evaluatable (Base t)
          , FreeVariables t
-         , MonadAddressable (LocationFor v) v (DeadCodeAnalysis t v)
+         , MonadAddressable (LocationFor v) (DeadCodeAnalysis t v)
-         , MonadValue t v (DeadCodeAnalysis t v)
+         , MonadValue v (DeadCodeAnalysis t v)
          , Ord t
          , Recursive t
          , Semigroup (CellFor v)
          )
-         => MonadAnalysis t v (DeadCodeAnalysis t v) where
+         => MonadAnalysis (DeadCodeAnalysis t v) where
   analyzeTerm term = do
     revive (embedSubterm term)
     eval term
+
+type instance AnalysisTerm (DeadCodeAnalysis term value) = term
+type instance AnalysisValue (DeadCodeAnalysis term value) = value

src/Analysis/Abstract/Evaluating.hs

@@ -15,8 +15,8 @@ import System.FilePath.Posix
 evaluate :: forall value term
          .  ( Evaluatable (Base term)
             , FreeVariables term
-            , MonadAddressable (LocationFor value) value (Evaluation term value)
+            , MonadAddressable (LocationFor value) (Evaluation term value)
-            , MonadValue term value (Evaluation term value)
+            , MonadValue value (Evaluation term value)
             , Ord (LocationFor value)
             , Recursive term
             , Semigroup (CellFor value)
@@ -29,8 +29,8 @@ evaluate = run @(EvaluatorEffects term value) . runEvaluator . runEvaluation . e
 evaluates :: forall value term
           .  ( Evaluatable (Base term)
              , FreeVariables term
-             , MonadAddressable (LocationFor value) value (Evaluation term value)
+             , MonadAddressable (LocationFor value) (Evaluation term value)
-             , MonadValue term value (Evaluation term value)
+             , MonadValue value (Evaluation term value)
              , Ord (LocationFor value)
              , Recursive term
              , Semigroup (CellFor value)
@@ -41,7 +41,7 @@ evaluates :: forall value term
 evaluates pairs (_, t) = run @(EvaluatorEffects term value) (runEvaluator (runEvaluation (withModules pairs (evaluateTerm t))))
 
 -- | Run an action with the passed ('Blob', @term@) pairs available for imports.
-withModules :: (MonadAnalysis term value m, MonadEvaluator term value m) => [(Blob, term)] -> m a -> m a
+withModules :: (MonadAnalysis m, MonadEvaluator m) => [(Blob, AnalysisTerm m)] -> m a -> m a
 withModules pairs = localModuleTable (const moduleTable)
   where moduleTable = Linker (Map.fromList (map (first (dropExtensions . blobPath)) pairs))
 
@@ -49,14 +49,17 @@ withModules pairs = localModuleTable (const moduleTable)
 newtype Evaluation term value a = Evaluation { runEvaluation :: Evaluator term value (EvaluatorEffects term value) a }
   deriving (Applicative, Functor, Monad, MonadFail)
 
-deriving instance MonadEvaluator term value (Evaluation term value)
+deriving instance Ord (LocationFor value) => MonadEvaluator (Evaluation term value)
 
 instance ( Evaluatable (Base term)
          , FreeVariables term
-         , MonadAddressable (LocationFor value) value (Evaluation term value)
+         , MonadAddressable (LocationFor value) (Evaluation term value)
-         , MonadValue term value (Evaluation term value)
+         , MonadValue value (Evaluation term value)
          , Recursive term
          , Semigroup (CellFor value)
          )
-         => MonadAnalysis term value (Evaluation term value) where
+         => MonadAnalysis (Evaluation term value) where
   analyzeTerm = eval
+
+type instance AnalysisTerm (Evaluation term value) = term
+type instance AnalysisValue (Evaluation term value) = value

src/Analysis/Abstract/Tracing.hs

@@ -1,4 +1,4 @@
-{-# LANGUAGE DataKinds, GeneralizedNewtypeDeriving, KindSignatures, MultiParamTypeClasses, ScopedTypeVariables, StandaloneDeriving, TypeApplications, TypeOperators, UndecidableInstances #-}
+{-# LANGUAGE DataKinds, GeneralizedNewtypeDeriving, KindSignatures, MultiParamTypeClasses, ScopedTypeVariables, StandaloneDeriving, TypeApplications, TypeFamilies, TypeOperators, UndecidableInstances #-}
 module Analysis.Abstract.Tracing where
 
 import Control.Abstract.Addressable
@@ -26,11 +26,13 @@ evaluateTrace :: forall trace value term
                 , Ord (CellFor value)
                 , Ord term
                 , Ord value
+                , AnalysisTerm (Evaluator term value (TracingEffects trace term value)) ~ term
+                , AnalysisValue (Evaluator term value (TracingEffects trace term value)) ~ value
                 , Recursive term
                 , Reducer (ConfigurationFor term value) trace
-                , MonadAddressable (LocationFor value) value (TracingAnalysis trace Evaluator term value (TracingEffects trace term value))
+                , MonadAddressable (LocationFor value) (TracingAnalysis trace (Evaluator term value) term value (TracingEffects trace term value))
-                , MonadAnalysis term value (Evaluator term value (TracingEffects trace term value))
+                , MonadAnalysis (Evaluator term value (TracingEffects trace term value))
-                , MonadValue term value (TracingAnalysis trace Evaluator term value (TracingEffects trace term value))
+                , MonadValue value (TracingAnalysis trace (Evaluator term value) term value (TracingEffects trace term value))
                 , Semigroup (CellFor value)
                 )
               => term
@@ -39,27 +41,32 @@ evaluateTrace = run @(TracingEffects trace term value) . runEvaluator . runTraci
 
 
 newtype TracingAnalysis trace underlying term value (effects :: [* -> *]) a
-  = TracingAnalysis { runTracingAnalysis :: underlying term value effects a }
+  = TracingAnalysis { runTracingAnalysis :: underlying effects a }
   deriving (Applicative, Functor, LiftEffect, Monad, MonadFail)
 
-deriving instance MonadEvaluator term value (underlying term value effects) => MonadEvaluator term value (TracingAnalysis trace underlying term value effects)
+deriving instance (AnalysisTerm (underlying effects) ~ term, AnalysisValue (underlying effects) ~ value, MonadEvaluator (underlying effects)) => MonadEvaluator (TracingAnalysis trace underlying term value effects)
 
 instance ( Corecursive term
          , Evaluatable (Base term)
          , FreeVariables term
-         , LiftEffect (underlying term value)
+         , LiftEffect underlying
          , Member (Writer trace) effects
-         , MonadAddressable (LocationFor value) value (TracingAnalysis trace underlying term value effects)
+         , MonadAddressable (LocationFor value) (TracingAnalysis trace underlying term value effects)
-         , MonadAnalysis term value (underlying term value effects)
+         , MonadAnalysis (underlying effects)
-         , MonadValue term value (TracingAnalysis trace underlying term value effects)
+         , AnalysisTerm (underlying effects) ~ term
+         , AnalysisValue (underlying effects) ~ value
+         , MonadValue value (TracingAnalysis trace underlying term value effects)
          , Recursive term
          , Reducer (ConfigurationFor term value) trace
          , Semigroup (CellFor value)
          )
-         => MonadAnalysis term value (TracingAnalysis trace underlying term value effects) where
+         => MonadAnalysis (TracingAnalysis trace underlying term value effects) where
   analyzeTerm term = getConfiguration (embedSubterm term) >>= trace . Reducer.unit >> analyzeTerm term
 
-trace :: (LiftEffect (underlying term value), Member (Writer trace) effects)
+type instance AnalysisTerm (TracingAnalysis trace underlying term value effects) = term
+type instance AnalysisValue (TracingAnalysis trace underlying term value effects) = value
+
+trace :: (LiftEffect underlying, Member (Writer trace) effects)
       => trace
       -> TracingAnalysis trace underlying term value effects ()
 trace w = lift (tell w)

src/Control/Abstract/Addressable.hs

@@ -1,10 +1,10 @@
 {-# LANGUAGE FunctionalDependencies, TypeFamilies, UndecidableInstances #-}
 module Control.Abstract.Addressable where
 
+import Control.Abstract.Analysis
 import Control.Abstract.Evaluator
 import Control.Applicative
 import Control.Monad ((<=<))
-import Control.Monad.Effect.Fail
 import Data.Abstract.Address
 import Data.Abstract.Environment
 import Data.Abstract.FreeVariables
@@ -16,19 +16,20 @@ import Data.Semigroup.Reducer
 import Prelude hiding (fail)
 
 -- | Defines 'alloc'ation and 'deref'erencing of 'Address'es in a Store.
-class (Monad m, Ord l, l ~ LocationFor a, Reducer a (Cell l a)) => MonadAddressable l a m | m -> a where
+class (Monad m, Ord l, l ~ LocationFor (AnalysisValue m), Reducer (AnalysisValue m) (Cell l (AnalysisValue m))) => MonadAddressable l m where
-  deref :: Address l a
+  deref :: Address l (AnalysisValue m)
-        -> m a
+        -> m (AnalysisValue m)
 
   alloc :: Name
-        -> m (Address l a)
+        -> m (Address l (AnalysisValue m))
 
 -- | Look up or allocate an address for a 'Name' free in a given term & assign it a given value, returning the 'Name' paired with the address.
 --
 --   The term is expected to contain one and only one free 'Name', meaning that care should be taken to apply this only to e.g. identifiers.
 lookupOrAlloc :: ( FreeVariables t
-                 , MonadAddressable (LocationFor a) a m
+                 , MonadAddressable (LocationFor a) m
-                 , MonadEvaluator t a m
+                 , MonadEvaluator m
+                 , a ~ AnalysisValue m
                  , Semigroup (CellFor a)
                  )
                  => t
@@ -40,8 +41,9 @@ lookupOrAlloc term = let [name] = toList (freeVariables term) in
   where
     -- | Look up or allocate an address for a 'Name' & assign it a given value, returning the 'Name' paired with the address.
     lookupOrAlloc' :: ( Semigroup (CellFor a)
-                      , MonadAddressable (LocationFor a) a m
+                      , MonadAddressable (LocationFor a) m
-                      , MonadEvaluator t a m
+                      , a ~ AnalysisValue m
+                      , MonadEvaluator m
                       )
                       => Name
                       -> a
@@ -54,7 +56,8 @@ lookupOrAlloc term = let [name] = toList (freeVariables term) in
 
 -- | Write a value to the given 'Address' in the 'Store'.
 assign :: ( Ord (LocationFor a)
-          , MonadEvaluator t a m
+          , MonadEvaluator m
+          , a ~ AnalysisValue m
           , Reducer a (CellFor a)
           )
           => Address (LocationFor a) a
@@ -66,7 +69,7 @@ assign address = modifyStore . storeInsert address
 -- Instances
 
 -- | 'Precise' locations are always 'alloc'ated a fresh 'Address', and 'deref'erence to the 'Latest' value written.
-instance (Monad m, MonadEvaluator t v m, LocationFor v ~ Precise) => MonadAddressable Precise v m where
+instance (Monad m, MonadEvaluator m, LocationFor (AnalysisValue m) ~ Precise) => MonadAddressable Precise m where
   deref = maybe uninitializedAddress (pure . unLatest) <=< flip fmap getStore . storeLookup
     where
       -- | Fail with a message denoting an uninitialized address (i.e. one which was 'alloc'ated, but never 'assign'ed a value before being 'deref'erenced).
@@ -77,7 +80,7 @@ instance (Monad m, MonadEvaluator t v m, LocationFor v ~ Precise) => MonadAddres
 
 
 -- | 'Monovariant' locations 'alloc'ate one 'Address' per unique variable name, and 'deref'erence once per stored value, nondeterministically.
-instance (Alternative m, Ord v, LocationFor v ~ Monovariant, Monad m, MonadEvaluator t v m) => MonadAddressable Monovariant v m where
+instance (Alternative m, Ord (AnalysisValue m), LocationFor (AnalysisValue m) ~ Monovariant, Monad m, MonadEvaluator m) => MonadAddressable Monovariant m where
   deref = asum . maybe [] (map pure . toList) <=< flip fmap getStore . storeLookup
 
   alloc = pure . Address . Monovariant

src/Control/Abstract/Analysis.hs

@@ -1,6 +1,8 @@
-{-# LANGUAGE DefaultSignatures, FunctionalDependencies #-}
+{-# LANGUAGE DefaultSignatures, KindSignatures, TypeFamilies #-}
 module Control.Abstract.Analysis
 ( MonadAnalysis(..)
+, AnalysisTerm
+, AnalysisValue
 , module X
 , Subterm(..)
 , SubtermAlgebra
@@ -12,16 +14,19 @@ import Control.Monad.Effect.Reader as X
 import Control.Monad.Effect.State as X
 import Prologue
 
+type family AnalysisTerm (m :: * -> *)
+type family AnalysisValue (m :: * -> *)
+
 -- | A 'Monad' in which one can evaluate some specific term type to some specific value type.
 --
 --   This typeclass is left intentionally unconstrained to avoid circular dependencies between it and other typeclasses.
-class Monad m => MonadAnalysis term value m | m -> term, m -> value where
+class Monad m => MonadAnalysis m where
   -- | Analyze a term using the semantics of the current analysis. This should generally only be called by definitions of 'evaluateTerm' and 'analyzeTerm' in this or other instances.
-  analyzeTerm :: SubtermAlgebra (Base term) term (m value)
+  analyzeTerm :: SubtermAlgebra (Base (AnalysisTerm m)) (AnalysisTerm m) (m (AnalysisValue m))
 
   -- | Evaluate a term to a value using the semantics of the current analysis.
   --
   --   This should always be called instead of explicitly folding either 'eval' or 'analyzeTerm' over subterms, except in 'MonadAnalysis' instances themselves.
-  evaluateTerm :: term -> m value
+  evaluateTerm :: AnalysisTerm m -> m (AnalysisValue m)
-  default evaluateTerm :: Recursive term => term -> m value
+  default evaluateTerm :: Recursive (AnalysisTerm m) => AnalysisTerm m -> m (AnalysisValue m)
   evaluateTerm = foldSubterms analyzeTerm

src/Control/Abstract/Evaluator.hs

@@ -1,14 +1,11 @@
-{-# LANGUAGE DataKinds, DefaultSignatures, FunctionalDependencies, GeneralizedNewtypeDeriving, RankNTypes, StandaloneDeriving, UndecidableInstances #-}
+{-# LANGUAGE DataKinds, DefaultSignatures, GeneralizedNewtypeDeriving, RankNTypes, StandaloneDeriving, TypeFamilies, UndecidableInstances #-}
 module Control.Abstract.Evaluator where
 
+import Control.Abstract.Analysis
 import Control.Applicative
-import Control.Effect
 import Control.Monad.Effect
-import Control.Monad.Effect.Fail
 import Control.Monad.Effect.Fresh
 import Control.Monad.Effect.NonDet
-import Control.Monad.Effect.Reader
-import Control.Monad.Effect.State
 import Data.Abstract.Configuration
 import Data.Abstract.Linker
 import Data.Abstract.Live
@@ -21,38 +18,38 @@ import Prelude hiding (fail)
 --   - environments binding names to addresses
 --   - a heap mapping addresses to (possibly sets of) values
 --   - tables of modules available for import
-class MonadFail m => MonadEvaluator term value m | m -> term, m -> value where
+class (MonadFail m, Ord (LocationFor (AnalysisValue m))) => MonadEvaluator m where
   -- | Retrieve the global environment.
-  getGlobalEnv :: m (EnvironmentFor value)
+  getGlobalEnv :: m (EnvironmentFor (AnalysisValue m))
   -- | Update the global environment.
-  modifyGlobalEnv :: (EnvironmentFor value -> EnvironmentFor value) -> m ()
+  modifyGlobalEnv :: (EnvironmentFor (AnalysisValue m) -> EnvironmentFor (AnalysisValue m)) -> m ()
 
   -- | Retrieve the local environment.
-  askLocalEnv :: m (EnvironmentFor value)
+  askLocalEnv :: m (EnvironmentFor (AnalysisValue m))
   -- | Run an action with a locally-modified environment.
-  localEnv :: (EnvironmentFor value -> EnvironmentFor value) -> m a -> m a
+  localEnv :: (EnvironmentFor (AnalysisValue m) -> EnvironmentFor (AnalysisValue m)) -> m a -> m a
 
   -- | Retrieve the heap.
-  getStore :: m (StoreFor value)
+  getStore :: m (StoreFor (AnalysisValue m))
   -- | Update the heap.
-  modifyStore :: (StoreFor value -> StoreFor value) -> m ()
+  modifyStore :: (StoreFor (AnalysisValue m) -> StoreFor (AnalysisValue m)) -> m ()
 
   -- | Retrieve the table of evaluated modules.
-  getModuleTable :: m (Linker value)
+  getModuleTable :: m (Linker (AnalysisValue m))
   -- | Update the table of evaluated modules.
-  modifyModuleTable :: (Linker value -> Linker value) -> m ()
+  modifyModuleTable :: (Linker (AnalysisValue m) -> Linker (AnalysisValue m)) -> m ()
 
   -- | Retrieve the table of unevaluated modules.
-  askModuleTable :: m (Linker term)
+  askModuleTable :: m (Linker (AnalysisTerm m))
   -- | Run an action with a locally-modified table of unevaluated modules.
-  localModuleTable :: (Linker term -> Linker term) -> m a -> m a
+  localModuleTable :: (Linker (AnalysisTerm m) -> Linker (AnalysisTerm m)) -> m a -> m a
 
   -- | Retrieve the current root set.
-  askRoots :: Ord (LocationFor value) => m (Live (LocationFor value) value)
+  askRoots :: m (Live (LocationFor (AnalysisValue m)) (AnalysisValue m))
   askRoots = pure mempty
 
   -- | Get the current 'Configuration' with a passed-in term.
-  getConfiguration :: Ord (LocationFor value) => term -> m (Configuration (LocationFor value) term value)
+  getConfiguration :: term -> m (Configuration (LocationFor (AnalysisValue m)) term (AnalysisValue m))
   getConfiguration term = Configuration term <$> askRoots <*> askLocalEnv <*> getStore
 
 type EvaluatorEffects term value
@@ -64,7 +61,9 @@ type EvaluatorEffects term value
      , State  (Linker value)         -- Cache of evaluated modules
      ]
 
-instance Members (EvaluatorEffects term value) effects => MonadEvaluator term value (Evaluator term value effects) where
+type instance AnalysisTerm (Evaluator term value effects) = term
+type instance AnalysisValue (Evaluator term value effects) = value
+instance (Ord (LocationFor value), Members (EvaluatorEffects term value) effects) => MonadEvaluator (Evaluator term value effects) where
   getGlobalEnv = Evaluator get
   modifyGlobalEnv f = Evaluator (modify f)
 
@@ -80,7 +79,7 @@ instance Members (EvaluatorEffects term value) effects => MonadEvaluator term va
   askModuleTable = Evaluator ask
   localModuleTable f a = Evaluator (local f (runEvaluator a))
 
-putStore :: MonadEvaluator t value m => StoreFor value -> m ()
+putStore :: MonadEvaluator m => StoreFor (AnalysisValue m) -> m ()
 putStore = modifyStore . const
 
 -- | An evaluator of @term@s to @value@s, producing incremental results of type @a@ using a list of @effects@.

src/Control/Abstract/Value.hs

@@ -1,4 +1,4 @@
-{-# LANGUAGE MultiParamTypeClasses, UndecidableInstances #-}
+{-# LANGUAGE MultiParamTypeClasses, TypeFamilies, UndecidableInstances #-}
 module Control.Abstract.Value where
 
 import Control.Abstract.Addressable
@@ -16,7 +16,7 @@ import Prelude hiding (fail)
 -- | A 'Monad' abstracting the evaluation of (and under) binding constructs (functions, methods, etc).
 --
 --   This allows us to abstract the choice of whether to evaluate under binders for different value types.
-class (MonadEvaluator t v m) => MonadValue t v m where
+class (MonadEvaluator m, v ~ AnalysisValue m) => MonadValue v m where
   -- | Construct an abstract unit value.
   unit :: m v
 
@@ -33,19 +33,21 @@ class (MonadEvaluator t v m) => MonadValue t v m where
   ifthenelse :: v -> m v -> m v -> m v
 
   -- | Evaluate an abstraction (a binder like a lambda or method definition).
-  abstract :: [Name] -> Subterm t (m v) -> m v
+  abstract :: [Name] -> Subterm (AnalysisTerm m) (m v) -> m v
   -- | Evaluate an application (like a function call).
-  apply :: v -> [Subterm t (m v)] -> m v
+  apply :: v -> [Subterm (AnalysisTerm m) (m v)] -> m v
 
 -- | Construct a 'Value' wrapping the value arguments (if any).
 instance ( FreeVariables t
-         , MonadAddressable location (Value location t) m
+         , MonadAddressable location m
-         , MonadAnalysis t (Value location t) m
+         , MonadAnalysis m
-         , MonadEvaluator t (Value location t) m
+         , AnalysisTerm m ~ t
+         , AnalysisValue m ~ Value location t
+         , MonadEvaluator m
          , Recursive t
          , Semigroup (Cell location (Value location t))
          )
-         => MonadValue t (Value location t) m where
+         => MonadValue (Value location t) m where
 
   unit    = pure $ inj Value.Unit
   integer = pure . inj . Integer
@@ -68,7 +70,7 @@ instance ( FreeVariables t
     localEnv (mappend bindings) (evaluateTerm body)
 
 -- | Discard the value arguments (if any), constructing a 'Type.Type' instead.
-instance (Alternative m, MonadEvaluator t Type m, MonadFresh m) => MonadValue t Type m where
+instance (Alternative m, MonadEvaluator m, MonadFresh m, AnalysisValue m ~ Type) => MonadValue Type m where
   abstract names (Subterm _ body) = do
     (env, tvars) <- foldr (\ name rest -> do
       a <- alloc name

src/Data/Abstract/Evaluatable.hs

@@ -1,4 +1,4 @@
-{-# LANGUAGE DefaultSignatures, FunctionalDependencies, UndecidableInstances #-}
+{-# LANGUAGE DefaultSignatures, FunctionalDependencies, TypeFamilies, UndecidableInstances #-}
 module Data.Abstract.Evaluatable
 ( Evaluatable(..)
 , module Addressable
@@ -30,10 +30,12 @@ import Prologue
 -- | The 'Evaluatable' class defines the necessary interface for a term to be evaluated. While a default definition of 'eval' is given, instances with computational content must implement 'eval' to perform their small-step operational semantics.
 class Evaluatable constr where
   eval :: ( FreeVariables term
-          , MonadAddressable (LocationFor value) value m
+          , MonadAddressable (LocationFor value) m
-          , MonadAnalysis term value m
+          , MonadAnalysis m
-          , MonadEvaluator term value m
+          , AnalysisTerm m ~ term
-          , MonadValue term value m
+          , AnalysisValue m ~ value
+          , MonadEvaluator m
+          , MonadValue value m
           , Ord (LocationFor value)
           , Semigroup (CellFor value)
           )
@@ -75,24 +77,24 @@ instance Evaluatable [] where
 -- | Require/import another term/file and return an Effect.
 --
 -- Looks up the term's name in the cache of evaluated modules first, returns a value if found, otherwise loads/evaluates the module.
-require :: ( FreeVariables term
+require :: ( FreeVariables (AnalysisTerm m)
-           , MonadAnalysis term v m
+           , MonadAnalysis m
-           , MonadEvaluator term v m
+           , MonadEvaluator m
            )
-        => term
+        => AnalysisTerm m
-        -> m v
+        -> m (AnalysisValue m)
 require term = getModuleTable >>= maybe (load term) pure . linkerLookup name
   where name = moduleName term
 
 -- | Load another term/file and return an Effect.
 --
 -- Always loads/evaluates.
-load :: ( FreeVariables term
+load :: ( FreeVariables (AnalysisTerm m)
-        , MonadAnalysis term v m
+        , MonadAnalysis m
-        , MonadEvaluator term v m
+        , MonadEvaluator m
         )
-     => term
+     => AnalysisTerm m
-     -> m v
+     -> m (AnalysisValue m)
 load term = askModuleTable >>= maybe notFound evalAndCache . linkerLookup name
   where name = moduleName term
         notFound = fail ("cannot find " <> show name)