diff --git a/src/BoolAlg.purs b/src/BoolAlg.purs
deleted file mode 100644
index f0479dd65..000000000
--- a/src/BoolAlg.purs
+++ /dev/null
@@ -1,68 +0,0 @@
-module BoolAlg where
-
-import Prelude
-
-import Ann (𝔹)
-import Control.Apply (lift2)
-import Control.Biapply (bilift2)
-import Data.Profunctor.Strong ((***))
-import Dict (lift2) as D
-import Data.Set (Set, intersection, union)
-import Data.Set (difference, empty) as S
-import Util (type (×), (×), Endo)
-import Val (Env)
-
--- Candidate replacement for Lattice.purs, using records rather than type classes as the latter are too
--- inflexible for the granularity of instande we require. Also flatten the hiearchy of types.
-type BoolAlg a =
-   { top :: a
-   , bot :: a
-   , meet :: a -> a -> a
-   , join :: a -> a -> a
-   , neg :: Endo a
-   }
-
-bool :: BoolAlg 𝔹
-bool =
-   { top: true
-   , bot: false
-   , meet: (&&)
-   , join: (||)
-   , neg: not
-   }
-
-powerset :: forall a. Ord a => Set a -> BoolAlg (Set a)
-powerset xs =
-   { top: xs
-   , bot: S.empty
-   , meet: intersection
-   , join: union
-   , neg: (xs `S.difference` _)
-   }
-
-slices :: forall f a b. Apply f => BoolAlg a -> f b -> BoolAlg (f a)
-slices 𝒶 x =
-   { top: x <#> const 𝒶.top
-   , bot: x <#> const 𝒶.bot
-   , meet: lift2 𝒶.meet
-   , join: lift2 𝒶.join
-   , neg: (_ <#> 𝒶.neg)
-   }
-
-prod :: forall a b. BoolAlg a -> BoolAlg b -> BoolAlg (a × b)
-prod 𝒶 𝒷 =
-   { top: 𝒶.top × 𝒷.top
-   , bot: 𝒶.bot × 𝒷.bot
-   , meet: 𝒶.meet `bilift2` 𝒷.meet
-   , join: 𝒶.join `bilift2` 𝒷.join
-   , neg: 𝒶.neg *** 𝒷.neg
-   }
-
-slicesγ :: forall a b. BoolAlg a -> Env b -> BoolAlg (Env a)
-slicesγ 𝒶 γ =
-   { top: (map $ const 𝒶.top) <$> γ
-   , bot: (map $ const 𝒶.bot) <$> γ
-   , meet: D.lift2 𝒶.meet
-   , join: D.lift2 𝒶.join
-   , neg: (_ <#> (_ <#> 𝒶.neg))
-   }
diff --git a/src/Desug.purs b/src/Desug.purs
index f3d005d09..440d92d76 100644
--- a/src/Desug.purs
+++ b/src/Desug.purs
@@ -1,25 +1,24 @@
 module Desug where
 
-import Desugarable (desug, desugBwd)
 import Prelude
+
 import Control.Monad.Error.Class (class MonadError)
+import Desugarable (desug, desugBwd)
 import Effect.Exception (Error)
 import Expr (Expr)
-import GaloisConnection (GaloisConnection)
-import Lattice (Raw, class BoundedJoinSemilattice)
+import GaloisConnection (GaloisConnection(..))
+import Lattice (class BoundedJoinSemilattice, Raw)
 import SExpr (Expr) as S
 import Util (successful)
 
-type DesugGaloisConnection a = GaloisConnection (S.Expr a) (Expr a) ()
-
 desugGC
    :: forall a m
     . MonadError Error m
    => BoundedJoinSemilattice a
    => Raw S.Expr
-   -> m (DesugGaloisConnection a)
+   -> m (GaloisConnection (S.Expr a) (Expr a))
 desugGC s0 = do
    let
       fwd s = successful $ desug s
       bwd e = desugBwd e s0
-   pure { fwd, bwd }
+   pure $ GC { fwd, bwd }
diff --git a/src/Desugarable2.purs b/src/Desugarable2.purs
deleted file mode 100644
index be7eeb46a..000000000
--- a/src/Desugarable2.purs
+++ /dev/null
@@ -1,12 +0,0 @@
-module Desugarable2 where
-
-import Prelude
-
-import Ann (Raw)
-import BoolAlg (BoolAlg)
-import Control.Monad.Error.Class (class MonadError)
-import Effect.Exception (Error)
-
-class (Functor s, Functor e) <= Desugarable s e | s -> e where
-   desug :: forall a m. MonadError Error m => BoolAlg a -> s a -> m (e a)
-   desugBwd :: forall a. BoolAlg a -> e a -> Raw s -> s a
diff --git a/src/Dict.purs b/src/Dict.purs
index 91c3fd70c..d53e118bd 100644
--- a/src/Dict.purs
+++ b/src/Dict.purs
@@ -38,14 +38,15 @@ import Util (Endo, type (×), (×), assert, definitely, error)
 
 type Dict a = O.Object a
 
+-- `Apply` instance would be an orphan
 apply :: forall a b. Dict (a -> b) -> Dict a -> Dict b
-apply d ds = intersectionWith ($) d ds
+apply = intersectionWith ($) -- why not require dicts to have same shape?
 
 apply2 :: forall f a b. Apply f => Dict (f (a -> b)) -> Dict (f a) -> Dict (f b)
-apply2 d ds = apply ((<*>) <$> d) ds
+apply2 d = apply ((<*>) <$> d)
 
 lift2 :: forall f a b c. Apply f => (a -> b -> c) -> Dict (f a) -> Dict (f b) -> Dict (f c)
-lift2 f d1 d2 = apply2 ((f <$> _) <$> d1) d2
+lift2 f d1 = apply2 ((f <$> _) <$> d1)
 
 -- Unfortunately Foreign.Object doesn't define this; could implement using Foreign.Object.ST instead.
 foreign import intersectionWith :: forall a b c. (a -> b -> c) -> Dict a -> Dict b -> Dict c
diff --git a/src/Eval2.purs b/src/Eval2.purs
deleted file mode 100644
index cfcaea23f..000000000
--- a/src/Eval2.purs
+++ /dev/null
@@ -1,176 +0,0 @@
-module Eval2 where
-
-import Prelude hiding (absurd, apply)
-
-import Ann (erase)
-import Bindings (varAnon)
-import BoolAlg (BoolAlg)
-import Control.Monad.Error.Class (class MonadError)
-import Data.Array (fromFoldable) as A
-import Data.Bifunctor (bimap)
-import Data.Either (Either(..))
-import Data.Exists (mkExists, runExists)
-import Data.List (List(..), (:), length, range, singleton, unzip, zip)
-import Data.Maybe (Maybe(..))
-import Data.Profunctor.Strong (first)
-import Data.Set (fromFoldable, toUnfoldable, singleton) as S
-import Data.Set (union, subset)
-import Data.Traversable (sequence, traverse)
-import Data.Tuple (fst, snd)
-import DataType (Ctr, arity, consistentWith, dataTypeFor, showCtr)
-import Dict (disjointUnion, get, empty, lookup, keys)
-import Dict (fromFoldable, singleton, unzip) as D
-import Effect.Exception (Error)
-import Expr (Cont(..), Elim(..), Expr(..), Module(..), RecDefs, VarDef(..), asExpr, fv)
-import Pretty2 (prettyP)
-import Primitive2 (intPair, string)
-import Trace2 (AppTrace(..), Trace(..), VarDef(..)) as T
-import Trace2 (AppTrace, ForeignTrace, ForeignTrace'(..), Match(..), Trace)
-import Util (type (×), absurd, both, check, error, orElse, successful, throw, with, (×))
-import Util.Pair (unzip) as P
-import Val2 (Fun(..), Val(..)) as V
-import Val2 (class Highlightable, DictRep(..), Env, ForeignOp'(..), MatrixRep(..), Val, for, lookup', restrict, (<+>))
-
-patternMismatch :: String -> String -> String
-patternMismatch s s' = "Pattern mismatch: found " <> s <> ", expected " <> s'
-
-match :: forall a m. MonadError Error m => Highlightable a => BoolAlg a -> Val a -> Elim a -> m (Env a × Cont a × a × Match)
-match 𝒶 v (ElimVar x κ)
-   | x == varAnon = pure (empty × κ × 𝒶.top × MatchVarAnon (erase v))
-   | otherwise = pure (D.singleton x v × κ × 𝒶.top × MatchVar x (erase v))
-match 𝒶 (V.Constr α c vs) (ElimConstr m) = do
-   with "Pattern mismatch" $ S.singleton c `consistentWith` keys m
-   κ <- lookup c m # orElse ("Incomplete patterns: no branch for " <> showCtr c)
-   γ × κ' × α' × ws <- matchMany 𝒶 vs κ
-   pure (γ × κ' × (α `𝒶.meet` α') × MatchConstr c ws)
-match _ v (ElimConstr m) = do
-   d <- dataTypeFor $ keys m
-   throw $ patternMismatch (prettyP v) (show d)
-match 𝒶 (V.Record α xvs) (ElimRecord xs κ) = do
-   check (subset xs (S.fromFoldable $ keys xvs)) $ patternMismatch (show (keys xvs)) (show xs)
-   let xs' = xs # S.toUnfoldable
-   γ × κ' × α' × ws <- matchMany 𝒶 (xs' <#> flip get xvs) κ
-   pure (γ × κ' × (α `𝒶.meet` α') × MatchRecord (D.fromFoldable (zip xs' ws)))
-match _ v (ElimRecord xs _) = throw $ patternMismatch (prettyP v) (show xs)
-
-matchMany :: forall a m. MonadError Error m => Highlightable a => BoolAlg a -> List (Val a) -> Cont a -> m (Env a × Cont a × a × List Match)
-matchMany 𝒶 Nil κ = pure (empty × κ × 𝒶.top × Nil)
-matchMany 𝒶 (v : vs) (ContElim σ) = do
-   γ × κ' × α × w <- match 𝒶 v σ
-   γ' × κ'' × β × ws <- matchMany 𝒶 vs κ'
-   pure $ γ `disjointUnion` γ' × κ'' × (α `𝒶.meet` β) × (w : ws)
-matchMany _ (_ : vs) (ContExpr _) = throw $
-   show (length vs + 1) <> " extra argument(s) to constructor/record; did you forget parentheses in lambda pattern?"
-matchMany _ _ _ = error absurd
-
-closeDefs :: forall a. Env a -> RecDefs a -> a -> Env a
-closeDefs γ ρ α = ρ <#> \σ ->
-   let ρ' = ρ `for` σ in V.Fun α $ V.Closure (γ `restrict` (fv ρ' `union` fv σ)) ρ' σ
-
-checkArity :: forall m. MonadError Error m => Ctr -> Int -> m Unit
-checkArity c n = do
-   n' <- arity c
-   check (n' >= n) (showCtr c <> " got " <> show n <> " argument(s), expects at most " <> show n')
-
-apply :: forall a m. MonadError Error m => Highlightable a => BoolAlg a -> Val a × Val a -> m (AppTrace × Val a)
-apply 𝒶 (V.Fun β (V.Closure γ1 ρ σ) × v) = do
-   let γ2 = closeDefs γ1 ρ β
-   γ3 × e'' × β' × w <- match 𝒶 v σ
-   t'' × v'' <- eval 𝒶 (γ1 <+> γ2 <+> γ3) (asExpr e'') (β `𝒶.meet` β')
-   pure $ T.AppClosure (S.fromFoldable (keys ρ)) w t'' × v''
-apply 𝒶 (V.Fun α (V.Foreign φ vs) × v) = do
-   t × v'' <- runExists apply' φ
-   pure $ T.AppForeign (length vs + 1) t × v''
-   where
-   vs' = vs <> singleton v
-
-   apply' :: forall t. ForeignOp' t -> m (ForeignTrace × Val _)
-   apply' (ForeignOp' φ') = do
-      t × v'' <- do
-         if φ'.arity > length vs' then pure $ Nothing × V.Fun α (V.Foreign φ vs')
-         else first Just <$> φ'.op 𝒶 vs'
-      pure $ mkExists (ForeignTrace' (ForeignOp' φ') t) × v''
-apply _ (V.Fun α (V.PartialConstr c vs) × v) = do
-   check (length vs < n) ("Too many arguments to " <> showCtr c)
-   pure $ T.AppConstr c × v'
-   where
-   n = successful (arity c)
-   v' =
-      if length vs < n - 1 then V.Fun α $ V.PartialConstr c (vs <> singleton v)
-      else V.Constr α c (vs <> singleton v)
-apply _ (_ × v) = throw $ "Found " <> prettyP v <> ", expected function"
-
-apply2 :: forall a m. MonadError Error m => Highlightable a => BoolAlg a -> Val a × Val a × Val a -> m ((AppTrace × AppTrace) × Val a)
-apply2 𝒶 (u1 × v1 × v2) = do
-   t1 × u2 <- apply 𝒶 (u1 × v1)
-   t2 × v <- apply 𝒶 (u2 × v2)
-   pure $ (t1 × t2) × v
-
-eval :: forall a m. MonadError Error m => Highlightable a => BoolAlg a -> Env a -> Expr a -> a -> m (Trace × Val a)
-eval _ γ (Var x) _ = (T.Var x × _) <$> lookup' x γ
-eval _ γ (Op op) _ = (T.Op op × _) <$> lookup' op γ
-eval 𝒶 _ (Int α n) α' = pure (T.Const × V.Int (α `𝒶.meet` α') n)
-eval 𝒶 _ (Float α n) α' = pure (T.Const × V.Float (α `𝒶.meet` α') n)
-eval 𝒶 _ (Str α str) α' = pure (T.Const × V.Str (α `𝒶.meet` α') str)
-eval 𝒶 γ (Record α xes) α' = do
-   xts × xvs <- traverse (flip (eval 𝒶 γ) α') xes <#> D.unzip
-   pure $ T.Record xts × V.Record (α `𝒶.meet` α') xvs
-eval 𝒶 γ (Dictionary α ees) α' = do
-   (ts × vs) × (ts' × us) <- traverse (traverse (flip (eval 𝒶 γ) α')) ees <#> (P.unzip >>> (unzip # both))
-   let
-      ss × αs = (vs <#> \u -> string.match u) # unzip
-      d = D.fromFoldable $ zip ss (zip αs us)
-   pure $ T.Dictionary (zip ss (zip ts ts')) (d <#> snd >>> erase) × V.Dictionary (α `𝒶.meet` α') (DictRep d)
-eval 𝒶 γ (Constr α c es) α' = do
-   checkArity c (length es)
-   ts × vs <- traverse (flip (eval 𝒶 γ) α') es <#> unzip
-   pure (T.Constr c ts × V.Constr (α `𝒶.meet` α') c vs)
-eval 𝒶 γ (Matrix α e (x × y) e') α' = do
-   t × v <- eval 𝒶 γ e' α'
-   let (i' × β) × (j' × β') = fst (intPair.match v)
-   check (i' × j' >= 1 × 1) ("array must be at least (" <> show (1 × 1) <> "); got (" <> show (i' × j') <> ")")
-   tss × vss <- unzipToArray <$> ((<$>) unzipToArray) <$>
-      ( sequence $ do
-           i <- range 1 i'
-           singleton $ sequence $ do
-              j <- range 1 j'
-              let γ' = D.singleton x (V.Int β i) `disjointUnion` (D.singleton y (V.Int β' j))
-              singleton (eval 𝒶 (γ <+> γ') e α')
-      )
-   pure $ T.Matrix tss (x × y) (i' × j') t × V.Matrix (α `𝒶.meet` α') (MatrixRep (vss × (i' × β) × (j' × β')))
-   where
-   unzipToArray :: forall b c. List (b × c) -> Array b × Array c
-   unzipToArray = unzip >>> bimap A.fromFoldable A.fromFoldable
-eval _ γ (Lambda σ) α =
-   pure $ T.Const × V.Fun α (V.Closure (γ `restrict` fv σ) empty σ)
-eval 𝒶 γ (Project e x) α = do
-   t × v <- eval 𝒶 γ e α
-   case v of
-      V.Record _ xvs -> (T.Project t x × _) <$> lookup' x xvs
-      _ -> throw $ "Found " <> prettyP v <> ", expected record"
-eval 𝒶 γ (App e e') α = do
-   t × v <- eval 𝒶 γ e α
-   t' × v' <- eval 𝒶 γ e' α
-   t'' × v'' <- apply 𝒶 (v × v')
-   pure $ T.App t t' t'' × v''
-eval 𝒶 γ (Let (VarDef σ e) e') α = do
-   t × v <- eval 𝒶 γ e α
-   γ' × _ × α' × w <- match 𝒶 v σ -- terminal meta-type of eliminator is meta-unit
-   t' × v' <- eval 𝒶 (γ <+> γ') e' α' -- (α ∧ α') for consistency with functions? (similarly for module defs)
-   pure $ T.Let (T.VarDef w t) t' × v'
-eval 𝒶 γ (LetRec ρ e) α = do
-   let γ' = closeDefs γ ρ α
-   t × v <- eval 𝒶 (γ <+> γ') e α
-   pure $ T.LetRec (erase <$> ρ) t × v
-
-eval_module :: forall a m. MonadError Error m => Highlightable a => BoolAlg a -> Env a -> Module a -> a -> m (Env a)
-eval_module 𝒶 γ = go empty
-   where
-   go :: Env a -> Module a -> a -> m (Env a)
-   go γ' (Module Nil) _ = pure γ'
-   go y' (Module (Left (VarDef σ e) : ds)) α = do
-      _ × v <- eval 𝒶 (γ <+> y') e α
-      γ'' × _ × α' × _ <- match 𝒶 v σ
-      go (y' <+> γ'') (Module ds) α'
-   go γ' (Module (Right ρ : ds)) α =
-      go (γ' <+> closeDefs (γ <+> γ') ρ α) (Module ds) α
diff --git a/src/EvalBwd.purs b/src/EvalBwd.purs
index 1b9b313be..d53ee8b1b 100644
--- a/src/EvalBwd.purs
+++ b/src/EvalBwd.purs
@@ -1,8 +1,6 @@
 module EvalBwd where
 
 import Prelude hiding (absurd)
-
-import BoolAlg (BoolAlg, slicesγ, slices, prod)
 import Bindings (Var, varAnon)
 import Control.Monad.Except (class MonadError, runExcept)
 import Data.Exists (mkExists, runExists)
@@ -22,7 +20,7 @@ import Dict (fromFoldable, singleton, toUnfoldable) as D
 import Effect.Exception (Error)
 import Eval (eval)
 import Expr (Cont(..), Elim(..), Expr(..), RecDefs, VarDef(..), bv)
-import GaloisConnection (GaloisConnection)
+import GaloisConnection (GaloisConnection(..))
 import Lattice (Raw, bot, botOf, expand, (∨))
 import Partial.Unsafe (unsafePartial)
 import Trace (AppTrace(..), Trace(..), VarDef(..)) as T
@@ -197,18 +195,15 @@ evalBwd' v (T.LetRec ρ t) =
    γ1' × ρ' × α' = closeDefsBwd γ2
 evalBwd' _ _ = error absurd
 
-type EvalGaloisConnection a = GaloisConnection (Env a × Expr a × a) (Val a)
-   ( dom :: BoolAlg (Env a × Expr a × a)
-   , codom :: BoolAlg (Val a)
+type TracedEval a =
+   { gc :: GaloisConnection (Env a × Expr a × a) (Val a)
    , v :: Raw Val
-   )
+   }
 
-traceGC :: forall a m. MonadError Error m => Ann a => BoolAlg a -> Raw Env -> Raw Expr -> m (EvalGaloisConnection a)
-traceGC 𝒶 γ e = do
+traceGC :: forall a m. MonadError Error m => Ann a => Raw Env -> Raw Expr -> m (TracedEval a)
+traceGC γ e = do
    t × v <- eval γ e bot
    let
-      dom = slicesγ 𝒶 γ `prod` (slices 𝒶 e `prod` 𝒶)
-      codom = slices 𝒶 v
       bwd v' = evalBwd γ e v' t
       fwd (γ' × e' × α) = snd $ fromRight $ runExcept $ eval γ' e' α
-   pure { dom, codom, v, fwd, bwd }
+   pure $ { gc: GC { fwd, bwd }, v }
diff --git a/src/EvalGraph.purs b/src/EvalGraph.purs
index d2dd155a2..a43965ed0 100644
--- a/src/EvalGraph.purs
+++ b/src/EvalGraph.purs
@@ -9,8 +9,6 @@ module EvalGraph
    ) where
 
 import Prelude hiding (apply, add)
-
-import BoolAlg (BoolAlg, powerset)
 import Bindings (varAnon)
 import Control.Monad.Error.Class (class MonadError)
 import Data.Array (range, singleton) as A
@@ -25,7 +23,7 @@ import DataType (checkArity, arity, consistentWith, dataTypeFor, showCtr)
 import Dict (disjointUnion, fromFoldable, empty, get, keys, lookup, singleton) as D
 import Effect.Exception (Error)
 import Expr (Cont(..), Elim(..), Expr(..), VarDef(..), RecDefs, Module(..), fv, asExpr)
-import GaloisConnection (GaloisConnection)
+import GaloisConnection (GaloisConnection(..))
 import Graph (class Graph, Vertex, sinks)
 import Graph (vertices) as G
 import Graph.GraphWriter (class MonadGraphAlloc, alloc, new, runWithGraphAllocT)
@@ -175,13 +173,13 @@ eval_module γ = go D.empty
       γ'' <- closeDefs (γ <+> γ') ρ αs
       go (γ' <+> γ'') (Module ds) αs
 
-type EvalGaloisConnection g = GaloisConnection (Set Vertex) (Set Vertex)
-   ( dom :: BoolAlg (Set Vertex)
-   , codom :: BoolAlg (Set Vertex)
+type GraphEval g =
+   { gc :: GaloisConnection (Set Vertex) (Set Vertex)
+   , γα :: Env Vertex
    , eα :: Expr Vertex
    , g :: g
    , vα :: Val Vertex
-   )
+   }
 
 graphGC
    :: forall g m
@@ -189,7 +187,7 @@ graphGC
    => Graph g
    => GraphConfig g
    -> Raw Expr
-   -> m (EvalGaloisConnection g)
+   -> m (GraphEval g)
 graphGC { g, n, γα } e = do
    (g' × _) × eα × vα <- do
       runWithGraphAllocT (g × n) $ do
@@ -197,9 +195,7 @@ graphGC { g, n, γα } e = do
          vα <- eval γα eα S.empty
          pure (eα × vα)
    let
-      dom = powerset (sinks g')
-      codom = powerset (vertices vα)
-      fwd αs = G.vertices (fwdSlice αs g') `intersection` vertices vα
       -- TODO: want (vertices eα `union` foldMap vertices γα) rather than sinks g' here?
+      fwd αs = G.vertices (fwdSlice αs g') `intersection` vertices vα
       bwd αs = G.vertices (bwdSlice αs g') `intersection` sinks g'
-   pure { dom, codom, eα, g: g', vα, fwd, bwd }
+   pure { gc: GC { fwd, bwd }, γα, eα, g: g', vα }
diff --git a/src/Expr.purs b/src/Expr.purs
index 0f66cffee..20342c3ae 100644
--- a/src/Expr.purs
+++ b/src/Expr.purs
@@ -135,15 +135,16 @@ derive instance Eq a => Eq (Elim a)
 derive instance Eq a => Eq (Cont a)
 
 instance Apply Expr where
-   apply (Var x) (Var _) = Var x
+   apply (Var x) (Var x') = Var (x ≜ x')
    apply (Op op) (Op _) = Op op
-   apply (Int fα n) (Int α _) = Int (fα α) n
-   apply (Float fα n) (Float α _) = Float (fα α) n
-   apply (Str fα s) (Str α _) = Str (fα α) s
+   apply (Int fα n) (Int α n') = Int (fα α) (n ≜ n')
+   apply (Float fα n) (Float α n') = Float (fα α) (n ≜ n')
+   apply (Str fα s) (Str α s') = Str (fα α) (s ≜ s')
    apply (Record fα fxvs) (Record α xvs) = Record (fα α) (D.apply2 fxvs xvs)
    apply (Dictionary fα fxvs) (Dictionary α xvs) = Dictionary (fα α) (zipWith (lift2 (<*>)) fxvs xvs)
-   apply (Constr fα c fes) (Constr α _ es) = Constr (fα α) c (zipWith (<*>) fes es)
-   apply (Matrix fα fe1 (x × y) fe2) (Matrix α e1 (_ × _) e2) = Matrix (fα α) (fe1 <*> e1) (x × y) (fe2 <*> e2)
+   apply (Constr fα c fes) (Constr α c' es) = Constr (fα α) (c ≜ c') (zipWith (<*>) fes es)
+   apply (Matrix fα fe1 (x × y) fe2) (Matrix α e1 (x' × y') e2) =
+      Matrix (fα α) (fe1 <*> e1) ((x ≜ x') × (y ≜ y')) (fe2 <*> e2)
    apply (Lambda fσ) (Lambda σ) = Lambda (fσ <*> σ)
    apply (Project fe x) (Project e _) = Project (fe <*> e) x
    apply (App fe1 fe2) (App e1 e2) = App (fe1 <*> e1) (fe2 <*> e2)
diff --git a/src/GaloisConnection.purs b/src/GaloisConnection.purs
index 37e89c157..4852541fb 100644
--- a/src/GaloisConnection.purs
+++ b/src/GaloisConnection.purs
@@ -2,20 +2,24 @@ module GaloisConnection where
 
 import Prelude
 
-import BoolAlg (BoolAlg)
+import Data.Newtype (class Newtype)
+import Lattice (class BooleanLattice, neg)
 import Util (Endo)
 
--- a and b are posets, but we don't enforce that here. Use record rather than type class so we can extend with
--- explicit value-level representation of index (e.g. graph or trace) for families of GCs.
-type GaloisConnection a b r =
-   { fwd :: a -> b
-   , bwd :: b -> a
-   | r
-   }
+newtype GaloisConnection a b = GC { fwd :: a -> b, bwd :: b -> a }
 
-deMorgan :: forall a b. BoolAlg a -> BoolAlg b -> Endo (a -> b)
-deMorgan 𝒶 𝒷 = (𝒶.neg >>> _) >>> (_ >>> 𝒷.neg)
+derive instance Newtype (GaloisConnection a b) _
+
+deMorgan :: forall a b. BooleanLattice a => BooleanLattice b => Endo (a -> b)
+deMorgan = (neg >>> _) >>> (_ >>> neg)
 
 -- Could unify deMorgan and dual but would need to reify notion of opposite category.
-dual :: forall a b r. BoolAlg a -> BoolAlg b -> GaloisConnection a b r -> GaloisConnection b a r
-dual 𝒶 𝒷 gc@{ fwd, bwd } = gc { fwd = deMorgan 𝒷 𝒶 bwd, bwd = deMorgan 𝒶 𝒷 fwd }
+dual :: forall a b. BooleanLattice a => BooleanLattice b => GaloisConnection a b -> GaloisConnection b a
+dual (GC { fwd, bwd }) = GC { fwd: deMorgan bwd, bwd: deMorgan fwd }
+
+instance Semigroupoid GaloisConnection where
+   compose (GC { fwd: fwd1, bwd: bwd1 }) (GC { fwd: fwd2, bwd: bwd2 }) =
+      GC { fwd: fwd1 <<< fwd2, bwd: bwd1 >>> bwd2 }
+
+instance Category GaloisConnection where
+   identity = GC { fwd: identity, bwd: identity }
diff --git a/src/Lattice.purs b/src/Lattice.purs
index 63f0715b4..c69a9a051 100644
--- a/src/Lattice.purs
+++ b/src/Lattice.purs
@@ -146,7 +146,7 @@ instance JoinSemilattice a => JoinSemilattice (Array a) where
 
 instance (BoundedJoinSemilattice a, BoundedMeetSemilattice a) => BoundedLattice a
 
--- To express as Expandable (t :: Type -> Type) requires functor composition..
+-- Expandable (t :: Type -> Type) requires functor composition..
 class Expandable t u | t -> u where
    expand :: t -> u -> t
 
diff --git a/src/Pretty2.purs b/src/Pretty2.purs
deleted file mode 100644
index c0b123046..000000000
--- a/src/Pretty2.purs
+++ /dev/null
@@ -1,461 +0,0 @@
-module Pretty2 (class Pretty, pretty, prettyP) where
-
-import Prelude hiding (absurd, between)
-
-import Bindings (Bind, key, val, Var, (↦))
-import Data.Array (foldl)
-import Data.Exists (runExists)
-import Data.Foldable (class Foldable)
-import Data.List (List(..), fromFoldable, null, uncons, (:))
-import Data.List.NonEmpty (NonEmptyList, groupBy, singleton, toList)
-import Data.Map (lookup)
-import Data.Maybe (Maybe(..))
-import Data.Profunctor.Choice ((|||))
-import Data.Profunctor.Strong (first)
-import Data.Set (Set, toUnfoldable) as S
-import Data.String (Pattern(..), Replacement(..), contains) as DS
-import Data.String (drop, replaceAll)
-import DataType (Ctr, cCons, cNil, cPair, showCtr)
-import Dict (Dict)
-import Dict (toUnfoldable) as D
-import Expr (Cont(..), Elim(..))
-import Expr (Expr(..), VarDef(..)) as E
-import Graph (Vertex(..))
-import Graph.GraphImpl (GraphImpl(..))
-import Parse (str)
-import Primitive.Parse (opDefs)
-import SExpr (Branch, Clause(..), Clauses(..), Expr(..), ListRest(..), ListRestPattern(..), Pattern(..), Qualifier(..), RecDefs, VarDef(..), VarDefs)
-import Util (type (+), type (×), Endo, absurd, assert, error, intersperse, (×))
-import Util.Pair (Pair(..), toTuple)
-import Util.Pretty (Doc(..), atop, beside, empty, hcat, render, text)
-import Val2 (Fun(..), Val(..)) as V
-import Val2 (class Highlightable, DictRep(..), ForeignOp', Fun, MatrixRep(..), Val, highlightIf)
-
-replacement :: Array (String × String)
-replacement =
-   [ "( " × "("
-   , " )" × ")"
-   , "[ " × "["
-   , " ]" × "]"
-   , "{ " × "{"
-   , " }" × "}"
-   , ". " × "."
-   , " ." × "."
-   , ". " × "."
-   , " ," × ","
-   , " ;" × ";"
-   , "| " × "|"
-   , " |" × "|"
-   , "⸨ " × "⸨"
-   , " ⸩" × "⸩"
-   ]
-
-pattRepPairs :: Array (DS.Pattern × DS.Replacement)
-pattRepPairs = map (\(x × y) -> (DS.Pattern x × DS.Replacement y)) replacement
-
-newtype FirstGroup a = First (RecDefs a)
-data ExprType = Simple | Expression
-type Sep = Doc -> Doc -> Doc
-
-exprType :: forall a. Expr a -> ExprType
-exprType (Var _) = Simple
-exprType (Op _) = Simple
-exprType (Int _ _) = Simple
-exprType (Float _ _) = Simple
-exprType (Str _ _) = Simple
-exprType (Constr _ _ Nil) = Simple
-exprType (Constr _ _ _) = Expression
-exprType (Record _ _) = Simple
-exprType (Dictionary _ _) = Simple
-exprType (Matrix _ _ _ _) = Simple
-exprType (Lambda _) = Simple
-exprType (Project _ _) = Simple
-exprType (App _ _) = Expression
-exprType (BinaryApp _ _ _) = Expression
-exprType (MatchAs _ _) = Simple
-exprType (IfElse _ _ _) = Simple
-exprType (ListEmpty _) = Simple -- try
-exprType (ListNonEmpty _ _ _) = Simple
-exprType (ListEnum _ _) = Simple
-exprType (ListComp _ _ _) = Simple
-exprType (Let _ _) = Expression
-exprType (LetRec _ _) = Expression
-
-prettySimple :: forall a. Highlightable a => Expr a -> Doc
-prettySimple s = case exprType s of
-   Simple -> pretty s
-   Expression -> parentheses (pretty s)
-
-prettyAppChain :: forall a. Highlightable a => Expr a -> Doc
-prettyAppChain (App s s') = prettyAppChain s .<>. prettySimple s'
-prettyAppChain s = prettySimple s
-
-prettyBinApp :: forall a. Highlightable a => Int -> Expr a -> Doc
-prettyBinApp n (BinaryApp s op s') =
-   let
-      prec' = getPrec op
-   in
-      case getPrec op of
-         -1 -> prettyBinApp prec' s .<>. (text ("`" <> op <> "`")) .<>. prettyBinApp prec' s'
-         _ ->
-            if prec' <= n then
-               parentheses (prettyBinApp prec' s .<>. text op .<>. prettyBinApp prec' s')
-            else
-               prettyBinApp prec' s .<>. text op .<>. prettyBinApp prec' s'
-prettyBinApp _ s = prettyAppChain s
-
-getPrec :: String -> Int
-getPrec x = case lookup x opDefs of
-   Just y -> y.prec
-   Nothing -> -1
-
-infixl 5 beside as .<>.
--- infixl 5 space as .<>.
-infixl 5 atop as .-.
-
-class Pretty p where
-   pretty :: p -> Doc
-
-removeLineWS :: String -> String
-removeLineWS str = foldl (\curr (x × y) -> replaceAll x y curr) str pattRepPairs
-
-removeDocWS :: Doc -> Doc
-removeDocWS (Doc d) = Doc
-   { width: d.width
-   , height: d.height
-   , lines: map (\x -> removeLineWS (drop 1 x)) d.lines
-   }
-
-instance Highlightable a => Pretty (Expr a) where
-   pretty (Var x) = text x
-   pretty (Op op) = parentheses (text op)
-   pretty (Int ann n) = (highlightIf ann $ text (show n))
-   pretty (Float ann n) = (highlightIf ann $ text (show n))
-   pretty (Str ann str) = (highlightIf ann $ (text ("\"" <> str <> "\"")))
-   pretty (Constr ann c x) = (prettyConstr ann c x)
-   pretty (Record ann xss) = (highlightIf ann $ curlyBraces (prettyOperator (.-.) xss))
-   pretty (Dictionary ann sss) = (highlightIf ann $ dictBrackets (pretty sss))
-   pretty (Matrix ann e (x × y) e') =
-      highlightIf ann $ arrayBrackets
-         ( pretty e .<>. text str.bar .<>. parentheses (text x .<>. text str.comma .<>. text y)
-              .<>. text str.in_
-              .<>. pretty e'
-         )
-   pretty (Lambda cs) = parentheses (text str.fun .<>. pretty cs)
-   pretty (Project s x) = pretty s .<>. text str.dot .<>. text x
-   pretty (App s s') = prettyAppChain (App s s')
-   pretty (BinaryApp s op s') = prettyBinApp 0 (BinaryApp s op s')
-   pretty (MatchAs s cs) = ((text str.match .<>. pretty s .<>. text str.as)) .-. curlyBraces (pretty cs)
-   pretty (IfElse s1 s2 s3) = text str.if_ .<>. pretty s1 .<>. text str.then_ .<>. pretty s2 .<>. text str.else_ .<>. pretty s3
-   pretty (ListEmpty ann) = (highlightIf ann $ brackets empty)
-   pretty (ListNonEmpty ann (Record _ xss) l) =
-      (((highlightIf ann $ text str.lBracket)) .<>. ((highlightIf ann $ curlyBraces (prettyOperator (.<>.) xss)))) .-. pretty l
-   pretty (ListNonEmpty ann e l) = ((highlightIf ann $ text str.lBracket)) .<>. pretty e .<>. pretty l
-   pretty (ListEnum s s') = brackets (pretty s .<>. text str.ellipsis .<>. pretty s')
-   pretty (ListComp ann s qs) = (highlightIf ann $ brackets (pretty s .<>. text str.bar .<>. pretty qs))
-   pretty (Let ds s) = (text str.let_ .<>. pretty ds .<>. text str.in_) .-. pretty s
-   pretty (LetRec h s) = (text str.let_ .<>. pretty (First h) .<>. text str.in_) .-. pretty s
-
-prettyOperator :: forall a. Highlightable a => (Doc -> Doc -> Doc) -> List (Bind (Expr a)) -> Doc
-prettyOperator _ (Cons s Nil) = text (key s) .<>. text str.colon .<>. pretty (val s)
-prettyOperator sep (Cons s xss) = sep (prettyOperator sep (toList (singleton s)) .<>. text str.comma) (prettyOperator sep xss)
-prettyOperator _ Nil = empty
-
-instance Highlightable a => Pretty (ListRest a) where
-   pretty (Next ann (Record _ xss) l) = ((highlightIf ann $ text str.comma)) .<>. ((highlightIf ann $ curlyBraces (prettyOperator (.<>.) xss))) .-. pretty l
-   pretty (Next ann s l) = ((highlightIf ann $ text str.comma)) .<>. pretty s .<>. pretty l
-   pretty (End ann) = (highlightIf ann $ text str.rBracket)
-
-instance Highlightable a => Pretty (List (Pair (Expr a))) where
-   pretty (Cons (Pair e e') Nil) = prettyPairs (Pair e e')
-   pretty (Cons (Pair e e') sss) = prettyPairs (Pair e e') .<>. text str.comma .<>. pretty sss
-   pretty Nil = empty
-
-prettyPairs :: forall a. Highlightable a => (Pair (Expr a)) -> Doc
-prettyPairs (Pair e e') = pretty e .<>. text str.colonEq .<>. pretty e'
-
-instance Pretty Pattern where
-   pretty (PVar x) = text x
-   pretty (PRecord xps) = curlyBraces (pretty xps)
-   pretty (PConstr c ps) = case uncons ps of
-      Just { head: p, tail: Nil } -> pretty c .<>. pretty p
-      _ ->
-         if c == cPair then (parentheses (prettyPattConstr (text str.comma) ps))
-         else if c == cCons then (parentheses (prettyPattConstr (text str.colon) ps))
-         else
-            parentheses (text c .<>. prettyPattConstr empty ps)
-
-   --pretty (PConstr c ps) = if c == cPair then parentheses (prettyPattConstr (text str.comma) ps)
-   --    if case uncons ps of
-   --       Nothing -> pretty ps
-   --    --    Just {head : p, tail: Nil} -> text c .<>. pretty p
-   --    --    _ -> parentheses (text c .<>. prettyPattConstr empty ps)
-   pretty (PListEmpty) = brackets empty
-   pretty (PListNonEmpty p l) = text str.lBracket .<>. pretty p .<>. pretty l
-
-instance Pretty (List (Bind Pattern)) where
-   pretty (Cons xp Nil) = text (key xp) .<>. text str.colon .<>. pretty (val xp)
-   pretty (Cons xp xps) = text (key xp) .<>. text str.colon .<>. pretty (val xp) .<>. text str.comma .-. pretty xps
-   pretty Nil = empty
-
-prettyPattConstr :: Doc -> List Pattern -> Doc
-prettyPattConstr _ Nil = empty
-prettyPattConstr _ (Cons p Nil) = pretty p
-prettyPattConstr sep (Cons p ps) = pretty p .<>. sep .<>. prettyPattConstr sep ps
-
-instance Pretty ListRestPattern where
-   pretty (PNext p l) = text str.comma .<>. pretty p .<>. pretty l
-   pretty PEnd = text str.rBracket
-
-prettyClause :: forall a. Highlightable a => Doc -> Clause a -> Doc
-prettyClause sep (Clause (ps × e)) = prettyPattConstr empty (toList ps) .<>. sep .<>. pretty e
-
-instance Highlightable a => Pretty (Clauses a) where
-   pretty (Clauses cs) = intersperse' (toList (map (prettyClause (text str.equals)) (cs))) (text str.semiColon)
-
-instance Highlightable a => Pretty (Branch a) where
-   pretty (x × Clause (ps × e)) = text x .<>. prettyClause (text str.equals) (Clause (ps × e))
-
-instance Highlightable a => Pretty (NonEmptyList (Branch a)) where
-   pretty h = intersperse' (toList (map pretty h)) (text str.semiColon)
-
-instance Highlightable a => Pretty (NonEmptyList (NonEmptyList (Branch a))) where
-   pretty hs = intersperse' (toList (map pretty hs)) (text str.semiColon)
-
-instance Highlightable a => Pretty (FirstGroup a) where
-   pretty (First h) = pretty (groupBy (\p q -> key p == key q) h)
-
-instance Highlightable a => Pretty (NonEmptyList (Pattern × Expr a)) where
-   pretty pss = intersperse' (map (prettyClause (text str.rArrow)) (map Clause (toList (helperMatch pss)))) (text str.semiColon)
-
-instance Highlightable a => Pretty (VarDef a) where
-   pretty (VarDef p s) = pretty p .<>. text str.equals .<>. pretty s
-
-instance Highlightable a => Pretty (VarDefs a) where
-   pretty ds = intersperse' (toList (map pretty ds)) (text str.semiColon)
-
-instance Highlightable a => Pretty (List (Expr a)) where
-   pretty (Cons s Nil) = pretty s
-   pretty (Cons s ss) = pretty s .<>. pretty ss
-   pretty Nil = empty
-
-instance Highlightable a => Pretty (List (Qualifier a)) where
-   pretty (Cons (Guard s) Nil) = pretty s
-   pretty (Cons (Declaration d) Nil) = text str.let_ .<>. pretty d
-   pretty (Cons (Generator p s) Nil) = pretty p .<>. text str.lArrow .<>. pretty s
-   pretty (Cons q qs) = pretty (toList (singleton q)) .<>. text str.comma .<>. pretty qs
-   pretty Nil = empty
-
-intersperse' :: List Doc -> Doc -> Doc
-intersperse' (Cons dc Nil) _ = dc
-intersperse' (Cons dc dcs) dc' = dc .<>. dc' .-. intersperse' dcs dc'
-intersperse' Nil _ = empty
-
-helperMatch :: forall a. NonEmptyList (Pattern × Expr a) -> NonEmptyList (NonEmptyList Pattern × Expr a)
-helperMatch pss = map (\(x × y) -> singleton x × y) pss
-
-prettyP :: forall d. Pretty d => d -> String
-prettyP x = render (removeDocWS (pretty x))
-
-between :: Doc -> Doc -> Endo Doc
-between l r doc = l .<>. doc .<>. r
-
-brackets :: Endo Doc
-brackets = between (text str.lBracket) (text str.rBracket)
-
-dictBrackets :: Endo Doc
-dictBrackets = between (text str.dictLBracket) (text str.dictRBracket)
-
-parentheses :: Endo Doc
-parentheses = between (text str.lparenth) (text str.rparenth)
-
--- slashes :: Endo Doc
--- slashes = between (text str.slash) (text str.slash)
-
--- backTicks :: Endo Doc
--- backTicks = between (text str.backtick) (text str.backtick)
-
-curlyBraces :: Endo Doc
-curlyBraces = between (text str.curlylBrace) (text str.curlyrBrace)
-
-arrayBrackets :: Endo Doc
-arrayBrackets = between (text str.arrayLBracket) (text str.arrayRBracket)
-
-comma :: Doc
-comma = text str.comma
-
-semi :: Doc
-semi = text str.semiColon
-
-hcomma :: forall f. Foldable f => f Doc -> Doc
-hcomma = fromFoldable >>> intersperse comma >>> hcat
-
-parens :: Endo Doc
-parens = between (text "(") (text ")")
-
-class ToList a where
-   toList2 :: a -> List a
-
-class ToPair a where
-   toPair :: a -> a × a
-
-instance ToPair (E.Expr a) where
-   toPair (E.Constr _ c (e : e' : Nil)) | c == cPair = e × e'
-   toPair _ = error absurd
-
-instance ToPair (Val a) where
-   toPair (V.Constr _ c (v : v' : Nil)) | c == cPair = v × v'
-   toPair _ = error absurd
-
-instance Pretty String where
-   pretty = text
-
-vert :: forall f. Foldable f => Doc -> f Doc -> Doc
-vert delim = fromFoldable >>> vert'
-   where
-   vert' :: List Doc -> Doc
-   vert' Nil = empty
-   vert' (x : Nil) = x
-   vert' (x : y : xs) = atop (x .<>. delim) (vert' (y : xs))
-
-prettyCtr :: Ctr -> Doc
-prettyCtr = showCtr >>> text
-
--- Cheap hack; revisit.
-prettyParensOpt :: forall a. Pretty a => a -> Doc
-prettyParensOpt x =
-   if DS.contains (DS.Pattern " ") (render doc) then parens doc
-   else doc
-   where
-   doc = pretty x
-
-nil :: Doc
-nil = text (str.lBracket <> str.rBracket)
-
--- (highlightIf α $ parens (hcomma [ pretty x, pretty y ]))
---  (highlightIf ann $ text str.lBracket)
-prettyConstr :: forall d a. Pretty d => Highlightable a => a -> Ctr -> List d -> Doc
-prettyConstr α c (x : y : ys)
-   | c == cPair = assert (null ys) $ (highlightIf α $ parens (hcomma [ pretty x, pretty y ]))
-prettyConstr α c ys
-   | c == cNil = assert (null ys) $ (highlightIf α nil)
-prettyConstr α c (x : y : ys)
-   | c == cCons = assert (null ys) $ parens (hcat [ pretty x, (highlightIf α $ text str.colon), pretty y ])
-prettyConstr α c (x : Nil) = (highlightIf α (prettyCtr c .<>. pretty x))
-prettyConstr α c xs = hcat ((highlightIf α (prettyCtr c)) : (prettyParensOpt <$> xs))
-
-prettyRecordOrDict
-   :: forall d b a
-    . Pretty d
-   => Highlightable a
-   => Doc
-   -> Endo Doc
-   -> (b -> Doc)
-   -> a
-   -> List (b × d)
-   -> Doc
-prettyRecordOrDict sep bracify prettyKey α xvs =
-   xvs <#> first prettyKey <#> (\(x × v) -> hcat [ x .<>. sep, pretty v ])
-      # hcomma >>> bracify >>> highlightIf α
-
-prettyDict :: forall d b a. Pretty d => Highlightable a => (b -> Doc) -> a -> List (b × d) -> Doc
-prettyDict = between (text str.dictLBracket) (text str.dictRBracket) # prettyRecordOrDict (text str.colonEq)
-
-prettyRecord :: forall d b a. Pretty d => Highlightable a => (b -> Doc) -> a -> List (b × d) -> Doc
-prettyRecord = curlyBraces # prettyRecordOrDict (text str.colon)
-
-prettyMatrix :: forall a. Highlightable a => E.Expr a -> Var -> Var -> E.Expr a -> Doc
-prettyMatrix e1 i j e2 = arrayBrackets (pretty e1 .<>. text str.lArrow .<>. text (i <> "×" <> j) .<>. text str.in_ .<>. pretty e2)
-
-instance Highlightable a => Pretty (E.Expr a) where
-   pretty (E.Var x) = text x
-   pretty (E.Int α n) = (highlightIf α (text (show n)))
-   pretty (E.Float _ n) = text (show n)
-   pretty (E.Str _ str) = text (show str)
-   pretty (E.Record α xes) = prettyRecord text α (xes # D.toUnfoldable)
-   pretty (E.Dictionary α ees) = prettyDict pretty α (ees <#> toTuple)
-   pretty (E.Constr α c es) = prettyConstr α c es
-   pretty (E.Matrix α e1 (i × j) e2) = (highlightIf α (prettyMatrix e1 i j e2))
-   pretty (E.Lambda σ) = hcat [ text str.fun, pretty σ ]
-   pretty (E.Op op) = parens (text op)
-   pretty (E.Let (E.VarDef σ e) e') = atop (hcat [ text str.let_, pretty σ, text str.equals, pretty e, text str.in_ ])
-      (pretty e')
-   pretty (E.LetRec δ e) = atop (hcat [ text str.let_, pretty δ, text str.in_ ]) (pretty e)
-   pretty (E.Project e x) = pretty e .<>. text str.dot .<>. pretty x
-   pretty (E.App e e') = hcat [ pretty e, pretty e' ]
-
-instance Highlightable a => Pretty (Dict (Elim a)) where
-   pretty x = go (D.toUnfoldable x)
-      where
-      go :: List (Var × Elim a) -> Doc
-      go Nil = error absurd -- non-empty
-      go (xσ : Nil) = pretty xσ
-      go (xσ : δ) = atop (go δ .<>. semi) (pretty xσ)
-
-instance Highlightable a => Pretty (Dict (Val a)) where
-   pretty γ = brackets $ go (D.toUnfoldable γ)
-      where
-      go :: List (Var × Val a) -> Doc
-      go Nil = empty
-      go ((x × v) : rest) = parens (text x .<>. text str.comma .<>. pretty v) .<>. text str.comma .<>. go rest
-
-instance Pretty (Dict (S.Set Vertex)) where
-   pretty d = brackets $ go (D.toUnfoldable d)
-      where
-      go :: List (String × S.Set Vertex) -> Doc
-      go Nil = empty
-      go ((α × βs) : rest) = text α .<>. text " ↦ " .<>. pretty (βs :: S.Set Vertex) .<>. text str.comma .<>. go rest
-
-instance Highlightable a => Pretty (Bind (Elim a)) where
-   pretty (x ↦ σ) = hcat [ text x, text str.equals, pretty σ ]
-
-instance Highlightable a => Pretty (Cont a) where
-   pretty ContNone = empty
-   pretty (ContExpr e) = pretty e
-   pretty (ContElim σ) = pretty σ
-
-instance Highlightable a => Pretty (Ctr × Cont a) where
-   pretty (c × κ) = hcat [ text (showCtr c), text str.rArrow, pretty κ ]
-
-instance Highlightable a => Pretty (Elim a) where
-   pretty (ElimVar x κ) = hcat [ text x, text str.rArrow, pretty κ ]
-   pretty (ElimConstr κs) = hcomma (pretty <$> κs) -- looks dodgy
-   pretty (ElimRecord xs κ) = hcat [ curlyBraces $ hcomma (text <$> (S.toUnfoldable xs :: List String)), text str.rArrow, curlyBraces (pretty κ) ]
-
-instance Highlightable a => Pretty (Val a) where
-   pretty (V.Int α n) = (highlightIf α (text (show n)))
-   pretty (V.Float α n) = (highlightIf α (text (show n)))
-   pretty (V.Str α str) = (highlightIf α (text (show str)))
-   pretty (V.Record α xvs) = prettyRecord text α (xvs # D.toUnfoldable)
-   pretty (V.Dictionary α (DictRep svs)) = prettyDict
-      (\(s × β) -> highlightIf β (text (show s)))
-      α
-      (svs # D.toUnfoldable <#> \(s × (β × v)) -> (s × β) × v)
-   pretty (V.Constr α c vs) = prettyConstr α c vs
-   pretty (V.Matrix _ (MatrixRep (vss × _ × _))) = vert comma (((<$>) pretty >>> hcomma) <$> vss)
-   pretty (V.Fun α φ) = pretty (α × φ)
-
-instance Highlightable a => Pretty (a × Fun a) where
-   pretty (α × V.Closure _ _ _) = (highlightIf α $ text "<closure>")
-   pretty (_ × V.Foreign φ _) = runExists pretty φ
-   pretty (α × V.PartialConstr c vs) = prettyConstr α c vs
-
-instance Pretty (ForeignOp' t) where
-   pretty _ = text "<extern op>" -- TODO
-
-instance (Pretty a, Pretty b) => Pretty (a + b) where
-   pretty = pretty ||| pretty
-
-instance Pretty GraphImpl where
-   pretty (GraphImpl g) =
-      text "GraphImpl \n  " .<>.
-         atop
-            ( text "{\n" .<>.
-                 atop (text "OUT: " .<>. pretty g.out) (text "IN: " .<>. pretty g.in)
-            )
-            (text "}")
-
-instance Pretty (S.Set Vertex) where
-   pretty αs = curlyBraces (hcomma (text <<< unwrap <$> (S.toUnfoldable αs :: List Vertex)))
-      where
-      unwrap (Vertex α) = α
diff --git a/src/Primitive2.purs b/src/Primitive2.purs
deleted file mode 100644
index 8ca6ee5ec..000000000
--- a/src/Primitive2.purs
+++ /dev/null
@@ -1,311 +0,0 @@
-module Primitive2 where
-
-import Prelude hiding (absurd, apply, div, top)
-
-import Ann (Raw, erase)
-import BoolAlg (BoolAlg)
-import Data.Either (Either(..))
-import Data.Exists (mkExists)
-import Data.Int (toNumber)
-import Data.List (List(..), (:))
-import Data.Profunctor.Choice ((|||))
-import Data.Set (singleton, insert)
-import DataType (cFalse, cPair, cTrue)
-import Dict (Dict)
-import Graph.GraphWriter (new)
-import Partial.Unsafe (unsafePartial)
-import Pretty2 (prettyP)
-import Util (type (+), type (×), (×), error)
-import Val2 (class Highlightable, ForeignOp'(..), Fun(..), MatrixRep, OpBwd, OpFwd, OpGraph, Val(..))
-
--- Mediate between values of annotation type a and (potential) underlying datatype d, analogous to
--- pattern-matching and construction for data types. Wasn't able to make a typeclass version of this
--- work with the required higher-rank polymorphism.
-type ToFrom d a =
-   { constr :: d × a -> Val a
-   , constr_bwd :: Val a -> d × a -- equivalent to match (except at Val)
-   , match :: Val a -> d × a
-   }
-
-int :: forall a. ToFrom Int a
-int =
-   { constr: \(n × α) -> Int α n
-   , constr_bwd: match'
-   , match: match'
-   }
-   where
-   match' :: _
-   match' (Int α n) = n × α
-   match' v = error ("Int expected; got " <> prettyP (erase v))
-
-number :: forall a. ToFrom Number a
-number =
-   { constr: \(n × α) -> Float α n
-   , constr_bwd: match'
-   , match: match'
-   }
-   where
-   match' :: _
-   match' (Float α n) = n × α
-   match' v = error ("Float expected; got " <> prettyP (erase v))
-
-string :: forall a. ToFrom String a
-string =
-   { constr: \(str × α) -> Str α str
-   , constr_bwd: match'
-   , match: match'
-   }
-   where
-   match' :: _
-   match' (Str α str) = str × α
-   match' v = error ("Str expected; got " <> prettyP (erase v))
-
-intOrNumber :: forall a. ToFrom (Int + Number) a
-intOrNumber =
-   { constr: case _ of
-        Left n × α -> Int α n
-        Right n × α -> Float α n
-   , constr_bwd: match'
-   , match: match'
-   }
-   where
-   match' :: Val a -> (Int + Number) × a
-   match' (Int α n) = Left n × α
-   match' (Float α n) = Right n × α
-   match' v = error ("Int or Float expected; got " <> prettyP (erase v))
-
-intOrNumberOrString :: forall a. ToFrom (Int + Number + String) a
-intOrNumberOrString =
-   { constr: case _ of
-        Left n × α -> Int α n
-        Right (Left n) × α -> Float α n
-        Right (Right str) × α -> Str α str
-   , constr_bwd: match'
-   , match: match'
-   }
-   where
-   match' :: Val a -> (Int + Number + String) × a
-   match' (Int α n) = Left n × α
-   match' (Float α n) = Right (Left n) × α
-   match' (Str α str) = Right (Right str) × α
-   match' v = error ("Int, Float or Str expected; got " <> prettyP (erase v))
-
-intPair :: forall a. ToFrom ((Int × a) × (Int × a)) a
-intPair =
-   { constr: \((nβ × mβ') × α) -> Constr α cPair (int.constr nβ : int.constr mβ' : Nil)
-   , constr_bwd: match'
-   , match: match'
-   }
-   where
-   match' :: Val a -> ((Int × a) × (Int × a)) × a
-   match' (Constr α c (v : v' : Nil)) | c == cPair = (int.match v × int.match v') × α
-   match' v = error ("Pair expected; got " <> prettyP (erase v))
-
-matrixRep :: forall a. Highlightable a => ToFrom (MatrixRep a) a
-matrixRep =
-   { constr: \(m × α) -> Matrix α m
-   , constr_bwd: match'
-   , match: match'
-   }
-   where
-   match' :: Highlightable a => Val a -> MatrixRep a × a
-   match' (Matrix α m) = m × α
-   match' v = error ("Matrix expected; got " <> prettyP v)
-
-record :: forall a. Highlightable a => ToFrom (Dict (Val a)) a
-record =
-   { constr: \(xvs × α) -> Record α xvs
-   , constr_bwd: match'
-   , match: match'
-   }
-   where
-   match' :: Highlightable a => _
-   match' (Record α xvs) = xvs × α
-   match' v = error ("Record expected; got " <> prettyP v)
-
-boolean :: forall a. ToFrom Boolean a
-boolean =
-   { constr: case _ of
-        true × α -> Constr α cTrue Nil
-        false × α -> Constr α cFalse Nil
-   , constr_bwd: match'
-   , match: match'
-   }
-   where
-   match' :: Val a -> Boolean × a
-   match' (Constr α c Nil)
-      | c == cTrue = true × α
-      | c == cFalse = false × α
-   match' v = error ("Boolean expected; got " <> prettyP (erase v))
-
-class IsZero a where
-   isZero :: a -> Boolean
-
-instance IsZero Int where
-   isZero = ((==) 0)
-
-instance IsZero Number where
-   isZero = ((==) 0.0)
-
-instance (IsZero a, IsZero b) => IsZero (a + b) where
-   isZero = isZero ||| isZero
-
--- Need to be careful about type variables escaping higher-rank quantification.
-type Unary i o a =
-   { i :: ToFrom i a
-   , o :: ToFrom o a
-   , fwd :: i -> o
-   }
-
-type Binary i1 i2 o a =
-   { i1 :: ToFrom i1 a
-   , i2 :: ToFrom i2 a
-   , o :: ToFrom o a
-   , fwd :: i1 -> i2 -> o
-   }
-
-type BinaryZero i o a =
-   { i :: ToFrom i a
-   , o :: ToFrom o a
-   , fwd :: i -> i -> o
-   }
-
-unary :: forall i o a'. BoolAlg a' -> (forall a. Unary i o a) -> Val a'
-unary 𝒶 op =
-   Fun 𝒶.bot $ flip Foreign Nil
-      $ mkExists
-      $ ForeignOp' { arity: 1, op': unsafePartial op', op: unsafePartial fwd, op_bwd: unsafePartial bwd }
-   where
-   op' :: Partial => OpGraph
-   op' (v : Nil) =
-      op.o.constr <$> ((op.fwd x × _) <$> new (singleton α))
-      where
-      x × α = op.i.match v
-
-   fwd :: Partial => OpFwd (Raw Val)
-   fwd _ (v : Nil) = pure $ erase v × op.o.constr (op.fwd x × α)
-      where
-      x × α = op.i.match v
-
-   bwd :: Partial => OpBwd (Raw Val)
-   bwd _ (u × v) = op.i.constr (x × α) : Nil
-      where
-      _ × α = op.o.constr_bwd v
-      (x × _) = op.i.match u
-
-binary :: forall i1 i2 o a'. BoolAlg a' -> (forall a. Binary i1 i2 o a) -> Val a'
-binary 𝒶 op =
-   Fun 𝒶.bot $ flip Foreign Nil
-      $ mkExists
-      $ ForeignOp' { arity: 2, op': unsafePartial op', op: unsafePartial fwd, op_bwd: unsafePartial bwd }
-   where
-   op' :: Partial => OpGraph
-   op' (v1 : v2 : Nil) =
-      op.o.constr <$> ((op.fwd x y × _) <$> new (singleton α # insert β))
-      where
-      (x × α) × (y × β) = op.i1.match v1 × op.i2.match v2
-
-   fwd :: Partial => OpFwd (Raw Val × Raw Val)
-   fwd 𝒶' (v1 : v2 : Nil) = pure $ (erase v1 × erase v2) × op.o.constr (op.fwd x y × (α `𝒶'.meet` β))
-      where
-      (x × α) × (y × β) = op.i1.match v1 × op.i2.match v2
-
-   bwd :: Partial => OpBwd (Raw Val × Raw Val)
-   bwd _ ((u1 × u2) × v) = op.i1.constr (x × α) : op.i2.constr (y × α) : Nil
-      where
-      _ × α = op.o.constr_bwd v
-      (x × _) × (y × _) = op.i1.match u1 × op.i2.match u2
-
--- If both are zero, depend only on the first.
-binaryZero :: forall i o a'. BoolAlg a' -> IsZero i => (forall a. BinaryZero i o a) -> Val a'
-binaryZero 𝒶 op =
-   Fun 𝒶.bot $ flip Foreign Nil
-      $ mkExists
-      $ ForeignOp' { arity: 2, op': unsafePartial op', op: unsafePartial fwd, op_bwd: unsafePartial bwd }
-   where
-   op' :: Partial => OpGraph
-   op' (v1 : v2 : Nil) =
-      let
-         αs =
-            if isZero x then singleton α
-            else if isZero y then singleton β
-            else singleton α # insert β
-      in
-         op.o.constr <$> ((op.fwd x y × _) <$> new αs)
-      where
-      (x × α) × (y × β) = op.i.match v1 × op.i.match v2
-
-   fwd :: Partial => OpFwd (Raw Val × Raw Val)
-   fwd 𝒶' (v1 : v2 : Nil) =
-      pure $ (erase v1 × erase v2) ×
-         op.o.constr (op.fwd x y × if isZero x then α else if isZero y then β else α `𝒶'.meet` β)
-      where
-      (x × α) × (y × β) = op.i.match v1 × op.i.match v2
-
-   bwd :: Partial => OpBwd (Raw Val × Raw Val)
-   bwd 𝒶' ((u1 × u2) × v) = op.i.constr (x × β1) : op.i.constr (y × β2) : Nil
-      where
-      _ × α = op.o.constr_bwd v
-      (x × _) × (y × _) = op.i.match u1 × op.i.match u2
-      β1 × β2 =
-         if isZero x then α × 𝒶'.bot
-         else if isZero y then 𝒶'.bot × α
-         else α × α
-
-class As a b where
-   as :: a -> b
-
-union1 :: forall a1 b. (a1 -> b) -> (Number -> b) -> a1 + Number -> b
-union1 f _ (Left x) = f x
-union1 _ g (Right x) = g x
-
--- Biased towards g: if arguments are of mixed types, we try to coerce to an application of g.
-union
-   :: forall a1 b1 c1 a2 b2 c2 c
-    . As c1 c
-   => As c2 c
-   => As a1 a2
-   => As b1 b2
-   => (a1 -> b1 -> c1)
-   -> (a2 -> b2 -> c2)
-   -> a1 + a2
-   -> b1 + b2
-   -> c
-union f _ (Left x) (Left y) = as (f x y)
-union _ g (Left x) (Right y) = as (g (as x) y)
-union _ g (Right x) (Right y) = as (g x y)
-union _ g (Right x) (Left y) = as (g x (as y))
-
--- Helper to avoid some explicit type annotations when defining primitives.
-unionStr
-   :: forall a b
-    . As a a
-   => As b String
-   => (b -> b -> a)
-   -> (String -> String -> a)
-   -> b + String
-   -> b + String
-   -> a
-unionStr = union
-
-instance asIntIntOrNumber :: As Int (Int + a) where
-   as = Left
-
-instance asNumberIntOrNumber :: As Number (a + Number) where
-   as = Right
-
-instance asIntNumber :: As Int Number where
-   as = toNumber
-
-instance asBooleanBoolean :: As Boolean Boolean where
-   as = identity
-
-instance asNumberString :: As Number String where
-   as _ = error "Non-uniform argument types"
-
-instance asIntNumberOrString :: As Int (Number + a) where
-   as = toNumber >>> Left
-
-instance asIntorNumberNumber :: As (Int + Number) Number where
-   as (Left n) = as n
-   as (Right n) = n
\ No newline at end of file
diff --git a/src/SExpr.purs b/src/SExpr.purs
index 47e9bf737..63ce20df0 100644
--- a/src/SExpr.purs
+++ b/src/SExpr.purs
@@ -326,19 +326,6 @@ listCompBwd (E.App (E.App (E.Var "concatMap") (E.Lambda σ)) e) ((Generator p s0
          α × qs' × s' -> (α ∨ β) × (Generator p (desugBwd e s0) : qs') × s'
 listCompBwd _ _ = error absurd
 
--- NonEmptyList Pattern × Expr
-pattsExprFwd :: forall a m. MonadError Error m => JoinSemilattice a => NonEmptyList Pattern × Expr a -> m (Elim a)
-pattsExprFwd (NonEmptyList (p :| Nil) × s) = (ContExpr <$> desug s) >>= pattContFwd p
-pattsExprFwd (NonEmptyList (p :| p' : ps) × s) =
-   pattContFwd p =<< ContExpr <$> E.Lambda <$> pattsExprFwd (NonEmptyList (p' :| ps) × s)
-
-pattsExprBwd :: forall a. BoundedJoinSemilattice a => NonEmptyList Pattern × Raw Expr -> Elim a -> Expr a
-pattsExprBwd (NonEmptyList (p :| Nil) × s) σ = desugBwd (asExpr (pattContBwd p σ)) s
-pattsExprBwd (NonEmptyList (p :| p' : ps) × s) σ = next (asExpr (pattContBwd p σ))
-   where
-   next (E.Lambda τ) = pattsExprBwd (NonEmptyList (p' :| ps) × s) τ
-   next _ = error absurd
-
 -- Pattern × Cont
 pattContFwd :: forall a m. MonadError Error m => Pattern -> Cont a -> m (Elim a)
 pattContFwd (PVar x) κ = pure (ElimVar x κ)
@@ -384,6 +371,11 @@ clausesFwd :: forall a m. MonadError Error m => JoinSemilattice a => Clauses a -
 clausesFwd (Clauses bs) = do
    NonEmptyList (σ :| σs) <- traverse pattsExprFwd (unwrap <$> bs)
    foldM maybeJoin σ σs
+   where
+   pattsExprFwd :: NonEmptyList Pattern × Expr a -> m (Elim a)
+   pattsExprFwd (NonEmptyList (p :| Nil) × s) = (ContExpr <$> desug s) >>= pattContFwd p
+   pattsExprFwd (NonEmptyList (p :| p' : ps) × s) =
+      pattContFwd p =<< ContExpr <$> E.Lambda <$> pattsExprFwd (NonEmptyList (p' :| ps) × s)
 
 clausesBwd :: forall a. BoundedJoinSemilattice a => Elim a -> Raw Clauses -> Clauses a
 clausesBwd σ (Clauses bs) = Clauses (clauseBwd <$> bs)
@@ -391,6 +383,13 @@ clausesBwd σ (Clauses bs) = Clauses (clauseBwd <$> bs)
    clauseBwd :: Raw Clause -> Clause a
    clauseBwd (Clause (πs × s)) = Clause (πs × pattsExprBwd (πs × s) σ)
 
+   pattsExprBwd :: NonEmptyList Pattern × Raw Expr -> Elim a -> Expr a
+   pattsExprBwd (NonEmptyList (p :| Nil) × s) σ' = desugBwd (asExpr (pattContBwd p σ')) s
+   pattsExprBwd (NonEmptyList (p :| p' : ps) × s) σ' = next (asExpr (pattContBwd p σ'))
+      where
+      next (E.Lambda τ) = pattsExprBwd (NonEmptyList (p' :| ps) × s) τ
+      next _ = error absurd
+
 -- orElse
 orElseFwd :: forall a. Cont a -> a -> Cont a
 orElseFwd ContNone _ = error absurd
diff --git a/src/SExpr2.purs b/src/SExpr2.purs
deleted file mode 100644
index 5e6678d4c..000000000
--- a/src/SExpr2.purs
+++ /dev/null
@@ -1,472 +0,0 @@
-module SExpr2 where
-
-import Prelude hiding (absurd, top)
-import Ann (Raw)
-import Bindings (Bind, Var, varAnon, (↦), keys)
-import BoolAlg (BoolAlg)
-import Control.Monad.Error.Class (class MonadError)
-import Data.Either (Either(..))
-import Data.Foldable (foldl)
-import Data.Function (applyN, on)
-import Data.Generic.Rep (class Generic)
-import Data.List (List(..), (:), (\\), length, sortBy, zip, zipWith)
-import Data.List (singleton) as L
-import Data.List.NonEmpty (NonEmptyList(..), groupBy, head, toList, singleton)
-import Data.List.NonEmpty (singleton) as NE
-import Data.Newtype (class Newtype, unwrap)
-import Data.NonEmpty ((:|))
-import Data.Profunctor.Strong (first, (***))
-import Data.Set (toUnfoldable) as S
-import Data.Show.Generic (genericShow)
-import Data.Traversable (traverse)
-import Data.Tuple (uncurry, fst, snd)
-import DataType (Ctr, arity, checkArity, ctrs, cCons, cFalse, cNil, cTrue, dataTypeFor)
-import Desugarable2 (class Desugarable, desugBwd, desug)
-import Dict (Dict, asSingletonMap, get)
-import Dict (fromFoldable, singleton) as D
-import Effect.Exception (Error)
-import Expr (Cont(..), Elim(..), asElim, asExpr)
-import Expr (Expr(..), Module(..), RecDefs, VarDef(..)) as E
-import Partial.Unsafe (unsafePartial)
-import Util (type (+), type (×), Endo, absurd, error, successful, (×))
-import Util.Pair (Pair(..))
-
--- Surface language expressions.
-data Expr a
-   = Var Var
-   | Op Var
-   | Int a Int
-   | Float a Number
-   | Str a String
-   | Constr a Ctr (List (Expr a))
-   | Record a (List (Bind (Expr a)))
-   | Dictionary a (List (Pair (Expr a)))
-   | Matrix a (Expr a) (Var × Var) (Expr a)
-   | Lambda (Clauses a)
-   | Project (Expr a) Var
-   | App (Expr a) (Expr a)
-   | BinaryApp (Expr a) Var (Expr a)
-   | MatchAs (Expr a) (NonEmptyList (Pattern × Expr a))
-   | IfElse (Expr a) (Expr a) (Expr a)
-   | ListEmpty a -- called [] in the paper
-   | ListNonEmpty a (Expr a) (ListRest a)
-   | ListEnum (Expr a) (Expr a)
-   | ListComp a (Expr a) (List (Qualifier a))
-   | Let (VarDefs a) (Expr a)
-   | LetRec (RecDefs a) (Expr a)
-
-derive instance Eq a => Eq (Expr a)
-derive instance generalExpr :: Generic (Expr a) _
-instance showExpr :: Show a => Show (Expr a) where
-   show c = genericShow c
-
-data ListRest a
-   = End a
-   | Next a (Expr a) (ListRest a)
-
-derive instance Eq a => Eq (ListRest a)
-derive instance genericListRest :: Generic (ListRest a) _
-instance showListRest :: Show a => Show (ListRest a) where
-   show c = genericShow c
-
-data Pattern
-   = PVar Var
-   | PConstr Ctr (List Pattern)
-   | PRecord (List (Bind Pattern))
-   | PListEmpty
-   | PListNonEmpty Pattern ListRestPattern
-
-derive instance Eq Pattern
-derive instance genericPattern :: Generic Pattern _
-instance showPattern :: Show Pattern where
-   show c = genericShow c
-
-data ListRestPattern
-   = PEnd
-   | PNext Pattern ListRestPattern
-
-derive instance Eq ListRestPattern
-derive instance genericListRestPattern :: Generic ListRestPattern _
-instance showListRestPattern :: Show ListRestPattern where
-   show c = genericShow c
-
-newtype Clause a = Clause (NonEmptyList Pattern × Expr a)
-
-derive instance Eq a => Eq (Clause a)
-derive instance genericClause :: Generic (Clause a) _
-instance showClause :: Show a => Show (Clause a) where
-   show c = genericShow c
-
-type Branch a = Var × Clause a
-
-newtype Clauses a = Clauses (NonEmptyList (Clause a))
-
-derive instance Eq a => Eq (Clauses a)
-derive instance genericClauses :: Generic (Clauses a) _
-instance showClauses :: Show a => Show (Clauses a) where
-   show c = genericShow c
-
-newtype RecDef a = RecDef (NonEmptyList (Branch a))
-type RecDefs a = NonEmptyList (Branch a)
-
--- The pattern/expr relationship is different to the one in branch (the expr is the "argument", not the "body").
--- Using a data type makes for easier overloading.
-data VarDef a = VarDef Pattern (Expr a)
-
-derive instance Eq a => Eq (VarDef a)
-derive instance genericVarDef :: Generic (VarDef a) _
-instance showVarDef :: Show a => Show (VarDef a) where
-   show c = genericShow c
-
-type VarDefs a = NonEmptyList (VarDef a)
-
-data Qualifier a
-   = Guard (Expr a)
-   | Generator Pattern (Expr a)
-   | Declaration (VarDef a) -- could allow VarDefs instead
-
-derive instance Eq a => Eq (Qualifier a)
-derive instance genericQualifier :: Generic (Qualifier a) _
-instance showQualifier :: Show a => Show (Qualifier a) where
-   show c = genericShow c
-
-data Module a = Module (List (VarDefs a + RecDefs a))
-
-instance Desugarable Expr E.Expr where
-   desug = exprFwd
-   desugBwd = exprBwd
-
-instance Desugarable ListRest E.Expr where
-   desug = listRestFwd
-   desugBwd = listRestBwd
-
-instance Desugarable Clauses Elim where
-   desug = clausesFwd
-   desugBwd = clausesBwd
-
-desugarModuleFwd :: forall a m. MonadError Error m => BoolAlg a -> Module a -> m (E.Module a)
-desugarModuleFwd = moduleFwd
-
--- helpers
-enil :: forall a. a -> E.Expr a
-enil α = E.Constr α cNil Nil
-
-econs :: forall a. a -> E.Expr a -> E.Expr a -> E.Expr a
-econs α e e' = E.Constr α cCons (e : e' : Nil)
-
-elimBool :: forall a. Cont a -> Cont a -> Elim a
-elimBool κ κ' = ElimConstr (D.fromFoldable [ cTrue × κ, cFalse × κ' ])
-
--- Module. Surface language supports "blocks" of variable declarations; core does not. Currently no backward.
-moduleFwd :: forall a m. MonadError Error m => BoolAlg a -> Module a -> m (E.Module a)
-moduleFwd 𝒶 (Module ds) = E.Module <$> traverse varDefOrRecDefsFwd (join (flatten <$> ds))
-   where
-   varDefOrRecDefsFwd :: VarDef a + RecDefs a -> m (E.VarDef a + E.RecDefs a)
-   varDefOrRecDefsFwd (Left d) = Left <$> varDefFwd 𝒶 d
-   varDefOrRecDefsFwd (Right xcs) = Right <$> recDefsFwd 𝒶 xcs
-
-   flatten :: VarDefs a + RecDefs a -> List (VarDef a + RecDefs a)
-   flatten (Left ds') = Left <$> toList ds'
-   flatten (Right δ) = pure (Right δ)
-
-varDefFwd :: forall a m. MonadError Error m => BoolAlg a -> VarDef a -> m (E.VarDef a)
-varDefFwd 𝒶 (VarDef π s) = E.VarDef <$> pattContFwd π (ContNone :: Cont a) <*> desug 𝒶 s
-
--- VarDefs
-varDefsFwd :: forall a m. MonadError Error m => BoolAlg a -> VarDefs a × Expr a -> m (E.Expr a)
-varDefsFwd 𝒶 (NonEmptyList (d :| Nil) × s) =
-   E.Let <$> varDefFwd 𝒶 d <*> desug 𝒶 s
-varDefsFwd 𝒶 (NonEmptyList (d :| d' : ds) × s) =
-   E.Let <$> varDefFwd 𝒶 d <*> varDefsFwd 𝒶 (NonEmptyList (d' :| ds) × s)
-
-varDefsBwd :: forall a. BoolAlg a -> E.Expr a -> Raw VarDefs × Raw Expr -> VarDefs a × Expr a
-varDefsBwd 𝒶 (E.Let (E.VarDef _ e1) e2) (NonEmptyList (VarDef π s1 :| Nil) × s2) =
-   NonEmptyList (VarDef π (desugBwd 𝒶 e1 s1) :| Nil) × desugBwd 𝒶 e2 s2
-varDefsBwd 𝒶 (E.Let (E.VarDef _ e1) e2) (NonEmptyList (VarDef π s1 :| d : ds) × s2) =
-   let
-      NonEmptyList (d' :| ds') × s2' = varDefsBwd 𝒶 e2 (NonEmptyList (d :| ds) × s2)
-   in
-      NonEmptyList (VarDef π (desugBwd 𝒶 e1 s1) :| d' : ds') × s2'
-varDefsBwd _ _ (NonEmptyList (_ :| _) × _) = error absurd
-
--- RecDefs
--- In the formalism, "group by name" is part of the syntax.
-recDefsFwd :: forall a m. MonadError Error m => BoolAlg a -> RecDefs a -> m (E.RecDefs a)
-recDefsFwd 𝒶 xcs = D.fromFoldable <$> traverse (recDefFwd 𝒶) xcss
-   where
-   xcss = map RecDef (groupBy (eq `on` fst) xcs) :: NonEmptyList (RecDef a)
-
-recDefsBwd :: forall a. BoolAlg a -> E.RecDefs a -> Raw RecDefs -> RecDefs a
-recDefsBwd 𝒶 ρ xcs = join (go (groupBy (eq `on` fst) xcs))
-   where
-   go :: NonEmptyList (Raw RecDefs) -> NonEmptyList (RecDefs a)
-   go (NonEmptyList (xcs1 :| xcss)) =
-      let
-         x = fst (head xcs1)
-         xcss' = case xcss of
-            Nil -> Nil
-            xcs2 : xcss'' -> toList (go (NonEmptyList (xcs2 :| xcss'')))
-      in
-         NonEmptyList (unwrap (recDefBwd 𝒶 (x ↦ get x ρ) (RecDef xcs1)) :| xcss')
-
--- RecDef
-recDefFwd :: forall a m. MonadError Error m => BoolAlg a -> RecDef a -> m (Bind (Elim a))
-recDefFwd 𝒶 xcs = (fst (head (unwrap xcs)) ↦ _) <$> clausesFwd 𝒶 (Clauses (snd <$> unwrap xcs))
-
-recDefBwd :: forall a. BoolAlg a -> Bind (Elim a) -> Raw RecDef -> RecDef a
-recDefBwd 𝒶 (x ↦ σ) (RecDef bs) = RecDef ((x × _) <$> unwrap (clausesBwd 𝒶 σ (Clauses (snd <$> bs))))
-
--- Expr
-exprFwd :: forall a m. MonadError Error m => BoolAlg a -> Expr a -> m (E.Expr a)
-exprFwd _ (Var x) = pure (E.Var x)
-exprFwd _ (Op op) = pure (E.Op op)
-exprFwd _ (Int α n) = pure (E.Int α n)
-exprFwd _ (Float α n) = pure (E.Float α n)
-exprFwd _ (Str α s) = pure (E.Str α s)
-exprFwd 𝒶 (Constr α c ss) = E.Constr α c <$> traverse (desug 𝒶) ss
-exprFwd 𝒶 (Record α xss) = E.Record α <$> D.fromFoldable <$> traverse (traverse (desug 𝒶)) xss
-exprFwd 𝒶 (Dictionary α sss) = E.Dictionary α <$> traverse (traverse (desug 𝒶)) sss
-exprFwd 𝒶 (Matrix α s (x × y) s') = E.Matrix α <$> desug 𝒶 s <@> x × y <*> desug 𝒶 s'
-exprFwd 𝒶 (Lambda bs) = E.Lambda <$> clausesFwd 𝒶 bs
-exprFwd 𝒶 (Project s x) = E.Project <$> desug 𝒶 s <@> x
-exprFwd 𝒶 (App s1 s2) = E.App <$> desug 𝒶 s1 <*> desug 𝒶 s2
-exprFwd 𝒶 (BinaryApp s1 op s2) = E.App <$> (E.App (E.Op op) <$> desug 𝒶 s1) <*> desug 𝒶 s2
-exprFwd 𝒶 (MatchAs s bs) =
-   E.App <$> (E.Lambda <$> clausesFwd 𝒶 (Clauses (Clause <$> first singleton <$> bs))) <*> desug 𝒶 s
-exprFwd 𝒶 (IfElse s1 s2 s3) =
-   E.App <$> (E.Lambda <$> (elimBool <$> (ContExpr <$> desug 𝒶 s2) <*> (ContExpr <$> desug 𝒶 s3))) <*> desug 𝒶 s1
-exprFwd _ (ListEmpty α) = pure (enil α)
-exprFwd 𝒶 (ListNonEmpty α s l) = econs α <$> desug 𝒶 s <*> desug 𝒶 l
-exprFwd 𝒶 (ListEnum s1 s2) = E.App <$> ((E.App (E.Var "enumFromTo")) <$> desug 𝒶 s1) <*> desug 𝒶 s2
-exprFwd 𝒶 (ListComp α s qs) = listCompFwd 𝒶 (α × qs × s)
-exprFwd 𝒶 (Let ds s) = varDefsFwd 𝒶 (ds × s)
-exprFwd 𝒶 (LetRec xcs s) = E.LetRec <$> recDefsFwd 𝒶 xcs <*> desug 𝒶 s
-
-exprBwd :: forall a. BoolAlg a -> E.Expr a -> Raw Expr -> Expr a
-exprBwd _ (E.Var _) (Var x) = Var x
-exprBwd _ (E.Op _) (Op op) = Op op
-exprBwd _ (E.Int α _) (Int _ n) = Int α n
-exprBwd _ (E.Float α _) (Float _ n) = Float α n
-exprBwd _ (E.Str α _) (Str _ str) = Str α str
-exprBwd 𝒶 (E.Constr α _ es) (Constr _ c ss) = Constr α c (uncurry (desugBwd 𝒶) <$> zip es ss)
-exprBwd 𝒶 (E.Record α xes) (Record _ xss) =
-   Record α $ xss <#> \(x ↦ s) -> x ↦ desugBwd 𝒶 (get x xes) s
-exprBwd 𝒶 (E.Dictionary α ees) (Dictionary _ sss) =
-   Dictionary α (zipWith (\(Pair e e') (Pair s s') -> Pair (desugBwd 𝒶 e s) (desugBwd 𝒶 e' s')) ees sss)
-exprBwd 𝒶 (E.Matrix α e1 _ e2) (Matrix _ s1 (x × y) s2) =
-   Matrix α (desugBwd 𝒶 e1 s1) (x × y) (desugBwd 𝒶 e2 s2)
-exprBwd 𝒶 (E.Lambda σ) (Lambda bs) = Lambda (clausesBwd 𝒶 σ bs)
-exprBwd 𝒶 (E.Project e _) (Project s x) = Project (desugBwd 𝒶 e s) x
-exprBwd 𝒶 (E.App e1 e2) (App s1 s2) = App (desugBwd 𝒶 e1 s1) (desugBwd 𝒶 e2 s2)
-exprBwd 𝒶 (E.App (E.App (E.Op _) e1) e2) (BinaryApp s1 op s2) =
-   BinaryApp (desugBwd 𝒶 e1 s1) op (desugBwd 𝒶 e2 s2)
-exprBwd 𝒶 (E.App (E.Lambda σ) e) (MatchAs s bs) =
-   MatchAs (desugBwd 𝒶 e s)
-      (first head <$> unwrap <$> unwrap (clausesBwd 𝒶 σ (Clauses (Clause <$> first NE.singleton <$> bs))))
-exprBwd 𝒶 (E.App (E.Lambda (ElimConstr m)) e1) (IfElse s1 s2 s3) =
-   IfElse (desugBwd 𝒶 e1 s1)
-      (desugBwd 𝒶 (asExpr (get cTrue m)) s2)
-      (desugBwd 𝒶 (asExpr (get cFalse m)) s3)
-exprBwd _ (E.Constr α _ Nil) (ListEmpty _) = ListEmpty α
-exprBwd 𝒶 (E.Constr α _ (e1 : e2 : Nil)) (ListNonEmpty _ s l) =
-   ListNonEmpty α (desugBwd 𝒶 e1 s) (desugBwd 𝒶 e2 l)
-exprBwd 𝒶 (E.App (E.App (E.Var "enumFromTo") e1) e2) (ListEnum s1 s2) =
-   ListEnum (desugBwd 𝒶 e1 s1) (desugBwd 𝒶 e2 s2)
-exprBwd 𝒶 e (ListComp _ s qs) =
-   let α × qs' × s' = listCompBwd 𝒶 e (qs × s) in ListComp α s' qs'
-exprBwd 𝒶 (E.Let d e) (Let ds s) = uncurry Let (varDefsBwd 𝒶 (E.Let d e) (ds × s))
-exprBwd 𝒶 (E.LetRec xσs e) (LetRec xcs s) = LetRec (recDefsBwd 𝒶 xσs xcs) (desugBwd 𝒶 e s)
-exprBwd _ _ _ = error absurd
-
--- ListRest
-listRestFwd :: forall a m. MonadError Error m => BoolAlg a -> ListRest a -> m (E.Expr a)
-listRestFwd _ (End α) = pure (enil α)
-listRestFwd 𝒶 (Next α s l) = econs α <$> desug 𝒶 s <*> desug 𝒶 l
-
-listRestBwd :: forall a. BoolAlg a -> E.Expr a -> Raw ListRest -> ListRest a
-listRestBwd _ (E.Constr α _ _) (End _) = End α
-listRestBwd 𝒶 (E.Constr α _ (e1 : e2 : Nil)) (Next _ s l) =
-   Next α (desugBwd 𝒶 e1 s) (desugBwd 𝒶 e2 l)
-listRestBwd _ _ _ = error absurd
-
--- List Qualifier × Expr
-listCompFwd :: forall a m. MonadError Error m => BoolAlg a -> a × List (Qualifier a) × Expr a -> m (E.Expr a)
-listCompFwd 𝒶 (α × Nil × s) =
-   econs α <$> desug 𝒶 s <@> enil α
-listCompFwd 𝒶 (α × (Guard s : qs) × s') = do
-   e <- listCompFwd 𝒶 (α × qs × s')
-   E.App (E.Lambda (elimBool (ContExpr e) (ContExpr (enil α)))) <$> desug 𝒶 s
-listCompFwd 𝒶 (α × (Declaration (VarDef π s) : qs) × s') = do
-   e <- ContExpr <$> listCompFwd 𝒶 (α × qs × s')
-   σ <- pattContFwd π e
-   E.App (E.Lambda σ) <$> desug 𝒶 s
-listCompFwd 𝒶 (α × (Generator p s : qs) × s') = do
-   e <- ContExpr <$> listCompFwd 𝒶 (α × qs × s')
-   σ <- pattContFwd p e
-   E.App (E.App (E.Var "concatMap") (E.Lambda (asElim (orElseFwd (ContElim σ) α)))) <$> desug 𝒶 s
-
-listCompBwd
-   :: forall a
-    . BoolAlg a
-   -> E.Expr a
-   -> List (Raw Qualifier) × Raw Expr
-   -> a × List (Qualifier a) × Expr a
-listCompBwd 𝒶 (E.Constr α2 c (e : E.Constr α1 c' Nil : Nil)) (Nil × s) | c == cCons && c' == cNil =
-   (α1 `𝒶.join` α2) × Nil × desugBwd 𝒶 e s
-listCompBwd 𝒶 (E.App (E.Lambda (ElimConstr m)) e) ((Guard s0 : qs) × s) =
-   case listCompBwd 𝒶 (asExpr (get cTrue m)) (qs × s) × asExpr (get cFalse m) of
-      (α × qs' × s') × E.Constr β c Nil | c == cNil -> (α `𝒶.join` β) × (Guard (desugBwd 𝒶 e s0) : qs') × s'
-      _ -> error absurd
-listCompBwd 𝒶 (E.App (E.Lambda σ) e) ((Declaration (VarDef π s0) : qs) × s) =
-   case listCompBwd 𝒶 (asExpr (pattContBwd π σ)) (qs × s) of
-      α × qs' × s' -> α × (Declaration (VarDef π (desugBwd 𝒶 e s0)) : qs') × s'
-listCompBwd 𝒶 (E.App (E.App (E.Var "concatMap") (E.Lambda σ)) e) ((Generator p s0 : qs) × s) =
-   case orElseBwd 𝒶 (ContElim σ) (Left p : Nil) of
-      σ' × β -> case listCompBwd 𝒶 (asExpr (pattContBwd p (asElim σ'))) (qs × s) of
-         α × qs' × s' -> (α `𝒶.join` β) × (Generator p (desugBwd 𝒶 e s0) : qs') × s'
-listCompBwd _ _ _ = error absurd
-
--- NonEmptyList Pattern × Expr
-pattsExprFwd :: forall a m. MonadError Error m => BoolAlg a -> NonEmptyList Pattern × Expr a -> m (Elim a)
-pattsExprFwd 𝒶 (NonEmptyList (p :| Nil) × s) = (ContExpr <$> desug 𝒶 s) >>= pattContFwd p
-pattsExprFwd 𝒶 (NonEmptyList (p :| p' : ps) × s) =
-   pattContFwd p =<< ContExpr <$> E.Lambda <$> pattsExprFwd 𝒶 (NonEmptyList (p' :| ps) × s)
-
-pattsExprBwd :: forall a. BoolAlg a -> NonEmptyList Pattern × Raw Expr -> Elim a -> Expr a
-pattsExprBwd 𝒶 (NonEmptyList (p :| Nil) × s) σ = desugBwd 𝒶 (asExpr (pattContBwd p σ)) s
-pattsExprBwd 𝒶 (NonEmptyList (p :| p' : ps) × s) σ = next (asExpr (pattContBwd p σ))
-   where
-   next (E.Lambda τ) = pattsExprBwd 𝒶 (NonEmptyList (p' :| ps) × s) τ
-   next _ = error absurd
-
--- Pattern × Cont
-pattContFwd :: forall a m. MonadError Error m => Pattern -> Cont a -> m (Elim a)
-pattContFwd (PVar x) κ = pure (ElimVar x κ)
-pattContFwd (PConstr c ps) κ =
-   checkArity c (length ps) *> (ElimConstr <$> D.singleton c <$> pattArgsFwd (Left <$> ps) κ)
-pattContFwd (PRecord xps) κ =
-   ElimRecord (keys xps) <$> pattArgsFwd ((snd >>> Left) <$> sortBy (compare `on` fst) xps) κ
-pattContFwd PListEmpty κ = pure (ElimConstr (D.singleton cNil κ))
-pattContFwd (PListNonEmpty p o) κ = ElimConstr <$> D.singleton cCons <$> pattArgsFwd (Left p : Right o : Nil) κ
-
-pattContBwd :: forall a. Pattern -> Elim a -> Cont a
-pattContBwd (PVar _) (ElimVar _ κ) = κ
-pattContBwd (PConstr c ps) (ElimConstr m) = pattArgsBwd (Left <$> ps) (get c m)
-pattContBwd (PListEmpty) (ElimConstr m) = get cNil m
-pattContBwd (PListNonEmpty p o) (ElimConstr m) = pattArgsBwd (Left p : Right o : Nil) (get cCons m)
-pattContBwd (PRecord xps) (ElimRecord _ κ) = pattArgsBwd ((snd >>> Left) <$> sortBy (compare `on` fst) xps) κ
-pattContBwd _ _ = error absurd
-
--- ListRestPattern × Cont
-pattCont_ListRest_Fwd :: forall a m. MonadError Error m => ListRestPattern -> Cont a -> m (Elim a)
-pattCont_ListRest_Fwd PEnd κ = pure (ElimConstr (D.singleton cNil κ))
-pattCont_ListRest_Fwd (PNext p o) κ = ElimConstr <$> D.singleton cCons <$> pattArgsFwd (Left p : Right o : Nil) κ
-
-pattCont_ListRest_Bwd :: forall a. Elim a -> ListRestPattern -> Cont a
-pattCont_ListRest_Bwd (ElimVar _ _) _ = error absurd
-pattCont_ListRest_Bwd (ElimRecord _ _) _ = error absurd
-pattCont_ListRest_Bwd (ElimConstr m) PEnd = get cNil m
-pattCont_ListRest_Bwd (ElimConstr m) (PNext p o) = pattArgsBwd (Left p : Right o : Nil) (get cCons m)
-
--- List (Pattern + ListRestPattern) × Cont
-pattArgsFwd :: forall a m. MonadError Error m => List (Pattern + ListRestPattern) -> Cont a -> m (Cont a)
-pattArgsFwd Nil κ = pure κ
-pattArgsFwd (Left p : πs) κ = ContElim <$> (pattArgsFwd πs κ >>= pattContFwd p)
-pattArgsFwd (Right o : πs) κ = ContElim <$> (pattArgsFwd πs κ >>= pattCont_ListRest_Fwd o)
-
-pattArgsBwd :: forall a. List (Pattern + ListRestPattern) -> Endo (Cont a)
-pattArgsBwd Nil κ = κ
-pattArgsBwd (Left p : πs) σ = pattArgsBwd πs (pattContBwd p (asElim σ))
-pattArgsBwd (Right o : πs) σ = pattArgsBwd πs (pattCont_ListRest_Bwd (asElim σ) o)
-
--- Clauses
-clausesFwd :: forall a m. MonadError Error m => BoolAlg a -> Clauses a -> m (Elim a)
-clausesFwd 𝒶 (Clauses bs) = do
-   NonEmptyList (_ :| _) <- traverse (pattsExprFwd 𝒶) (unwrap <$> bs)
-   error "todo" -- foldM maybeJoin σ σs
-
-clausesBwd :: forall a. BoolAlg a -> Elim a -> Raw Clauses -> Clauses a
-clausesBwd 𝒶 σ (Clauses bs) = Clauses (clauseBwd <$> bs)
-   where
-   clauseBwd :: Raw Clause -> Clause a
-   clauseBwd (Clause (πs × s)) = Clause (πs × pattsExprBwd 𝒶 (πs × s) σ)
-
--- orElse
-orElseFwd :: forall a. Cont a -> a -> Cont a
-orElseFwd ContNone _ = error absurd
-orElseFwd (ContExpr e) _ = ContExpr e
-orElseFwd (ContElim (ElimConstr m)) α = ContElim (ElimConstr (unlessFwd (c × orElseFwd κ α) α))
-   where
-   c × κ = asSingletonMap m
-orElseFwd (ContElim (ElimRecord xs κ)) α = ContElim (ElimRecord xs (orElseFwd κ α))
-orElseFwd (ContElim (ElimVar x κ)) α = ContElim (ElimVar x (orElseFwd κ α))
-
-orElseBwd :: forall a. BoolAlg a -> Cont a -> List (Pattern + ListRestPattern) -> Cont a × a
-orElseBwd 𝒶 κ Nil = κ × 𝒶.bot
-orElseBwd _ ContNone _ = error absurd
-orElseBwd 𝒶 (ContElim (ElimVar _ κ')) (Left (PVar x) : πs) =
-   orElseBwd 𝒶 κ' πs # first (\κ'' -> ContElim (ElimVar x κ''))
-orElseBwd 𝒶 (ContElim (ElimRecord _ κ')) (Left (PRecord xps) : πs) =
-   orElseBwd 𝒶 κ' ((xps <#> (snd >>> Left)) <> πs) # first (\κ'' -> ContElim (ElimRecord (keys xps) κ''))
-orElseBwd 𝒶 (ContElim (ElimConstr m)) (π : πs) =
-   let
-      c × πs' = case π of
-         -- TODO: refactor so these two cases aren't necessary
-         Left (PVar _) -> error absurd
-         Left (PRecord _) -> error absurd
-         Left (PConstr c ps) -> c × (Left <$> ps)
-         Left PListEmpty -> cNil × Nil
-         Left (PListNonEmpty p o) -> cCons × (Left p : Right o : Nil)
-         Right PEnd -> cNil × Nil
-         Right (PNext p o) -> cCons × (Left p : Right o : Nil)
-      κ' × α = unlessBwd 𝒶 m c
-   in
-      orElseBwd 𝒶 κ' (πs' <> πs) #
-         (\κ'' -> ContElim (ElimConstr (D.fromFoldable (singleton (c × κ''))))) *** (α `𝒶.join` _)
-orElseBwd _ _ _ = error absurd
-
--- In forward direction, extend singleton branch to set of branches where any missing constructors have
--- been mapped to the empty list, using anonymous variables in any generated patterns. Going backward, discard
--- all synthesised branches, returning the original singleton branch for c, plus join of annotations on the
--- empty lists used for bodies of synthesised branches.
-unlessFwd :: forall a. Ctr × Cont a -> a -> Dict (Cont a)
-unlessFwd (c × κ) α =
-   let
-      defaultBranch c' = c' × applyN (ContElim <<< ElimVar varAnon) (successful (arity c')) (ContExpr (enil α))
-      cκs = defaultBranch <$> ((ctrs (successful (dataTypeFor c)) # S.toUnfoldable) \\ L.singleton c)
-   in
-      D.fromFoldable ((c × κ) : cκs)
-
-unlessBwd :: forall a. BoolAlg a -> Dict (Cont a) -> Ctr -> Cont a × a
-unlessBwd 𝒶 m c =
-   let
-      cs = (ctrs (successful (dataTypeFor c)) # S.toUnfoldable) \\ L.singleton c
-   in
-      unsafePartial $ get c m × foldl (𝒶.join) 𝒶.bot ((bodyAnn <<< body) <$> cs)
-   where
-   body :: Partial => Ctr -> Cont a
-   body c' = applyN (\(ContElim (ElimVar _ κ)) -> κ) (successful $ arity c') (get c' m)
-
-   bodyAnn :: Partial => Cont a -> a
-   bodyAnn (ContExpr (E.Constr α c' Nil)) | c' == cNil = α
-
--- ======================
--- boilerplate
--- ======================
-derive instance Newtype (Clause a) _
-derive instance Newtype (Clauses a) _
-derive instance Newtype (RecDef a) _
-derive instance Functor Clause
-derive instance Functor Clauses
-derive instance Functor Expr
-derive instance Functor ListRest
-derive instance Functor VarDef
-derive instance Functor Qualifier
-
-instance Functor Module where
-   map f (Module defs) = Module (mapDefs f <$> defs)
-      where
-      mapDefs :: forall a b. (a -> b) -> VarDefs a + RecDefs a -> VarDefs b + RecDefs b
-      mapDefs g (Left ds) = Left $ map g <$> ds
-      mapDefs g (Right ds) = Right $ (\(x × Clause (ps × s)) -> x × Clause (ps × (g <$> s))) <$> ds
-
diff --git a/src/Trace2.purs b/src/Trace2.purs
deleted file mode 100644
index be775091b..000000000
--- a/src/Trace2.purs
+++ /dev/null
@@ -1,51 +0,0 @@
-module Trace2 where
-
-import Prelude
-
-import Ann (Raw)
-import Bindings (Var)
-import Data.Exists (Exists)
-import Data.List (List)
-import Data.Maybe (Maybe)
-import Data.Set (Set, empty, singleton, unions)
-import DataType (Ctr)
-import Dict (Dict)
-import Expr (class BV, RecDefs, bv)
-import Util (type (×))
-import Val2 (Array2, ForeignOp', Val)
-
-data Trace
-   = Var Var
-   | Op Var
-   | Const
-   | Record (Dict Trace)
-   | Dictionary (List (String × Trace × Trace)) (Dict (Raw Val))
-   | Constr Ctr (List Trace)
-   | Matrix (Array2 Trace) (Var × Var) (Int × Int) Trace
-   | Project Trace Var
-   | App Trace Trace AppTrace
-   | Let VarDef Trace
-   | LetRec (Raw RecDefs) Trace
-
-data AppTrace
-   = AppClosure (Set Var) Match Trace
-   -- these two forms represent partial (unsaturated) applications
-   | AppForeign Int ForeignTrace -- record number of arguments
-   | AppConstr Ctr
-
-data ForeignTrace' t = ForeignTrace' (ForeignOp' t) (Maybe t)
-type ForeignTrace = Exists ForeignTrace'
-
-data VarDef = VarDef Match Trace
-
-data Match
-   = MatchVar Var (Raw Val)
-   | MatchVarAnon (Raw Val)
-   | MatchConstr Ctr (List Match)
-   | MatchRecord (Dict Match)
-
-instance BV Match where
-   bv (MatchVar x _) = singleton x
-   bv (MatchVarAnon _) = empty
-   bv (MatchConstr _ ws) = unions (bv <$> ws)
-   bv (MatchRecord xws) = unions (bv <$> xws)
diff --git a/src/Util.purs b/src/Util.purs
index 98626ea74..6d43dfae6 100644
--- a/src/Util.purs
+++ b/src/Util.purs
@@ -22,6 +22,8 @@ import Effect.Exception (Error, message)
 import Effect.Exception (error) as E
 import Effect.Unsafe (unsafePerformEffect)
 
+type 𝔹 = Boolean
+
 infixr 6 type Tuple as × -- standard library has \/
 infixr 6 Tuple as ×
 
diff --git a/src/Val.purs b/src/Val.purs
index 58ef59c05..a8c7e94f0 100644
--- a/src/Val.purs
+++ b/src/Val.purs
@@ -146,10 +146,10 @@ derive instance Foldable Fun
 derive instance Traversable Fun
 
 instance Apply Val where
-   apply (Int fα n) (Int α _) = Int (fα α) n
-   apply (Float fα n) (Float α _) = Float (fα α) n
-   apply (Str fα s) (Str α _) = Str (fα α) s
-   apply (Constr fα c fes) (Constr α _ es) = Constr (fα α) c (zipWith (<*>) fes es)
+   apply (Int fα n) (Int α n') = Int (fα α) (n ≜ n')
+   apply (Float fα n) (Float α n') = Float (fα α) (n ≜ n')
+   apply (Str fα s) (Str α s') = Str (fα α) (s ≜ s')
+   apply (Constr fα c fes) (Constr α c' es) = Constr (fα α) (c ≜ c') (zipWith (<*>) fes es)
    apply (Record fα fxvs) (Record α xvs) = Record (fα α) (D.apply2 fxvs xvs)
    apply (Dictionary fα fxvs) (Dictionary α xvs) = Dictionary (fα α) (fxvs <*> xvs)
    apply (Matrix fα fm) (Matrix α m) = Matrix (fα α) (fm <*> m)
@@ -159,14 +159,16 @@ instance Apply Val where
 instance Apply Fun where
    apply (Closure fγ fρ fσ) (Closure γ ρ σ) = Closure (D.apply2 fγ γ) (D.apply2 fρ ρ) (fσ <*> σ)
    apply (Foreign op fvs) (Foreign _ vs) = Foreign op (zipWith (<*>) fvs vs)
-   apply (PartialConstr c fvs) (PartialConstr _ vs) = PartialConstr c (zipWith (<*>) fvs vs)
+   apply (PartialConstr c fvs) (PartialConstr c' vs) = PartialConstr (c ≜ c') (zipWith (<*>) fvs vs)
    apply _ _ = error "Apply Fun: shape mismatch"
 
 instance Apply DictRep where
-   apply (DictRep fxvs) (DictRep xvs) = DictRep $ D.intersectionWith (\(fα' × fv') (α' × v') -> (fα' α') × (fv' <*> v')) fxvs xvs
+   apply (DictRep fxvs) (DictRep xvs) =
+      DictRep $ D.intersectionWith (\(fα × fv) (α × v) -> fα α × (fv <*> v)) fxvs xvs
 
 instance Apply MatrixRep where
-   apply (MatrixRep (fvss × (n × fnα) × (m × fmα))) (MatrixRep (vss × (_ × nα) × (_ × mα))) = MatrixRep $ (A.zipWith (A.zipWith (<*>)) fvss vss) × (n × fnα nα) × (m × fmα mα)
+   apply (MatrixRep (fvss × (n × fnα) × (m × fmα))) (MatrixRep (vss × (n' × nα) × (m' × mα))) =
+      MatrixRep $ (A.zipWith (A.zipWith (<*>)) fvss vss) × ((n ≜ n') × fnα nα) × ((m ≜ m') × fmα mα)
 
 instance Foldable DictRep where
    foldl f acc (DictRep d) = foldl (\acc' (a × v) -> foldl f (acc' `f` a) v) acc d
diff --git a/src/Val2.purs b/src/Val2.purs
deleted file mode 100644
index 5b122e60a..000000000
--- a/src/Val2.purs
+++ /dev/null
@@ -1,182 +0,0 @@
-module Val2 where
-
-import Prelude hiding (absurd, append)
-
-import Bindings (Var)
-import BoolAlg (BoolAlg)
-import Control.Monad.Error.Class (class MonadError, class MonadThrow)
-import Data.Array ((!!))
-import Data.Array (zipWith) as A
-import Data.Bitraversable (bitraverse)
-import Data.Exists (Exists)
-import Data.Foldable (class Foldable, foldl, foldrDefault, foldMapDefaultL)
-import Data.List (List(..), (:), zipWith)
-import Data.Set (Set, empty, fromFoldable, intersection, member, singleton, toUnfoldable, union)
-import Data.Traversable (class Traversable, sequenceDefault, traverse)
-import DataType (Ctr)
-import Dict (Dict, get)
-import Dict (apply2, intersectionWith) as D
-import Effect.Exception (Error)
-import Expr (Elim, RecDefs, fv)
-import Foreign.Object (filterKeys, lookup, unionWith)
-import Foreign.Object (keys) as O
-import Graph (Vertex(..))
-import Graph.GraphWriter (class MonadGraphAlloc)
-import Util (type (×), Endo, error, orElse, unsafeUpdateAt, (!), (×))
-import Util.Pretty (Doc, beside, text)
-
-data Val a
-   = Int a Int
-   | Float a Number
-   | Str a String
-   | Constr a Ctr (List (Val a)) -- always saturated
-   | Record a (Dict (Val a)) -- always saturated
-   | Dictionary a (DictRep a)
-   | Matrix a (MatrixRep a)
-   | Fun a (Fun a)
-
-data Fun a
-   = Closure (Env a) (RecDefs a) (Elim a)
-   | Foreign ForeignOp (List (Val a)) -- never saturated
-   | PartialConstr Ctr (List (Val a)) -- never saturated
-
-instance Highlightable a => Highlightable (a × b) where
-   highlightIf (a × _) doc = highlightIf a doc
-
--- similar to an isomorphism lens with complement t
-type OpFwd t = forall a m. Highlightable a => MonadError Error m => BoolAlg a -> List (Val a) -> m (t × Val a)
-type OpBwd t = forall a. Highlightable a => BoolAlg a -> t × Val a -> List (Val a)
-type OpGraph = forall m. MonadGraphAlloc m => MonadError Error m => List (Val Vertex) -> m (Val Vertex)
-
-data ForeignOp' t = ForeignOp'
-   { arity :: Int
-   , op :: OpFwd t
-   , op' :: OpGraph
-   , op_bwd :: OpBwd t
-   }
-
-type ForeignOp = Exists ForeignOp'
-
--- Environments.
-type Env a = Dict (Val a)
-
-lookup' :: forall a m. MonadThrow Error m => Var -> Dict a -> m a
-lookup' x γ = lookup x γ # orElse ("variable " <> x <> " not found")
-
--- Want a monoid instance but needs a newtype
-append :: forall a. Env a -> Endo (Env a)
-append = unionWith (const identity)
-
-infixl 5 append as <+>
-
-append_inv :: forall a. Set Var -> Env a -> Env a × Env a
-append_inv xs γ = filterKeys (_ `not <<< member` xs) γ × restrict γ xs
-
-restrict :: forall a. Dict a -> Set Var -> Dict a
-restrict γ xs = filterKeys (_ `member` xs) γ
-
-reaches :: forall a. RecDefs a -> Endo (Set Var)
-reaches ρ xs = go (toUnfoldable xs) empty
-   where
-   dom_ρ = fromFoldable $ O.keys ρ
-
-   go :: List Var -> Endo (Set Var)
-   go Nil acc = acc
-   go (x : xs') acc | x `member` acc = go xs' acc
-   go (x : xs') acc | otherwise =
-      go (toUnfoldable (fv σ `intersection` dom_ρ) <> xs')
-         (singleton x `union` acc)
-      where
-      σ = get x ρ
-
-for :: forall a. RecDefs a -> Elim a -> RecDefs a
-for ρ σ = ρ `restrict` reaches ρ (fv σ `intersection` (fromFoldable $ O.keys ρ))
-
--- Wrap internal representations to provide foldable/traversable instances.
-newtype DictRep a = DictRep (Dict (a × Val a))
-newtype MatrixRep a = MatrixRep (Array2 (Val a) × (Int × a) × (Int × a))
-
-type Array2 a = Array (Array a)
-
-matrixGet :: forall a m. MonadThrow Error m => Int -> Int -> MatrixRep a -> m (Val a)
-matrixGet i j (MatrixRep (vss × _ × _)) =
-   orElse "Index out of bounds" $ do
-      us <- vss !! (i - 1)
-      us !! (j - 1)
-
-matrixUpdate :: forall a. Int -> Int -> Endo (Val a) -> Endo (MatrixRep a)
-matrixUpdate i j δv (MatrixRep (vss × h × w)) =
-   MatrixRep (vss' × h × w)
-   where
-   vs_i = vss ! (i - 1)
-   v_j = vs_i ! (j - 1)
-   vss' = unsafeUpdateAt (i - 1) (unsafeUpdateAt (j - 1) (δv v_j) vs_i) vss
-
-class Highlightable a where
-   highlightIf :: a -> Endo Doc
-
-instance Highlightable Unit where
-   highlightIf _ = identity
-
-instance Highlightable Boolean where
-   highlightIf false = identity
-   highlightIf true = \doc -> text "⸨" `beside` doc `beside` text "⸩"
-
-instance Highlightable Vertex where
-   highlightIf (Vertex α) = \doc -> doc `beside` text "_" `beside` text ("⟨" <> α <> "⟩")
-
--- ======================
--- boilerplate
--- ======================
-derive instance Functor DictRep
-derive instance Functor MatrixRep
-derive instance Functor Val
-derive instance Foldable Val
-derive instance Traversable Val
-derive instance Functor Fun
-derive instance Foldable Fun
-derive instance Traversable Fun
-
-instance Apply Val where
-   apply (Int fα n) (Int α _) = Int (fα α) n
-   apply (Float fα n) (Float α _) = Float (fα α) n
-   apply (Str fα s) (Str α _) = Str (fα α) s
-   apply (Constr fα c fes) (Constr α _ es) = Constr (fα α) c (zipWith (<*>) fes es)
-   apply (Record fα fxvs) (Record α xvs) = Record (fα α) (D.apply2 fxvs xvs)
-   apply (Dictionary fα fxvs) (Dictionary α xvs) = Dictionary (fα α) (fxvs <*> xvs)
-   apply (Matrix fα fm) (Matrix α m) = Matrix (fα α) (fm <*> m)
-   apply (Fun fα ff) (Fun α f) = Fun (fα α) (ff <*> f)
-   apply _ _ = error "Apply Expr: shape mismatch"
-
-instance Apply Fun where
-   apply (Closure fγ fρ fσ) (Closure γ ρ σ) = Closure (D.apply2 fγ γ) (D.apply2 fρ ρ) (fσ <*> σ)
-   apply (Foreign op fvs) (Foreign _ vs) = Foreign op (zipWith (<*>) fvs vs)
-   apply (PartialConstr c fvs) (PartialConstr _ vs) = PartialConstr c (zipWith (<*>) fvs vs)
-   apply _ _ = error "Apply Fun: shape mismatch"
-
-instance Apply DictRep where
-   apply (DictRep fxvs) (DictRep xvs) = DictRep $ D.intersectionWith (\(fα' × fv') (α' × v') -> (fα' α') × (fv' <*> v')) fxvs xvs
-
-instance Apply MatrixRep where
-   apply (MatrixRep (fvss × (n × fnα) × (m × fmα))) (MatrixRep (vss × (_ × nα) × (_ × mα))) = MatrixRep $ (A.zipWith (A.zipWith (<*>)) fvss vss) × (n × fnα nα) × (m × fmα mα)
-
-instance Foldable DictRep where
-   foldl f acc (DictRep d) = foldl (\acc' (a × v) -> foldl f (acc' `f` a) v) acc d
-   foldr f = foldrDefault f
-   foldMap f = foldMapDefaultL f
-
-instance Traversable DictRep where
-   traverse f (DictRep d) = DictRep <$> traverse (bitraverse f (traverse f)) d
-   sequence = sequenceDefault
-
-instance Foldable MatrixRep where
-   foldl f acc (MatrixRep (vss × (_ × βi) × (_ × βj))) = foldl (foldl (foldl f)) (acc `f` βi `f` βj) vss
-   foldr f = foldrDefault f
-   foldMap f = foldMapDefaultL f
-
-instance Traversable MatrixRep where
-   traverse f (MatrixRep m) =
-      MatrixRep <$> bitraverse (traverse (traverse (traverse f)))
-         (bitraverse (traverse f) (traverse f))
-         m
-   sequence = sequenceDefault
diff --git a/test/Util.purs b/test/Util.purs
index 486739405..3a716319f 100644
--- a/test/Util.purs
+++ b/test/Util.purs
@@ -4,7 +4,6 @@ import Prelude hiding (absurd)
 
 import App.Fig (LinkFigSpec)
 import App.Util (Selector)
-import BoolAlg (bool)
 import Benchmark.Util (BenchRow(..), GraphRow, TraceRow, zeroRow, sumRow, preciseTime, tdiff)
 import Control.Monad.Error.Class (class MonadThrow, liftEither)
 import Control.Monad.Except (runExceptT)
@@ -23,12 +22,14 @@ import Effect.Class.Console (log)
 import Effect.Exception (Error)
 import EvalBwd (traceGC)
 import EvalGraph (GraphConfig, graphGC)
-import Graph (sinks, vertices)
+import Graph (sinks)
+import Graph (vertices) as G
 import Graph.GraphImpl (GraphImpl)
-import Graph.Slice (selectαs, select𝔹s)
 import Graph.Slice (bwdSliceDual, fwdSliceDual, fwdSliceDeMorgan) as G
+import Graph.Slice (selectαs, select𝔹s, vertices)
+import GaloisConnection (GaloisConnection(..))
 import Heterogeneous.Mapping (hmap)
-import Lattice (botOf, erase, Raw)
+import Lattice (Raw, botOf, erase)
 import Module (parse)
 import Parse (program)
 import Pretty (class Pretty, prettyP)
@@ -44,7 +45,6 @@ type TestConfig =
    }
 
 -- fwd_expect: prettyprinted value after bwd then fwd round-trip
--- testWithSetup :: Boolean -> SE.Expr Unit -> GraphConfig (GraphImpl S.Set) -> TestConfig -> Aff BenchRow
 testWithSetup ∷ String -> SE.Expr Unit → GraphConfig GraphImpl → TestConfig → Aff BenchRow
 testWithSetup _name s gconfig tconfig =
    liftEither =<<
@@ -68,35 +68,35 @@ testParse s = do
 testTrace :: Raw SE.Expr -> GraphConfig GraphImpl -> TestConfig -> MayFailT Aff TraceRow
 testTrace s { γα } { δv, bwd_expect, fwd_expect } = do
    -- | Desugaring Galois connections for Unit and Boolean type selections
-   gc_desug <- desugGC s
-   gc_desug𝔹 <- desugGC s
+   GC desug <- desugGC s
+   GC desug𝔹 <- desugGC s
 
    -- | Eval
-   let e = gc_desug.fwd s
+   let e = desug.fwd s
    t_eval1 <- preciseTime
-   gc <- traceGC bool (erase <$> γα) e
+   { gc: GC eval, v } <- traceGC (erase <$> γα) e
    t_eval2 <- preciseTime
 
    -- | Backward
    t_bwd1 <- preciseTime
-   let γ𝔹 × e𝔹 × _ = gc.bwd (δv (botOf gc.v))
+   let γ𝔹 × e𝔹 × _ = eval.bwd (δv (botOf v))
    t_bwd2 <- preciseTime
-   let s𝔹 = gc_desug𝔹.bwd e𝔹
+   let s𝔹 = desug𝔹.bwd e𝔹
 
    -- | Forward (round-tripping)
-   let e𝔹' = gc_desug𝔹.fwd s𝔹
+   let e𝔹' = desug𝔹.fwd s𝔹
    t_fwd1 <- preciseTime
-   let v𝔹 = gc.fwd (γ𝔹 × e𝔹' × top)
+   let v𝔹 = eval.fwd (γ𝔹 × e𝔹' × top)
    t_fwd2 <- preciseTime
 
    lift do
-      unless (isGraphical gc.v) $
+      unless (isGraphical v) $
          log (prettyP v𝔹)
       -- | Check backward selections
       unless (null bwd_expect) $
          checkPretty "Trace-based source selection" bwd_expect s𝔹
       -- | Check round-trip selections
-      unless (isGraphical gc.v) $
+      unless (isGraphical v) $
          checkPretty "Trace-based value" fwd_expect v𝔹
 
    pure { tEval: tdiff t_eval1 t_eval2, tBwd: tdiff t_bwd1 t_bwd2, tFwd: tdiff t_fwd1 t_fwd2 }
@@ -104,58 +104,58 @@ testTrace s { γα } { δv, bwd_expect, fwd_expect } = do
 testGraph :: Raw SE.Expr -> GraphConfig GraphImpl -> TestConfig -> MayFailT Aff GraphRow
 testGraph s gconfig { δv, bwd_expect, fwd_expect } = do
    -- | Desugaring Galois connections for Unit and Boolean type selections
-   gc_desug <- desugGC s
-   gc_desug𝔹 <- desugGC s
+   GC desug <- desugGC s
+   GC desug𝔹 <- desugGC s
 
    -- | Eval
-   let e = gc_desug.fwd s
+   let e = desug.fwd s
    t_eval1 <- preciseTime
-   gc <- graphGC gconfig e
+   { gc: GC eval, eα, g, vα } <- graphGC gconfig e
    t_eval2 <- preciseTime
 
    -- | Backward
    t_bwd1 <- preciseTime
    let
-      αs_out = selectαs (δv (botOf gc.vα)) gc.vα
-      αs_in = gc.bwd αs_out
-      e𝔹 = select𝔹s (gc.eα) αs_in
+      αs_out = selectαs (δv (botOf vα)) vα
+      αs_in = eval.bwd αs_out
+      e𝔹 = select𝔹s eα αs_in
    t_bwd2 <- preciseTime
-   let s𝔹 = gc_desug𝔹.bwd e𝔹
+   let s𝔹 = desug𝔹.bwd e𝔹
 
    -- | De Morgan dual of backward
    t_bwdDual1 <- preciseTime
    let
-      αs_out_dual = selectαs (δv (botOf gc.vα)) gc.vα
-      gbwd_dual = G.bwdSliceDual αs_out_dual gc.g
+      αs_out_dual = selectαs (δv (botOf vα)) vα
+      gbwd_dual = G.bwdSliceDual αs_out_dual g
       αs_in_dual = sinks gbwd_dual
-      e𝔹_dual = select𝔹s (gc.eα) αs_in_dual
+      e𝔹_dual = select𝔹s eα αs_in_dual
    t_bwdDual2 <- preciseTime
 
    -- | Backward (all outputs selected)
    t_bwdAll1 <- preciseTime
    let
-      e𝔹_all = select𝔹s gc.eα $ gc.bwd $ gc.codom.top
+      e𝔹_all = select𝔹s eα $ eval.bwd (vertices vα)
    t_bwdAll2 <- preciseTime
 
    -- | Forward (round-tripping)
    t_fwd1 <- preciseTime
    let
-      αs_out' = gc.fwd αs_in
-      v𝔹 = select𝔹s gc.vα αs_out'
+      αs_out' = eval.fwd αs_in
+      v𝔹 = select𝔹s vα αs_out'
    t_fwd2 <- preciseTime
 
    -- | De Morgan dual of forward
    t_fwdDual1 <- preciseTime
    let
-      gfwd_dual = G.fwdSliceDual αs_in gc.g
-      v𝔹_dual = select𝔹s gc.vα (vertices gfwd_dual)
+      gfwd_dual = G.fwdSliceDual αs_in g
+      v𝔹_dual = select𝔹s vα (G.vertices gfwd_dual)
    t_fwdDual2 <- preciseTime
 
    -- | Forward (round-tripping) using De Morgan dual
    t_fwdAsDeMorgan1 <- preciseTime
    let
-      gfwd_demorgan = G.fwdSliceDeMorgan αs_in gc.g
-      v𝔹_demorgan = select𝔹s gc.vα (vertices gfwd_demorgan) <#> not
+      gfwd_demorgan = G.fwdSliceDeMorgan αs_in g
+      v𝔹_demorgan = select𝔹s vα (G.vertices gfwd_demorgan) <#> not
    t_fwdAsDeMorgan2 <- preciseTime
 
    lift do