Using type families and Generics to find an Id val

This question is related to this one, where I wanted to avoid the boilerplate of extracting an Id value from a data structure, but in a type-safe manner.

I'll repeat the relevant details of the problem here: suppose you have a type Id:

newtype Id = Id { _id :: Int }

And you want to define a function getId that extracts this Id from any structure that contains at least one Id value:

class Identifiable e where
    getId :: e -> Id

Now the problem is how to define such a class in a type-safe manner, while at the same time avoiding the boilerplate using Generics.

In my previous question I was pointed to type families, and in particular to the ideas described in this blog post. As far as I understand the idea is to define a type-class MkIdentifiable such that:

class MakeIdentifiable (res :: Res) e where
    mkGetId :: Proxy res -> e -> Id

Where a value is of type Res only if there is at least one Id value that is nested inside of it:

data Crumbs = Here | L Crumbs | R Crumbs
data Res = Found Crumbs | NotFound

Then, it seems, one could define:

instance MakeIdentifiable (Found e) e => Identifiable e where
    getId = mkGetId (Proxy :: Proxy (Found e))

Now the question is how to define a type family for Res that is associated to the types of GHC.Generics (U1, K1, :*:, :+:).

I've tried the following:

type family HasId e :: Res where
    HasId Id = Found Here
    HasId ((l :+: r) p) = Choose (HasId (l p)) (HasId (r p))

Where Choose would be something like what is defined in the aforementioned blog post:

type family Choose e f :: Res where
    Choose (Found a) b = Found (L1 a)
    Choose a (Found b) = Found (R1 b)
    Choose a b = NotFound

But this won't compile as HasId (l p) has kind Res and a type is expected instead.

You're pretty close to making Choose typecheck. L1 and R1 are constructors of (:+:), not Crumbs. There's also a type GHC.Generics.R :: * which hides the R constructor from Crumbs at the type level, but you can use 'R to disambiguate (singly-quoted names are constructors, doubly-quoted are type constructors).

It's also good practice to annotate kinds of types, much like we annotate types of toplevel functions.

type family Choose (e :: Res) (f :: Res) :: Res where
  Choose (Found a) b = Found ('L a)
  Choose a (Found b) = Found ('R b)
  Choose NotFound NotFound = NotFound  -- I'm not a fan of overlapping families