content: {-# LANGUAGE CPP #-}
  {-# LANGUAGE ConstraintKinds #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE ImplicitParams #-}
  {-# LANGUAGE KindSignatures #-}
  {-# LANGUAGE MagicHash #-}
  {-# LANGUAGE RankNTypes #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TypeOperators #-}
  
  module T12133 where
  
  import           GHC.Classes (IP(..))
  import           Data.Kind (Constraint, Type)
  
  -- | From "Data.Constraint":
  data Dict :: Constraint -> Type where Dict :: a => Dict a
  
  newtype a :- b = Sub (a => Dict b)
  
  infixl 1 \\ -- required comment
  
  (\\) :: a => (b => r) -> (a :- b) -> r
  r \\ Sub Dict = r
  
  -- | GHC 7.10.2 type checks this function but GHC 8.0.1 does not unless
  -- you modify this example in one of the following ways:
  --
  --   * uncomments the type signature for 'Sub'
  --
  --   * flatten the nested pairs of constraints into a triple of constraints
  --
  --   * replace 'IP sym ty' with 'c9', where 'c9' is a new constraint variable.
  --
  -- The error message is listed below.
  foo :: forall c1 c2 c3 sym ty
      .  (c1, c2) :- c3
      -> (c1, (IP sym ty, c2)) :- (IP sym ty, c3)
  foo sp = ( Sub
  --           :: ((c1, (IP sym ty, c2)) => Dict (IP sym ty, c3))
  --              -> (c1, ((IP sym ty), c2)) :- (IP sym ty, c3)
           )
           ( (Dict \\ sp) :: Dict (IP sym ty, c3) )
  
  {- Compiler error message:
  
  GHCi, version 8.0.1: http://www.haskell.org/ghc/  :? for help
  [1 of 1] Compiling T                ( t.hs, interpreted )
  
  t.hs:44:13: error:
      • Could not deduce: IP sym ty arising from a use of ‘Dict’
        from the context: (c1, (IP sym ty, c2))
          bound by a type expected by the context:
                     (c1, (IP sym ty, c2)) => Dict (IP sym ty, c3)
          at t.hs:(40,10)-(44,49)
        or from: c3
          bound by a type expected by the context:
                     c3 => Dict (IP sym ty, c3)
          at t.hs:44:13-22
      • In the first argument of ‘(\\)’, namely ‘Dict’
        In the first argument of ‘Sub’, namely
          ‘((Dict \\ sp) :: Dict (IP sym ty, c3))’
        In the expression: (Sub) ((Dict \\ sp) :: Dict (IP sym ty, c3))
      • Relevant bindings include
          foo :: (c1, c2) :- c3 -> (c1, (IP sym ty, c2)) :- (IP sym ty, c3)
            (bound at t.hs:40:1)
  Failed, modules loaded: none.
  -}
  