A different approach to fields

[treeowl]

Data.Generics.Product.Fields forces s field b -> t, t field a -> s in a rather complicated way. But this fundep isn't even always desirable. For example, the getConst lens is quite reasonably type-changing.

A different approach:

1. Use (or crib from) coercible-utils to impose Similar s t, which means they both have the same type constructor and kind arguments.
2. Let the fact that s field b -> Rep t and t field a -> Rep s for each concrete type fall out of the constraint solving.

I think this way is much simpler, and it avoids unnecessary constraints; inference should be quite good, handling all non-phantom types.

If you don't want to do that in this package, let me know and I'll make my own for that.

[kcsongor]

There might be some subtleties I'm missing, but I think we already a have a similar lens:

generic-lens/generic-lens/src/Data/Generics/Product/Fields.hs

Lines 112 to 124 in 8e1fc7d

	-- |Records that have a field with a given name.
	--
	-- This is meant to be more general than 'HasField', but that is not quite the
	-- case due to the lack of functional dependencies.
	--
	-- The types @s@ and @t@ must be applications of the same type constructor.
	-- In contrast, 'HasField' also requires the parameters of that type constructor
	-- to have representational roles.
	--
	-- One use case of 'HasField_' over 'HasField' is for records defined with
	-- @data instance@.
	class HasField_ (field :: Symbol) s t a b where
	field_ :: VL.Lens s t a b

with the instance defined as

generic-lens/generic-lens/src/Data/Generics/Product/Fields.hs

Lines 167 to 168 in 8e1fc7d

	instance (Core.Context_ field s t a b , HasField0 field s t a b) => HasField_ field s t a b where
	field_ f s = field0 @field f s

generic-lens/generic-lens-core/src/Data/Generics/Product/Internal/Fields.hs

Lines 44 to 50 in 8e1fc7d

	-- Alternative type inference
	type Context_ field s t a b
	= ( HasTotalFieldP field (Rep s) ~ 'Just a
	, HasTotalFieldP field (Rep t) ~ 'Just b
	, UnifyHead s t
	, UnifyHead t s
	)

This uses

generic-lens/generic-lens-core/src/Data/Generics/Internal/Families/Changing.hs

Lines 133 to 137 in 8e1fc7d

	-- | Ensure that the types @a@ and @b@ are both applications of the same
	-- constructor. The arguments may be different.
	class UnifyHead (a :: k) (b :: k)
	instance {-# OVERLAPPING #-} (gb ~ g b, UnifyHead f g) => UnifyHead (f a) gb
	instance (a ~ b) => UnifyHead a b

This machinery looks similar to Similar at a first glance. Is this what you're after? If there's anything more we can do, I'm happy to add it to the package.

For concrete types this works out quite well, but in my experience, the fundeps come in really handy in a polymorphic context (like when a function has a HasField constraint, then without the fundeps, GHC will complain about ambiguous constraints).

[treeowl]

It's not quite the same, no. I'm talking about something like

class (Similar s t, FindFieldType fld s ~ 'Just a, FindFieldType fld t ~ 'Just b) => Fielded fld s t a b where
  fielded :: Lens s t a b

This gives you fld s -> a and fld t -> b.
If you have s ~ T y z, then you immediately get t ~ T _ _ and vice versa; I'm not sure if your Field_ does the latter; it seems not to do the former.

[treeowl]

My version makes an a priori assumption over HasField_ that the type is not void. This buys those two fundeps. I think that's a reasonable restriction. For a version offering only a Traversal, the restriction is best phrased a bit differently: at least one constructor must have a field by the given name. In that context, the restriction not only improves inference but also catches typos—you wouldn't usually want to get guaranteed-empty traversals if you misspell a field name.

[kcsongor]

The purpose of UnifyHead is exactly to infer from s ~ T y z that t ~ T _ _. Having UnifyHead (T y z) t will give you t ~ T _ _ after instance resolution (the first instance matches twice to take apart the application, then finally the second instance unifies the constructors). Looking at Similar, it seems to achieve the same thing in a slightly different way, using type families.

We run UnifyHead in both directions because we don't know which of t or s is more refined, i.e. which one will allow us to learn the shape of the other.

Assuming that UnifyHead and Similar achieve the same thing (if they don't I'm happy to be corrected), the other thing you propose is writing the class declaration in the following way:

class ... => Fielded fld s t a b | fld s -> a, fld t -> s where

in other words, we could perhaps add those fundeps to HasField_? Inference should be pretty good in concrete contexts. In fact HasField_s inference is already as good as the way more complex HasField's in concrete contexts. It's polymorphic contexts that HasField is better in. Adding those two fundeps might bring them a little closer?