diff --git a/src/App/Fig.purs b/src/App/Fig.purs
index ebeccaa78..8f7d81479 100644
--- a/src/App/Fig.purs
+++ b/src/App/Fig.purs
@@ -174,7 +174,7 @@ valViews γ xs = sequence (flip varView γ <$> xs)
 figViews :: Fig -> Selector Val -> MayFail (View × Array View)
 figViews { spec: { xs }, γ0, γ, e, t, v } δv = do
    let
-      { γ: γ0γ, e: e', α } = evalBwd (erase <$> (γ0 <+> γ)) (erase e) (δv v) t
+      γ0γ × e' × α = evalBwd (erase <$> (γ0 <+> γ)) (erase e) (δv v) t
    _ × v' <- eval γ0γ e' α
    views <- valViews γ0γ xs
    pure $ view "output" v' × views
@@ -182,7 +182,7 @@ figViews { spec: { xs }, γ0, γ, e, t, v } δv = do
 linkResult :: Var -> Env 𝔹 -> Env 𝔹 -> Expr 𝔹 -> Expr 𝔹 -> Trace -> Trace -> Val 𝔹 -> MayFail LinkResult
 linkResult x γ0 γ e1 e2 t1 _ v1 = do
    let
-      { γ: γ0γ } = evalBwd (erase <$> (γ0 <+> γ)) (erase e1) v1 t1
+      γ0γ × _ = evalBwd (erase <$> (γ0 <+> γ)) (erase e1) v1 t1
       _ × γ' = append_inv (S.singleton x) γ0γ
    v0' <- lookup x γ' # orElse absurd
    -- make γ0 and e2 fully available; γ0 was previously too big to operate on, so we use
diff --git a/src/BoolAlg.purs b/src/BoolAlg.purs
index 13b73fd88..40136ee42 100644
--- a/src/BoolAlg.purs
+++ b/src/BoolAlg.purs
@@ -5,10 +5,12 @@ import Prelude
 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 Lattice (𝔹)
 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.
@@ -55,3 +57,12 @@ prod 𝒶 𝒷 =
    , 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
new file mode 100644
index 000000000..f3d005d09
--- /dev/null
+++ b/src/Desug.purs
@@ -0,0 +1,25 @@
+module Desug where
+
+import Desugarable (desug, desugBwd)
+import Prelude
+import Control.Monad.Error.Class (class MonadError)
+import Effect.Exception (Error)
+import Expr (Expr)
+import GaloisConnection (GaloisConnection)
+import Lattice (Raw, class BoundedJoinSemilattice)
+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)
+desugGC s0 = do
+   let
+      fwd s = successful $ desug s
+      bwd e = desugBwd e s0
+   pure { fwd, bwd }
diff --git a/src/EvalBwd.purs b/src/EvalBwd.purs
index 29798f332..1b9b313be 100644
--- a/src/EvalBwd.purs
+++ b/src/EvalBwd.purs
@@ -2,6 +2,7 @@ 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)
@@ -70,17 +71,11 @@ matchManyBwd γγ' κ α (w : ws) =
    v × σ = matchBwd γ κ α w
    vs × κ' = matchManyBwd γ' (ContElim σ) α ws
 
-type EvalBwdResult a =
-   { γ :: Env a
-   , e :: Expr a
-   , α :: a
-   }
-
 applyBwd :: forall a. Ann a => AppTrace × Val a -> Val a × Val a
 applyBwd (T.AppClosure xs w t3 × v) =
    V.Fun (β ∨ β') (V.Closure (γ1 ∨ γ1') δ' σ) × v'
    where
-   { γ: γ1γ2γ3, e, α: β } = evalBwd' v t3
+   γ1γ2γ3 × e × β = evalBwd' v t3
    γ1γ2 × γ3 = append_inv (bv w) γ1γ2γ3
    γ1 × γ2 = append_inv xs γ1γ2
    γ1' × δ' × β' = closeDefsBwd γ2
@@ -112,44 +107,45 @@ apply2Bwd ((t1 × t2) × v) =
    in
       u1 × v1 × v2
 
-evalBwd :: forall a. Ann a => Raw Env -> Raw Expr -> Val a -> Trace -> EvalBwdResult a
+evalBwd :: forall a. Ann a => Raw Env -> Raw Expr -> Val a -> Trace -> Env a × Expr a × a
 evalBwd γ e v t =
-   { γ: expand γ' γ, e: expand e' e, α }
+   expand γ' γ × expand e' e × α
    where
-   { γ: γ', e: e', α } = evalBwd' v t
+   γ' × e' × α = evalBwd' v t
 
 -- Computes a partial slice which evalBwd expands to a full slice.
-evalBwd' :: forall a. Ann a => Val a -> Trace -> EvalBwdResult a
-evalBwd' v (T.Var x) = { γ: D.singleton x v, e: Var x, α: bot }
-evalBwd' v (T.Op op) = { γ: D.singleton op v, e: Op op, α: bot }
-evalBwd' (V.Str α str) T.Const = { γ: empty, e: Str α str, α }
-evalBwd' (V.Int α n) T.Const = { γ: empty, e: Int α n, α }
-evalBwd' (V.Float α n) T.Const = { γ: empty, e: Float α n, α }
-evalBwd' (V.Fun α (V.Closure γ _ σ)) T.Const = { γ, e: Lambda σ, α }
+evalBwd' :: forall a. Ann a => Val a -> Trace -> Env a × Expr a × a
+evalBwd' v (T.Var x) = D.singleton x v × Var x × bot
+evalBwd' v (T.Op op) = D.singleton op v × Op op × bot
+evalBwd' (V.Str α str) T.Const = empty × Str α str × α
+evalBwd' (V.Int α n) T.Const = empty × Int α n × α
+evalBwd' (V.Float α n) T.Const = empty × Float α n × α
+evalBwd' (V.Fun α (V.Closure γ _ σ)) T.Const = γ × Lambda σ × α
 evalBwd' (V.Record α xvs) (T.Record xts) =
-   { γ: foldr (∨) empty (xγeαs <#> _.γ), e: Record α (xγeαs <#> _.e), α: foldr (∨) α (xγeαs <#> _.α) }
+   foldr (∨) empty (xγeαs <#> fst)
+      × Record α (xγeαs <#> (fst <<< snd))
+      × foldr (∨) α (xγeαs <#> (snd <<< snd))
    where
    xvts = intersectionWith (×) xvs xts
    xγeαs = xvts <#> uncurry evalBwd'
 evalBwd' (V.Dictionary α (DictRep sαvs)) (T.Dictionary stts sus) =
-   { γ: foldr (∨) empty ((γeαs <#> _.γ) <> (γeαs' <#> _.γ))
-   , e: Dictionary α ((γeαs <#> _.e) `P.zip` (γeαs' <#> _.e))
-   , α: foldr (∨) α ((γeαs <#> _.α) <> (γeαs' <#> _.α))
-   }
+   foldr (∨) empty ((γeαs <#> fst) <> (γeαs' <#> fst))
+      × Dictionary α ((γeαs <#> (fst <<< snd)) `P.zip` (γeαs' <#> (fst <<< snd)))
+      × foldr (∨) α ((γeαs <#> (snd <<< snd)) <> (γeαs' <#> (snd <<< snd)))
    where
    sαvs' = expand sαvs (sus <#> (bot × _))
    γeαs = stts <#> \(s × t × _) -> evalBwd' (V.Str (fst (get s sαvs')) s) t
    γeαs' = stts <#> \(s × _ × t) -> evalBwd' (snd (get s sαvs')) t
 evalBwd' (V.Constr α _ vs) (T.Constr c ts) =
-   { γ: γ', e: Constr α c es, α: α' }
+   γ' × Constr α c es × α'
    where
    evalArg_bwd :: Val a × Trace -> Endo (Env a × List (Expr a) × a)
    evalArg_bwd (v' × t') (γ' × es × α') = (γ' ∨ γ'') × (e : es) × (α' ∨ α'')
       where
-      { γ: γ'', e, α: α'' } = evalBwd' v' t'
+      γ'' × e × α'' = evalBwd' v' t'
    γ' × es × α' = foldr evalArg_bwd (empty × Nil × α) (zip vs ts)
 evalBwd' (V.Matrix α (MatrixRep (vss × (_ × βi) × (_ × βj)))) (T.Matrix tss (x × y) (i' × j') t') =
-   { γ: γ ∨ γ', e: Matrix α e (x × y) e', α: α ∨ α' ∨ α'' }
+   (γ ∨ γ') × Matrix α e (x × y) e' × (α ∨ α' ∨ α'')
    where
    NonEmptyList ijs = nonEmpty $ do
       i <- range 1 i'
@@ -159,7 +155,7 @@ evalBwd' (V.Matrix α (MatrixRep (vss × (_ × βi) × (_ × βj)))) (T.Matrix t
    evalBwd_elem :: (Int × Int) -> Env a × Expr a × a × a × a
    evalBwd_elem (i × j) =
       case evalBwd' (vss ! (i - 1) ! (j - 1)) (tss ! (i - 1) ! (j - 1)) of
-         { γ: γ'', e, α: α' } ->
+         γ'' × e × α' ->
             let
                γ × γ' = append_inv (S.singleton x `union` S.singleton y) γ''
                γ0 = (D.singleton x (V.Int bot i') `disjointUnion` D.singleton y (V.Int bot j')) <+> γ'
@@ -174,44 +170,45 @@ evalBwd' (V.Matrix α (MatrixRep (vss × (_ × βi) × (_ × βj)))) (T.Matrix t
            ((γ1 ∨ γ2) × (e1 ∨ e2) × (α1 ∨ α2) × (β1 ∨ β2) × (β1' ∨ β2'))
       )
       (evalBwd_elem <$> ijs)
-   { γ: γ', e: e', α: α'' } =
+   γ' × e' × α'' =
       evalBwd' (V.Constr bot cPair (V.Int (β ∨ βi) i' : V.Int (β' ∨ βj) j' : Nil)) t'
 evalBwd' v (T.Project t x) =
-   { γ, e: Project e x, α }
+   γ × Project e x × α
    where
-   { γ, e, α } = evalBwd' (V.Record bot (D.singleton x v)) t
+   γ × e × α = evalBwd' (V.Record bot (D.singleton x v)) t
 evalBwd' v (T.App t1 t2 t3) =
-   { γ: γ ∨ γ', e: App e e', α: α ∨ α' }
+   (γ ∨ γ') × App e e' × (α ∨ α')
    where
    u × v2 = applyBwd (t3 × v)
-   { γ, e, α } = evalBwd' u t1
-   { γ: γ', e: e', α: α' } = evalBwd' v2 t2
+   γ × e × α = evalBwd' u t1
+   γ' × e' × α' = evalBwd' v2 t2
 evalBwd' v (T.Let (T.VarDef w t1) t2) =
-   { γ: γ1 ∨ γ1', e: Let (VarDef σ e1) e2, α: α1 }
+   (γ1 ∨ γ1') × Let (VarDef σ e1) e2 × α1
    where
-   { γ: γ1γ2, e: e2, α: α2 } = evalBwd' v t2
+   γ1γ2 × e2 × α2 = evalBwd' v t2
    γ1 × γ2 = append_inv (bv w) γ1γ2
    v' × σ = matchBwd γ2 ContNone α2 w
-   { γ: γ1', e: e1, α: α1 } = evalBwd' v' t1
+   γ1' × e1 × α1 = evalBwd' v' t1
 evalBwd' v (T.LetRec ρ t) =
-   { γ: γ1 ∨ γ1', e: LetRec ρ' e, α: α ∨ α' }
+   (γ1 ∨ γ1') × LetRec ρ' e × (α ∨ α')
    where
-   { γ: γ1γ2, e, α } = evalBwd' v t
+   γ1γ2 × e × α = evalBwd' v t
    γ1 × γ2 = append_inv (S.fromFoldable $ keys ρ) γ1γ2
    γ1' × ρ' × α' = closeDefsBwd γ2
 evalBwd' _ _ = error absurd
 
-type EvalGaloisConnection a = GaloisConnection (EvalBwdResult a) (Val a)
-   ( γ :: Raw Env
-   , e :: Raw Expr
-   , t :: Trace
+type EvalGaloisConnection a = GaloisConnection (Env a × Expr a × a) (Val a)
+   ( dom :: BoolAlg (Env a × Expr a × a)
+   , codom :: BoolAlg (Val a)
    , v :: Raw Val
    )
 
-traceGC :: forall a m. MonadError Error m => Ann a => Raw Env -> Raw Expr -> m (EvalGaloisConnection a)
-traceGC γ e = do
+traceGC :: forall a m. MonadError Error m => Ann a => BoolAlg a -> Raw Env -> Raw Expr -> m (EvalGaloisConnection 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: e', α } = snd $ fromRight $ runExcept $ eval γ' e' α
-   pure { γ, e, t, v, fwd, bwd }
+      fwd (γ' × e' × α) = snd $ fromRight $ runExcept $ eval γ' e' α
+   pure { dom, codom, v, fwd, bwd }
diff --git a/src/GaloisConnection.purs b/src/GaloisConnection.purs
index 97ca08d7d..37e89c157 100644
--- a/src/GaloisConnection.purs
+++ b/src/GaloisConnection.purs
@@ -5,7 +5,8 @@ import Prelude
 import BoolAlg (BoolAlg)
 import Util (Endo)
 
--- Galois connections are more general, this is specialised to Boolean algebras.
+-- 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
diff --git a/test/Util.purs b/test/Util.purs
index 614514b07..1c7ad3b87 100644
--- a/test/Util.purs
+++ b/test/Util.purs
@@ -4,6 +4,7 @@ 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)
@@ -16,7 +17,7 @@ import Data.Set (subset)
 import Data.String (null)
 import DataType (dataTypeFor, typeName)
 import Debug (trace)
-import Desugarable (desug, desugBwd)
+import Desug (desugGC)
 import Effect.Aff (Aff)
 import Effect.Class.Console (log)
 import Effect.Exception (Error)
@@ -32,7 +33,7 @@ import Parse (program)
 import Pretty (class Pretty, prettyP)
 import SExpr (Expr) as SE
 import Test.Spec.Assertions (fail)
-import Util (MayFailT, successful)
+import Util (MayFailT, successful, (×))
 import Val (Val(..), class Ann)
 
 type TestConfig =
@@ -65,23 +66,27 @@ 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
+
    -- | Eval
-   e <- desug s
-   tEval1 <- preciseTime
-   gc <- traceGC (erase <$> γα) e
-   tEval2 <- preciseTime
+   let e = gc_desug.fwd s
+   t_eval1 <- preciseTime
+   gc <- traceGC bool (erase <$> γα) e
+   t_eval2 <- preciseTime
 
    -- | Backward
-   tBwd1 <- preciseTime
-   let { γ: γ𝔹, e: e𝔹 } = gc.bwd (δv (botOf gc.v))
-   tBwd2 <- preciseTime
-   let s𝔹 = desugBwd e𝔹 s
+   t_bwd1 <- preciseTime
+   let γ𝔹 × e𝔹 × _ = gc.bwd (δv (botOf gc.v))
+   t_bwd2 <- preciseTime
+   let s𝔹 = gc_desug𝔹.bwd e𝔹
 
    -- | Forward (round-tripping)
-   e𝔹' <- desug s𝔹
-   tFwd1 <- preciseTime
-   let v𝔹 = gc.fwd { γ: γ𝔹, e: e𝔹', α: top }
-   tFwd2 <- preciseTime
+   let e𝔹' = gc_desug𝔹.fwd s𝔹
+   t_fwd1 <- preciseTime
+   let v𝔹 = gc.fwd (γ𝔹 × e𝔹' × top)
+   t_fwd2 <- preciseTime
 
    lift do
       unless (isGraphical gc.v) $
@@ -93,60 +98,64 @@ testTrace s { γα } { δv, bwd_expect, fwd_expect } = do
       unless (isGraphical gc.v) $
          checkPretty "Trace-based value" fwd_expect v𝔹
 
-   pure { tEval: tdiff tEval1 tEval2, tBwd: tdiff tBwd1 tBwd2, tFwd: tdiff tFwd1 tFwd2 }
+   pure { tEval: tdiff t_eval1 t_eval2, tBwd: tdiff t_bwd1 t_bwd2, tFwd: tdiff t_fwd1 t_fwd2 }
 
 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
+
    -- | Eval
-   e <- desug s
-   tEval1 <- preciseTime
+   let e = gc_desug.fwd s
+   t_eval1 <- preciseTime
    gc <- graphGC gconfig e
-   tEval2 <- preciseTime
+   t_eval2 <- preciseTime
 
    -- | Backward
-   tBwd1 <- preciseTime
+   t_bwd1 <- preciseTime
    let
       αs_out = gc.runδv δv
       αs_in = gc.bwd αs_out
       e𝔹 = gc.selecte𝔹 αs_in
-   tBwd2 <- preciseTime
-   let s𝔹 = desugBwd e𝔹 s
+   t_bwd2 <- preciseTime
+   let s𝔹 = gc_desug𝔹.bwd e𝔹
 
    -- | De Morgan dual of backward
-   tBwdDual1 <- preciseTime
+   t_bwdDual1 <- preciseTime
    let
       αs_out_dual = gc.runδv δv
       gbwd_dual = G.bwdSliceDual αs_out_dual gc.g
       αs_in_dual = sinks gbwd_dual
       e𝔹_dual = gc.selecte𝔹 αs_in_dual
-   tBwdDual2 <- preciseTime
+   t_bwdDual2 <- preciseTime
 
    -- | Backward (all outputs selected)
-   tBwdAll1 <- preciseTime
+   t_bwdAll1 <- preciseTime
    let
       e𝔹_all = (gc.selecte𝔹 <<< gc.bwd <<< gc.runδv) topOf
-   tBwdAll2 <- preciseTime
+   t_bwdAll2 <- preciseTime
 
    -- | Forward (round-tripping)
-   tFwd1 <- preciseTime
+   t_fwd1 <- preciseTime
    let
       αs_out' = gc.fwd αs_in
       v𝔹 = gc.selectv𝔹 αs_out'
-   tFwd2 <- preciseTime
+   t_fwd2 <- preciseTime
 
    -- | De Morgan dual of forward
-   tFwdDual1 <- preciseTime
+   t_fwdDual1 <- preciseTime
    let
       gfwd_dual = G.fwdSliceDual αs_in gc.g
       v𝔹_dual = gc.selectv𝔹 (vertices gfwd_dual)
-   tFwdDual2 <- preciseTime
+   t_fwdDual2 <- preciseTime
 
    -- | Forward (round-tripping) using De Morgan dual
-   tFwdAsDeMorgan1 <- preciseTime
+   t_fwdAsDeMorgan1 <- preciseTime
    let
       gfwd_demorgan = G.fwdSliceDeMorgan αs_in gc.g
       v𝔹_demorgan = gc.selectv𝔹 (vertices gfwd_demorgan) <#> not
-   tFwdAsDeMorgan2 <- preciseTime
+   t_fwdAsDeMorgan2 <- preciseTime
 
    lift do
       -- | Check backward selections
@@ -164,7 +173,7 @@ testGraph s gconfig { δv, bwd_expect, fwd_expect } = do
          log (prettyP e𝔹_all)
          log (prettyP v𝔹_dual)
 
-   pure { tEval: tdiff tEval1 tEval2, tBwd: tdiff tBwd1 tBwd2, tBwdDual: tdiff tBwdDual1 tBwdDual2, tBwdAll: tdiff tBwdAll1 tBwdAll2, tFwd: tdiff tFwd1 tFwd2, tFwdDual: tdiff tFwdDual1 tFwdDual2, tFwdAsDemorgan: tdiff tFwdAsDeMorgan1 tFwdAsDeMorgan2 }
+   pure { tEval: tdiff t_eval1 t_eval2, tBwd: tdiff t_bwd1 t_bwd2, tBwdDual: tdiff t_bwdDual1 t_bwdDual2, tBwdAll: tdiff t_bwdAll1 t_bwdAll2, tFwd: tdiff t_fwd1 t_fwd2, tFwdDual: tdiff t_fwdDual1 t_fwdDual2, tFwdAsDemorgan: tdiff t_fwdAsDeMorgan1 t_fwdAsDeMorgan2 }
 
 type TestSpec =
    { file :: String