content: -- This used to produce Core Lint errors
  
  {-# Language ConstraintKinds       #-}
  {-# Language DataKinds             #-}
  {-# Language FlexibleInstances     #-}
  {-# Language GADTs                 #-}
  {-# Language ImpredicativeTypes    #-}
  {-# Language KindSignatures        #-}
  {-# Language MultiParamTypeClasses #-}
  {-# Language PolyKinds             #-}
  {-# Language QuantifiedConstraints #-}
  {-# Language RankNTypes            #-}
  {-# Language TypeOperators         #-}
  {-# Language UndecidableInstances  #-}
  
  {-# Options_GHC -dcore-lint #-}
  
  module Dict where
  
  import Data.Kind (Type)
  import Data.Maybe (isJust, isNothing)
  import Data.Type.Equality ((:~:))
  
  data LoT k where
    LoT0   :: LoT Type
    (:&&:) :: k -> LoT ks -> LoT (k -> ks)
  
  data Dict cls where
   Dict :: cls => Dict cls
  
  class GTE a b x y (f :: LoT kf -> Type) (g :: LoT kg -> Type) where
    gTE :: f x -> g y -> Maybe (a :~: b)
  
  class    (forall a b. GTE a b (a :&&: LoT0) (b :&&: LoT0) rep rep) => As f rep
  instance (forall a b. GTE a b (a :&&: LoT0) (b :&&: LoT0) rep rep) => As f rep
  
  ok :: Dict (As f rep) -> Dict (forall a b. GTE a b (a :&&: LoT0) (b :&&: LoT0) rep rep)
  ok Dict = Dict
  