content: {-# LANGUAGE ConstraintKinds #-}
  {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE FlexibleInstances #-}
  {-# LANGUAGE MultiParamTypeClasses #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE RankNTypes #-}
  {-# LANGUAGE TypeFamilies #-}
  {-# LANGUAGE TypeOperators #-}
  {- # OPTIONS_GHC -fno-defer-type-errors #-}
  module T13446 where
  
  import Data.Coerce (Coercible)
  import Data.Kind (Type, Constraint)
  import GHC.TypeLits (Symbol)
  
  data Dict :: Constraint -> Type where
    Dict :: a => Dict a
  
  infixr 9 :-
  newtype a :- b = Sub (a => Dict b)
  instance a => Show (a :- b) where
    showsPrec d (Sub Dict) = showParen (d > 10) $ showString "Sub Dict"
  
  class Lifting p f where
    lifting :: p a :- p (f a)
  
  data Blah a = Blah
  
  newtype J (a :: JType) = J (Blah (J a))
  newtype JComparable a = JComparable (J (T (JTy a)))
  
  instance Lifting JReference JComparable where
    lifting = Sub 'a'
  
  class (Coercible a (J (JTy a))) => JReference a where
    type JTy a :: JType
  
  type T a
    = 'Generic ('Iface "java.lang.Comparable") '[a]
  data JType = Class Symbol
             | Generic JType [JType]
             | Iface Symbol
  type JObject = J (Class "java.lang.Object")
  instance JReference JObject where
    type JTy JObject = 'Class "java.lang.Object"
  