Flatten on intervals seems incorrect

[dorchard]

@rls42 and I just stumbled across this:

badFlat : forall {a : Type} . (a [5..5]) [0..1] -> a [0..5]
badFlat [[x]] = [x]

This doesn't sound right... the result could be used 3 times say, but the input says that either is used or not used (first layer of boxing) and inside there is something that is used exactly 5 times.

According to our ICFP paper this kind of flattening shouldn't happen, so its the implementation that is wrong here rather than the theory.