diff --git a/index.html b/index.html
index eae7148..9716a53 100644
--- a/index.html
+++ b/index.html
@@ -671,7 +671,7 @@
       (Eq a c)
 
       -------------- eq-a-comp
-      (Eq "a" (Foo Bar))
+      (Eq "a" Foo)
     </hol-string>
     <hol-string-proof id="index.html/string-silliness-trip" deps="index.html/myconfig index.html/string-silliness">
       ------------- eq-a-c
diff --git a/src/AtomDef.res b/src/AtomDef.res
new file mode 100644
index 0000000..c41cd07
--- /dev/null
+++ b/src/AtomDef.res
@@ -0,0 +1,168 @@
+// type level stuff to enable well-typed coercions
+type typeTag<_> = ..
+type rec eq<_, _> = Refl: eq<'a, 'a>
+// coercion<t> represents a coercion from some type 'a to t
+type rec coercion<_> = Coercion(typeTag<'a>, 'a => option<'b>): coercion<'b>
+
+module type ATOM = {
+  type t
+  type subst = Map.t<int, t>
+  let tagEq: typeTag<'a> => option<eq<t, 'a>>
+  let tag: typeTag<t>
+  let unify: (t, t, ~gen: ref<int>=?) => Seq.t<subst>
+  let prettyPrint: (t, ~scope: array<string>) => string
+  let parse: (string, ~scope: array<string>, ~gen: ref<int>=?) => result<(t, string), string>
+  let substitute: (t, subst) => t
+  let upshift: (t, int, ~from: int=?) => t
+  // used for when trying to substitute a variable of the wrong type
+  let lowerVar: int => option<t>
+  let lowerSchematic: (int, array<int>) => option<t>
+  let substDeBruijn: (t, array<option<t>>, ~from: int=?) => t
+  let concrete: t => bool
+}
+
+module type COERCIBLE_ATOM = {
+  include ATOM
+  let coercions: array<coercion<t>>
+}
+
+module MakeCoercible = (
+  Atom: ATOM,
+  Coercions: {
+    let coercions: array<coercion<Atom.t>>
+  },
+): (COERCIBLE_ATOM with type t = Atom.t) => {
+  include Atom
+  let coercions = Coercions.coercions
+}
+
+exception RawVarOrSchematic
+module CombineAtom = (Left: COERCIBLE_ATOM, Right: COERCIBLE_ATOM): {
+  type base =
+    | Left(Left.t)
+    | Right(Right.t)
+    // neither of the below should appear organically. they're purely so we can lower
+    // substitutions to both Left.t and Right.t
+    | Var({idx: int})
+    | Schematic({schematic: int, allowed: array<int>})
+  include COERCIBLE_ATOM with type t = base
+  let match: (t, Left.t => 'a, Right.t => 'a) => 'a
+} => {
+  type base =
+    | Left(Left.t)
+    | Right(Right.t)
+    | Var({idx: int})
+    | Schematic({schematic: int, allowed: array<int>})
+  type t = base
+  type subst = Map.t<int, t>
+  type gen = ref<int>
+  type typeTag<_> += Tag: typeTag<t>
+  let tag = Tag
+  let tagEq = (type a, tag: typeTag<a>): option<eq<t, a>> =>
+    switch tag {
+    | Tag => Some(Refl)
+    | _ => None
+    }
+  let coercions = {
+    let left =
+      Left.coercions->Array.map((Coercion((tag, f))) => Coercion((
+        tag,
+        x => f(x)->Option.map(v => Left(v)),
+      )))
+    let right =
+      Right.coercions->Array.map((Coercion((tag, f))) => Coercion((
+        tag,
+        x => f(x)->Option.map(v => Right(v)),
+      )))
+    Array.concat(left, right)
+  }
+  let match = (t, leftBranch: Left.t => 'a, rightBranch: Right.t => 'a): 'a =>
+    switch t {
+    | Left(s) => leftBranch(s)
+    | Right(s) => rightBranch(s)
+    | _ => throw(RawVarOrSchematic)
+    }
+  let parse = (s, ~scope, ~gen: option<gen>=?) => {
+    Left.parse(s, ~scope, ~gen?)
+    ->Result.map(((r, rest)) => (Left(r), rest))
+    ->Util.Result.or(() =>
+      Right.parse(s, ~scope, ~gen?)->Result.map(((r, rest)) => (Right(r), rest))
+    )
+  }
+  let prettyPrint = (s, ~scope) =>
+    s->match(left => Left.prettyPrint(left, ~scope), right => Right.prettyPrint(right, ~scope))
+  let unify = (s1, s2, ~gen=?) =>
+    switch (s1, s2) {
+    | (Left(s1), Left(s2)) =>
+      Left.unify(s1, s2, ~gen?)->Seq.map(subst => subst->Util.mapMapValues(v => Left(v)))
+    | (Right(s1), Right(s2)) =>
+      Right.unify(s1, s2, ~gen?)->Seq.map(subst => subst->Util.mapMapValues(v => Right(v)))
+    | (_, _) => Seq.empty
+    }
+  let coerceLeft = (left: Left.t): option<Right.t> =>
+    Array.findMap(Right.coercions, (Coercion((tag, f))) =>
+      switch Left.tagEq(tag) {
+      | Some(Refl) => f(left)
+      | None => None
+      }
+    )
+  let coerceRight = (right: Right.t): option<Left.t> => {
+    Array.findMap(Left.coercions, (Coercion((tag, f))) =>
+      switch Right.tagEq(tag) {
+      | Some(Refl) => f(right)
+      | None => None
+      }
+    )
+  }
+  let substitute = (s, subst: subst) => {
+    s->match(
+      left => {
+        let leftSubs =
+          subst->Util.Map.filterMap((_, v) => v->match(left => Some(left), coerceRight))
+        Left(Left.substitute(left, leftSubs))
+      },
+      right => {
+        let rightSubs =
+          subst->Util.Map.filterMap((_, v) => v->match(coerceLeft, right => Some(right)))
+        Right(Right.substitute(right, rightSubs))
+      },
+    )
+  }
+  let upshift = (s, amount: int, ~from=?) =>
+    s->match(
+      left => Left(left->Left.upshift(amount, ~from?)),
+      right => Right(right->Right.upshift(amount, ~from?)),
+    )
+  let lowerVar = idx => Some(Var({idx: idx}))
+  let lowerSchematic = (schematic, allowed) => Some(Schematic({schematic, allowed}))
+  let substDeBruijn = (s, substs: array<option<t>>, ~from=?) =>
+    s->match(
+      left => {
+        let leftSubs = substs->Array.map(o =>
+          o->Option.flatMap(s =>
+            switch s {
+            | Left(s) => Some(s)
+            | Var({idx}) => Left.lowerVar(idx)
+            | Schematic({schematic, allowed}) => Left.lowerSchematic(schematic, allowed)
+            | Right(s) => coerceRight(s)
+            }
+          )
+        )
+        Left(Left.substDeBruijn(left, leftSubs, ~from?))
+      },
+      right => {
+        let rightSubs = substs->Array.map(o =>
+          o->Option.flatMap(s =>
+            switch s {
+            | Right(s) => Some(s)
+            | Var({idx}) => Right.lowerVar(idx)
+            | Schematic({schematic, allowed}) => Right.lowerSchematic(schematic, allowed)
+            | Left(s) => coerceLeft(s)
+            }
+          )
+        )
+        Right(Right.substDeBruijn(right, rightSubs, ~from?))
+      },
+    )
+  let concrete = s => s->match(Left.concrete, Right.concrete)
+}
diff --git a/src/Coercible.res b/src/Coercible.res
new file mode 100644
index 0000000..33ed493
--- /dev/null
+++ b/src/Coercible.res
@@ -0,0 +1,15 @@
+open AtomDef
+
+module StringA = MakeCoercible(
+  StringA.Atom,
+  {
+    let coercions = [Coercion((Symbolic.Atom.tag, s => Some([StringA.String(s)])))]
+  },
+)
+
+module Symbolic = MakeCoercible(
+  Symbolic.Atom,
+  {
+    let coercions = []
+  },
+)
diff --git a/src/CombinedAtom.res b/src/CombinedAtom.res
index 95f3d12..2e7a6da 100644
--- a/src/CombinedAtom.res
+++ b/src/CombinedAtom.res
@@ -1,7 +1,7 @@
 module type ATOM = SExpFunc.ATOM
 exception RawVarOrSchematic
 
-module MakeAtom = (Left: ATOM, Right: ATOM): {
+module MakeAtom = (Left: AtomDef.COERCIBLE_ATOM, Right: AtomDef.COERCIBLE_ATOM): {
   type base =
     | Left(Left.t)
     | Right(Right.t)
@@ -11,100 +11,13 @@ module MakeAtom = (Left: ATOM, Right: ATOM): {
     | Schematic({schematic: int, allowed: array<int>})
   include ATOM with type t = base
   let match: (t, Left.t => 'a, Right.t => 'a) => 'a
-} => {
-  type base =
-    | Left(Left.t)
-    | Right(Right.t)
-    | Var({idx: int})
-    | Schematic({schematic: int, allowed: array<int>})
-  type t = base
-  type subst = Map.t<int, t>
-  type gen = ref<int>
-  let match = (t, leftBranch: Left.t => 'a, rightBranch: Right.t => 'a): 'a =>
-    switch t {
-    | Left(s) => leftBranch(s)
-    | Right(s) => rightBranch(s)
-    | _ => throw(RawVarOrSchematic)
-    }
-  let parse = (s, ~scope, ~gen: option<gen>=?) => {
-    Left.parse(s, ~scope, ~gen?)
-    ->Result.map(((r, rest)) => (Left(r), rest))
-    ->Util.Result.or(() =>
-      Right.parse(s, ~scope, ~gen?)->Result.map(((r, rest)) => (Right(r), rest))
-    )
-  }
-  let prettyPrint = (s, ~scope) =>
-    s->match(left => Left.prettyPrint(left, ~scope), right => Right.prettyPrint(right, ~scope))
-  let unify = (s1, s2, ~gen=?) =>
-    switch (s1, s2) {
-    | (Left(s1), Left(s2)) =>
-      Left.unify(s1, s2, ~gen?)->Seq.map(subst => subst->Util.mapMapValues(v => Left(v)))
-    | (Right(s1), Right(s2)) =>
-      Right.unify(s1, s2, ~gen?)->Seq.map(subst => subst->Util.mapMapValues(v => Right(v)))
-    | (_, _) => Seq.empty
-    }
-  let substitute = (s, subst: subst) => {
-    s->match(
-      left => {
-        let leftSubs = subst->Util.Map.filterMap((_, v) =>
-          switch v {
-          | Left(s) => Some(s)
-          | _ => None
-          }
-        )
-        Left(Left.substitute(left, leftSubs))
-      },
-      right => {
-        let rightSubs = subst->Util.Map.filterMap((_, v) =>
-          switch v {
-          | Right(s) => Some(s)
-          | _ => None
-          }
-        )
-        Right(Right.substitute(right, rightSubs))
-      },
-    )
-  }
-  let upshift = (s, amount: int, ~from=?) =>
-    s->match(
-      left => Left(left->Left.upshift(amount, ~from?)),
-      right => Right(right->Right.upshift(amount, ~from?)),
-    )
-  let lowerVar = idx => Some(Var({idx: idx}))
-  let lowerSchematic = (schematic, allowed) => Some(Schematic({schematic, allowed}))
-  let substDeBruijn = (s, substs: array<option<t>>, ~from=?) =>
-    s->match(
-      left => {
-        let leftSubs = substs->Array.map(s =>
-          switch s {
-          | Some(Left(s)) => Some(s)
-          | Some(Var({idx})) => Left.lowerVar(idx)
-          | Some(Schematic({schematic, allowed})) => Left.lowerSchematic(schematic, allowed)
-          | _ => None
-          }
-        )
-        Left(Left.substDeBruijn(left, leftSubs, ~from?))
-      },
-      right => {
-        let rightSubs = substs->Array.map(s =>
-          switch s {
-          | Some(Right(s)) => Some(s)
-          | Some(Var({idx})) => Right.lowerVar(idx)
-          | Some(Schematic({schematic, allowed})) => Right.lowerSchematic(schematic, allowed)
-          | _ => None
-          }
-        )
-        Right(Right.substDeBruijn(right, rightSubs, ~from?))
-      },
-    )
-  let concrete = s => s->match(Left.concrete, Right.concrete)
-}
+} => AtomDef.CombineAtom(Left, Right)
 
 module type ATOM_VIEW = SExpViewFunc.ATOM_VIEW
 module MakeAtomView = (
-  Left: ATOM,
+  Left: AtomDef.COERCIBLE_ATOM,
   LeftView: ATOM_VIEW with module Atom := Left,
-  Right: ATOM,
+  Right: AtomDef.COERCIBLE_ATOM,
   RightView: ATOM_VIEW with module Atom := Right,
   Combined: module type of MakeAtom(Left, Right),
 ): {
@@ -119,9 +32,9 @@ module MakeAtomView = (
 }
 
 module MakeAtomAndView = (
-  Left: ATOM,
+  Left: AtomDef.COERCIBLE_ATOM,
   LeftView: ATOM_VIEW with module Atom := Left,
-  Right: ATOM,
+  Right: AtomDef.COERCIBLE_ATOM,
   RightView: ATOM_VIEW with module Atom := Right,
 ) => {
   module Atom = MakeAtom(Left, Right)
diff --git a/src/SExpFunc.res b/src/SExpFunc.res
index 6672150..3a3aba2 100644
--- a/src/SExpFunc.res
+++ b/src/SExpFunc.res
@@ -1,19 +1,6 @@
 exception SubstNotCompatible(string)
 
-module type ATOM = {
-  type t
-  type subst = Map.t<int, t>
-  let unify: (t, t, ~gen: ref<int>=?) => Seq.t<subst>
-  let prettyPrint: (t, ~scope: array<string>) => string
-  let parse: (string, ~scope: array<string>, ~gen: ref<int>=?) => result<(t, string), string>
-  let substitute: (t, subst) => t
-  let upshift: (t, int, ~from: int=?) => t
-  // used for when trying to substitute a variable of the wrong type
-  let lowerVar: int => option<t>
-  let lowerSchematic: (int, array<int>) => option<t>
-  let substDeBruijn: (t, array<option<t>>, ~from: int=?) => t
-  let concrete: t => bool
-}
+module type ATOM = AtomDef.ATOM
 
 module IntCmp = Belt.Id.MakeComparable({
   type t = int
diff --git a/src/Scratch.res b/src/Scratch.res
index 9232766..94ea949 100644
--- a/src/Scratch.res
+++ b/src/Scratch.res
@@ -43,9 +43,9 @@ module TheoremS = Editable.TextArea(Theorem.Make(HOTerm, HOTerm, HOTermJView, DL
 module ConfS = ConfigBlock.Make(HOTerm, HOTerm)
 
 module StringSymbol = CombinedAtom.MakeAtomAndView(
-  StringA.Atom,
+  Coercible.StringA,
   StringA.AtomView,
-  Symbolic.Atom,
+  Coercible.Symbolic,
   Symbolic.AtomView,
 )
 module StringSExp = SExpFunc.Make(StringSymbol.Atom)
diff --git a/src/StringA.res b/src/StringA.res
index 440c747..23c7128 100644
--- a/src/StringA.res
+++ b/src/StringA.res
@@ -12,8 +12,16 @@ type meta = string
 type schematic = int
 
 module Atom = {
+  open AtomDef
   type t = t
   type subst = Map.t<schematic, t>
+  type typeTag<_> += Tag: typeTag<t>
+  let tag = Tag
+  let tagEq = (type a, tag: typeTag<a>): option<eq<t, a>> =>
+    switch tag {
+    | Tag => Some(Refl)
+    | _ => None
+    }
   let substitute = (term: t, subst: subst) =>
     Array.flatMap(term, piece => {
       switch piece {
@@ -482,12 +490,6 @@ module AtomView = {
       </span>
     }
 
-  let makeMeta = (str: string) =>
-    <span className="rule-binder">
-      {React.string(str)}
-      {React.string(".")}
-    </span>
-
   let parenthesise = f =>
     [
       <span className="symbol" key={"-1"}> {React.string("(")} </span>,
diff --git a/src/StringA.resi b/src/StringA.resi
index 6a92125..a6492c6 100644
--- a/src/StringA.resi
+++ b/src/StringA.resi
@@ -4,5 +4,5 @@ type rec piece =
   | Schematic({schematic: int, allowed: array<int>})
 type t = array<piece>
 
-module Atom: SExpFunc.ATOM with type t = t
+module Atom: AtomDef.ATOM with type t = t
 module AtomView: SExpViewFunc.ATOM_VIEW with module Atom := Atom
diff --git a/src/StringAxiomSet.res b/src/StringAxiomSet.res
index eda40f1..f455d97 100644
--- a/src/StringAxiomSet.res
+++ b/src/StringAxiomSet.res
@@ -1,9 +1,9 @@
 open Component
 
 module StringSymbol = CombinedAtom.MakeAtomAndView(
-  StringA.Atom,
+  Coercible.StringA,
   StringA.AtomView,
-  Symbolic.Atom,
+  Coercible.Symbolic,
   Symbolic.AtomView,
 )
 module StringSExp = SExpFunc.Make(StringSymbol.Atom)
diff --git a/src/Symbolic.res b/src/Symbolic.res
index 7ffba16..47a9827 100644
--- a/src/Symbolic.res
+++ b/src/Symbolic.res
@@ -1,7 +1,15 @@
 type t = string
 module Atom = {
+  open AtomDef
   type t = string
   type subst = Map.t<int, string>
+  type typeTag<_> += Tag: typeTag<t>
+  let tag = Tag
+  let tagEq = (type a, tag: typeTag<a>): option<eq<t, a>> =>
+    switch tag {
+    | Tag => Some(Refl)
+    | _ => None
+    }
   let unify = (a, b, ~gen as _=?) =>
     if a == b {
       Seq.once(Map.make())
diff --git a/src/Symbolic.resi b/src/Symbolic.resi
index 9e9279f..1a2ca55 100644
--- a/src/Symbolic.resi
+++ b/src/Symbolic.resi
@@ -1,3 +1,3 @@
 type t = string
-module Atom: SExpFunc.ATOM with type t = t
+module Atom: AtomDef.ATOM with type t = t
 module AtomView: SExpViewFunc.ATOM_VIEW with module Atom := Atom