From 28496867613f3c6371bc7e7ae8e20b0ef40f6a95 Mon Sep 17 00:00:00 2001
From: Victor Taelin <victor.taelin@gmail.com>
Date: Fri, 18 Oct 2024 17:51:51 -0300
Subject: [PATCH] minor stuff

---
 src/Kind/Check.hs | 10 ++++++----
 src/Kind/Parse.hs |  4 +++-
 2 files changed, 9 insertions(+), 5 deletions(-)

diff --git a/src/Kind/Check.hs b/src/Kind/Check.hs
index a143f28c0..e142ff276 100644
--- a/src/Kind/Check.hs
+++ b/src/Kind/Check.hs
@@ -289,10 +289,12 @@ check src val typ dep = debug ("check: " ++ termShower True val dep ++ "\n    ::
       envFail
 
 unreachable :: Maybe Cod -> Term -> Int -> Env ()
-unreachable src (Lam nam bod) dep = unreachable src (bod (Con "void" [])) (dep+1)
-unreachable src (Hol nam ctx) dep = envLog (Found nam (Hol "unreachable" []) ctx dep) >> return ()
-unreachable _   (Src src val) dep = unreachable (Just src) val dep
-unreachable src term          dep = return ()
+unreachable src (Lam nam bod)     dep = unreachable src (bod (Con "void" [])) (dep+1)
+unreachable src (Hol nam ctx)     dep = envLog (Found nam (Hol "unreachable" []) ctx dep) >> return ()
+unreachable src (Let nam val bod) dep = unreachable src (bod (Con "void" [])) (dep+1)
+unreachable src (Use nam val bod) dep = unreachable src (bod (Con "void" [])) (dep+1)
+unreachable _   (Src src val)     dep = unreachable (Just src) val dep
+unreachable src term              dep = return ()
 
 checkTele :: Maybe Cod -> Tele -> Term -> Int -> Env ()
 checkTele src tele typ dep = case tele of
diff --git a/src/Kind/Parse.hs b/src/Kind/Parse.hs
index 2d2940cca..191517d87 100644
--- a/src/Kind/Parse.hs
+++ b/src/Kind/Parse.hs
@@ -6,6 +6,7 @@ import Debug.Trace
 import Prelude hiding (EQ, LT, GT)
 import Kind.Type
 import Kind.Reduce
+import Kind.Show
 import Highlight (highlightError, highlight)
 import Data.Char (ord)
 import qualified Data.Map.Strict as M
@@ -585,7 +586,8 @@ parseDef = do
         body <- parseTerm
         return (pats, body)
       let (mat, bods) = unzip rules
-      return (flattenDef mat bods 0)
+      let flat = (flattenDef mat bods 0)
+      return $ {-trace (termShow flat)-} flat
     ]
   (_, uses) <- P.getState
   let name' = expandUses uses name