Comment Comment by bidirectional Can you type that in System F? It doesn't seem logically valid, a -> a is trivially true, but apparently implies any a? parent bidirectional 5 years ago