Field accessor type inference woes

[Adam Gundry]

Unfortunately, I don't think we get away with this...

On 02/07/13 11:45, AntC wrote:
> There's **three** alternatives. ...
> 
>>
>>           data R a = MkR { foo :: a -> a }
>>           data S    = MkS { bar :: forall b. b -> b }
>>  
> 
> Try Plan C: use a cleverer (associated) type function
> 
>     class Has r f t    where
>        type GetResult r f t :: *               -- ?? default to t
>        getFld :: r -> GetResult r f t
> 
>     instance (t ~ a->a) => Has (R a) “foo” t where
>        type GetResult (R a) "foo" t = a -> a   -- ?? ignore t
>        getFld ...
>     instance (t ~ b->b) => Has S “bar” t where 
>        type GetResult S "bar" t = t      -- 'improved' t
>        getFld ...
> 
> In the 'chained' accessors that Edward raises,
> I think the presence of the type function 'fools' type inference into 
> thinking there's a dependency.
> 
> So (foo . bar) has type (and abusing notation):
> 
>     ( Has r "bar" t_bar, Has (GetResult r "bar" t_bar) "foo" t_foo )
>      => r -> (GetResult (GetResult r "bar" t_bar) "foo" t_foo)

GetResult isn't necessarily injective (and GHC couldn't tell if it was)
so there is no way to determine `t` from `GetResult r f t`. I tried
prototyping this, and it leads to errors like

    Couldn't match type `GetResult (GetResult a "bar" t1) "foo" t0'
                  with `GetResult (GetResult a "bar" t2) "foo" t'
    NB: `GetResult' is a type function, and may not be injective
    The type variables `t0', `t1' are ambiguous
    Possible fix: add a type signature that fixes these type variable(s)
    Expected type: a -> GetResult (GetResult a "bar" t2) "foo" t
      Actual type: a -> GetResult (GetResult a "bar" t1) "foo" t0


I agree with Simon that we should stick with the current plan, and
accept the fact that composition of polymorphic record selectors isn't
going to work, though this does make me sad. I'm not sure about
restricting quantification over the Has class, because some uses are
perfectly fine (aliasing a selector, for example).

Adam


-- 
The University of Strathclyde is a charitable body, registered in
Scotland, with registration number SC015263.