Improve error messages, which mention module parameters.

Fixes #1560

CHANGES.md

@@ -24,6 +24,9 @@
 
 ## New features
 
+* Improved error messages mentioning module parameters
+  ([#1560](https://github.com/GaloisInc/cryptol/issues/1560))
+
 * Improved the naming convention for anonymous modules generated by the
   module system ([#1810](https://github.com/GaloisInc/cryptol/issues/1810))
 

src/Cryptol/TypeCheck/Error.hs

@@ -819,6 +819,7 @@ explainUnsolvable names gs =
 computeFreeVarNames :: [(Range,Warning)] -> [(Range,Error)] -> NameMap
 computeFreeVarNames warns errs =
   mkMap numRoots numVaras `IntMap.union` mkMap otherRoots otherVars
+    `IntMap.union` mpNames
 
   {- XXX: Currently we pick the names based on the unique of the variable:
      smaller uniques get an earlier name (e.g., 100 might get `a` and 200 `b`)
@@ -831,20 +832,16 @@ computeFreeVarNames warns errs =
   mkName x v = (tvUnique x, v)
   mkMap roots vs = IntMap.fromList (zipWith mkName vs (variants roots))
 
-  (numVaras,otherVars) = partition ((== KNum) . kindOf)
-                       $ Set.toList
-                       $ Set.filter isFreeTV
-                       $ fvs (map snd warns, map snd errs)
+  (uvars,non_uvars) = partition isFreeTV
+                    $ Set.toList
+                    $ fvs (map snd warns, map snd errs)
+
+  mpNames = computeModParamNames [ tp | TVBound tp <- non_uvars ] mempty
+
+  (numVaras,otherVars) = partition ((== KNum) . kindOf) uvars
 
   otherRoots = [ "a", "b", "c", "d" ]
   numRoots   = [ "m", "n", "u", "v" ]
 
-  useUnicode = True
+  variants roots = [ nameVariant n r | n <- [ 0 .. ], r <- roots ]
 
-  suff n
-    | n < 10 && useUnicode = [toEnum (0x2080 + n)]
-    | otherwise = show n
-
-  variant n x = if n == 0 then x else x ++ suff n
-
-  variants roots = [ variant n r | n <- [ 0 .. ], r <- roots ]

src/Cryptol/TypeCheck/InferTypes.hs

@@ -21,7 +21,7 @@ module Cryptol.TypeCheck.InferTypes where
 import           Control.Monad(guard)
 
 import           Cryptol.Parser.Position
-import           Cryptol.ModuleSystem.Name (asPrim,nameLoc)
+import           Cryptol.ModuleSystem.Name (asPrim,nameLoc,nameIdent)
 import           Cryptol.TypeCheck.AST
 import           Cryptol.TypeCheck.PP
 import           Cryptol.TypeCheck.Subst
@@ -31,10 +31,13 @@ import           Cryptol.Utils.Ident (PrimIdent(..), preludeName)
 import           Cryptol.Utils.Panic(panic)
 import           Cryptol.Utils.Misc(anyJust)
 
+import           Data.List(mapAccumL,partition)
+import           Data.Maybe(mapMaybe)
 import           Data.Set ( Set )
 import qualified Data.Set as Set
 import           Data.Map ( Map )
 import qualified Data.Map as Map
+import qualified Data.IntMap as IntMap
 
 import GHC.Generics (Generic)
 import Control.DeepSeq
@@ -323,14 +326,17 @@ cppKind ki =
     _     -> pp ki
 
 addTVarsDescsAfter :: FVS t => NameMap -> t -> Doc -> Doc
-addTVarsDescsAfter nm t d
+addTVarsDescsAfter nm t = addTVarsDescsAfterFVS nm (fvs t)
+
+addTVarsDescsAfterFVS :: NameMap -> Set TVar -> Doc -> Doc
+addTVarsDescsAfterFVS nm vs d
   | Set.null vs = d
 -- TODO? use `hang` here instead to indent things after "where"
   | otherwise   = d $$ text "where" $$ vcat (map desc (Set.toList vs))
   where
-  vs     = fvs t
   desc v = ppWithNames nm v <+> text "is" <+> pp (tvInfo v)
 
+
 addTVarsDescsBefore :: FVS t => NameMap -> t -> Doc -> Doc
 addTVarsDescsBefore nm t d = vcat (frontMsg ++ [d] ++ backMsg)
   where
@@ -393,13 +399,16 @@ instance PP (WithNames DelayedCt) where
   ppPrec _ (WithNames d names) =
     sig $$
     hang "we need to show that"
-       2 (vcat ( vars ++ asmps ++
+
+       2 (explain (vcat ( vars ++ asmps ++
                [ hang "the following constraints hold:"
                     2 (vcat
                        $ bullets
                        $ map (ppWithNames ns1)
-                       $ dctGoals d )]))
+                       $ dctGoals d )])))
     where
+
+
     bullets xs = [ "•" <+> x | x <- xs ]
 
     sig = case name of
@@ -408,12 +417,59 @@ instance PP (WithNames DelayedCt) where
             Nothing -> "when checking the module's parameters,"
 
     name  = dctSource d
-    vars = case dctForall d of
+    vars = case otherTPs of
              [] -> []
              xs -> ["for any type" <+> commaSep (map (ppWithNames ns1) xs)]
     asmps = case dctAsmps d of
               [] -> []
               xs -> [hang "assuming"
                        2 (vcat (bullets (map (ppWithNames ns1) xs)))]
 
-    ns1 = addTNames (dctForall d) names
+    tvars = fvs (dctAsmps d, dctGoals d)
+    used = filter ((`Set.member` tvars) . TVBound) (dctForall d)
+    isModP tp =
+      case tpFlav tp of
+        TPModParam {} -> True
+        _ -> False
+    (mpTPs,otherTPs) = partition isModP used
+    explain = addTVarsDescsAfterFVS ns1 (Set.fromList (map TVBound mpTPs))
+
+    mps = computeModParamNames mpTPs names
+    ns1 = addTNames otherTPs mps
+
+
+
+-- | Add a suffix to a name to make a different label.
+nameVariant :: Int -> String -> String
+nameVariant n x = if n == 0 then x else x ++ suff
+  where
+  useUnicode = True
+
+  suff
+    | n < 10 && useUnicode = [toEnum (0x2080 + n)]
+    | otherwise = show n
+
+
+
+-- | Pick names for the type parameters that correspond to module parameters,
+-- avoiding strings that already appear in the given name map.
+-- Returns and extended name map.
+computeModParamNames :: [TParam] -> NameMap -> NameMap
+computeModParamNames tps names = IntMap.fromList newNames `IntMap.union` names
+  where
+  newNames = snd (mapAccumL pickName used0 (mapMaybe isModP tps))
+
+  used0 = Set.fromList (IntMap.elems names)
+
+  pickName used (u,i) =
+    let ns   = filter (not . (`Set.member` used))
+              $ map (`nameVariant` i) [0..]
+        name = case ns of
+                 x : _ -> x
+                 []    -> panic "computeModParamNames" ["Out of names!"]
+    in (Set.insert name used, (u,name))
+
+  isModP tp =
+    case tpFlav tp of
+      TPModParam x -> Just (tpUnique tp, show (pp (nameIdent x)))
+      _ -> Nothing

src/Cryptol/Utils/Ident.hs

@@ -53,6 +53,7 @@ module Cryptol.Utils.Ident
   , mkInfix
   , isInfixIdent
   , isUpperIdent
+  , isAnonIfaceModIdnet
   , nullIdent
   , identText
   , identAnonArg
@@ -354,6 +355,14 @@ isUpperIdent (Ident _ mb t) =
     NormalName | Just (c,_) <- T.uncons t -> isUpper c
     _ -> False
 
+-- | Is this an ident for an anonymous module interface
+-- (i.e., a `parameter` block)
+isAnonIfaceModIdnet :: Ident -> Bool
+isAnonIfaceModIdnet (Ident _ ty _) =
+  case ty of
+    AnonIfaceModName -> True
+    _                -> False
+
 nullIdent :: Ident -> Bool
 nullIdent = T.null . identText
 

src/Cryptol/Utils/PP.hs

@@ -415,8 +415,8 @@ instance PP OrigName where
         Qualified m -> ppQual (TopModule m) (pp (ogName og))
         NotInScope  -> ppQual (ogModule og)
                        case ogFromParam og of
-                         Just x  -> pp x <.> "::" <.> pp (ogName og)
-                         Nothing -> pp (ogName og)
+                         Just x | not (isAnonIfaceModIdnet x) -> pp x <.> "::" <.> pp (ogName og)
+                         _ -> pp (ogName og)
     where
     ppQual mo x =
       case mo of

tests/docstrings/T02.icry.stdout

@@ -4,7 +4,7 @@ Loading module T02
 Checking module T02
   Docstrings on T02
   Docstrings on T02::where_at__27_11::n
-  Docstrings on T02::F7::F__parameter::n
+  Docstrings on T02::F7::n
   Docstrings on T02::F7::c
     :check c == 1
       Using exhaustive testing.

tests/docstrings/T07.icry.stdout

@@ -8,5 +8,5 @@ Checking module T07
   Docstrings on T07
     42 : [N]
       0x2a
-  Docstrings on T07::T07F__parameter::N
+  Docstrings on T07::N
 Successes: 1, No fences: 1, Failures: 0

tests/docstrings/T08.icry.stdout

@@ -4,7 +4,7 @@ Loading module Main
 Checking module Main
   Docstrings on Main
   Docstrings on Main::where_at__16_11::n
-  Docstrings on Main::M::F__parameter::n
+  Docstrings on Main::M::n
   Docstrings on submodule Main::where_at__16_11
   Docstrings on submodule Main::M
     "M"

tests/docstrings/T10.icry.stdout

@@ -20,7 +20,7 @@ Checking module T10
       Testing... Passed 1 tests.
       Q.E.D.
   Docstrings on T10::where_at__30_11::N
-  Docstrings on T10::F1::F__parameter::N
+  Docstrings on T10::F1::N
   Docstrings on T10::M::q
   Docstrings on T10::M::r
   Docstrings on T10::F1::s

tests/issues/issue058.icry.stdout

@@ -16,7 +16,7 @@ Loading module Main
   Failed to validate user-specified signature.
     in the definition of 'Main::last', at issue058.cry:7:1--7:5,
     we need to show that
-      for any type n, a
+      for any type n
       assuming
         • n >= 1
       the following constraints hold:

tests/issues/issue1560.icry

@@ -0,0 +1,4 @@
+:load issue1560/T1.cry
+:load issue1560/T2.cry
+:load issue1560/T3.cry
+:load issue1560/T4.cry

tests/issues/issue1560.icry.stdout

@@ -0,0 +1,82 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading interface module T1__parameter
+Loading module T1
+
+[error] at issue1560/T1.cry:7:5--7:6:
+  Unsolved constraints:
+    • fin n
+        arising from
+        use of literal or demoted expression
+        at issue1560/T1.cry:7:5--7:6
+  where
+  n is module parameter T1::n at issue1560/T1.cry:1:8--1:10
+[error] at issue1560/T1.cry:7:5--7:6:
+  Unsolved constraints:
+    • n >= 1
+        arising from
+        use of literal or demoted expression
+        at issue1560/T1.cry:7:5--7:6
+  where
+  n is module parameter T1::n at issue1560/T1.cry:1:8--1:10
+Loading module Cryptol
+Loading interface module T2__parameter
+Loading module T2
+
+[error] at issue1560/T2.cry:15:3--15:10:
+  Failed to validate user-specified signature.
+    in the definition of 'T2::F::b', at issue1560/T2.cry:15:3--15:4,
+    we need to show that
+      for any type m
+      assuming
+        • fin n
+      the following constraints hold:
+        • m == n
+            arising from
+            matching types
+            at issue1560/T2.cry:15:9--15:10
+      where
+      n is module parameter T2::n at issue1560/T2.cry:1:8--1:10
+Loading module Cryptol
+Loading module T3
+
+[error] at issue1560/T3.cry:1:1--23:13:
+  Failed to validate user-specified signature.
+    when checking the module's parameters,
+    we need to show that
+      assuming
+        • x₁ >= 1
+        • x₁ <= 4
+        • x >= 1
+        • x <= 3
+      the following constraints hold:
+        • x₁ == x
+            arising from
+            matching types
+            at issue1560/T3.cry:23:12--23:13
+      where
+      x is module parameter T3::F::I::x at issue1560/T3.cry:14:30--14:32
+      x₁ is module parameter T3::F::G::I::x at issue1560/T3.cry:20:32--20:34
+Loading module Cryptol
+Loading module T3
+
+[error] at issue1560/T4.cry:1:1--24:13:
+  Failed to validate user-specified signature.
+    when checking the module's parameters,
+    we need to show that
+      assuming
+        • x₂ >= 1
+        • x₂ <= 4
+        • x₁ >= 1
+        • x₁ <= 4
+        • x >= 1
+        • x <= 3
+      the following constraints hold:
+        • x₁ == x
+            arising from
+            matching types
+            at issue1560/T4.cry:24:12--24:13
+      where
+      x is module parameter T3::F::I::x at issue1560/T4.cry:14:30--14:32
+      x₁ is module parameter T3::F::G::I::x at issue1560/T4.cry:20:32--20:34
+      x₂ is module parameter T3::F::G::J::x at issue1560/T4.cry:21:32--21:34

tests/issues/issue1560/T1.cry

@@ -0,0 +1,7 @@
+module T1 where
+
+parameter
+  type n: #
+
+y: [n]
+y = 1

tests/issues/issue1560/T2.cry

@@ -0,0 +1,16 @@
+module T2 where
+
+parameter
+  type n: #
+  type constraint (fin n)
+
+a:[n]
+a = a
+
+submodule F where
+  parameter
+    type n: #
+
+  b: {m} [n] -> [m]
+  b _ = a
+

tests/issues/issue1560/T3.cry

@@ -0,0 +1,26 @@
+module T3 where
+
+interface submodule I1 where
+  type x: #
+  type constraint (x >= 1, x <= 3)
+
+interface submodule I2 where
+  type x: #
+  type constraint (x >= 1, x <= 4)
+
+
+
+submodule F where
+  import interface submodule I1 as I
+
+  y: [I::x]
+  y = 1
+
+  submodule G where
+    import interface submodule I2 as I
+
+    csum : [I::x]
+    csum = y
+
+
+