content: {-# LANGUAGE PolyKinds #-}
  {-# LANGUAGE KindSignatures #-}
  {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE DefaultSignatures #-}
  {-# LANGUAGE GADTs #-}
  
  module T13998 where
  
  import Data.Type.Equality
  
  class EqForall f where
    eqForall :: f a -> f a -> Bool
  
  class EqForall f => EqForallPoly f where
    eqForallPoly :: f a -> f b -> Bool
    default eqForallPoly :: TestEquality f => f a -> f b -> Bool
    eqForallPoly = defaultEqForallPoly
  
  defaultEqForallPoly :: (TestEquality f, EqForall f) => f a -> f b -> Bool
  defaultEqForallPoly x y = case testEquality x y of
    Nothing -> False
    Just Refl -> eqForall x y
  
  
  data Atom = AtomInt | AtomString | AtomBool
  
  data Value (a :: Atom) where
    ValueInt :: Int -> Value 'AtomInt
    ValueString :: String -> Value 'AtomString
    ValueBool :: Bool -> Value 'AtomBool
  
  instance TestEquality Value where
    testEquality (ValueInt _) (ValueInt _) = Just Refl
    testEquality (ValueString _) (ValueString _) = Just Refl
    testEquality (ValueBool _) (ValueBool _) = Just Refl
    testEquality _ _ = Nothing
  
  instance EqForall Value where
    eqForall (ValueInt a) (ValueInt b) = a == b
    eqForall (ValueString a) (ValueString b) = a == b
    eqForall (ValueBool a) (ValueBool b) = a == b
  
  instance EqForallPoly Value
  