ORF for fields of higher-ranked type [was: TDNR without new operators or syntax changes]

[Adam Gundry]

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/