Improvements to naming of variables.

This does a bunch of small changes, that should improve the usability
of Cryptol.  Namely:
  * When we are forced to make up a name, pick something derived from
    the source of the variable, annotated with the unique.
  * When pretty printing a schema, use "n,m,i,j,k" for numeric variables
    and "a,b,c,d,e" for value type vairable.
  * When generalizing, put numeric vairables first.

src/Cryptol/TypeCheck/Default.hs

@@ -25,8 +25,8 @@ defaultLiterals as gs = let (binds,warns) = unzip (mapMaybe tryDefVar as)
   gSet = goalsFromList gs
   tryDefVar a =
     do gt <- Map.lookup a (literalGoals gSet)
-       d  <- tvInfo a
-       let defT = tWord (tWidth (goal gt))
+       let d    = tvInfo a
+           defT = tWord (tWidth (goal gt))
            w    = DefaultingTo d defT
        guard (not (Set.member a (fvs defT)))  -- Currently shouldn't happen
                                               -- but future proofing.

src/Cryptol/TypeCheck/Error.hs

@@ -179,14 +179,15 @@ instance FVS Error where
       UnsolvedGoals _ gs        -> fvs gs
       UnsolvedDelayedCt g       -> fvs g
       UnexpectedTypeWildCard    -> Set.empty
-      TypeVariableEscaped t _   -> fvs t
-      NotForAll _ t             -> fvs t
+      TypeVariableEscaped t xs  -> fvs t `Set.union`
+                                            Set.fromList (map TVBound xs)
+      NotForAll x t             -> Set.insert x (fvs t)
       UnusableFunction _ p      -> fvs p
       TooManyPositionalTypeParams -> Set.empty
       CannotMixPositionalAndNamedTypeParams -> Set.empty
-      AmbiguousType _ _vs       ->  Set.empty
-      UndefinedTypeParameter {} -> Set.empty
-      RepeatedTypeParameter {}  -> Set.empty
+      AmbiguousType _ _vs                   ->  Set.empty
+      UndefinedTypeParameter {}             -> Set.empty
+      RepeatedTypeParameter {}              -> Set.empty
 
 
 

src/Cryptol/TypeCheck/Infer.hs

@@ -39,7 +39,7 @@ import           Cryptol.Utils.PP
 import qualified Data.Map as Map
 import           Data.Map (Map)
 import qualified Data.Set as Set
-import           Data.List(foldl')
+import           Data.List(foldl',sortBy)
 import           Data.Either(partitionEithers)
 import           Data.Maybe(mapMaybe,isJust, fromMaybe)
 import           Data.List(partition,find)
@@ -236,7 +236,7 @@ checkE expr tGoal =
       do let src = case l of
                      RecordSel la _ -> TypeOfRecordField la
                      TupleSel n _   -> TypeOfTupleField n
-                     ListSel n _    -> TypeOfSeqAt n
+                     ListSel _ _    -> TypeOfSeqElement
          t <- newType src KType
          e' <- checkE e t
          f <- newHasGoal l t tGoal
@@ -727,7 +727,8 @@ generalize bs0 gs0 =
      {- This is the variables we'll be generalizing:
           * any ones that survived the defaulting
           * and vars in the inferred types that do not appear anywhere else. -}
-     let as   = as0 ++ Set.toList (Set.difference inSigs asmpVs)
+     let as   = sortBy numFst
+              $ as0 ++ Set.toList (Set.difference inSigs asmpVs)
          asPs = [ TParam { tpUnique = x, tpKind = k, tpFlav = TPOther Nothing
                          , tpInfo = i  } | TVFree x k _ i <- as ]
 
@@ -750,6 +751,12 @@ generalize bs0 gs0 =
 
      return (map genB bs)
 
+  where
+  numFst x y = case (kindOf x, kindOf y) of
+                 (KNum, KNum) -> EQ
+                 (KNum, _)    -> LT
+                 (_,KNum)     -> GT
+                 _            -> EQ
 
 -- | Check a monomorphic binding.
 checkMonoB :: P.Bind Name -> Type -> InferM Decl

src/Cryptol/TypeCheck/InferTypes.hs

@@ -242,9 +242,8 @@ addTVarsDescs nm t d
   | Set.null vs = d
   | otherwise   = d $$ text "where" $$ vcat (map desc (Set.toList vs))
   where
-  vs                      = Set.filter isFreeTV (fvs t)
-  desc v@(TVFree _ _ _ x) = ppWithNames nm v <+> text "is" <+> pp x
-  desc (TVBound {})       = empty
+  vs     = fvs t -- Set.filter isFreeTV (fvs t)
+  desc v = ppWithNames nm v <+> text "is" <+> pp (tvInfo v)
 
 
 

src/Cryptol/TypeCheck/PP.hs

@@ -12,7 +12,7 @@ module Cryptol.TypeCheck.PP
   ( NameMap, WithNames(..)
   , emptyNameMap
   , ppWithNamesPrec, ppWithNames
-  , intToName, nameList
+  , nameList
   , dump
   , module Cryptol.Utils.PP
   ) where
@@ -57,6 +57,4 @@ nameList names = concat $ transpose $ map nameVariants baseNames
   baseNames | null names = map (:[]) [ 'a' .. 'z' ]
             | otherwise  = names
 
-intToName :: Int -> String
-intToName x = nameList [] !! x
 

src/Cryptol/TypeCheck/Type.hs

@@ -124,11 +124,11 @@ data TVar   = TVFree !Int Kind (Set TParam) TVarInfo
             | TVBound {-# UNPACK #-} !TParam
               deriving (Show, Generic, NFData)
 
-tvInfo :: TVar -> Maybe TVarInfo
+tvInfo :: TVar -> TVarInfo
 tvInfo tv =
   case tv of
-    TVFree _ _ _ d -> Just d
-    _              -> Nothing
+    TVFree _ _ _ d -> d
+    TVBound tp     -> tpInfo tp
 
 data TVarInfo = TVarInfo { tvarSource :: Range -- ^ Source code that gave rise
                          , tvarDesc   :: TVarSource -- ^ Description
@@ -141,7 +141,6 @@ data TVarSource = TVFromModParam Name     -- ^ Name of module parameter
                 | TypeWildCard
                 | TypeOfRecordField Ident
                 | TypeOfTupleField Int
-                | TypeOfSeqAt Int
                 | TypeOfSeqElement
                 | LenOfSeq
                 | TypeParamInstNamed {-Fun-}Name {-Param-}Ident
@@ -784,14 +783,18 @@ instance PP (WithNames TParam) where
 
 addTNames :: [TParam] -> NameMap -> NameMap
 addTNames as ns = foldr (uncurry IntMap.insert) ns
-                $ named ++ zip unnamed avail
+                $ named ++ zip unnamed_nums numNames
+                        ++ zip unnamed_vals valNames
 
-  where avail   = filter (`notElem` used) (nameList [])
+  where avail xs = filter (`notElem` used) (nameList xs)
+        numNames = avail ["n","m","i","j","k"]
+        valNames = avail ["a","b","c","d","e"]
 
-        nm x = (tpUnique x, tpName x)
+        nm x = (tpUnique x, tpName x, tpKind x)
 
-        named   = [ (u,show (pp n)) | (u,Just n)  <- map nm as ]
-        unnamed = [ u               | (u,Nothing) <- map nm as ]
+        named        = [ (u,show (pp n)) | (u,Just n,_)  <- map nm as ]
+        unnamed_nums = [ u               | (u,Nothing,KNum)  <- map nm as ]
+        unnamed_vals = [ u               | (u,Nothing,KType) <- map nm as ]
 
         used    = map snd named ++ IntMap.elems ns
 
@@ -809,7 +812,7 @@ instance PP Schema where
 instance PP (WithNames Schema) where
   ppPrec _ (WithNames s ns)
     | null (sVars s) && null (sProps s) = body
-    | otherwise = hang (vars <+> props) 2 body 
+    | otherwise = hang (vars <+> props) 2 body
     where
     body = ppWithNames ns1 (sType s)
 
@@ -921,11 +924,39 @@ instance PP (WithNames TVar) where
       Just a  -> text a
       Nothing ->
         case tpFlav x of
-          TPModParam n -> ppPrefixName n
-          _ -> text ("a`" ++ show (tpUnique x))
-
-  ppPrec _ (WithNames (TVFree x _ _ _) _) =
-    char '?' <.> text (intToName x)
+          TPModParam n     -> ppPrefixName n
+          TPOther (Just n) -> pp n <> "`" <> int (tpUnique x)
+          _  -> pickTVarName (tpKind x) (tvarDesc (tpInfo x)) (tpUnique x)
+
+  ppPrec _ (WithNames (TVFree x k _ d) _) =
+    char '?' <.> pickTVarName k (tvarDesc d) x
+
+pickTVarName :: Kind -> TVarSource -> Int -> Doc
+pickTVarName k src uni =
+  text $
+  case src of
+    TVFromModParam n       -> using n
+    TVFromSignature n      -> using n
+    TypeWildCard           -> case k of
+                                KNum -> "n"
+                                _    -> "a"
+    TypeOfRecordField i    -> using i
+    TypeOfTupleField n     -> mk ("tup_" ++ show n)
+    TypeOfSeqElement       -> mk "a"
+    LenOfSeq               -> mk "n"
+    TypeParamInstNamed _ i -> using i
+    TypeParamInstPos f n   -> mk (sh f ++ "_" ++ show n)
+    DefinitionOf x         -> using x
+    LenOfCompGen           -> mk "n"
+    TypeOfArg mb           -> mk (case mb of
+                                    Nothing -> "arg"
+                                    Just n  -> "arg_" ++ show n)
+    TypeOfRes              -> "res"
+    TypeErrorPlaceHolder   -> "err"
+  where
+  sh a      = show (pp a)
+  using a   = mk (sh a)
+  mk a      = a ++ "`" ++ show uni
 
 instance PP TVar where
   ppPrec = ppWithNamesPrec IntMap.empty
@@ -1006,11 +1037,10 @@ instance PP TVarSource where
   ppPrec _ tvsrc =
     case tvsrc of
       TVFromModParam m    -> "module parameter" <+> pp m
-      TVFromSignature x   -> "type variable" <+> quotes (pp x)
+      TVFromSignature x   -> "signature variable" <+> quotes (pp x)
       TypeWildCard        -> "type wildcard (_)"
       TypeOfRecordField l -> "type of field" <+> quotes (pp l)
       TypeOfTupleField n  -> "type of" <+> ordinal n <+> "tuple field"
-      TypeOfSeqAt n       -> "type of" <+> ordinal n <+> "sequence member"
       TypeOfSeqElement    -> "type of sequence member"
       LenOfSeq            -> "length of sequnce"
       TypeParamInstNamed f i -> "type argument" <+> quotes (pp i) <+>

tests/issues/T146.icry.stdout

@@ -3,12 +3,14 @@ Loading module Cryptol
 Loading module Main
 
 [error] at ./T146.cry:1:18--6:10:
-  The type ?s33 is not sufficiently polymorphic.
-    It cannot depend on quantified variables: a`860
+  The type ?fv`876 is not sufficiently polymorphic.
+    It cannot depend on quantified variables: fv`860
   where
-  ?s33 is type argument 'fv' of 'Main::ec_v1' at ./T146.cry:4:19--4:24
+  ?fv`876 is type argument 'fv' of 'Main::ec_v1' at ./T146.cry:4:19--4:24
+  fv`860 is signature variable 'fv' at ./T146.cry:11:10--11:12
 [error] at ./T146.cry:5:19--5:24:
-  The type ?u33 is not sufficiently polymorphic.
-    It cannot depend on quantified variables: a`860
+  The type ?fv`878 is not sufficiently polymorphic.
+    It cannot depend on quantified variables: fv`860
   where
-  ?u33 is type argument 'fv' of 'Main::ec_v2' at ./T146.cry:5:19--5:24
+  ?fv`878 is type argument 'fv' of 'Main::ec_v2' at ./T146.cry:5:19--5:24
+  fv`860 is signature variable 'fv' at ./T146.cry:11:10--11:12

tests/issues/issue150.icry.stdout

@@ -1,4 +1,4 @@
 Loading module Cryptol
 Loading module Cryptol
 Loading module Main
-maxSeq' : {a, b} (Cmp a, Literal 0 a) => [b]a -> [1 + b]a
+maxSeq' : {n, a} (Cmp a, Literal 0 a) => [n]a -> [1 + n]a

tests/issues/issue290v2.icry.stdout

@@ -4,7 +4,9 @@ Loading module Main
 
 [error] at ./issue290v2.cry:2:1--2:19:
   Unsolved constraints:
-    a`857 == 1
+    n`857 == 1
       arising from
       checking a pattern: type of 1st argument of Main::minMax
       at ./issue290v2.cry:2:8--2:11
+  where
+  n`857 is signature variable 'n' at ./issue290v2.cry:1:11--1:12

tests/issues/issue410.icry.stdout

@@ -1,8 +1,8 @@
 Loading module Cryptol
-{a, b} (Logic b) => a == min (1 + a) a
-{a, b} (Logic b) => Logic b
-{a, b} (Logic b) => Logic b
-{a, b} (Logic b) => True
+{n, a} (Logic a) => n == min (1 + n) n
+{n, a} (Logic a) => Logic a
+{n, a} (Logic a) => Logic a
+{n, a} (Logic a) => True
 (s
  where
    s x =
@@ -11,11 +11,11 @@ Loading module Cryptol
           bs = [complement b | b <- [complement x] # bs
                              | _ <- bs]
         )
- ) : {a, b} (Logic b) => b -> [a]b
-{a, b} a == a
+ ) : {n, a} (Logic a) => a -> [n]a
+{n, a} n == n
 (bs
  where
    bs = [b | b <- bs]
- ) : {a, b} [a]b
+ ) : {n, a} [n]a
 1 == 1
 [b | b <- [True]] : [1]

tests/mono-binds/test01.icry.stdout

@@ -4,13 +4,13 @@ Loading module test01
 module test01
 import Cryptol
 /* Not recursive */
-test01::a : {a, b} (fin a) => [a]b -> [2 * a]b
-test01::a = \{a, b} (fin a) (x : [a]b) ->
-            test01::f a x
+test01::a : {n, a} (fin n) => [n]a -> [2 * n]a
+test01::a = \{n, a} (fin n) (x : [n]a) ->
+            test01::f n x
             where
               /* Not recursive */
-              test01::f : {c} [c]b -> [a + c]b
-              test01::f = \{c} (y : [c]b) -> (Cryptol::#) a c b <> x y
+              test01::f : {m} [m]a -> [n + m]a
+              test01::f = \{m} (y : [m]a) -> (Cryptol::#) n m a <> x y
 
 
 
@@ -19,13 +19,13 @@ Loading module test01
 module test01
 import Cryptol
 /* Not recursive */
-test01::a : {a, b} (fin a) => [a]b -> [2 * a]b
-test01::a = \{a, b} (fin a) (x : [a]b) ->
+test01::a : {n, a} (fin n) => [n]a -> [2 * n]a
+test01::a = \{n, a} (fin n) (x : [n]a) ->
             test01::f x
             where
               /* Not recursive */
-              test01::f : [a]b -> [2 * a]b
-              test01::f = \ (y : [a]b) -> (Cryptol::#) a a b <> x y
+              test01::f : [n]a -> [2 * n]a
+              test01::f = \ (y : [n]a) -> (Cryptol::#) n n a <> x y
 
 
 

tests/mono-binds/test05.icry.stdout

@@ -14,27 +14,27 @@ test05::foo : [10]
 test05::foo = Cryptol::demote 10 [10] <>
 
 /* Not recursive */
-test05::test : {a, b, c} (Zero b, Literal 10 c) => [a]b -> c
-test05::test = \{a, b, c} (Zero b, Literal 10 c) (a : [a]b) ->
-               Cryptol::demote 10 c <>
+test05::test : {n, a, b} (Zero a, Literal 10 b) => [n]a -> b
+test05::test = \{n, a, b} (Zero a, Literal 10 b) (a : [n]a) ->
+               Cryptol::demote 10 b <>
                where
                  /* Not recursive */
                  test05::foo : [10]
                  test05::foo = Cryptol::demote 10 [10] <>
 
                  /* Not recursive */
-                 test05::f : {d} (fin d) => [a + d]b
-                 test05::f = \{d} (fin d) ->
-                             test05::bar d <>
+                 test05::f : {m} (fin m) => [n + m]a
+                 test05::f = \{m} (fin m) ->
+                             test05::bar m <>
                              where
                                /* Not recursive */
-                               test05::foo : [a]b
+                               test05::foo : [n]a
                                test05::foo = a
 
                                /* Not recursive */
-                               test05::bar : {e} (fin e) => [e + a]b
-                               test05::bar = \{e} (fin e) ->
-                                             (Cryptol::#) e a b <> (Cryptol::zero ([e]b) <>) test05::foo
+                               test05::bar : {i} (fin i) => [i + n]a
+                               test05::bar = \{i} (fin i) ->
+                                             (Cryptol::#) i n a <> (Cryptol::zero ([i]a) <>) test05::foo
 
 
 
@@ -57,25 +57,25 @@ test05::foo : [10]
 test05::foo = Cryptol::demote 10 [10] <>
 
 /* Not recursive */
-test05::test : {a, b, c} (Zero b, Literal 10 c) => [a]b -> c
-test05::test = \{a, b, c} (Zero b, Literal 10 c) (a : [a]b) ->
-               Cryptol::demote 10 c <>
+test05::test : {n, a, b} (Zero a, Literal 10 b) => [n]a -> b
+test05::test = \{n, a, b} (Zero a, Literal 10 b) (a : [n]a) ->
+               Cryptol::demote 10 b <>
                where
                  /* Not recursive */
                  test05::foo : [10]
                  test05::foo = Cryptol::demote 10 [10] <>
 
                  /* Not recursive */
-                 test05::f : [a]b
+                 test05::f : [n]a
                  test05::f = test05::bar
                              where
                                /* Not recursive */
-                               test05::foo : [a]b
+                               test05::foo : [n]a
                                test05::foo = a
 
                                /* Not recursive */
-                               test05::bar : [a]b
-                               test05::bar = (Cryptol::#) 0 a b <> (Cryptol::zero ([0]b) <>) test05::foo
+                               test05::bar : [n]a
+                               test05::bar = (Cryptol::#) 0 n a <> (Cryptol::zero ([0]a) <>) test05::foo