Overlapping instances vs closed type families

Main.hs

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DuplicateRecordFields #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TemplateHaskell #-}

-- | Getting fields from the "union" of two records.
--
-- Inspired by section 3.1 or Hiromi Ishii's "Witness Me — Constructive
-- Arguments Must Be Guided with Concrete Witness" functional pearl.
module Main (main) where

import Splicy

import Data.Kind
import GHC.Records
import GHC.TypeLits
import Data.Type.Equality

type List :: [Symbol] -> Type
data List l where
    Nil :: List '[]
    Cons :: Bool -> List xs -> List (k ': xs)

-- with Overlapping instances
type Find :: Symbol -> [Symbol] -> Constraint
class Find k xs where
    find :: List xs -> Bool

instance {-# OVERLAPS #-} Find k (k : xs) where
    find (Cons b _) = b

instance {-# OVERLAPPABLE #-} Find k xs =>  Find k (z : xs) where
    find (Cons _ rest) = find @k @xs rest
--

-- using closed type families
type Find2 :: Symbol -> [Symbol] -> Constraint
class Find2 k xs where
    find2 :: List xs -> Bool

type Find2' :: Bool -> Symbol -> [Symbol] -> Constraint
class Find2' eq k xs where
    find2' :: List xs -> Bool

instance ((k == k') ~ eq, Find2' eq k (k' : xs)) => Find2 k (k' : xs) where
    find2 = find2' @eq @k

instance Find2' True k (k' : xs) where
    find2' (Cons x _) = x

instance ((k == k'') ~ eq, Find2' eq k (k'' : xs)) => Find2' False k (k' : (k'' : xs)) where
    find2' (Cons _ rest) = find2' @eq @k rest
--

-- example :: List ["foo","bar","baz"]
-- example = Cons False (Cons False (Cons True Nil))

$(makeSig (take 150 (sequence (replicate 10 ['a'..'y']))))

main :: IO ()
main = print (find @"zzz" exampleTH)

Splicy.hs

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DuplicateRecordFields #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TemplateHaskell #-}

module Splicy (makeSig) where

import Data.Kind
import GHC.Records
import GHC.TypeLits
import Data.Type.Equality

import Language.Haskell.TH

makeSig :: [String] -> Q [Dec]
makeSig symbols = pure $ [
    SigD (mkName "exampleTH") (AppT (ConT (mkName "List")) (foldr  (\x acc -> AppT (AppT PromotedConsT (LitT (StrTyLit x))) acc) (AppT (AppT PromotedConsT (LitT (StrTyLit "zzz"))) PromotedNilT) symbols)),
    let exp = AppE (AppE (ConE (mkName "Cons")) (ConE (mkName "True"))) (ConE (mkName "Nil"))
     in ValD (VarP (mkName "exampleTH")) (NormalB (foldr (\x acc -> (AppE (AppE (ConE (mkName "Cons")) (ConE (mkName "False"))) acc)) exp symbols)) []
    ]