content: {-# LANGUAGE ScopedTypeVariables, AllowAmbiguousTypes, TypeApplications,
               TypeFamilies, PolyKinds, DataKinds, FlexibleInstances,
               MultiParamTypeClasses, FlexibleContexts, PartialTypeSignatures #-}
  {-# OPTIONS_GHC -Wno-partial-type-signatures #-}
  
  module InstanceGivenOverlap2 where
  
  import Data.Proxy
  
  class P a
  class Q a
  class R a b
  
  newtype Tagged (t :: k) a = Tagged a
  
  type family F a
  type instance F (Tagged @Bool t a) = [a]
  
  instance P x => Q [x]
  instance (x ~ y) => R y [x]
  
  wob :: forall a b. (Q [b], R b a) => a -> Int
  wob = undefined
  
  it'sABoolNow :: forall (t :: Bool). Int
  it'sABoolNow = undefined
  
  class HasBoolKind t
  instance k ~ Bool => HasBoolKind (t :: k)
  
  it'sABoolLater :: forall t. HasBoolKind t => Int
  it'sABoolLater = undefined
  
  -- This test 'g' used to pass, prior to my fix of #18929
  -- But it is /extremely/ delicate, relying on inhibiting constraint
  -- solving because of overlapping Givens (couldMatchLater)
  -- We are content for it to fail now; see #18929
  -- If it starts to pass in some later universe, that's fine too
  g :: forall t a. Q (F (Tagged t a)) => Proxy t -> [a] -> _
  g _ x = it'sABoolNow @t + wob x
  
  {- Notes about 'g'
     [G] Q (F (Tagged @Bool t a))
     [W] Q [beta]    ==> Q [a]  ==>{instance}  P a
     [W] R beta [a]  ==>{instance}   beta ~ a
  -}
  
  {-  Commenting out these because they all fail
      in the same way as 'g'
  
  g2 :: forall t a. Q (F (Tagged t a)) => Proxy t -> [a] -> _
  g2 _ x = wob x + it'sABoolNow @t
  
  g3 :: forall t a. Q (F (Tagged t a)) => Proxy t -> [a] -> _
  g3 _ x = it'sABoolLater @t + wob x
  
  g4 :: forall t a. Q (F (Tagged t a)) => Proxy t -> [a] -> _
  g4 _ x = wob x + it'sABoolLater @t
  -}
  