| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Cryptol.TypeCheck.Default
Synopsis
- defaultLiterals :: [TVar] -> [Goal] -> ([TVar], Subst, [Warning])
- flitDefaultCandidates :: Goals -> Map TVar (Maybe ((TVar, Type), Warning))
- improveByDefaultingWithPure :: [TVar] -> [Goal] -> ([TVar], [Goal], Subst, [Error])
- defaultReplExpr' :: Solver -> [TParam] -> [Prop] -> IO (Maybe [(TParam, Type)])
Documentation
defaultLiterals :: [TVar] -> [Goal] -> ([TVar], Subst, [Warning]) Source #
We default constraints of the form Literal t a and FLiteral m n r a.
For 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.
For FLiteral t a we always default to Rational.
defaultReplExpr' :: Solver -> [TParam] -> [Prop] -> IO (Maybe [(TParam, Type)]) Source #
Try to pick a reasonable instantiation for an expression with the given type. This is useful when we do evaluation at the REPL. The resulting types should satisfy the constraints of the schema. The parameters should be all of numeric kind, and the props should als be numeric