Defaulting

src/Cryptol/REPL/Command.hs

@@ -1608,11 +1608,8 @@ replEvalExpr expr =
   warnDefaults ts =
     case ts of
       [] -> return ()
-      _  ->
-        do warnDefaulting <- getKnownUser "warnDefaulting"
-           when warnDefaulting $
-             do rPutStrLn "Showing a specific instance of polymorphic result:"
-                mapM_ warnDefault ts
+      _  -> do rPutStrLn "Showing a specific instance of polymorphic result:"
+               mapM_ warnDefault ts
 
   warnDefault (x,t) =
     rPrint ("  *" <+> nest 2  ("Using" <+> quotes (pp t) <+> "for" <+>

src/Cryptol/REPL/Monad.hs

@@ -765,7 +765,7 @@ userOptions  = mkOptionMap
     "The maximum number of :sat solutions to display (\"all\" for no limit)."
   , simpleOpt "prover" (EnvString "z3") checkProver $
     "The external SMT solver for ':prove' and ':sat'\n(" ++ proverListString ++ ")."
-  , simpleOpt "warnDefaulting" (EnvBool True) noCheck
+  , simpleOpt "warnDefaulting" (EnvBool False) noCheck
     "Choose whether to display warnings when defaulting."
   , simpleOpt "warnShadowing" (EnvBool True) noCheck
     "Choose whether to display warnings when shadowing symbols."

src/Cryptol/TypeCheck/Default.hs

@@ -4,11 +4,11 @@ import qualified Data.Set as Set
 import qualified Data.Map as Map
 import Data.Maybe(mapMaybe)
 import Data.List((\\),nub)
-import Control.Monad(guard)
+import Control.Monad(guard,mzero)
 
 import Cryptol.TypeCheck.Type
-import Cryptol.TypeCheck.SimpType(tMax,tWidth)
-import Cryptol.TypeCheck.Error(Warning(..))
+import Cryptol.TypeCheck.SimpType(tMax)
+import Cryptol.TypeCheck.Error(Warning(..), Error(..))
 import Cryptol.TypeCheck.Subst(Subst,apSubst,listSubst,substBinds,uncheckedSingleSubst)
 import Cryptol.TypeCheck.InferTypes(Goal,goal,Goals(..),goalsFromList)
 import Cryptol.TypeCheck.Solver.SMT(Solver,tryGetModel,shrinkModel)
@@ -17,16 +17,29 @@ import Cryptol.Utils.Panic(panic)
 
 --------------------------------------------------------------------------------
 
--- | We default constraints of the form @Literal t a@ to @a := [width t]@
+-- | We default constraints of the form @Literal t a@.
+--
+--   We examine the context of constraints on the type @a@
+--   to decide how to default.  If @Logic a@ is required,
+--   we cannot do any defaulting.  Otherwise, we default
+--   to either @Integer@ or @Rational@.  In particular, if
+--   we need to satisfy the @Field a@, constraint, we choose
+--   @Rational@ and otherwise we choose @Integer@.
 defaultLiterals :: [TVar] -> [Goal] -> ([TVar], Subst, [Warning])
 defaultLiterals as gs = let (binds,warns) = unzip (mapMaybe tryDefVar as)
                         in (as \\ map fst binds, listSubst binds, warns)
   where
   gSet = goalsFromList gs
+  allProps = saturatedPropSet gSet
   tryDefVar a =
-    do gt <- Map.lookup a (literalGoals gSet)
+    do _gt <- Map.lookup a (literalGoals gSet)
+       defT <- if Set.member (pLogic (TVar a)) allProps then
+                  mzero
+               else if Set.member (pField (TVar a)) allProps then
+                  pure tRational
+               else
+                  pure tInteger
        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.
@@ -35,9 +48,6 @@ defaultLiterals as gs = let (binds,warns) = unzip (mapMaybe tryDefVar as)
        return ((a,defT),w)
 
 
-
-
-
 --------------------------------------------------------------------------------
 
 -- This is what we use to avoid ambiguity when generalizing.
@@ -72,7 +82,7 @@ improveByDefaultingWithPure :: [TVar] -> [Goal] ->
     ( [TVar]    -- non-defaulted
     , [Goal]    -- new constraints
     , Subst     -- improvements from defaulting
-    , [Warning] -- warnings about defaulting
+    , [Error]   -- width defaulting errors
     )
 improveByDefaultingWithPure as ps =
   classify (Map.fromList [ (a,([],Set.empty)) | a <- as ]) [] [] ps
@@ -88,7 +98,7 @@ improveByDefaultingWithPure as ps =
         su                 = listSubst defs
         warn (x,t) =
           case x of
-            TVFree _ _ _ d -> DefaultingTo d t
+            TVFree _ _ _ d -> AmbiguousSize d t
             TVBound {} -> panic "Crypto.TypeCheck.Infer"
                  [ "tryDefault attempted to default a quantified variable."
                  ]

src/Cryptol/TypeCheck/Error.hs

@@ -114,6 +114,9 @@ data Error    = ErrorMsg Doc
 
               | RepeatedTypeParameter Ident [Range]
 
+              | AmbiguousSize TVarInfo 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.
                 deriving (Show, Generic, NFData)
 
 instance TVars Warning where
@@ -152,6 +155,7 @@ instance TVars Error where
 
       UndefinedTypeParameter {} -> err
       RepeatedTypeParameter {} -> err
+      AmbiguousSize x t -> AmbiguousSize x (apSubst su t)
 
 
 instance FVS Error where
@@ -176,7 +180,7 @@ instance FVS Error where
       CannotMixPositionalAndNamedTypeParams -> Set.empty
       UndefinedTypeParameter {}             -> Set.empty
       RepeatedTypeParameter {}              -> Set.empty
-
+      AmbiguousSize _ t -> fvs t
 
 
 instance PP Warning where
@@ -316,6 +320,11 @@ instance PP (WithNames Error) where
         "Multiple definitions for type parameter `" <.> pp x <.> "`:"
           $$ 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
+
     where
     bullets xs = vcat [ "•" <+> d | d <- xs ]
 

src/Cryptol/TypeCheck/Infer.hs

@@ -26,7 +26,7 @@ where
 import qualified Data.Text as Text
 
 
-import           Cryptol.ModuleSystem.Name (asPrim,lookupPrimDecl,nameLoc)
+import           Cryptol.ModuleSystem.Name (lookupPrimDecl,nameLoc)
 import           Cryptol.Parser.Position
 import qualified Cryptol.Parser.AST as P
 import qualified Cryptol.ModuleSystem.Exports as P
@@ -43,7 +43,6 @@ import           Cryptol.TypeCheck.Kind(checkType,checkSchema,checkTySyn,
 import           Cryptol.TypeCheck.Instantiate
 import           Cryptol.TypeCheck.Depends
 import           Cryptol.TypeCheck.Subst (listSubst,apSubst,(@@),isEmptySubst)
-import           Cryptol.TypeCheck.Solver.InfNat(genLog)
 import           Cryptol.Utils.Ident
 import           Cryptol.Utils.Panic(panic)
 import           Cryptol.Utils.PP
@@ -104,8 +103,8 @@ mkPrim' str =
 
 
 
-desugarLiteral :: Bool -> P.Literal -> InferM (P.Expr Name)
-desugarLiteral fixDec lit =
+desugarLiteral :: P.Literal -> InferM (P.Expr Name)
+desugarLiteral lit =
   do l <- curRange
      numberPrim <- mkPrim "number"
      fracPrim   <- mkPrim "fraction"
@@ -121,13 +120,7 @@ desugarLiteral fixDec lit =
            P.BinLit n    -> [ ("rep", tBits (1 * toInteger n)) ]
            P.OctLit n    -> [ ("rep", tBits (3 * toInteger n)) ]
            P.HexLit n    -> [ ("rep", tBits (4 * toInteger n)) ]
-           P.DecLit
-            | fixDec     -> if num == 0
-                              then [ ("rep", tBits 0)]
-                              else case genLog num 2 of
-                                     Just (x,_) -> [ ("rep", tBits (x + 1)) ]
-                                     _          -> []
-            | otherwise  -> [ ]
+           P.DecLit      -> [ ]
            P.PolyLit _n  -> [ ("rep", P.TSeq P.TWild P.TBit) ]
 
        P.ECFrac fr info ->
@@ -161,7 +154,7 @@ appTys expr ts tGoal =
          checkHasType t tGoal
          return e'
 
-    P.ELit l -> do e <- desugarLiteral False l
+    P.ELit l -> do e <- desugarLiteral l
                    appTys e ts tGoal
 
 
@@ -251,7 +244,7 @@ checkE expr tGoal =
          checkE (P.EApp prim e) tGoal
 
     P.ELit l@(P.ECNum _ P.DecLit) ->
-      do e <- desugarLiteral False l
+      do e <- desugarLiteral l
          -- NOTE: When 'l' is a decimal literal, 'desugarLiteral' does
          -- not generate an instantiation for the 'rep' type argument
          -- of the 'number' primitive. Therefore we explicitly
@@ -263,7 +256,7 @@ checkE expr tGoal =
                            }
          appTys e [arg] tGoal
 
-    P.ELit l -> (`checkE` tGoal) =<< desugarLiteral False l
+    P.ELit l -> (`checkE` tGoal) =<< desugarLiteral l
 
     P.ETuple es ->
       do etys <- expectTuple (length es) tGoal
@@ -335,16 +328,6 @@ checkE expr tGoal =
 
     P.EAppT e fs -> appTys e (map uncheckedTypeArg fs) tGoal
 
-    P.EApp fun@(dropLoc -> P.EApp (dropLoc -> P.EVar c) _)
-           arg@(dropLoc -> P.ELit l)
-      | Just n <- asPrim c
-      , n `elem` map prelPrim [ "<<", ">>", "<<<", ">>>" , "@", "!" ] ->
-        do newArg <- do l1 <- desugarLiteral True l
-                        return $ case arg of
-                                   P.ELocated _ pos -> P.ELocated l1 pos
-                                   _ -> l1
-           checkE (P.EApp fun newArg) tGoal
-
     P.EApp e1 e2 ->
       do t1  <- newType (TypeOfArg Nothing) KType
          e1' <- checkE e1 (tFun t1 tGoal)
@@ -821,10 +804,11 @@ generalize bs0 gs0 =
      {- See if we might be able to default some of the potentially ambiguous
         variables using the constraints that will be part of the newly
         generalized schema.  -}
-     let (as0,here1,defSu,ws) = defaultAndSimplify maybeAmbig here0
+     let (as0,here1,defSu,ws,errs) = defaultAndSimplify maybeAmbig here0
 
      extendSubst defSu
      mapM_ recordWarning ws
+     mapM_ recordError errs
      let here = map goal here1
 
 

src/Cryptol/TypeCheck/InferTypes.hs

@@ -104,7 +104,9 @@ insertGoal g gls
        -- XXX: here we are arbitrarily using the info of the first goal,
        -- which could lead to a confusing location for a constraint.
        let jn g1 g2 = g1 { goal = tMax (goal g1) (goal g2) } in
-       gls { literalGoals = Map.insertWith jn a newG (literalGoals gls) }
+       gls { literalGoals = Map.insertWith jn a newG (literalGoals gls)
+           , saturatedPropSet = Set.insert (pFin (TVar a)) (saturatedPropSet gls)
+           }
 
   -- If the goal is already implied by some other goal, skip it
   | Set.member (goal g) (saturatedPropSet gls) = gls

src/Cryptol/TypeCheck/Monad.hs

@@ -310,7 +310,9 @@ curRange = IM $ asks iRange
 -- | Report an error.
 recordError :: Error -> InferM ()
 recordError e =
-  do r <- curRange
+  do r <- case e of
+            AmbiguousSize d _ -> return (tvarSource d)
+            _ -> curRange
      IM $ sets_ $ \s -> s { iErrors = (r,e) : iErrors s }
 
 recordWarning :: Warning -> InferM ()

src/Cryptol/TypeCheck/Solve.hs

@@ -155,11 +155,12 @@ defaultReplExpr sol expr sch =
                       (sProps sch)
 
 
-defaultAndSimplify :: [TVar] -> [Goal] -> ([TVar],[Goal],Subst,[Warning])
+defaultAndSimplify :: [TVar] -> [Goal] -> ([TVar],[Goal],Subst,[Warning],[Error])
 defaultAndSimplify as gs =
-  let (as1, gs1, su1, ws1) = defLit
-      (as2, gs2, su2, ws2) = improveByDefaultingWithPure as1 gs1
-  in (as2,gs2,su2 @@ su1, ws1 ++ ws2)
+  let (as1, gs1, su1, ws) = defLit
+      (as2, gs2, su2, errs) = improveByDefaultingWithPure as1 gs1
+  in (as2,gs2,su2 @@ su1, ws, errs)
+
   where
   defLit
     | isEmptySubst su = nope
@@ -207,9 +208,10 @@ proveModuleTopLevel =
   do simplifyAllConstraints
      gs <- getGoals
      let vs = Set.toList (Set.filter isFreeTV (fvs gs))
-         (_,gs1,su1,ws) = defaultAndSimplify vs gs
+         (_,gs1,su1,ws,errs) = defaultAndSimplify vs gs
      extendSubst su1
      mapM_ recordWarning ws
+     mapM_ recordError errs
 
      cs <- getParamConstraints
      case cs of
@@ -230,8 +232,8 @@ proveImplication lnam as ps gs =
      (mbErr,su) <- io (proveImplicationIO solver lnam evars
                             (extraAs ++ as) (extra ++ ps) gs)
      case mbErr of
-       Right ws -> mapM_ recordWarning ws
-       Left err -> recordError err
+       Right ws  -> mapM_ recordWarning ws
+       Left errs -> mapM_ recordError errs
      return su
 
 
@@ -242,13 +244,13 @@ proveImplicationIO :: Solver
                    -> [TParam] -- ^ Type parameters
                    -> [Prop]   -- ^ Assumed constraint
                    -> [Goal]   -- ^ Collected constraints
-                   -> IO (Either Error [Warning], Subst)
+                   -> IO (Either [Error] [Warning], Subst)
 proveImplicationIO _   _     _         _  [] [] = return (Right [], emptySubst)
 proveImplicationIO s f varsInEnv ps asmps0 gs0 =
   do let ctxt = buildSolverCtxt asmps
      res <- quickSolverIO ctxt gs
      case res of
-       Left (msg,bad) -> return (Left (UnsolvedGoals (Just msg) [bad]), emptySubst)
+       Left (msg,bad) -> return (Left [UnsolvedGoals (Just msg) [bad]], emptySubst)
        Right (su,[]) -> return (Right [], su)
        Right (su,gs1) ->
          do gs2 <- proveImp s asmps gs1
@@ -259,25 +261,27 @@ proveImplicationIO s f varsInEnv ps asmps0 gs0 =
                             $ Set.toList
                             $ Set.difference (fvs (map goal gs3)) varsInEnv
                    case defaultAndSimplify free gs3 of
-                     (_,_,newSu,_)
+                     (_,_,newSu,_,errs)
                         | isEmptySubst newSu ->
-                                 return (err gs3, su) -- XXX: Old?
-                     (_,newGs,newSu,ws) ->
+                                 return (Left (err gs3:errs), su) -- XXX: Old?
+                     (_,newGs,newSu,ws,errs) ->
                        do let su1 = newSu @@ su
                           (res1,su2) <- proveImplicationIO s f varsInEnv ps
                                                  (apSubst su1 asmps0) newGs
                           let su3 = su2 @@ su1
                           case res1 of
-                            Left bad -> return (Left bad, su3)
-                            Right ws1 -> return (Right (ws++ws1),su3)
+                            Left bad -> return (Left (bad ++ errs), su3)
+                            Right ws1
+                              | null errs -> return (Right (ws++ws1),su3)
+                              | otherwise -> return (Left errs, su3)
   where
-  err us =  Left $ cleanupError
-                 $ UnsolvedDelayedCt
-                 $ DelayedCt { dctSource = f
-                             , dctForall = ps
-                             , dctAsmps  = asmps0
-                             , dctGoals  = us
-                             }
+  err us = cleanupError
+           $ UnsolvedDelayedCt
+           $ DelayedCt { dctSource = f
+                       , dctForall = ps
+                       , dctAsmps  = asmps0
+                       , dctGoals  = us
+                       }
 
 
   asmps1 = concatMap pSplitAnd asmps0
@@ -319,9 +323,12 @@ buildSolverCtxt ps0 =
  saturateProps gs [] = gs
  saturateProps gs (p:ps)
    | Set.member p gs = saturateProps gs ps
-   | otherwise       = saturateProps gs' ps
-       where
-       gs' = Set.singleton p <> superclassSet p <> gs
+   | Just (n,_) <- pIsLiteral p =
+       let gs' = Set.fromList [p, pFin n] <> gs
+        in saturateProps gs' ps
+   | otherwise =
+        let gs' = Set.singleton p <> superclassSet p <> gs
+         in saturateProps gs' ps
 
  assumptionIntervals as ps =
    case computePropIntervals as ps of

tests/issues/allexamples.icry

@@ -1,4 +1,3 @@
-:set warnDefaulting = off
 :cd ../../examples
 :l AE.cry
 :l AES.cry

tests/issues/issue084.icry.stdout

@@ -2,8 +2,6 @@ Loading module Cryptol
 Showing a specific instance of polymorphic result:
   * Using '5' for type argument 'n' of 'Cryptol::lg2'
 0x03
-[warning] at <interactive>:1:1--1:4:
-  Defaulting type argument 'n' of 'lg2' to 5
 
 [error] at <interactive>:1:1--1:4:
   Type mismatch:

tests/issues/issue116.icry

@@ -1,3 +1,2 @@
-:set warnDefaulting = off
 :l issue116.cry
 bug116fixed

tests/issues/issue138.icry

@@ -1,4 +1,3 @@
-:s warnDefaulting=off
 :l issue138.cry
 down
 down'

tests/issues/issue148.icry

@@ -1,3 +1,2 @@
-:set warnDefaulting = off
 :l issue148.cry
 :sat (\(e:[64]) -> (e@@[8..24]) != zero)