search

nick8325 / quickspec

Equational laws for free
BSD 3-Clause "New" or "Revised" License
250 stars 24 forks source link

Add a flag to disable closing under antisubstitution #54

Closed isovector closed 3 years ago

isovector commented 4 years ago

This PR introduces withAutoGeneralizeTypes, which when disabled prevents the QS universe from being closed under anti-substitution. I have absolutely no idea what the implications of this are, --- neither the code nor a quick skim of the paper explain why this closure is necessary. That being said, disabling this option gets rid of some silly warnings.

For example, under today's behavior if my signature contains Foo () (), QuickSpec will yell at me:

== Functions ==                  
A :: () -> Foo () ()

WARNING: The following types have no 'Arbitrary' instance declared.
You will not get any variables of the following types:
  Foo Int Int
  Foo Int ()
  Foo () Int

WARNING: The following types have no 'Ord' or 'Observe' instance declared.
You will not get any equations about the following types:
  Foo Int Int
  Foo Int ()
  Foo () Int

Where do these warnings come from? As a user I have no idea! QS is creating every one-hole type for Foo, and then immediately defaulting them each to Int, but as far as I can tell, this isn't useful behavior whatsoever.

Fixes #41

isovector commented 4 years ago

To take this a step further, without know what functionality I'm breaking, I'd suggest that this option be set to False by default.