ucsd-progsys/liquidhaskell — pull request #95 by ranjitjhala (2013-07-22 15:45:17+00:00)
Title: Qualshrink: remove the global constants generated by GHC `Literal` values

The `Literal` were converted to `int` constants that polluted the global namespace,
making solving unnecessarily slow, due to bogus instantiations. Worse, the damn
things aren't even needed!

Data/ByteString.hs now runs in 5mins or so (with the SMTLIB2 Z3 bindings,
probably even faster if we can link against z3 v4 api).

Also, don't generalize `Sort` in qualifier definition unless sort is a lower-case identifier
(i.e. type variable). Earlier, things like

qualif Foo(v:ByteString, x: ByteString): v = x

were generalized to

qualif Foo(v:@(0), x:@(0)): v = x

which was also slowing things down.

co-request with XXX