Bug fixes to the modules system.

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       ->

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

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

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

tests/issues/Issue796_Sig.cry

@@ -0,0 +1,7 @@
+module Issue796_Sig where
+
+parameter
+  type Key: *
+  type Block: *
+
+  encrypt_block: Key -> Block -> Block

tests/issues/Issue883.cry

@@ -0,0 +1,6 @@
+module Issue883 where
+
+import Issue883_Impl
+
+zeros : [4][8]
+zeros = getZeros

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

tests/issues/Issue883_Impl.cry

@@ -0,0 +1,3 @@
+module Issue883_Impl = Issue883_Sig where
+
+type w = 32

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

tests/issues/issue796.icry

@@ -0,0 +1 @@
+:load Issue796.cry

tests/issues/issue796.icry.stdout

@@ -0,0 +1,4 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Issue796_Sig
+Loading module Issue796

tests/issues/issue883.icry

@@ -0,0 +1 @@
+:load Issue883.cry

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

tests/issues/issue883_A.icry

@@ -0,0 +1 @@
+:load Issue883_A.cry

tests/issues/issue883_A.icry.stdout

@@ -0,0 +1,3 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Issue883_A