On 15/06/16 04:29, AntC wrote:
...
The earlier design for SORF tried to support higher-ranked fields. https://ghc.haskell.org/trac/ghc/wiki/Records/OverloadedRecordFields/SORF
That had to be abandoned, until explicit type application was available IIRC.
We now have type application in GHC 8.0.
Is there some hope for higher-rank type fields?
Unfortunately, doing ORF with higher-rank fields is a bit of a non-starter, even with explicit type application, because the combination would break bidirectional type inference and require impredicativity. This was part of the reason we ended up preferring an explicit syntactic marker for ORF-style overloaded labels. For example, consider this (rather artificial) type: data T = MkT { foo :: ((forall a . a -> a) -> Bool) -> Bool } -- foo :: T -> ((forall a . a -> a) -> Bool) -> Bool Suppose `t :: T`. When type-checking `foo t (\ k -> k k True)`, the compiler will infer (look up) the type of `foo` and use it to check the types of the arguments. The second argument type-checks only because we are "pushing in" the type `(forall a . a -> a) -> Bool` and hence we know that the type of `k` will be `forall a . a -> a`. Now suppose we want to type-check `#foo t (\ k -> k k True)` using ORF instead. That ends up deferring a constraint `HasField r "foo" a` to the constraint solver, and inferring a type `a` for `#foo t`, so we can't type-check the second argument. Only the constraint solver will figure out that `a` should be impredicatively instantiated with a polytype. We end up needing to do type inference in the presence of impredicativity, which is a Hard Problem. There is some work aimed at improving GHC's type inference for impredicativity, so perhaps there's hope for this in the future. Explicit type application makes it possible (in principle, modulo #11352) for the user to write something like #foo @T @(((forall a . a -> a) -> Bool) -> Bool) t (\ k -> k k True) although they might not want to! But the ramifications haven't been fully thought through, e.g. we'd need to be able to solve the constraint HasField T "foo" (((forall a . a -> a) -> Bool) -> Bool) even though it has a polytype as an argument. Sorry to be the bearer of bad news, Adam -- Adam Gundry, Haskell Consultant Well-Typed LLP, http://www.well-typed.com/