2 files changed, 26 insertions, 3 deletions
diff --git a/src/Data/Expr/SharingRecovery.hs b/src/Data/Expr/SharingRecovery.hs
index 34fd4ec..95524dd 100644
--- a/src/Data/Expr/SharingRecovery.hs
+++ b/src/Data/Expr/SharingRecovery.hs
@@ -1,6 +1,7 @@
 module Data.Expr.SharingRecovery (
   -- * Sharing recovery
   sharingRecovery,
+  sharingRecoveryUnsafe,
 
   -- * Expressions
   PHOASExpr(..),
diff --git a/src/Data/Expr/SharingRecovery/Internal.hs b/src/Data/Expr/SharingRecovery/Internal.hs
index adf655d..9d00355 100644
--- a/src/Data/Expr/SharingRecovery/Internal.hs
+++ b/src/Data/Expr/SharingRecovery/Internal.hs
@@ -78,7 +78,10 @@ class Functor1 f => Traversable1 f where
 --
 -- * @v@ is the type of variables in the expression. A PHOAS expression is
 --     required to be parametric in the @v@ parameter; the only place you will
---     obtain a @v@ is inside a @PHOASLam@ function body.
+--     obtain a @v@ is inside a @PHOASLam@ function body. Even if you use
+--     'sharingRecoveryUnsafe' which allows you to pass in a monomorphic
+--     expression with 'Tag', it is expressly disallowed to inspect or
+--     manipulate 'Tag' values.
 --
 -- * @f@ should be your type of operations for your language. It is indexed by
 --     the type of subexpressions and the result type of the operation; thus, it
@@ -109,6 +112,12 @@ data PHOASExpr typ v f t where
   PHOASLam :: typ (a -> b) -> typ a -> (v a -> PHOASExpr typ v f b) -> PHOASExpr typ v f (a -> b)
   PHOASVar :: typ t -> v t -> PHOASExpr typ v f t
 
+-- | Tag values identify a variable, and are created in the sharing recovery
+-- process (in 'pruneExpr'). Applying the sharing recovery algorithm to a term
+-- with manually constructed Tag values, or inspecting Tag values in the
+-- expression and computing with them or branching based on them, results in
+-- "impossible terms" and behaviour of the sharing recovery algorithm is
+-- undefined. Consider Tag an opaque value.
 newtype Tag t = Tag Natural
   deriving (Show, Eq)
   deriving (Hashable) via Natural
@@ -188,6 +197,11 @@ pruneExpr term =
   let ((term', _), (_, mp)) = runState (pruneExpr' term) (0, mempty)
   in (mp, term')
 
+pruneExprUnsafe :: Traversable1 f => PHOASExpr typ Tag f t -> (OccMap typ f, PExpr0 typ f t)
+pruneExprUnsafe term =
+  let ((term', _), (_, mp)) = runState (pruneExpr' term) (0, mempty)
+  in (mp, term')
+
 -- | Returns pruned expression with its height.
 -- State: (ID generator, occurrence map being accumulated)
 pruneExpr' :: Traversable1 f => PHOASExpr typ Tag f t -> State (Natural, OccMap typ f) (PExpr0 typ f t, Natural)
@@ -467,8 +481,16 @@ retypeExpr' env (UBVar ty idx) =
 -- abstract syntax form to a well-typed well-scoped De Bruijn expression with
 -- explicit let-bindings.
 sharingRecovery :: (Traversable1 f, TestEquality typ) => (forall v. PHOASExpr typ v f t) -> BExpr typ '[] f t
-sharingRecovery e =
-  let (occmap, pexpr) = pruneExpr e
+sharingRecovery = sharingRecoveryUnsafe
+
+-- | The 'sharingRecovery' function instantiates the @v@ parameter to 'Tag',
+-- and this function is provided as a convenience in case constructing a
+-- polymorphic expression value is difficult. However, it is /disallowed/ to
+-- inspect or manipulate 'Tag' values obtained by lambda abstraction inside the
+-- expression. Violating this rule results in undefined behaviour.
+sharingRecoveryUnsafe :: (Traversable1 f, TestEquality typ) => PHOASExpr typ Tag f t -> BExpr typ '[] f t
+sharingRecoveryUnsafe e =
+  let (occmap, pexpr) = pruneExprUnsafe e
       lexpr = floatExpr occmap pexpr
       ubexpr = lowerExpr lexpr
   in -- trace ("PExpr: " ++ prettyPExpr 0 pexpr "") $