This PR fixes issue #7. Credit to @slindley for the fix. Before the fix, the should-fail example would type check, run, but produce the value a of type A, thus breaking preservation.
Explanation of bug and fix
Abilites are snoc lists, and so the rightmost interface instance is the active one. Suppose we have an interface Eff X and that the ambient ability, when restricted to Eff, is [Eff A, Eff B]. The list ns in applyAdaptor is a list of indices into the restricted ambient ability as a snoc list, i.e. right-to-left so 0 corresponds to Eff B. Thus, when indexing into instances, we should index from the back. Thus the first change is for clarity. The order of the indices in ns, however, is cons list order, i.e. left-to-right. Suppose that ns is [0,0,1]. Then this represents the adaptor <Eff(s a b -> s a b b)>. Therefore, we should not reverse instances' as it is already in the correct form of a cons list. Thus the second change is for correctness.
This PR fixes issue #7. Credit to @slindley for the fix. Before the fix, the should-fail example would type check, run, but produce the value
aof typeA, thus breaking preservation.Explanation of bug and fix
Abilites are snoc lists, and so the rightmost interface instance is the active one. Suppose we have an interface
Eff Xand that the ambient ability, when restricted toEff, is[Eff A, Eff B]. The listnsinapplyAdaptoris a list of indices into the restricted ambient ability as a snoc list, i.e. right-to-left so 0 corresponds toEff B. Thus, when indexing intoinstances, we should index from the back. Thus the first change is for clarity. The order of the indices inns, however, is cons list order, i.e. left-to-right. Suppose thatnsis[0,0,1]. Then this represents the adaptor<Eff(s a b -> s a b b)>. Therefore, we should not reverseinstances'as it is already in the correct form of a cons list. Thus the second change is for correctness.