{-# LANGUAGE AllowAmbiguousTypes, ConstraintKinds, FlexibleContexts, FlexibleInstances, GADTs, PolyKinds, RankNTypes, DataKinds, ScopedTypeVariables, TypeApplications, TypeFamilies, TypeOperators,  OverloadedLabels #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE TypeFamilyDependencies #-}

import GHC.OverloadedLabels
import GHC.TypeLits

data Assoc x v = x := v

data HList (ts :: [Assoc Symbol *]) where
  HNil  :: HList '[]
  HCons :: forall a k ts.  a -> HList ts -> HList (k := a : ts)

nil :: HList '[]
nil = HNil

class FindElem x ts where
  findElem :: String

type family LookupType x ts where
  LookupType x ((x ':= v) : ts) = v
  LookupType x ((x' ':= v) : ts) = LookupType x ts

data Var (x :: Symbol) where
  Var :: KnownSymbol x => Var x

instance (KnownSymbol x, x ~ x') => IsLabel x (Var x') where
  fromLabel = Var

instance {-# OVERLAPPING #-}  FindElem x '[x ':= v] where
  findElem = "a"
-- instance {-#  OVERLAPPING #-} FindElem x ((x ':= v) ': ts) where
--   findElem = "b"
-- instance {-#  OVERLAPPING #-} FindElem x ts => FindElem x (xv ': ts) where
--   findElem = "c"
instance {-#  INCOHERENT #-} FindElem x ts => FindElem x ts where
  findElem = "d"

get :: forall x ts. FindElem x ts => Var x -> HList ts -> String
get _ _ = findElem @x @ts

env :: HList '["r" ':= Integer]
env = HCons 5 HNil

f :: String
f = findElem @"r" @'["r" ':= Integer]

g :: String
g = get #r env