Type discrepancy vs SimpleSub

[AshleyYakeley]

Consider:

m = fn x => x x;
i = fn x => x;
mi = m i;

What is the type of mi?

• Pinafore gives rec a, Any -> a (same as rec a, b -> a).
• SimpleSub gives ('b ∨ ('b -> 'a)) as 'a, i.e., rec a, b | b -> a.

These types are not identical. Pinafore gives a strictly more specific type, but it may not be correct.

[AshleyYakeley]

Per AS sec. 5.3.1, substitution works like this:

• a <: T => [(rec b, a & [b/a-]T)/a-]
• T <: a => [(rec b, a | [b/a+]T)/a+]

By hand:

m: ((a -> b) & a) -> b
i: c -> c

c -> c <: (a -> b) & a
---
c -> c <: a -> b
c -> c <: a
---
c <: b
a <: c
c -> c <: a
---
c <: b
c -> c <: c
---
[c'/c+](c -> c) = c -> c'
subst = [(rec c', c|(c -> c'))/c+]

rec c', c|(c -> c') <: b

[AshleyYakeley]

See #206

[AshleyYakeley]

Fixed.