Internal consistency violation with added 'if' statement

[seizethedave]

here's a spec:

TokenGroupIfBug:
    type Float = Native "float"

    state scores : Set<(Int, Float)>
    assume unique [s.0 | s <- scores];

    op addTokenScore(score : Float)
        assume not ((len scores, score) in scores);
        assume not ((len scores) in [s.0 | s <- scores]);
        if (len scores) < 50:
            scores.add((len scores, score))

    query getScore(i : Int)
        assume i >= 0 and i < len scores;
        the [s.1 | s <- scores, s.0 == i]

and the output:

D-173-250-185-41:cozy dgrant$ cozy --simple  --java out.java specs/TokenGroupIfBug.ds
Checking assumptions...
Done!

_var150 : Bag<(Int, float)> = scores

TokenGroupIfBug:
  type Float = float
  state _var150 : Bag<(Int, float)>
  query getScore(i : Int):
    (the Map {(\s -> (s).1)} (Filter {(\s -> ((s).0 == i))} (_var150)))
  query _query151(score : float):
    ((((sum Map {(\_var14 -> 1)} (_var150)) < 50) ? (_var150 + [((sum Map {(\_var15 -> 1)} (_var150)), score)]) : _var150) - _var150)
  query _query152(score : float):
    (_var150 - (((sum Map {(\_var14 -> 1)} (_var150)) < 50) ? (_var150 + [((sum Map {(\_var15 -> 1)} (_var150)), score)]) : _var150))
  op addTokenScore(score : float):
    for _var153 in _query152(score):
      _var150.remove(_var153)
    for _var153 in _query151(score):
      _var150.add(_var153)

Generating final concrete implementation...
At _var150: expression has type NativeSet<(Int, float)> instead of Bag<(Int, float)>
At _var150: expression has type NativeSet<(Int, float)> instead of Bag<(Int, float)>
Traceback (most recent call last):
  File "/Library/Frameworks/Python.framework/Versions/3.5/bin/cozy", line 11, in <module>
    load_entry_point('Cozy', 'console_scripts', 'cozy')()
  File "/Users/dgrant/Dev/cozy/cozy/cozy/main.py", line 124, in run
    impls = list(autotuning.enumerate_impls(code, state_map, lib, assumptions=ast.spec.assumptions))
  File "/Users/dgrant/Dev/cozy/cozy/cozy/autotuning.py", line 55, in enumerate_impls
    wq.append(apply_rewrite(statevar, new_type, ast))
  File "/Users/dgrant/Dev/cozy/cozy/cozy/autotuning.py", line 37, in apply_rewrite
    raise Exception("internal consistency violation: refined spec does not typecheck")
Exception: internal consistency violation: refined spec does not typecheck

(Commenting out the 'if' statement fixes it.)

[Calvin-L]

There's been a longstanding problem where the ternary operator e ? x : y does not typecheck if the types of x and y are not exactly equal. The correct behavior is for the whole ternary expression to have the "least upper bound" of the two types. So for instance, if x is a bag and y is a set, then the whole thing should be a bag.

The commit I made fixes this exact case, but at some point we'll need to document Cozy's type hierarchy and fully implement the least-upper-bound function.