content: {-# LANGUAGE ConstraintKinds           #-}
  {-# LANGUAGE InstanceSigs              #-}
  {-# LANGUAGE FlexibleContexts          #-}
  {-# LANGUAGE FlexibleInstances         #-}
  {-# LANGUAGE GADTs                     #-}
  {-# LANGUAGE MultiParamTypeClasses     #-}
  {-# LANGUAGE RankNTypes                #-}
  {-# LANGUAGE TypeFamilies              #-}
  {-# LANGUAGE TypeFamilyDependencies    #-}
  {-# LANGUAGE PolyKinds                 #-}
  {-# LANGUAGE DataKinds                 #-}
  {-# LANGUAGE TypeOperators             #-}
  {-# LANGUAGE UndecidableInstances      #-}
  {-# LANGUAGE QuantifiedConstraints     #-}
  
  module T14961 where
  
  import           Data.Kind
  
  import           Control.Arrow              (left, right, (&&&), (|||))
  import           Control.Category
  import           Prelude                    hiding (id, (.))
  
  import           Data.Coerce
  
  class    (forall x. f x => g x) => f ~=> g
  instance (forall x. f x => g x) => f ~=> g
  
  type family (#) (p :: Type -> Type -> Type) (ab :: (Type, Type))
    = (r :: Type) | r -> p ab where
    p # '(a, b) = p a b
  
  newtype Glass
    :: ((Type -> Type -> Type) -> Constraint)
    -> (Type, Type) -> (Type, Type) -> Type where
    Glass :: (forall p. z p => p # ab -> p # st) -> Glass z st ab
  
  data A_Prism
  
  type family ConstraintOf (tag :: Type)
    = (r :: (Type -> Type -> Type) -> Constraint) where
    ConstraintOf A_Prism = Choice
  
  _Left0
    :: Glass Choice
         '(Either a x, Either b x)
         '(a, b)
  _Left0 = Glass left'
  
  _Left1
    :: c ~=> Choice
    => Glass c '(Either a x, Either b x) '(a, b)
  _Left1 = Glass left'
  
  -- fails with
  -- • Could not deduce (Choice p)
  -- _Left2
  --   :: (forall p. c p => ConstraintOf A_Prism p)
  --   => Glass c '(Either a x, Either b x) '(a, b)
  -- _Left2 = Glass left'
  
  _Left3
    :: d ~ ConstraintOf A_Prism
    => (forall p . c p => d p)
    => Glass c
         '(Either a x, Either b x)
         '(a, b)
  _Left3 = Glass left'
  
  -- fails to typecheck unless at least a partial type signature is provided
  -- l :: c ~=> Choice => Glass c _ _
  -- l = _Left1 . _Left1
  
  newtype Optic o st ab where
    Optic
      :: (forall c d. (d ~ ConstraintOf o, c ~=> d) => Glass c st ab)
      -> Optic o st ab
  
  _Left
    :: Optic A_Prism
         '(Either a x, Either b x)
         '(a, b)
  _Left = Optic _Left1
  
  instance Category (Glass z) where
    id :: Glass z a a
    id = Glass id
  
    (.) :: Glass z uv ab -> Glass z st uv -> Glass z st ab
    Glass abuv . Glass uvst = Glass (uvst . abuv)
  
  class Profunctor (p :: Type -> Type -> Type) where
    dimap :: (a -> b) -> (c -> d) -> p b c -> p a d
    lmap :: (a -> b) -> p b c -> p a c
    rmap :: (b -> c) -> p a b -> p a c
  
  class Profunctor p => Choice (p :: Type -> Type -> Type) where
    left' :: p a b -> p (Either a c) (Either b c)
    right' :: p a b -> p (Either c a) (Either c b)
  