Field accessor type inference woes

[Adam Gundry]

On 04/07/13 12:27, AntC wrote:
> H-R fields are a limitation because we can't update them either. So I
> think it's a fair question whether supporting h-r polymorphism is
> worth the limitations?

Yes, higher rank polymorphism is bound to cause trouble with polymorphic
projections, and perhaps it won't matter if we limit ourselves to one or
the other.


> Edward pointed out earlier, circumstances where lenses:
>>> required inference to flow backwards from the 'field' to the
>>> 'record'

Crucially, Edward pointed out that this is needed to make polymorphic
record fields into lenses automatically [1], which I'm quite keen on. So
that's an additional reason for sticking with the current story.


> This would be a strong motivation for overloaded fields refraining
> from generating the fully polymorphic field selector functions.
> That is, set -XNoRecordSelectorFunctions, then I could declare:
>
>     personId :: r { personId :: Int } => r -> Int
>     personId = getFld
>
> Or perhaps there could be some way to declare that a given field is
> always at a specific type?
>
> Does this help with Edward's chained/nested records example?
> Does the field name in the outer record determine the type of the inner?
> (I guess we're in trouble if the inner is (parametric) polymorphic?)

In some circumstances, it might well remove ambiguity if we knew that a
field always had a consistent type. I wonder how to declare this. If we
were using the type family version then the user could declare

type instance GetResult r "personId" = Int

independently of any data declarations.


Alas...

On 04/07/13 13:47, Barney Hilken wrote:
| The two points in AntC's message suggest a possible compromise
solution. Unless I've missed something,
| this allows nested fields, fixed type projections, and HR fields. The
only restriction is that HR fields must be
| fixed type, though they can still be used in multiple records.

| [...]

| 	class Has_bar r where
| 		bar :: r -> forall b. b -> b
|
| 	instance Has_bar r => Has r "bar" where
| 		GetType r "bar" = forall b. b -> b
| 		getField = bar
|
| which doesn't look impredicative to me.
|
| Does this work, or have I missed something?

...this associated type declaration isn't legal, because type families
are not allowed to return polymorphic type schemes. (It's far from clear
how one would do type inference for such monsters.)


Adam

[1]
http://hackage.haskell.org/trac/ghc/wiki/Records/OverloadedRecordFields/Plan#Polymorphicrecordupdateforlenses