Bug fixes to the modules system.

This fixes #796.
It also fixes the @bboston7's example on #883, but not the original
example in #883.   The issue there is that `asdf` function generates
a constraint only involving the module parameter.

Normally we don't try to solve constraint that don't mention a schema's
parameters, because they can always be solved "later", and hopefully with
more things instantiated.

The weird thing in this case is that the schema adds *local" constraint to
the module parameters, but we end up ignoring these.

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

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