diff --git a/lib/Check.hs b/lib/Check.hs
index 1a6cc43..0259790 100644
--- a/lib/Check.hs
+++ b/lib/Check.hs
@@ -60,17 +60,18 @@ findType g e@(App m n) = do
 findType g f@(Abs x a asc m) = do
     validateType g a
     b <- findType (incIndices a : map incIndices g) m
-    whenJust asc (betaEquiv' f b)
+    whenJust asc (void . liftA2 ($>) (findType g) (betaEquiv' f b))
     validateType g (Pi x a Nothing b)
     pure $ if occursFree 0 b then Pi x a Nothing b else Pi "" a Nothing b
 findType g f@(Pi _ a asc b) = do
     aSort <- findType g a
     bSort <- findType (incIndices a : map incIndices g) b
-    whenJust asc $ betaEquiv' f bSort
+    whenJust asc (void . liftA2 ($>) (findType g) (betaEquiv' f bSort))
     liftEither $ compSort a b aSort bSort
 findType g (Let _ Nothing v b) = findType g (subst 0 v b)
 findType g e@(Let _ (Just t) v b) = do
     res <- findType g (subst 0 v b)
+    _ <- findType g t
     betaEquiv' e t res
     pure t