BROKEN

pattern binds at source toplevel
DON'T USE show (too tricky)
DON'T USE diverge (use assert false)
nested recursives
(possibly) measures over nested recursives
-> measures and complex pattern matches (what does the shape of the matched variable look like?)

rule from paper L_product not followed (e0... not bound in consgen)
* solved by nosimple or adding subt in consgen for tuple or implementing paper rule (dependencies on other code?)

add: more general z3 type casting

fix: wellformedness should start using ml types (and we should guarantee an ml type for every id) to get rid of the hack for unifying functions with arguments

try: convert paths to strings w/ envls in instantiate_per_environment to time string comparison against path comparison

fix: tuple/record binds don't assert v = blah.e[0, 1, ...]

fix/add: let user choose between generalizing some mlq qualifiers and not generalizing some qualifiers as they want to by dumping mlq qualifiers to a seperate file

fix: explicitly casting all implicit functions (ie, relationals) to int causes dramatic slowdown

fix: single param variant types don't parse in param (int option parsed as 'a option)

fix: nested pattern matches only seem to work for measures