diff --git a/src/Cryptol/ModuleSystem/InstantiateModule.hs b/src/Cryptol/ModuleSystem/InstantiateModule.hs
index f699cab76..8544c898a 100644
--- a/src/Cryptol/ModuleSystem/InstantiateModule.hs
+++ b/src/Cryptol/ModuleSystem/InstantiateModule.hs
@@ -14,6 +14,7 @@ import Cryptol.Parser.Position(Located(..))
 import Cryptol.ModuleSystem.Name
 import Cryptol.TypeCheck.AST
 import Cryptol.TypeCheck.Subst(listParamSubst, apSubst)
+import Cryptol.TypeCheck.SimpType(tRebuild)
 import Cryptol.Utils.Ident(ModName,modParamIdent)
 
 {-
@@ -232,6 +233,7 @@ instance Inst Schema where
 
 instance Inst Type where
   inst env ty =
+    tRebuild $
     case ty of
       TCon tc ts    -> TCon (inst env tc) (inst env ts)
       TVar tv       ->
diff --git a/src/Cryptol/TypeCheck.hs b/src/Cryptol/TypeCheck.hs
index d12d87e44..5c2799972 100644
--- a/src/Cryptol/TypeCheck.hs
+++ b/src/Cryptol/TypeCheck.hs
@@ -58,12 +58,11 @@ tcModuleInst :: Module                  {- ^ functor -} ->
                 IO (InferOutput Module) {- ^ new version of instance -}
 tcModuleInst func m inp = runInferM inp
                         $ do x <- inferModule m
-                             y <- checkModuleInstance func x
                              flip (foldr withParamType) (mParamTypes x) $
                                withParameterConstraints (mParamConstraints x) $
-                               proveModuleTopLevel
-
-                             return y
+                               do y <- checkModuleInstance func x
+                                  proveModuleTopLevel
+                                  pure y
 
 tcExpr :: P.Expr Name -> InferInput -> IO (InferOutput (Expr,Schema))
 tcExpr e0 inp = runInferM inp
diff --git a/src/Cryptol/TypeCheck/Infer.hs b/src/Cryptol/TypeCheck/Infer.hs
index cd5c0b674..80475e07a 100644
--- a/src/Cryptol/TypeCheck/Infer.hs
+++ b/src/Cryptol/TypeCheck/Infer.hs
@@ -902,7 +902,9 @@ checkSigB b (Forall as asmps0 t0, validSchema) = case thing (P.bDef b) of
                    addGoals validSchema
                    () <- simplifyAllConstraints  -- XXX: using `asmps` also?
                    return e1
-     cs <- applySubstGoals cs0
+
+     asmps1 <- applySubstPreds asmps0
+     cs     <- applySubstGoals cs0
 
      let findKeep vs keep todo =
           let stays (_,cvs)    = not $ Set.null $ Set.intersection vs cvs
@@ -912,12 +914,14 @@ checkSigB b (Forall as asmps0 t0, validSchema) = case thing (P.bDef b) of
                [] -> (keep,map fst todo)
                _  -> findKeep (Set.unions (vs:newVars)) (stayPs ++ keep) perhaps
 
-     let (stay,leave) = findKeep (Set.fromList (map tpVar as)) []
+     let -- if a goal mentions any of these variables, we'll commit to
+         -- solving it now.
+         stickyVars = Set.fromList (map tpVar as) `Set.union` fvs asmps1
+         (stay,leave) = findKeep stickyVars []
                             [ (c, fvs c) | c <- cs ]
 
      addGoals leave
 
-     asmps1 <- applySubstPreds asmps0
 
      su <- proveImplication (Just (thing (P.bName b))) as asmps1 stay
      extendSubst su
diff --git a/tests/issues/Issue796.cry b/tests/issues/Issue796.cry
new file mode 100644
index 000000000..3c653f117
--- /dev/null
+++ b/tests/issues/Issue796.cry
@@ -0,0 +1,19 @@
+module Issue796 = Issue796_Sig where
+
+parameter
+  type _k: #
+
+type Key = [8 * _k]
+type Block = [64]
+type RoundKey = [64]
+
+aux : RoundKey -> Block -> Block
+aux RK P = zero
+
+// key_schedule : Key -> RoundKey
+key_schedule K = zero
+  where
+    _ = [ groupBy`{4} K ]
+
+// encrypt_block : Key -> Block -> Block
+encrypt_block key pt = aux (key_schedule key) pt
diff --git a/tests/issues/Issue796_Sig.cry b/tests/issues/Issue796_Sig.cry
new file mode 100644
index 000000000..ee885ffc7
--- /dev/null
+++ b/tests/issues/Issue796_Sig.cry
@@ -0,0 +1,7 @@
+module Issue796_Sig where
+
+parameter
+  type Key: *
+  type Block: *
+
+  encrypt_block: Key -> Block -> Block
diff --git a/tests/issues/Issue883.cry b/tests/issues/Issue883.cry
new file mode 100644
index 000000000..0992171d5
--- /dev/null
+++ b/tests/issues/Issue883.cry
@@ -0,0 +1,6 @@
+module Issue883 where
+
+import Issue883_Impl
+
+zeros : [4][8]
+zeros = getZeros
diff --git a/tests/issues/Issue883_A.cry b/tests/issues/Issue883_A.cry
new file mode 100644
index 000000000..119f203ca
--- /dev/null
+++ b/tests/issues/Issue883_A.cry
@@ -0,0 +1,13 @@
+module Issue883_A where
+parameter
+    type c : #
+    type constraint ( fin c, c >= 1, 64 >= width (c-1) )
+
+dumbHash : {n} (fin n, 64 >= width n) => [n] -> [128]
+dumbHash msg = zero
+
+asdf : {n} (64 >= width (n+192), 64 >= width (128 * c), fin n) => [n] -> [128]
+asdf msg = dumbHash (join (drop`{1} ys))
+ where
+   ys : [c+1][128]
+   ys = zero
diff --git a/tests/issues/Issue883_Impl.cry b/tests/issues/Issue883_Impl.cry
new file mode 100644
index 000000000..f8799de2a
--- /dev/null
+++ b/tests/issues/Issue883_Impl.cry
@@ -0,0 +1,3 @@
+module Issue883_Impl = Issue883_Sig where
+
+type w = 32
diff --git a/tests/issues/Issue883_Sig.cry b/tests/issues/Issue883_Sig.cry
new file mode 100644
index 000000000..494af39a0
--- /dev/null
+++ b/tests/issues/Issue883_Sig.cry
@@ -0,0 +1,8 @@
+module Issue883_Sig where
+
+parameter
+  type w : #
+  type constraint (fin w)
+
+getZeros : [w/8][8]
+getZeros = split`{each=8} zero
diff --git a/tests/issues/issue796.icry b/tests/issues/issue796.icry
new file mode 100644
index 000000000..811c353f6
--- /dev/null
+++ b/tests/issues/issue796.icry
@@ -0,0 +1 @@
+:load Issue796.cry
diff --git a/tests/issues/issue796.icry.stdout b/tests/issues/issue796.icry.stdout
new file mode 100644
index 000000000..a40bb511e
--- /dev/null
+++ b/tests/issues/issue796.icry.stdout
@@ -0,0 +1,4 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Issue796_Sig
+Loading module Issue796
diff --git a/tests/issues/issue883.icry b/tests/issues/issue883.icry
new file mode 100644
index 000000000..3e6be5bad
--- /dev/null
+++ b/tests/issues/issue883.icry
@@ -0,0 +1 @@
+:load Issue883.cry
diff --git a/tests/issues/issue883.icry.stdout b/tests/issues/issue883.icry.stdout
new file mode 100644
index 000000000..8f7e2e57c
--- /dev/null
+++ b/tests/issues/issue883.icry.stdout
@@ -0,0 +1,5 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Issue883_Sig
+Loading module Issue883_Impl
+Loading module Issue883
diff --git a/tests/issues/issue883_A.icry b/tests/issues/issue883_A.icry
new file mode 100644
index 000000000..67aefabce
--- /dev/null
+++ b/tests/issues/issue883_A.icry
@@ -0,0 +1 @@
+:load Issue883_A.cry
diff --git a/tests/issues/issue883_A.icry.stdout b/tests/issues/issue883_A.icry.stdout
new file mode 100644
index 000000000..f2e511217
--- /dev/null
+++ b/tests/issues/issue883_A.icry.stdout
@@ -0,0 +1,3 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Issue883_A