[tomp]

You're right, interesting example! Although I'd prefer to "fix" this by incorporating first-class polymorphism [1] with MLsub - I guess non-polymorphic functions satisfying the constraint `(a -> b) & (b -> c)` are quite rare (although I'm sure that you can think of an example).

[1] https://github.com/tomprimozic/type-systems/tree/master/firs...

Edit: although on second thought, just first-class polymorphism isn't enough to fix this... any type system where the function `twice` has the same type as the function `three_times` will exhibit the same problem!

[kvb]

Non-polymorphic functions of the type `a->a` trivially satisfy it, of course. Also, I think polymorphic functions are the most interesting case where you can't use twice as desired in an ML-like language, so it's too bad that despite the fancier type they don't work too well in MLsub. Here's another example that fails when I'd hope for it to succeed:

  let one = twice (fun o -> o.x) { x = { x = 1 } }