Yes, we can't make IV the magic class for which instances are generated. As I pointed out earlier in the thread, we need to give an instance for the function space that enforces the functional dependency (either with an actual fundep or a type family), and keep a distinguished HasField class. AFAICS it's still an open question as to whether that instance should provide (a) selector functions r -> a (b) lenses (a -> f b) -> s -> f t (c) both (d) neither but I'm starting to think (b) is the sanest option. Otherwise, I think we've more or less converged on the issues (apart from the syntax question) and I'll update the wiki page appropriately. On the syntax question, Edward, could you say more about how you would expect the magic imports to work? If a module both declares (or imports) a record field `x` and magically imports `x`, what does a use of `x` mean? (In the original ORF, we didn't have the magic module, but just said that record fields were automatically polymorphic... that works but is a bit fiddly in the renamer, and isn't a conservative extension.) Adam On 27/01/15 00:59, Edward Kmett wrote:
I'm also rather worried, looking over the IV proposal, that it just doesn't actually work.
We actually tried the code under "Haskell 98 records" back when Gundry first started his proposal and it fell apart when you went to compose them.
A fundep/class associated type in the class is a stronger constraint that a type equality defined on an individual instance.
I don't see how
@foo . @bar . @baz
(or #foo . #bar . #baz as would be written under the concrete proposal on the wiki)
is ever supposed to figure out the intermediate types when working polymorphically in the data type involved.
What happens when the type of that chain of accessors is left to inference? You get stuck wallowing in AllowAmbiguousTypes territory:
(#foo . #bar . #baz) :: (IV "foo" (c -> d), IV "bar" (b -> c), IV "baz" (a -> b)) => a -> d
has a variables 'b' and 'c' that don't occur on the right hand side, and which are only determinable by knowing that the instances you expect to see look something like:
instance (a ~ Bool) => IV "x" (S -> a) where iv (MkS x) = x
but that is too weak to figure out that "S" determines "a" unless S is already known, even if we just limit ourselves to field accessors as functions.
-Edward
-- Adam Gundry, Haskell Consultant Well-Typed LLP, http://www.well-typed.com/