When `:set mono-binds=on`, any local definitions lacking type
signatures will not be generalized (i.e., will be monomorphic). This
reduces what is in most cases unnecessary polymorphism that can give
rise to constraints that are difficult to solve. This also improves
the performance of the Cryptol interpreter by lifting many polymorphic
type applications out of the inner loops that are commonly defined as
bindings in `where` clauses.
The flag is on by default in the Cryptol REPL, and in most cases makes
it possible to leave out more type signatures in `where` clauses than
before. However, some programs really do rely on inferring polymorphic
types for local variables; in this case adding an explicit polymorphic
type signature to the local binding in question will make the program
typecheck.
This makes it easier to get the behavior of the TVars instance under control,
as we can choose to only apply the substitution to the values of the map after
first applying it to the keys, and thus possibly removing redundant goals.
mono-binds/test03 is no longer a really relevant test since mono-binds
doesn't do any generalization. However I fixed up the type signature
and updated the output in case it becomes relevant again in the
future.
issues/issue225 is fine, but work on the master branch increased the
verbosity of constraint solver failures when mono-binds is off. It
still works fine when we monomorphize the local definition.
The Smtlib solver was translating Fin constraints to True, as it didn't know
how to handle them. They should have been skipped, and returned back as
unsolved goals instead.
Tracking the closed environment was tricky, and it wasn't clear how easy it
would be to find free type variables in bindings that lack signatures, as we
don't kind check the AST before making the decision about making it monomorphic.
It was possible to exploit shadowing to get a name into the closed environment
that wasn't actually closed. The change here is that `partitionClosed` now
returns a completely new closed environment with any shadowed names removed, and
that environment is used when checking the declarations it describes, instead.
Setting `mono-binds` to `yes` will cause bindings to be made monomorphic when
they don't refer to closed values, and setting `mono-binds` to no will cause
them to always be generalized.
Partition out declarations that should be monomorphic, based on what they
reference in the environment; declarations that lack signatures but don't
reference anything in the local environment can still be generalized.
A first pass on skipping generalization for bindings in a where clause that
lack type signatures. The tests that fail as a result of this change are either
because of error locations changing, or a changing number of defaulting
warnings.
This tries to address #125 by making the errors from the renamer a little bit
more clear.
Squashed commit of the following:
commit 8afd3d7961b58df042fe801c3c5e1b9787f813bc
Author: Trevor Elliott <trevor@galois.com>
Date: Wed Dec 3 19:33:59 2014 -0800
Update tests for new renamer errors
commit 7cac01836d8943cf3b08d6715ac328e3b6658cef
Author: Trevor Elliott <trevor@galois.com>
Date: Wed Dec 3 19:33:49 2014 -0800
Add `at` on errors and warnings to be more consistent
commit 308908ba318a4cdc839710f66f1a487543f8c07e
Author: Trevor Elliott <trevor@galois.com>
Date: Wed Dec 3 19:06:57 2014 -0800
More consistent renamer warnings
commit be8100a78e9eaba6d554591121c24ed5dcd3c780
Author: Trevor Elliott <trevor@galois.com>
Date: Wed Dec 3 18:56:53 2014 -0800
More consistent error formatting from the renamer
commit 26c45c3b51e0bdbcf6a1431cab8e1eb8760ea0bb
Author: Trevor Elliott <trevor@galois.com>
Date: Wed Dec 3 18:56:36 2014 -0800
Remove an un-triggerable error
commit ccdb93e036ba1e111ccd977c8b3b35523f3c1bf0
Author: Trevor Elliott <trevor@galois.com>
Date: Wed Dec 3 16:38:44 2014 -0800
Try to give better errors for unbound identifiers
commit eb5784145985bb55c761088eaba27c67d08c1326
Author: Trevor Elliott <trevor@galois.com>
Date: Wed Dec 3 16:38:23 2014 -0800
Remove old TODOs about located errors
commit b984bb5f451f3aa7b4fc8f15167483c5142ee9a3
Author: Trevor Elliott <trevor@galois.com>
Date: Wed Dec 3 14:37:34 2014 -0800
Differentiate missing type and expression symbols
commit b9e6f13856db6765dced3cb9565cdc8387a7976d
Author: Trevor Elliott <trevor@galois.com>
Date: Wed Dec 3 14:36:52 2014 -0800
Remove a shadowing warning
