From 250077cf93737a5dcf62acfce557821f26b1e505 Mon Sep 17 00:00:00 2001
From: LeitMoth <col.phillips2004@gmail.com>
Date: Sat, 21 Sep 2024 18:39:14 -0500
Subject: [PATCH] Exploration of the Lower Your Guards paper (#401)

* Init stack project explore/lower-your-guards

* lyg test language parser works

* basic gaurd tree desugaring

* add basic uncovered set function

* add pair datacons and pretty printer

* inhabitants N function kind of works

* Add types

* inhabitants mostly working

* pretty print patterns

* start work on fresh

* Fresh works!

* Fixed arg id bug, fresh actually works now!

* implement Show to make some printing better

* done for day. Strange behavoir, check complex2/3

* switch to MaybeT / cleanup

* nested patterns work! Still must tune up Int literal stuff, also see type equal TODO

* positive info works

* positive info and integer negative info work!

* no longer list all dataconstructors anyway when covered

* remove old negative only inhab code

* cleanup comments in inhab hs

* remove old TODO message

* change refinement type formulas datatype to match paper

Originally, I thought I had outsmarted the paper
Not so, they broke things up into `Formula`s and `Literal`s for a
good reason, which I rediscovered

* auto run on files in test folder

* huge overhaul to Inhabitants.hs. more to go, but significant cleanup done

* refactor / cleanup adding constraints

* refactor addLiteral previously known as (<+>) for readability

* rename matching to onVar to avoid confusion

* major cleanup to inhabitants + lots of documentation

* cleanup Pos suffix, all functions use positive info now

* small inhabitant cleanup + ready for big changes

* play with map merge instead of logic solver idea in inhab2

* add Annotated tree and redundancy checking

* attempt my own version of exhaustiveness checking

* BROKEN, about to try list monad

* match tree broken, might be a lost cause

* combined UA function done!

* Properly use Fresh moand in Inhabitation checks

Before I was manually threading state
By rewriting a few things, Fresh and Monad [] can coexist
Really hope there are no regressions, I didn't spot any

* add comments, prepare for simplification

* add throol testcase, proves necessity of cart prod

* create Possibilities newtype for lists, to make things more clear

* cleanup inhabitants

* document + move Possibilities to a new file

* attempting to remove MatchInt (CURRENTLY BROKEN)

* add int as opaque type, not weird exception (BROKEN)

* inhab works again! needs cleanup

* remove traces of IntLit, ready for MatchInfo merge

* introduce HerebyBe, reads better, hopefully no regressions

* Switch to TypedVar everywhere, add Be to MatchInfo

* cleanup, commit to TypedVar

* More cleanup

* document bug, already fixed

* clean up bug stuff / test case for termeq bug

* small cleanup before merge

* Remove unneeded todo

* Restyle Exploration of the Lower Your Guards paper (#402)

* Restyled by fourmolu

* Restyled by hlint

---------

Co-authored-by: Restyled.io <commits@restyled.io>

* Restyled by fourmolu (#403)

Co-authored-by: Restyled.io <commits@restyled.io>

---------

Co-authored-by: restyled-io[bot] <32688539+restyled-io[bot]@users.noreply.github.com>
Co-authored-by: Restyled.io <commits@restyled.io>
---
 explore/lower-your-guards/LICENSE             |   0
 explore/lower-your-guards/Setup.hs            |   3 +
 explore/lower-your-guards/hie.yaml            |   2 +
 .../lower-your-guards/lower-your-guards.cabal |  50 ++++
 explore/lower-your-guards/src/Annotated.hs    |  21 ++
 explore/lower-your-guards/src/Fresh.hs        |  44 ++++
 explore/lower-your-guards/src/GuardTree.hs    |  50 ++++
 explore/lower-your-guards/src/Inhabitants.hs  | 225 ++++++++++++++++++
 explore/lower-your-guards/src/Main.hs         | 151 ++++++++++++
 explore/lower-your-guards/src/MatchInfo.hs    |  16 ++
 explore/lower-your-guards/src/MatchTree.hs    | 162 +++++++++++++
 explore/lower-your-guards/src/Parse.hs        | 149 ++++++++++++
 explore/lower-your-guards/src/Play.hs         |  66 +++++
 .../lower-your-guards/src/Possibilities.hs    |  64 +++++
 explore/lower-your-guards/src/Types.hs        |  92 +++++++
 explore/lower-your-guards/src/UA.hs           |  52 ++++
 explore/lower-your-guards/src/Uncovered.hs    |  46 ++++
 explore/lower-your-guards/stack.yaml          |  68 ++++++
 explore/lower-your-guards/test/bool1.disc     |   3 +
 explore/lower-your-guards/test/bool2.disc     |   5 +
 explore/lower-your-guards/test/complex1.disc  |   4 +
 explore/lower-your-guards/test/complex2.disc  |   6 +
 explore/lower-your-guards/test/complex22.disc |  17 ++
 explore/lower-your-guards/test/complex3.disc  |   3 +
 explore/lower-your-guards/test/complex4.disc  |   4 +
 explore/lower-your-guards/test/complex5.disc  |   3 +
 explore/lower-your-guards/test/either.disc    |   5 +
 explore/lower-your-guards/test/pair1.disc     |   4 +
 explore/lower-your-guards/test/pair2.disc     |   4 +
 explore/lower-your-guards/test/pair3.disc     |   3 +
 explore/lower-your-guards/test/pair4.disc     |  12 +
 explore/lower-your-guards/test/t1.disc        |  12 +
 explore/lower-your-guards/test/test1.disc     |   6 +
 explore/lower-your-guards/test/test2.disc     |   3 +
 explore/lower-your-guards/test/throol1.disc   |   2 +
 explore/lower-your-guards/test/throol2.disc   |   3 +
 explore/lower-your-guards/test/triple1.disc   |   4 +
 37 files changed, 1364 insertions(+)
 create mode 100644 explore/lower-your-guards/LICENSE
 create mode 100644 explore/lower-your-guards/Setup.hs
 create mode 100644 explore/lower-your-guards/hie.yaml
 create mode 100644 explore/lower-your-guards/lower-your-guards.cabal
 create mode 100644 explore/lower-your-guards/src/Annotated.hs
 create mode 100644 explore/lower-your-guards/src/Fresh.hs
 create mode 100644 explore/lower-your-guards/src/GuardTree.hs
 create mode 100644 explore/lower-your-guards/src/Inhabitants.hs
 create mode 100644 explore/lower-your-guards/src/Main.hs
 create mode 100644 explore/lower-your-guards/src/MatchInfo.hs
 create mode 100644 explore/lower-your-guards/src/MatchTree.hs
 create mode 100644 explore/lower-your-guards/src/Parse.hs
 create mode 100644 explore/lower-your-guards/src/Play.hs
 create mode 100644 explore/lower-your-guards/src/Possibilities.hs
 create mode 100644 explore/lower-your-guards/src/Types.hs
 create mode 100644 explore/lower-your-guards/src/UA.hs
 create mode 100644 explore/lower-your-guards/src/Uncovered.hs
 create mode 100644 explore/lower-your-guards/stack.yaml
 create mode 100644 explore/lower-your-guards/test/bool1.disc
 create mode 100644 explore/lower-your-guards/test/bool2.disc
 create mode 100644 explore/lower-your-guards/test/complex1.disc
 create mode 100644 explore/lower-your-guards/test/complex2.disc
 create mode 100644 explore/lower-your-guards/test/complex22.disc
 create mode 100644 explore/lower-your-guards/test/complex3.disc
 create mode 100644 explore/lower-your-guards/test/complex4.disc
 create mode 100644 explore/lower-your-guards/test/complex5.disc
 create mode 100644 explore/lower-your-guards/test/either.disc
 create mode 100644 explore/lower-your-guards/test/pair1.disc
 create mode 100644 explore/lower-your-guards/test/pair2.disc
 create mode 100644 explore/lower-your-guards/test/pair3.disc
 create mode 100644 explore/lower-your-guards/test/pair4.disc
 create mode 100644 explore/lower-your-guards/test/t1.disc
 create mode 100644 explore/lower-your-guards/test/test1.disc
 create mode 100644 explore/lower-your-guards/test/test2.disc
 create mode 100644 explore/lower-your-guards/test/throol1.disc
 create mode 100644 explore/lower-your-guards/test/throol2.disc
 create mode 100644 explore/lower-your-guards/test/triple1.disc

diff --git a/explore/lower-your-guards/LICENSE b/explore/lower-your-guards/LICENSE
new file mode 100644
index 00000000..e69de29b
diff --git a/explore/lower-your-guards/Setup.hs b/explore/lower-your-guards/Setup.hs
new file mode 100644
index 00000000..e8ef27db
--- /dev/null
+++ b/explore/lower-your-guards/Setup.hs
@@ -0,0 +1,3 @@
+import Distribution.Simple
+
+main = defaultMain
diff --git a/explore/lower-your-guards/hie.yaml b/explore/lower-your-guards/hie.yaml
new file mode 100644
index 00000000..4ef275e0
--- /dev/null
+++ b/explore/lower-your-guards/hie.yaml
@@ -0,0 +1,2 @@
+cradle:
+  stack:
diff --git a/explore/lower-your-guards/lower-your-guards.cabal b/explore/lower-your-guards/lower-your-guards.cabal
new file mode 100644
index 00000000..59c08ea9
--- /dev/null
+++ b/explore/lower-your-guards/lower-your-guards.cabal
@@ -0,0 +1,50 @@
+cabal-version:       2.2
+
+name:                lower-your-guards
+version:             0.1.0.0
+license:             BSD-3-Clause
+license-file:        LICENSE
+author:              Colin Phillips
+maintainer:          col.phillips2004@gmail.com
+copyright:           2024 Colin Phillips
+category:            Language
+build-type:          Simple
+
+executable lower-your-guards
+  hs-source-dirs:      src
+  main-is:             Main.hs
+  default-language:    Haskell2010
+  build-depends:       base >= 4.7 && < 5,
+                       megaparsec >= 6.1.1 && < 9.7,
+                       text >= 2.0.2 && < 2.1,
+                       pretty-simple,
+                       containers,
+                       mtl,
+                       transformers,
+                       directory
+  ghc-options:         -Wall
+                       -Wcompat
+                       -Widentities
+                       -Wincomplete-record-updates
+                       -Wincomplete-uni-patterns
+                       -Wmissing-export-lists
+                       -Wmissing-home-modules
+                       -Wpartial-fields
+                       -Wredundant-constraints
+  default-extensions:  GADTs,
+                       OverloadedStrings,
+                       LambdaCase,
+                       TupleSections
+  other-modules:       Parse,
+                       GuardTree,
+                       Uncovered
+                       Inhabitants,
+                       Inhabitants2,
+                       Types,
+                       Fresh,
+                       Play,
+                       Annotated,
+                       MatchTree,
+                       UA,
+                       Possibilities,
+                       MatchInfo
diff --git a/explore/lower-your-guards/src/Annotated.hs b/explore/lower-your-guards/src/Annotated.hs
new file mode 100644
index 00000000..70def529
--- /dev/null
+++ b/explore/lower-your-guards/src/Annotated.hs
@@ -0,0 +1,21 @@
+{-# OPTIONS_GHC -Wno-missing-export-lists #-}
+
+module Annotated where
+
+import qualified GuardTree as G
+import MatchInfo
+import qualified Uncovered as U
+
+data Ant where
+  Grhs :: U.RefinementType -> Int -> Ant
+  Branch :: Ant -> Ant -> Ant
+
+annotated :: U.RefinementType -> G.Gdt -> Ant
+annotated ref gdt = case gdt of
+  G.Grhs i -> Grhs ref i
+  G.Branch t1 t2 -> Branch (annotated ref t1) (annotated (U.uncovered ref t1) t2)
+  G.Guarded (var, g) t -> case g of
+    G.GMatch k args -> annotated (ref `U.liftAndLit` varInfo (Match k args)) t
+    G.GWas new -> annotated (ref `U.liftAndLit` varInfo (WasOriginally new)) t
+   where
+    varInfo = U.Info var
diff --git a/explore/lower-your-guards/src/Fresh.hs b/explore/lower-your-guards/src/Fresh.hs
new file mode 100644
index 00000000..370fdd89
--- /dev/null
+++ b/explore/lower-your-guards/src/Fresh.hs
@@ -0,0 +1,44 @@
+{-# OPTIONS_GHC -Wno-missing-export-lists #-}
+
+module Fresh where
+
+import Control.Monad.State
+import Data.List.NonEmpty (NonEmpty ((:|)))
+import qualified Data.List.NonEmpty as NE
+import qualified Data.Map as M
+import qualified Data.Text as T
+
+type Fresh = State (NE.NonEmpty Frame)
+
+data Frame = Frame {fBound :: M.Map VarID (Maybe T.Text), fNextID :: Int}
+  deriving (Show, Eq, Ord)
+
+newtype VarID = Var Int
+  deriving (Show, Eq, Ord)
+
+blank :: NE.NonEmpty Frame
+blank = Frame {fBound = M.empty, fNextID = 0} :| []
+
+fresh :: Maybe T.Text -> Fresh VarID
+fresh mName = do
+  Frame {fBound = bound, fNextID = nextID} <- gets NE.head
+  t <- gets NE.tail
+  let h = Frame {fBound = M.insert (Var nextID) mName bound, fNextID = nextID + 1}
+  put $ h :| t
+  return (Var nextID)
+
+enterScope :: Fresh ()
+enterScope = do
+  nextID <- gets (fNextID . NE.head)
+  stack <- get
+  put $ Frame {fBound = M.empty, fNextID = nextID} :| NE.toList stack
+
+exitScope :: Fresh ()
+exitScope = modify (NE.fromList . NE.tail)
+
+performInNewScope :: Fresh a -> Fresh a
+performInNewScope m = do
+  enterScope
+  a <- m
+  exitScope
+  return a
diff --git a/explore/lower-your-guards/src/GuardTree.hs b/explore/lower-your-guards/src/GuardTree.hs
new file mode 100644
index 00000000..bfbee784
--- /dev/null
+++ b/explore/lower-your-guards/src/GuardTree.hs
@@ -0,0 +1,50 @@
+{-# OPTIONS_GHC -Wno-missing-export-lists #-}
+
+module GuardTree where
+
+import Control.Monad (replicateM, zipWithM)
+import Data.List.NonEmpty (NonEmpty (..))
+import qualified Data.List.NonEmpty as NE
+import qualified Fresh as F
+import MatchInfo
+import qualified Parse as P
+import qualified Types as Ty
+
+data Gdt where
+  Grhs :: Int -> Gdt
+  Branch :: Gdt -> Gdt -> Gdt
+  Guarded :: (TypedVar, Guard) -> Gdt -> Gdt
+  deriving (Show, Eq)
+
+data Guard where
+  GMatch :: Ty.DataConstructor -> [TypedVar] -> Guard
+  GWas :: TypedVar -> Guard
+  deriving (Show, Eq)
+
+enumerate :: NonEmpty a -> NonEmpty (Int, a)
+enumerate = NE.zip (1 :| [2 ..])
+
+desugarClauses :: [F.VarID] -> NonEmpty P.Clause -> F.Fresh Gdt
+desugarClauses args clauses = do
+  cl <- mapM (desugarClause args) (enumerate clauses)
+  return $ foldr1 Branch cl
+
+desugarClause :: [F.VarID] -> (Int, P.Clause) -> F.Fresh Gdt
+desugarClause args (i, P.Clause pat typeIn _) = do
+  let x1 = head args -- we only suport 1 arg for this toy lyg
+  guards <- desugarMatch (x1, typeIn) pat
+  return $ foldr Guarded (Grhs i) guards
+
+desugarMatch :: TypedVar -> P.Pattern -> F.Fresh [(TypedVar, Guard)]
+desugarMatch var@(_, ty) pat = do
+  case pat of
+    P.PWild -> return []
+    P.PVar name -> do
+      x <- F.fresh (Just name)
+      let xTy = (x, ty)
+      return [(xTy, GWas var)]
+    P.PMatch dataCon subPats -> do
+      ys <- replicateM (length subPats) (F.fresh Nothing)
+      let typedYs = zip ys (Ty.dcTypes dataCon)
+      guards <- zipWithM desugarMatch typedYs subPats
+      return $ (var, GMatch dataCon typedYs) : concat guards
diff --git a/explore/lower-your-guards/src/Inhabitants.hs b/explore/lower-your-guards/src/Inhabitants.hs
new file mode 100644
index 00000000..f18231d1
--- /dev/null
+++ b/explore/lower-your-guards/src/Inhabitants.hs
@@ -0,0 +1,225 @@
+{-# OPTIONS_GHC -Wno-missing-export-lists #-}
+
+module Inhabitants where
+
+import qualified Annotated as A
+import Control.Applicative
+import Control.Monad (foldM, forM, guard, replicateM)
+import Control.Monad.Trans (lift)
+import Control.Monad.Trans.Maybe
+import Data.List (nub, partition)
+import Data.Maybe (catMaybes, isJust, listToMaybe, mapMaybe)
+import qualified Data.Set as S
+import qualified Fresh as F
+import MatchInfo
+import qualified Possibilities as Poss
+import qualified Types as Ty
+import qualified Uncovered as U
+
+data InhabPat where
+  IPIs :: Ty.DataConstructor -> [InhabPat] -> InhabPat
+  IPNot :: [Ty.DataConstructor] -> InhabPat
+  deriving (Show, Eq, Ord)
+
+type NormRefType = (U.Context, [ConstraintFor])
+
+type ConstraintFor = (TypedVar, Constraint)
+
+data Constraint where
+  MatchInfo :: MatchInfo -> Constraint
+  deriving (Show, Eq, Ord)
+
+-- old, use UA
+accessableRedundant :: A.Ant -> U.Context -> F.Fresh ([Int], [Int])
+accessableRedundant ant args = case ant of
+  A.Grhs ref i -> do
+    nothing <- Poss.none <$> genInhab ref args
+    return $
+      if nothing
+        then ([], [i])
+        else ([i], [])
+  A.Branch a1 a2 -> mappend <$> accessableRedundant a1 args <*> accessableRedundant a2 args
+
+-- Resolves term equalities, finding the leftmost id for a variable
+-- I believe I3 of section 3.4 allows us to
+-- do a linear scan from right to left
+lookupVar :: TypedVar -> [ConstraintFor] -> TypedVar
+lookupVar x = foldr getNextId x
+ where
+  getNextId (x', MatchInfo (WasOriginally y)) | x' == x = const y
+  getNextId _ = id
+
+alistLookup :: (Eq a) => a -> [(a, b)] -> [b]
+alistLookup a = map snd . filter ((== a) . fst)
+
+onVar :: TypedVar -> [ConstraintFor] -> [Constraint]
+onVar x cs = alistLookup (lookupVar x cs) cs
+
+genInhab :: U.RefinementType -> U.Context -> F.Fresh (Poss.Possibilities InhabPat)
+genInhab (ctx, formula) args = do
+  nrefs <- S.toList <$> normalize (ctx, []) formula
+  genInhabNorm nrefs args
+
+genInhabNorm :: [NormRefType] -> U.Context -> F.Fresh (Poss.Possibilities InhabPat)
+genInhabNorm nrefs args = do
+  n <- sequence [findVarInhabitants arg nref | nref <- nrefs, arg <- args]
+  return $ Poss.anyOf n
+
+-- Sanity check: are we giving the dataconstructor the
+-- correct number of arguments?
+mkIPMatch :: Ty.DataConstructor -> [InhabPat] -> InhabPat
+mkIPMatch k pats =
+  if length (Ty.dcTypes k) /= length pats
+    then error $ "Wrong number of DataCon args" ++ show (k, pats)
+    else IPIs k pats
+
+findVarInhabitants :: TypedVar -> NormRefType -> F.Fresh (Poss.Possibilities InhabPat)
+findVarInhabitants var nref@(_, cns) =
+  case posMatch of
+    Just (k, args) -> do
+      argPats <- forM args (`findVarInhabitants` nref)
+      let argPossibilities = Poss.allCombinations argPats
+
+      return (mkIPMatch k <$> argPossibilities)
+    Nothing -> case nub negMatch of
+      [] -> Poss.retSingle $ IPNot []
+      neg -> do
+        case getDataCons var of
+          Nothing -> Poss.retSingle $ IPNot neg
+          Just dcs ->
+            do
+              let tryAddDc dc = do
+                    newVars <- mkNewVars (Ty.dcTypes dc)
+                    runMaybeT (nref `addConstraint` (var, MatchInfo $ Match dc newVars))
+
+              -- Try to add a positive constraint for each data constructor
+              -- to the current nref
+              -- If any of these additions succeed, save that nref,
+              -- it now has positive information
+              posNrefs <- catMaybes <$> forM dcs tryAddDc
+
+              if null posNrefs
+                then Poss.retSingle $ IPNot []
+                else Poss.anyOf <$> forM posNrefs (findVarInhabitants var)
+ where
+  constraintsOnX = onVar var cns
+  posMatch = listToMaybe $ mapMaybe (\case MatchInfo (Match k ys) -> Just (k, ys); _ -> Nothing) constraintsOnX
+  negMatch = mapMaybe (\case MatchInfo (Not k) -> Just k; _ -> Nothing) constraintsOnX
+
+normalize :: NormRefType -> U.Formula -> F.Fresh (S.Set NormRefType)
+normalize nref (f1 `U.And` f2) = do
+  n1 <- S.toList <$> normalize nref f1
+  rest <- traverse (`normalize` f2) n1
+  return $ S.unions rest
+normalize nref (f1 `U.Or` f2) = S.union <$> normalize nref f1 <*> normalize nref f2
+normalize nref (U.Literal fl) = maybe S.empty S.singleton <$> runMaybeT (nref `addLiteral` fl)
+
+addLiteral :: NormRefType -> U.Literal -> MaybeT F.Fresh NormRefType
+addLiteral n@(context, constraints) flit = case flit of
+  U.F -> MaybeT $ pure Nothing
+  U.T -> return n
+  U.Info x info@(Match _ args) -> (context ++ args, constraints) `addConstraint` (x, MatchInfo info)
+  U.Info x info@(Not _) -> (context, constraints) `addConstraint` (x, MatchInfo info)
+  U.Info x info@(WasOriginally _) -> (context ++ [x], constraints) `addConstraint` (x, MatchInfo info)
+
+addConstraints :: NormRefType -> [ConstraintFor] -> MaybeT F.Fresh NormRefType
+addConstraints = foldM addConstraint
+
+addConstraint :: NormRefType -> ConstraintFor -> MaybeT F.Fresh NormRefType
+addConstraint nref@(_, cns) (x, c) = do
+  breakIf $ any (conflictsWith c) (onVar x cns)
+  addConstraintHelper nref (lookupVar x cns, c)
+
+addConstraintHelper :: NormRefType -> ConstraintFor -> MaybeT F.Fresh NormRefType
+addConstraintHelper nref@(ctx, cns) cf@(origX, c) = case c of
+  MatchInfo info -> case info of
+    --- Equation (10)
+    Match k args -> do
+      case getConstructorArgs k (onVar origX cns) of
+        -- 10c -- NOTE: This is where we would add type constraints, if we needed them
+        Just args' ->
+          addConstraints
+            nref
+            (zipWith (\a b -> (a, MatchInfo (WasOriginally b))) args args')
+        Nothing -> return added
+    --- Equation (11)
+    Not _ -> do
+      inh <- lift (inhabited added origX)
+      guard inh -- ensure that origX is still inhabited, as per I2
+      return added
+    -- Equation (14)
+    WasOriginally y -> do
+      let origY = lookupVar y cns
+      if origX == origY
+        then return nref
+        else do
+          let (noX', withX') = partition ((/= origX) . fst) cns
+          addConstraints (ctx, noX' ++ [cf]) (substituteVarIDs origY origX withX')
+ where
+  added = (ctx, cns ++ [cf])
+
+-----
+----- Helper functions for adding constraints:
+-----
+
+breakIf :: (Alternative f) => Bool -> f ()
+breakIf = guard . not
+
+-- Returns a predicate that returns true if another
+-- constraint conflicts with the one given.
+-- This alone is not sufficient to test
+-- if a constraint can be added, but it
+-- filters out the easy negatives early on
+conflictsWith :: Constraint -> (Constraint -> Bool)
+conflictsWith c = case c of
+  MatchInfo info -> case info of
+    Match k _ -> \case
+      MatchInfo (Match k' _) | k /= k' -> True -- 10a
+      MatchInfo (Not k') | k == k' -> True -- 10b
+      _ -> False
+    Not k -> \case
+      MatchInfo (Match k' _) | k == k' -> True -- 11a
+      _ -> False
+    WasOriginally _ -> const False
+
+-- TermEquality _ -> const False
+
+-- Search for a MatchDataCon that is matching on k specifically
+-- (there should be at most one, see I4 in section 3.4)
+-- and if it exists, return the variable ids of its arguments
+getConstructorArgs :: Ty.DataConstructor -> [Constraint] -> Maybe [TypedVar]
+getConstructorArgs k cfs =
+  listToMaybe $
+    mapMaybe (\case MatchInfo (Match k' vs) | k' == k -> Just vs; _ -> Nothing) cfs
+
+-- substituting y *for* x
+-- ie replace the second with the first, replace x with y
+substituteVarIDs :: TypedVar -> TypedVar -> [ConstraintFor] -> [ConstraintFor]
+substituteVarIDs y x = map (\case (x', c) | x' == x -> (y, c); cf -> cf)
+
+-- Deals with I2 form section 3.4
+-- if a variable in the context has a resolvable type, there must be at least one constructor
+-- which can be instantiated without contradiction of the refinement type
+-- This function tests if this is true
+-- NOTE: we may eventually have type constraints
+-- and we would need to worry pulling them from nref here
+inhabited :: NormRefType -> TypedVar -> F.Fresh Bool
+inhabited n var@(_, xTy) = case Ty.dataCons xTy of
+  Nothing -> return True -- assume opaque types are inhabited
+  Just constructors -> do
+    or <$> mapM (instantiate n var) constructors
+
+mkNewVars :: [Ty.Type] -> F.Fresh [TypedVar]
+mkNewVars tys = do
+  newVarIDs <- replicateM (length tys) (F.fresh Nothing)
+  return $ zip newVarIDs tys
+
+-- Attempts to "instantiate" a match of the dataconstructor k on x
+-- If we can add the MatchDataCon constraint to the normalized refinement
+-- type without contradiction (a Nothing value),
+-- then x is inhabited by k and we return true
+instantiate :: NormRefType -> TypedVar -> Ty.DataConstructor -> F.Fresh Bool
+instantiate (ctx, cns) var k = do
+  newVars <- mkNewVars $ Ty.dcTypes k
+  let attempt = (ctx ++ newVars, cns) `addConstraint` (var, MatchInfo $ Match k newVars)
+  isJust <$> runMaybeT attempt
diff --git a/explore/lower-your-guards/src/Main.hs b/explore/lower-your-guards/src/Main.hs
new file mode 100644
index 00000000..c75727da
--- /dev/null
+++ b/explore/lower-your-guards/src/Main.hs
@@ -0,0 +1,151 @@
+module Main (main, pUA, pFullUA, nicePattern, evalGdt, pfg, pdu, pda, pdun, pduip, inhabNice) where
+
+import qualified Annotated as A
+import Control.Monad.State
+import Data.List (sort)
+import Data.List.NonEmpty (fromList)
+import qualified Data.List.NonEmpty as NE
+import qualified Data.Set as S
+import Data.Text (Text)
+import qualified Data.Text as T
+import qualified Data.Text.IO as TIO
+import qualified Fresh as F
+import qualified GuardTree as G
+import qualified Inhabitants as I
+import qualified Parse as P
+import qualified Possibilities as Poss
+import System.Directory (listDirectory)
+import Text.Megaparsec (eof, errorBundlePretty, many, runParser)
+import Text.Pretty.Simple (pPrint)
+import qualified Types as Ty
+import qualified UA
+import qualified Uncovered as U
+
+parseFile :: String -> IO [P.FunctionDef]
+parseFile file = do
+  let pf = P.sc *> many P.pFn <* eof
+  contents <- TIO.readFile file
+  case runParser pf file contents of
+    Left e -> error $ errorBundlePretty e
+    Right defs -> return defs
+
+handleFunctions :: ([P.Clause] -> Ty.Type -> a) -> String -> IO [(Text, a)]
+handleFunctions handler file = do
+  defs <- parseFile file
+  return $
+    map
+      ( \(P.FunctionDef (P.FunctionDecl name tIn _) clauses) ->
+          (name, handler clauses tIn)
+      )
+      defs
+
+main :: IO ()
+main = do
+  files <- listDirectory "./test"
+  let fileNames = map ("test/" ++) . sort $ files
+  sequence_ $ concatMap (\f -> [pPrint f, pFullUA f >>= pPrint]) fileNames
+
+desGdt :: [P.Clause] -> F.Fresh G.Gdt
+desGdt clauses = do
+  x1 <- F.fresh (Just "x_1")
+  G.desugarClauses [x1] . fromList $ clauses
+
+evalGdt :: [P.Clause] -> G.Gdt
+evalGdt clauses = evalState (desGdt clauses) F.blank
+
+runGdt :: [P.Clause] -> (G.Gdt, NE.NonEmpty F.Frame)
+runGdt clauses = runState (desGdt clauses) F.blank
+
+uncov :: [P.Clause] -> Ty.Type -> F.Fresh (U.RefinementType, U.Context)
+uncov clauses tIn = do
+  x1 <- F.fresh (Just "x_1")
+  gdt <- G.desugarClauses [x1] . fromList $ clauses
+  let argsCtx = [(x1, tIn)]
+  return (U.uncovered (argsCtx, U.Literal U.T) gdt, argsCtx)
+
+evalUncov :: [P.Clause] -> Ty.Type -> U.RefinementType
+evalUncov clauses tIn = fst $ evalState (uncov clauses tIn) F.blank
+
+inhab :: [P.Clause] -> Ty.Type -> F.Fresh [I.InhabPat]
+inhab clauses tIn = do
+  (u, args) <- uncov clauses tIn
+  Poss.getPossibilities <$> I.genInhab u args
+
+evalInhab :: [P.Clause] -> Ty.Type -> [I.InhabPat]
+evalInhab clauses tIn = evalState (inhab clauses tIn) F.blank
+
+norm :: [P.Clause] -> Ty.Type -> F.Fresh (S.Set I.NormRefType)
+norm clauses tIn = do
+  ((context, formula), _args) <- uncov clauses tIn
+  I.normalize (context, []) formula
+
+evalNorm :: [P.Clause] -> Ty.Type -> S.Set I.NormRefType
+evalNorm clauses tIn = evalState (norm clauses tIn) F.blank
+
+pfg :: String -> IO [(Text, (G.Gdt, NE.NonEmpty F.Frame))]
+pfg = handleFunctions (\c _ -> runGdt c)
+
+pdu :: String -> IO [(Text, U.RefinementType)]
+pdu = handleFunctions evalUncov
+
+evalAnt :: [P.Clause] -> Ty.Type -> ([Int], [Int])
+evalAnt clauses tIn = evalState (ant clauses tIn) F.blank
+
+ant :: [P.Clause] -> Ty.Type -> F.Fresh ([Int], [Int])
+ant clauses tIn = do
+  x1 <- F.fresh (Just "x_1")
+  gdt <- G.desugarClauses [x1] . fromList $ clauses
+  let argsCtx = [(x1, tIn)]
+  let a = A.annotated (argsCtx, U.Literal U.T) gdt
+  I.accessableRedundant a argsCtx
+
+pda :: String -> IO [(Text, ([Int], [Int]))]
+pda = handleFunctions evalAnt
+
+evalUA :: [P.Clause] -> Ty.Type -> ([I.NormRefType], UA.NAnt)
+evalUA clauses tIn = flip evalState F.blank $ do
+  x1 <- F.fresh (Just "x_1")
+  gdt <- G.desugarClauses [x1] . fromList $ clauses
+  let argsCtx = [(x1, tIn)]
+  UA.ua [(argsCtx, [])] gdt
+
+pUA :: String -> IO [(Text, ([I.NormRefType], UA.NAnt))]
+pUA = handleFunctions evalUA
+
+evalFullUA :: [P.Clause] -> Ty.Type -> ([String], [Int])
+evalFullUA clauses tIn = flip evalState F.blank $ do
+  x1 <- F.fresh (Just "x_1")
+  gdt <- G.desugarClauses [x1] . fromList $ clauses
+  let argsCtx = [(x1, tIn)]
+  (nref, nant) <- UA.ua [(argsCtx, [])] gdt
+  ipats <- I.genInhabNorm nref argsCtx
+  redundant <- UA.redundantNorm nant argsCtx
+
+  return (map niceInhabPattern (Poss.getPossibilities ipats), redundant)
+
+pFullUA :: String -> IO [(Text, ([String], [Int]))]
+pFullUA = handleFunctions evalFullUA
+
+pduip :: String -> IO [(Text, [I.InhabPat])]
+pduip = handleFunctions evalInhab
+
+pdun :: String -> IO [(Text, S.Set I.NormRefType)]
+pdun = handleFunctions evalNorm
+
+inhabNice :: String -> IO [(Text, [String])]
+inhabNice = handleFunctions (\clauses ty -> map niceInhabPattern $ evalInhab clauses ty)
+
+nicePattern :: P.Pattern -> String
+nicePattern (P.PMatch k ps) = T.unpack (Ty.dcName k) ++ concatMap ((" " ++) . nicePattern) ps
+nicePattern P.PWild = "_"
+nicePattern (P.PVar x) = T.unpack x
+
+niceInhabPattern :: I.InhabPat -> String
+niceInhabPattern (I.IPIs k ps) = T.unpack (Ty.dcName k) ++ concatMap ((" " ++) . niceInhabPattern) ps
+niceInhabPattern (I.IPNot []) = "_"
+niceInhabPattern (I.IPNot nots) = "(Not " ++ niceList (map Ty.dcName nots) ++ ")"
+
+niceList :: [Text] -> String
+niceList as = concat $ tail $ concatMap comma as
+ where
+  comma x = [", ", T.unpack x]
diff --git a/explore/lower-your-guards/src/MatchInfo.hs b/explore/lower-your-guards/src/MatchInfo.hs
new file mode 100644
index 00000000..bd1fb166
--- /dev/null
+++ b/explore/lower-your-guards/src/MatchInfo.hs
@@ -0,0 +1,16 @@
+module MatchInfo (MatchInfo (..), TypedVar, getDataCons) where
+
+import qualified Fresh as F
+import qualified Types as Ty
+
+-- type VarMatchInfo = (F.VarID, MatchInfo)
+data MatchInfo where
+  Match :: Ty.DataConstructor -> [TypedVar] -> MatchInfo
+  Not :: Ty.DataConstructor -> MatchInfo
+  WasOriginally :: TypedVar -> MatchInfo
+  deriving (Show, Eq, Ord)
+
+type TypedVar = (F.VarID, Ty.Type)
+
+getDataCons :: TypedVar -> Maybe [Ty.DataConstructor]
+getDataCons = Ty.dataCons . snd
diff --git a/explore/lower-your-guards/src/MatchTree.hs b/explore/lower-your-guards/src/MatchTree.hs
new file mode 100644
index 00000000..b713ec4d
--- /dev/null
+++ b/explore/lower-your-guards/src/MatchTree.hs
@@ -0,0 +1,162 @@
+{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
+
+{-# HLINT ignore "Eta reduce" #-}
+
+module MatchTree where
+
+import Data.Maybe (listToMaybe, mapMaybe)
+import qualified Data.Text as T
+import qualified Types as Ty
+
+data MatchTree where
+  Pair :: MatchTree -> MatchTree -> MatchTree
+  Either :: [MatchTree] -> [MatchTree] -> MatchTree
+  Status :: Status -> MatchTree
+  deriving (Show, Eq)
+
+-- Not should be read as "everything except for"
+data Status where
+  Is :: Maybe Ty.DataConstructor -> Status
+  Not :: [Ty.DataConstructor] -> Status
+  deriving (Show, Eq)
+
+full = Status (Not [])
+
+empty = Status (Is Nothing)
+
+intCon i = Ty.DataConstructor {Ty.dcIdent = Ty.NameInt i, Ty.dcTypes = []}
+
+isInt i = Status (Is (Just (intCon i)))
+
+c1 = Pair (isInt 1) full
+
+c2 = Pair full (isInt 2)
+
+final = ([full] \\\ c1) \\\ c2
+
+final2 = ([full] \\\ c2) \\\ c1
+
+-- true = Status $ Is $ Just $ head $ Ty.dataCons Ty.bool
+
+e1 = Pair (Either [isInt 10] []) (isInt 2)
+
+e2 = Pair (Either [isInt 4] []) (isInt 5)
+
+-- e3 = Pair (Either [] [true]) (isInt 5)
+
+-- a1 = Either [true] []
+
+b1 = Pair (isInt 7) (isInt 5)
+
+(\\) :: MatchTree -> MatchTree -> [MatchTree]
+(\\) = treeMinus
+
+(\\\) :: [MatchTree] -> MatchTree -> [MatchTree]
+a \\\ b = concatMap (\\ b) a
+
+treeMinus :: MatchTree -> MatchTree -> [MatchTree]
+treeMinus t1 t2 = case (t1, t2) of
+  (Status (Is Nothing), _) -> []
+  (t, Status (Is Nothing)) -> [t]
+  (_, Status (Not [])) -> []
+  (Status s1, Status s2) -> case statMinus s1 s2 of
+    Is Nothing -> []
+    s -> [Status s]
+  (Status (Not []), p@(Pair _ _)) -> treeMinus (Pair (Status (Not [])) (Status (Not []))) p
+  (Status (Not []), e@(Either _ _)) -> treeMinus (Either [Status (Not [])] [Status (Not [])]) e
+  (Status _, Pair _ _) -> error "type error"
+  (Pair _ _, Status _) -> error "type error2"
+  (Status _, Either _ _) -> error "type error3"
+  (Either _ _, Status _) -> error "type error4"
+  (Either _ _, Pair _ _) -> error "type error5"
+  (Pair _ _, Either _ _) -> error "type error6"
+  (Pair a b, Pair c d) ->
+    map mkPairL aMinusC ++ map mkPairR bMinusD ++ both
+   where
+    mkPairL aSubC = Pair aSubC d
+    mkPairR bSubD = Pair c bSubD
+    both = [Pair aSubC bSubD | aSubC <- aMinusC, bSubD <- bMinusD]
+    c' = treeIntersect a c
+    d' = treeIntersect b d
+    aMinusC = concatMap (a \\) c'
+    bMinusD = concatMap (b \\) d'
+  -- [Pair d' aSubC, Pair c' bSubD, Pair aSubC bSubD]
+  (Either a b, Either c d) ->
+    [Either left right]
+   where
+    -- l = foldr a (flip map (\\)) c
+    left = concat [x \\ y | x <- a, y <- c]
+    right = concat [x \\ y | x <- b, y <- d]
+
+treeIntersect :: MatchTree -> MatchTree -> [MatchTree]
+treeIntersect m1 m2 = case (m1, m2) of
+  (Status (Is Nothing), _) -> []
+  (_, Status (Is Nothing)) -> []
+  (a, Status (Not [])) -> [a]
+  (Status (Not []), a) -> [a]
+  (Status s1, Status s2) -> case statIntersect s1 s2 of
+    Is Nothing -> []
+    s -> [Status s]
+  (Status _, Pair _ _) -> error "type error"
+  (Pair _ _, Status _) -> error "type error2"
+  (Status _, Either _ _) -> error "type error3"
+  (Either _ _, Status _) -> error "type error4"
+  (Either _ _, Pair _ _) -> error "type error5"
+  (Pair _ _, Either _ _) -> error "type error6"
+  (Pair a b, Pair c d) -> error "pairs"
+  -- map mkPairL (a \\ c) ++ map mkPairR (b \\ d) ++ both
+  -- where
+  --   mkPairL aSubC = Pair aSubC d
+  --   mkPairR bSubD = Pair c bSubD
+  --   both = [Pair aSubC bSubD | aSubC <- a \\ c, bSubD <- b \\ d]
+  -- c' = statIntersect a c
+  -- d' = statIntersect b d
+  (Either a b, Either c d) -> error "eithers"
+
+-- [Either left right]
+-- where
+--   -- l = foldr a (flip map (\\)) c
+--   left = concat [x \\ y | x <- a, y <- c]
+--   right = concat [x \\ y | x <- b, y <- d]
+
+-- (a-c)*(b-d) + c*(b-d) + (a-c)*d
+
+-- (a X b) \ (c X d) = (a X (b\d)) U ((a\c) X b)
+-- I eventually stumbled onto the correct solution,
+-- here a proof of it:
+-- https://proofwiki.org/wiki/Set_Difference_of_Cartesian_Products
+-- This actually doesn't do quite what we want,
+-- because it doesn't return a disjoint union, the union overlaps
+--
+-- see b1 and foo6 for example
+-- this may be the fatal flaw that makes this not work
+-- the above formula seems to be required for associativity
+-- possibly required for correctness at all
+--
+-- also either seems to not be working, but
+-- that may be an artifact of the above issue
+
+statMinus :: Status -> Status -> Status
+statMinus s1 s2 = case (s1, s2) of
+  (s, Is Nothing) -> s
+  (_, Not []) -> Is Nothing
+  (_, Not _) -> error "Attempted to subtract negative information"
+  (Is Nothing, _) -> Is Nothing
+  (Not [], Is (Just x)) -> Not [x]
+  (Not xs, Is (Just x)) -> Not (x : xs)
+  (Is (Just x), Is (Just x')) -> if x == x' then Is Nothing else Is (Just x)
+
+statIntersect :: Status -> Status -> Status
+statIntersect s1 s2 = case (s1, s2) of
+  (Is Nothing, _) -> Is Nothing
+  (_, Is Nothing) -> Is Nothing
+  (Not a, Not b) -> Not (a ++ b)
+  (Is (Just k), Not b) -> if k `elem` b then Is Nothing else Is (Just k)
+  (Not b, Is (Just k)) -> if k `elem` b then Is Nothing else Is (Just k)
+  (Is (Just k1), Is (Just k2)) -> if k1 == k2 then Is (Just k1) else Is Nothing
+
+-- (IsInt i1, IsInt i2) -> if i1 == i2 then Empty else IsInt i1
+
+-- (Full, NotInt is) -> error "what2?"
+-- (NotInt is, NotInt is2) -> error "what?"
+-- (IsInt i, NotInt is) -> error "what?"
diff --git a/explore/lower-your-guards/src/Parse.hs b/explore/lower-your-guards/src/Parse.hs
new file mode 100644
index 00000000..6c2b0e50
--- /dev/null
+++ b/explore/lower-your-guards/src/Parse.hs
@@ -0,0 +1,149 @@
+{-# OPTIONS_GHC -Wno-missing-export-lists #-}
+{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
+
+{-# HLINT ignore "Use <$>" #-}
+
+module Parse where
+
+import Control.Applicative (some)
+import Data.Char (isUpper)
+import Data.Functor (($>), (<&>))
+import Data.Text (Text)
+import qualified Data.Text as T
+import Data.Void (Void)
+import GHC.Unicode (isDigit)
+import Text.Megaparsec (Parsec, choice, lookAhead, satisfy)
+import Text.Megaparsec.Char as C (alphaNumChar, space1, string)
+import qualified Text.Megaparsec.Char.Lexer as L
+import qualified Types as Ty
+
+data FunctionDecl where
+  FunctionDecl :: Text -> Ty.Type -> Ty.Type -> FunctionDecl
+  deriving (Show, Eq)
+
+data FunctionDef where
+  FunctionDef :: FunctionDecl -> [Clause] -> FunctionDef
+  deriving (Show, Eq)
+
+-- data Type where
+--   TInt :: Type
+--   TBool :: Type
+--   TPair :: Type -> Type -> Type
+--   TFn :: Type -> Type -> Type
+--   ColinMistake :: Type
+--   deriving (Show, Eq, Ord)
+
+data Clause where
+  Clause :: Pattern -> Ty.Type -> Expr -> Clause
+  deriving (Show, Eq)
+
+data Pattern where
+  -- PLit :: Int -> Pattern
+  PWild :: Pattern
+  PVar :: Text -> Pattern
+  PMatch :: Ty.DataConstructor -> [Pattern] -> Pattern
+  deriving (Show, Eq, Ord)
+
+newtype Expr = Expr Text
+  deriving (Show, Eq)
+
+---
+---
+---
+
+type Parser = Parsec Void Text
+
+sc :: Parser ()
+sc =
+  L.space
+    space1 -- (2)
+    (L.skipLineComment "//") -- (3)
+    (L.skipBlockComment "/*" "*/") -- (4)
+
+lexeme :: Parser a -> Parser a
+lexeme = L.lexeme sc
+
+symbol :: Text -> Parser Text
+symbol = L.symbol sc
+
+pName :: Parser Text
+pName = lexeme $ T.pack <$> some alphaNumChar
+
+pInteger :: Parser Int
+pInteger = lexeme L.decimal
+
+pFnDecl :: Parser FunctionDecl
+pFnDecl = do
+  name <- pName
+  _ <- symbol ":"
+  tFrom <- pType
+  _ <- symbol "->"
+  tTo <- pType
+
+  return $ FunctionDecl name tFrom tTo
+
+pDataCons :: [Ty.DataConstructor] -> Parser Ty.DataConstructor
+pDataCons possible = choice $ map (\dc -> dc <$ symbol (Ty.dcName dc)) possible
+
+pDataConsMatch :: Ty.Type -> Parser Pattern
+pDataConsMatch typeIn =
+  do
+    _ <- lookAhead $ satisfy (\x -> isUpper x || x == ',' || isDigit x)
+    let cons = Ty.dataCons typeIn
+    case cons of
+      Just dc -> do
+        dataCon <- pDataCons dc
+        terms <- mapM pPattern (Ty.dcTypes dataCon)
+        return $ PMatch dataCon terms
+      Nothing ->
+        if typeIn /= Ty.int
+          then error "Found opaque type that's not an int while parsing. How??"
+          else do
+            i <- Ty.intCon <$> pInteger
+            return $ PMatch i []
+
+pPattern :: Ty.Type -> Parser Pattern
+pPattern typeIn =
+  choice
+    [ symbol "_" $> PWild
+    , pDataConsMatch typeIn
+    , pName <&> PVar
+    ]
+
+pClause :: Text -> Ty.Type -> Parser Clause
+pClause name typeIn = do
+  _ <- lexeme (string name)
+
+  pat <- pPattern typeIn
+
+  _ <- symbol "="
+
+  expr <- Expr . T.pack <$> some (satisfy (/= '\n')) <* sc
+
+  return $ Clause pat typeIn expr
+
+pFn :: Parser FunctionDef
+pFn = do
+  fnDecl <- pFnDecl
+  let FunctionDecl name typeIn _ = fnDecl
+  clauses <- some (pClause name typeIn)
+
+  return $ FunctionDef fnDecl clauses
+
+pType :: Parser Ty.Type
+pType =
+  choice
+    [ Ty.int <$ lexeme (string "Int")
+    , Ty.bool <$ lexeme (string "Bool")
+    , Ty.throol <$ lexeme (string "Throol")
+    , do
+        _ <- symbol ","
+        l <- pType
+        r <- pType
+        return $ Ty.pair l r
+    , do
+        _ <- lexeme (string "Either")
+        l <- pType
+        r <- pType
+        return $ Ty.either l r
+    ]
diff --git a/explore/lower-your-guards/src/Play.hs b/explore/lower-your-guards/src/Play.hs
new file mode 100644
index 00000000..9ff61c5e
--- /dev/null
+++ b/explore/lower-your-guards/src/Play.hs
@@ -0,0 +1,66 @@
+module Play where
+
+thing :: (Int, Bool) -> ()
+thing (n, True) = ()
+thing (0, n) = ()
+
+triple :: (Int, Int, Int) -> ()
+triple (7, 5, 3) = ()
+
+triple2 :: (Int, (Int, Int)) -> ()
+triple2 (7, (5, 3)) = ()
+
+foo :: (Either Int Bool, Int) -> Bool
+foo (Left 1, 2) = True
+foo (Right False, n) = True
+foo (Right True, n) = True
+foo (Left 3, n) = True
+foo (Left 3, n) = True
+
+foo2 :: (Either Int Bool, Int) -> Bool
+foo2 (Left 1, n) = True
+foo2 (Right False, n) = True
+
+foo3 :: (Either Bool Bool, Bool) -> Bool
+foo3 (Left True, b) = True
+foo3 (Right False, b) = True
+
+foo4 :: (Int, Int) -> Bool
+foo4 (1, n) = True
+foo4 (n, 2) = False
+
+foo5 :: (Int, Int, Int) -> Bool
+foo5 (1, 2, _) = False
+foo5 (4, _, 6) = True
+foo5 (_, 8, 9) = False
+
+foo6 :: (Int, Int) -> Bool
+foo6 (1, 2) = False
+
+foo7 :: (Int, Int, Int) -> Bool
+foo7 (1, 2, 3) = False
+
+foo8 :: (Either Int Bool, Int) -> ()
+foo8 (Left 10, 2) = ()
+
+-- foo8 (Right True, 5) = ()
+
+data Pat where
+  Base :: Pat
+  Kon :: Pat -> Pat
+  DonKon :: Pat -> Pat -> Pat
+  deriving (Show, Eq)
+
+timelineSplitter :: Int -> [Pat]
+timelineSplitter p = do
+  case p of
+    0 -> return Base
+    2 -> [Base, Base]
+    4 -> do
+      a <- timelineSplitter (p - 1)
+      b <- timelineSplitter (p - 2)
+
+      return $ DonKon a b
+    _ -> do
+      n <- timelineSplitter (p - 1)
+      return $ Kon n
diff --git a/explore/lower-your-guards/src/Possibilities.hs b/explore/lower-your-guards/src/Possibilities.hs
new file mode 100644
index 00000000..96232977
--- /dev/null
+++ b/explore/lower-your-guards/src/Possibilities.hs
@@ -0,0 +1,64 @@
+module Possibilities (Possibilities, retSingle, allCombinations, anyOf, none, getPossibilities) where
+
+import Data.Foldable (Foldable (fold))
+
+newtype Possibilities a = Possibilities {getPossibilities :: [a]}
+  deriving (Show, Eq, Ord)
+
+instance Functor Possibilities where
+  fmap f (Possibilities a) = Possibilities (f <$> a)
+
+instance Semigroup (Possibilities a) where
+  (Possibilities p1) <> (Possibilities p2) = Possibilities $ p1 <> p2
+
+instance Monoid (Possibilities a) where
+  mempty = Possibilities []
+
+anyOf :: [Possibilities a] -> Possibilities a
+anyOf = fold
+
+none :: Possibilities a -> Bool
+none = null . getPossibilities
+
+retSingle :: (Monad m) => a -> m (Possibilities a)
+retSingle i = return $ Possibilities [i]
+
+-- | List all possible paths through the list of Possibilites
+--
+-- Ex.
+-- > allCombinations
+--     [ Possibilities [1]
+--     , Possibilities [2,3]
+--     , Possibilities [4]
+--     , Possibilities [5,6,7]
+--     ]
+-- ===
+-- Possibilities {getPossibilities =
+--   [[1,2,4,5]
+--   ,[1,2,4,6]
+--   ,[1,2,4,7]
+--   ,[1,3,4,5]
+--   ,[1,3,4,6]
+--   ,[1,3,4,7]
+--   ]}
+--
+--       2       5
+--     /   \   /
+--   1       4 --6
+--     \   /   \
+--       3       7
+--
+-- If any any of the Possibilities is empty,
+-- an empty Possibility is returned
+--
+-- In other words, this lists all elements of the
+-- cartesian product of multiple sets
+allCombinations :: [Possibilities a] -> Possibilities [a]
+allCombinations = foldr prod nil
+ where
+  -- note, nil /= mempty
+  -- VERY important
+  nil = Possibilities [[]]
+
+prod :: Possibilities a -> Possibilities [a] -> Possibilities [a]
+prod (Possibilities xs) (Possibilities yss) = Possibilities [x : ys | x <- xs, ys <- yss]
diff --git a/explore/lower-your-guards/src/Types.hs b/explore/lower-your-guards/src/Types.hs
new file mode 100644
index 00000000..81f25aec
--- /dev/null
+++ b/explore/lower-your-guards/src/Types.hs
@@ -0,0 +1,92 @@
+{-# OPTIONS_GHC -Wno-missing-export-lists #-}
+
+module Types where
+
+import Data.Text (Text)
+import qualified Data.Text as T
+
+data TypeConstructor = TBool | TPair | TEither | TInt | TThrool
+  deriving (Show, Eq, Ord)
+
+data Type = Type
+  { typeCons :: TypeConstructor
+  , dataCons :: Maybe [DataConstructor]
+  }
+  deriving (Eq, Ord)
+
+instance Show Type where
+  show Type {typeCons = t} = "Type: " ++ show t
+
+data DataConstructor = DataConstructor
+  { dcIdent :: DataConName
+  , dcTypes :: [Type]
+  }
+  deriving (Eq, Ord)
+
+dcName :: DataConstructor -> Text
+dcName dc = case dcIdent dc of
+  NameText t -> t
+  NameInt i -> T.pack $ show i
+
+data DataConName where
+  NameText :: Text -> DataConName
+  NameInt :: Int -> DataConName
+  deriving (Show, Eq, Ord)
+
+instance Show DataConstructor where
+  show dc = "(\'" ++ T.unpack (dcName dc) ++ "\' <" ++ (show . length $ dcTypes dc) ++ ">)"
+
+intCon :: Int -> DataConstructor
+intCon i = DataConstructor {dcIdent = NameInt i, dcTypes = []}
+
+bool :: Type
+bool =
+  Type
+    { typeCons = TBool
+    , dataCons =
+        Just
+          [ DataConstructor {dcIdent = NameText "True", dcTypes = []}
+          , DataConstructor {dcIdent = NameText "False", dcTypes = []}
+          ]
+    }
+
+throol :: Type
+throol =
+  Type
+    { typeCons = TThrool
+    , dataCons =
+        Just
+          [ DataConstructor {dcIdent = NameText "Foo", dcTypes = []}
+          , DataConstructor {dcIdent = NameText "Bar", dcTypes = []}
+          , DataConstructor {dcIdent = NameText "Baz", dcTypes = []}
+          ]
+    }
+
+pair :: Type -> Type -> Type
+pair a b =
+  Type
+    { typeCons = TPair
+    , dataCons =
+        Just
+          [ DataConstructor {dcIdent = NameText ",", dcTypes = [a, b]}
+          ]
+    }
+
+either :: Type -> Type -> Type
+either a b =
+  Type
+    { typeCons = TEither
+    , dataCons =
+        Just
+          [ DataConstructor {dcIdent = NameText "Left", dcTypes = [a]}
+          , DataConstructor {dcIdent = NameText "Right", dcTypes = [b]}
+          ]
+    }
+
+int :: Type
+int =
+  Type
+    { typeCons = TInt
+    , -- int is an opaque type
+      dataCons = Nothing
+    }
diff --git a/explore/lower-your-guards/src/UA.hs b/explore/lower-your-guards/src/UA.hs
new file mode 100644
index 00000000..b70d1825
--- /dev/null
+++ b/explore/lower-your-guards/src/UA.hs
@@ -0,0 +1,52 @@
+{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
+
+module UA (ua, redundantNorm, NAnt) where
+
+import Control.Monad.Trans.Maybe
+import qualified Fresh as F
+import qualified GuardTree as G
+import qualified Inhabitants as I
+import MatchInfo
+import qualified Possibilities as Poss
+import qualified Uncovered as U
+
+data NAnt where
+  Grhs :: [I.NormRefType] -> Int -> NAnt
+  Branch :: NAnt -> NAnt -> NAnt
+  deriving (Show)
+
+ua :: [I.NormRefType] -> G.Gdt -> F.Fresh ([I.NormRefType], NAnt)
+ua nrefs gdt = case gdt of
+  G.Grhs k -> return ([], Grhs nrefs k)
+  G.Branch t1 t2 -> do
+    (n1, u1) <- ua nrefs t1
+    (n2, u2) <- ua n1 t2
+    return (n2, Branch u1 u2)
+  G.Guarded (var, g) t -> case g of
+    G.GWas old -> do
+      n <- addLitMulti nrefs $ varInfo (WasOriginally old)
+      ua n t
+    G.GMatch k args -> do
+      n <- addLitMulti nrefs $ varInfo (Match k args)
+      (n', u) <- ua n t
+      n'' <- addLitMulti nrefs $ varInfo (Not k)
+      return (n'' ++ n', u)
+   where
+    varInfo = U.Info var
+
+addLitMulti :: [I.NormRefType] -> U.Literal -> F.Fresh [I.NormRefType]
+addLitMulti [] _ = return []
+addLitMulti (n : ns) lit = do
+  r <- runMaybeT $ I.addLiteral n lit
+  case r of
+    Nothing -> addLitMulti ns lit
+    Just (ctx, cfs) -> do
+      ns' <- addLitMulti ns lit
+      return $ (ctx, cfs) : ns'
+
+redundantNorm :: NAnt -> U.Context -> F.Fresh [Int]
+redundantNorm ant args = case ant of
+  Grhs ref i -> do
+    nothing <- Poss.none <$> I.genInhabNorm ref args
+    return ([i | nothing])
+  Branch a1 a2 -> mappend <$> redundantNorm a1 args <*> redundantNorm a2 args
diff --git a/explore/lower-your-guards/src/Uncovered.hs b/explore/lower-your-guards/src/Uncovered.hs
new file mode 100644
index 00000000..875025f0
--- /dev/null
+++ b/explore/lower-your-guards/src/Uncovered.hs
@@ -0,0 +1,46 @@
+{-# OPTIONS_GHC -Wno-missing-export-lists #-}
+
+module Uncovered where
+
+import qualified GuardTree as G
+import MatchInfo
+
+type RefinementType = (Context, Formula)
+
+type Context = [TypedVar]
+
+data Formula where
+  And :: Formula -> Formula -> Formula
+  Or :: Formula -> Formula -> Formula
+  Literal :: Literal -> Formula
+  deriving (Show, Eq)
+
+data Literal where
+  T :: Literal
+  F :: Literal
+  Info :: TypedVar -> MatchInfo -> Literal
+  deriving (Show, Eq)
+
+uncovered :: RefinementType -> G.Gdt -> RefinementType
+uncovered r g = case g of
+  G.Grhs _ ->
+    let (context, _) = r in (context, Literal F)
+  G.Branch t1 t2 ->
+    uncovered (uncovered r t1) t2
+  G.Guarded (var, guard) t -> case guard of
+    G.GMatch dataCon ys -> noMatch `union` matchedPath
+     where
+      noMatch = r `liftAndLit` varInfo (Not dataCon)
+      matchedPath = uncovered (r `liftAndLit` varInfo (Match dataCon ys)) t
+    G.GWas old -> uncovered (r `liftAndLit` varInfo (WasOriginally old)) t
+   where
+    varInfo = Info var
+
+liftAndLit :: RefinementType -> Literal -> RefinementType
+liftAndLit (cont, form) f = (cont, form `And` Literal f)
+
+-- Note: I think this should only be called in situations
+-- where cont1 == cont2. The paper doesn't specify.
+-- I am just using the first
+union :: RefinementType -> RefinementType -> RefinementType
+union (cont1, f1) (_cont2, f2) = (cont1, f1 `Or` f2)
diff --git a/explore/lower-your-guards/stack.yaml b/explore/lower-your-guards/stack.yaml
new file mode 100644
index 00000000..60693f0e
--- /dev/null
+++ b/explore/lower-your-guards/stack.yaml
@@ -0,0 +1,68 @@
+# This file was automatically generated by 'stack init'
+#
+# Some commonly used options have been documented as comments in this file.
+# For advanced use and comprehensive documentation of the format, please see:
+# https://docs.haskellstack.org/en/stable/yaml_configuration/
+
+# Resolver to choose a 'specific' stackage snapshot or a compiler version.
+# A snapshot resolver dictates the compiler version and the set of packages
+# to be used for project dependencies. For example:
+#
+# resolver: lts-21.13
+# resolver: nightly-2023-09-24
+# resolver: ghc-9.6.2
+#
+# The location of a snapshot can be provided as a file or url. Stack assumes
+# a snapshot provided as a file might change, whereas a url resource does not.
+#
+# resolver: ./custom-snapshot.yaml
+# resolver: https://example.com/snapshots/2023-01-01.yaml
+resolver: lts-21.25
+# resolver:
+#   url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/22/22.yaml
+
+# User packages to be built.
+# Various formats can be used as shown in the example below.
+#
+# packages:
+# - some-directory
+# - https://example.com/foo/bar/baz-0.0.2.tar.gz
+#   subdirs:
+#   - auto-update
+#   - wai
+packages:
+- .
+# Dependency packages to be pulled from upstream that are not in the resolver.
+# These entries can reference officially published versions as well as
+# forks / in-progress versions pinned to a git hash. For example:
+#
+# extra-deps:
+# - acme-missiles-0.3
+# - git: https://github.com/commercialhaskell/stack.git
+#   commit: e7b331f14bcffb8367cd58fbfc8b40ec7642100a
+#
+# extra-deps: []
+
+# Override default flag values for local packages and extra-deps
+# flags: {}
+
+# Extra package databases containing global packages
+# extra-package-dbs: []
+
+# Control whether we use the GHC we find on the path
+# system-ghc: true
+#
+# Require a specific version of Stack, using version ranges
+# require-stack-version: -any # Default
+# require-stack-version: ">=2.13"
+#
+# Override the architecture used by Stack, especially useful on Windows
+# arch: i386
+# arch: x86_64
+#
+# Extra directories used by Stack for building
+# extra-include-dirs: [/path/to/dir]
+# extra-lib-dirs: [/path/to/dir]
+#
+# Allow a newer minor version of GHC than the snapshot specifies
+# compiler-check: newer-minor
diff --git a/explore/lower-your-guards/test/bool1.disc b/explore/lower-your-guards/test/bool1.disc
new file mode 100644
index 00000000..86910d66
--- /dev/null
+++ b/explore/lower-your-guards/test/bool1.disc
@@ -0,0 +1,3 @@
+foo : Bool -> Bool
+foo True = False
+// foo False = True
diff --git a/explore/lower-your-guards/test/bool2.disc b/explore/lower-your-guards/test/bool2.disc
new file mode 100644
index 00000000..107e08aa
--- /dev/null
+++ b/explore/lower-your-guards/test/bool2.disc
@@ -0,0 +1,5 @@
+foo : Bool -> Bool
+foo True = False
+foo True = False
+foo True = False
+// foo False = True
diff --git a/explore/lower-your-guards/test/complex1.disc b/explore/lower-your-guards/test/complex1.disc
new file mode 100644
index 00000000..166767b5
--- /dev/null
+++ b/explore/lower-your-guards/test/complex1.disc
@@ -0,0 +1,4 @@
+
+foo : , Either Int Bool Int -> Bool
+foo , Left  1    n = True
+foo , Right False n = True
diff --git a/explore/lower-your-guards/test/complex2.disc b/explore/lower-your-guards/test/complex2.disc
new file mode 100644
index 00000000..a87e44ff
--- /dev/null
+++ b/explore/lower-your-guards/test/complex2.disc
@@ -0,0 +1,6 @@
+foo : , Either Int Bool Int -> Bool
+foo , Left  1     2 = True
+foo , Right False n = True
+foo , Right True  n = True
+foo , Left  3     n = True
+foo , Left  3     n = True
diff --git a/explore/lower-your-guards/test/complex22.disc b/explore/lower-your-guards/test/complex22.disc
new file mode 100644
index 00000000..9d621621
--- /dev/null
+++ b/explore/lower-your-guards/test/complex22.disc
@@ -0,0 +1,17 @@
+foo : , Either Int Bool Int -> Bool
+foo , Left  1     2 = True
+foo , Right False n = True
+foo , Right True  n = True
+foo , Left  3     n = True
+foo , Left  3     n = True
+foo , Left  3     n = True
+foo , Left  3     n = True
+foo , Left  3     n = True
+foo , Left  3     n = True
+foo , Left  3     n = True
+
+/*
+UA makes this near instant!
+Before combining UA,
+this took about ~10 seconds to run
+*/
diff --git a/explore/lower-your-guards/test/complex3.disc b/explore/lower-your-guards/test/complex3.disc
new file mode 100644
index 00000000..0dba77c7
--- /dev/null
+++ b/explore/lower-your-guards/test/complex3.disc
@@ -0,0 +1,3 @@
+foo : , Either Int Bool Int -> Bool
+foo , Left  a     x = False
+foo , Right b     y = False
diff --git a/explore/lower-your-guards/test/complex4.disc b/explore/lower-your-guards/test/complex4.disc
new file mode 100644
index 00000000..1c9edde4
--- /dev/null
+++ b/explore/lower-your-guards/test/complex4.disc
@@ -0,0 +1,4 @@
+foo : , Either Int Bool Int -> Bool
+foo , Right _        _ = True
+foo , Left  0         _ = True
+foo , Left  0         _ = True
diff --git a/explore/lower-your-guards/test/complex5.disc b/explore/lower-your-guards/test/complex5.disc
new file mode 100644
index 00000000..6cca513b
--- /dev/null
+++ b/explore/lower-your-guards/test/complex5.disc
@@ -0,0 +1,3 @@
+foo : , Either Bool Bool Bool -> Bool
+foo , Left  True    b = True
+foo , Right False   b = True
diff --git a/explore/lower-your-guards/test/either.disc b/explore/lower-your-guards/test/either.disc
new file mode 100644
index 00000000..4383eaec
--- /dev/null
+++ b/explore/lower-your-guards/test/either.disc
@@ -0,0 +1,5 @@
+
+bar : Either Int Bool -> Int
+bar Left n = 20 * n
+bar Right b = -1
+
diff --git a/explore/lower-your-guards/test/pair1.disc b/explore/lower-your-guards/test/pair1.disc
new file mode 100644
index 00000000..649a3f9f
--- /dev/null
+++ b/explore/lower-your-guards/test/pair1.disc
@@ -0,0 +1,4 @@
+
+foo : , Int Int -> Bool
+foo , 1 n = True
+foo , n 2 = False
diff --git a/explore/lower-your-guards/test/pair2.disc b/explore/lower-your-guards/test/pair2.disc
new file mode 100644
index 00000000..858c8a58
--- /dev/null
+++ b/explore/lower-your-guards/test/pair2.disc
@@ -0,0 +1,4 @@
+
+foo : , Int Int -> Bool
+foo , 7 5 = False
+//foo , 1 b = False
diff --git a/explore/lower-your-guards/test/pair3.disc b/explore/lower-your-guards/test/pair3.disc
new file mode 100644
index 00000000..5ecbdae2
--- /dev/null
+++ b/explore/lower-your-guards/test/pair3.disc
@@ -0,0 +1,3 @@
+foo : , Int Int -> Bool
+foo , 1 5 = False
+foo , b y = False
diff --git a/explore/lower-your-guards/test/pair4.disc b/explore/lower-your-guards/test/pair4.disc
new file mode 100644
index 00000000..8de99121
--- /dev/null
+++ b/explore/lower-your-guards/test/pair4.disc
@@ -0,0 +1,12 @@
+foo : , Int Bool -> Bool
+foo , 0 n = False
+foo , n True = False
+
+revfoo : , Int Bool -> Bool
+revfoo , n True = False
+revfoo , 0 n = False
+
+bar : , Int Bool -> Bool
+bar , 0 n = False
+bar , n True = False
+bar , 0 n = False
diff --git a/explore/lower-your-guards/test/t1.disc b/explore/lower-your-guards/test/t1.disc
new file mode 100644
index 00000000..679d30c5
--- /dev/null
+++ b/explore/lower-your-guards/test/t1.disc
@@ -0,0 +1,12 @@
+
+f : Int -> Bool
+f 0 = False
+f 10 = True
+
+f n = False
+f _ = True
+
+
+g : Bool -> Bool
+g b = not b
+
diff --git a/explore/lower-your-guards/test/test1.disc b/explore/lower-your-guards/test/test1.disc
new file mode 100644
index 00000000..e29e78db
--- /dev/null
+++ b/explore/lower-your-guards/test/test1.disc
@@ -0,0 +1,6 @@
+notCovered : Int -> Int
+notCovered 10 = -1
+
+covered : Int -> Int
+covered 10 = -1
+covered x = x
diff --git a/explore/lower-your-guards/test/test2.disc b/explore/lower-your-guards/test/test2.disc
new file mode 100644
index 00000000..810c82b9
--- /dev/null
+++ b/explore/lower-your-guards/test/test2.disc
@@ -0,0 +1,3 @@
+shouldntPass : Int -> Bool
+shouldntPass 123 = asdf
+shouldntPass 123 = asdf
diff --git a/explore/lower-your-guards/test/throol1.disc b/explore/lower-your-guards/test/throol1.disc
new file mode 100644
index 00000000..59ddcc76
--- /dev/null
+++ b/explore/lower-your-guards/test/throol1.disc
@@ -0,0 +1,2 @@
+foo : Throol -> Bool
+foo Foo = False
diff --git a/explore/lower-your-guards/test/throol2.disc b/explore/lower-your-guards/test/throol2.disc
new file mode 100644
index 00000000..72b5e455
--- /dev/null
+++ b/explore/lower-your-guards/test/throol2.disc
@@ -0,0 +1,3 @@
+foo : , Throol Throol -> Bool
+foo , Baz Foo = False
+// foo , Bar Baz = False
diff --git a/explore/lower-your-guards/test/triple1.disc b/explore/lower-your-guards/test/triple1.disc
new file mode 100644
index 00000000..12a0accf
--- /dev/null
+++ b/explore/lower-your-guards/test/triple1.disc
@@ -0,0 +1,4 @@
+
+foo : , Int , Int Int -> Bool
+foo , 7 , 5 3 = False
+//foo , 1 b = False