Merge pull request #817 from GaloisInc/issue802

Suppress the `Must be at least` line of defaulting error

src/Cryptol/TypeCheck/Default.hs

@@ -96,19 +96,20 @@ improveByDefaultingWithPure as ps =
     let -- First, we use the `leqs` to choose some definitions.
         (defs, newOthers)  = select [] [] (fvs others) (Map.toList leqs)
         su                 = listSubst defs
-        warn (x,t) =
+        names              = substBinds su
+        mkErr (x,t) =
           case x of
-            TVFree _ _ _ d -> AmbiguousSize d t
+            TVFree _ _ _ d
+              | Just 0 <- tIsNum t -> AmbiguousSize d Nothing
+              | otherwise -> AmbiguousSize d (Just t)
             TVBound {} -> panic "Crypto.TypeCheck.Infer"
                  [ "tryDefault attempted to default a quantified variable."
                  ]
 
-        names = substBinds su
-
     in ( [ a | a <- as, not (a `Set.member` names) ]
        , newOthers ++ others ++ nub (apSubst su fins)
        , su
-       , map warn defs
+       , map mkErr defs
        )
 
 

src/Cryptol/TypeCheck/Error.hs

@@ -114,9 +114,10 @@ data Error    = ErrorMsg Doc
 
               | RepeatedTypeParameter Ident [Range]
 
-              | AmbiguousSize TVarInfo Type
+              | AmbiguousSize TVarInfo (Maybe Type)
                 -- ^ Could not determine the value of a numeric type variable,
-                --   but we know it must be at least as large as the given type.
+                --   but we know it must be at least as large as the given type
+                --   (or unconstrained, if Nothing).
                 deriving (Show, Generic, NFData)
 
 instance TVars Warning where
@@ -325,9 +326,11 @@ instance PP (WithNames Error) where
           $$ nest 2 (bullets (map pp rs))
 
       AmbiguousSize x t ->
-        addTVarsDescsAfter names err $
-        "Ambiguous numeric type:" <+> pp (tvarDesc x)
-          $$ "Must be at least:" <+> ppWithNames names t
+        let sizeMsg =
+               case t of
+                 Just t' -> "Must be at least:" <+> ppWithNames names t'
+                 Nothing -> empty
+         in addTVarsDescsAfter names err ("Ambiguous numeric type:" <+> pp (tvarDesc x) $$ sizeMsg)
 
     where
     bullets xs = vcat [ "•" <+> d | d <- xs ]

tests/mono-binds/test05.icry.stdout

@@ -51,4 +51,3 @@ Loading module test05
 
 [error] at test05.cry:14:11--14:21:
   Ambiguous numeric type: type argument 'front' of '(#)'
-  Must be at least: 0