{-# LANGUAGE DataKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Kind (Constraint)

class Bottom where
  giveMeAString :: String

main :: IO ()
main = putStrLn (case veryBad of MkDict -> giveMeAString)


data Set = Empty | Russel

-- Note the perhaps more natural superclass constraints 
-- `b ~ Empty => Bottom` or `forall t. In t Empty => Bottom`
-- do lead to loops at compile time
type In :: Set -> Set -> Constraint
class (In Russel Empty => Bottom) => In a b

instance (In t Russel, In t t) => In t Empty

instance (In t t => In t Empty) => In t Russel

data Dict a where
  MkDict :: c => Dict c

bad :: Dict (In Russel Empty)
bad = MkDict

veryBad :: Dict Bottom
veryBad = case bad of MkDict -> MkDict