How can I use a type parameter determined via the functional dependency of an instance constraint as the RHS of an associated type family equation?

user_1726343 0
Viewed 92

I have a typeclass like this:

class (Coercible a b) => Foo a b | a -> b

I would like to declare the following instance of Generic:

data Thing a
  where
  Thing :: Foo a b => b -> Thing a

-- If the @b@ uniquely determined by @a@ is @Generic@, so is @Thing a@ ...
instance (Foo a b, Generic b) => Generic (Thing a)
  where
  type Rep (Thing a) = Rep b

Unfortunately this does not compile, the error message being:

[typecheck] [E] • Type variable ‘r’ is mentioned in the RHS,
    but not bound on the LHS of the family instance
• In the type instance declaration for ‘Rep’
  In the instance declaration for ‘Generic (UnvalidatedData v)’

I know that what I want is possible at a semantic level, because if I use a type family instead of a functional dependency as follows:

class (Coercible a (B a)) => Foo' a
  where
  type B a :: Type

I can declare:

data Thing a
  where
  Thing :: Foo' a => B a -> Thing a

-- If the @B a@ uniquely determined by @a@ is @Generic@, so is @Thing a@ ...
instance (Foo' a, Generic (B a)) => Generic (Thing a)
  where
  type Rep (Thing a) = Rep (B a)

Unfortunately associated type families do not show up at all in the kinds of typeclasses, so it is not possible to do higher order reasoning over associated type families when passing classes around. For this reason I would prefer to use a functional dependency instead of a type family.

What (if anything) is the closest working approximation of Foo, Thing and Thing's Generic instance that uses a multi-parameter typeclass?

functional-dependencies type-families typeclass haskell
1 Answers

The best I could come up with is to use both functional dependencies and a type family and try to get a best-of-both-worlds situation:

class (Coercible a b, b ~ B a) => Foo a b | a -> b where
  type B a :: Type

data Thing a where
  Thing :: Foo a b => b -> Thing a

instance (Foo a b, Generic b) => Generic (Thing a) where
  type Rep (Thing a) = Rep (B a)

It's not super elegant, but the use of b ~ B a in the constraint for Foo means that you cannot accidentally screw up instances of Foo. For instance, you can write:

instance Foo (Sum a) a where
  type B (Sum a) = a

but if you try to write, say, type B (Sum a) = Int, you'll get a an error arising from the superclasses of an instance declaration.

user_148023840
Related