QuantifiedConstraints: Can't deduce `c' from `(a, b)' and `a |- b |- c'

#14833 (closed) fixes #14835 (closed): we can witness curryC :: ((a, b) |- c) :- (a |- b |- c).

Now for the entirely predictable, how about **un**curryC

{-# Language QuantifiedConstraints, RankNTypes, PolyKinds, ConstraintKinds, UndecidableInstances, GADTs, LiberalTypeSynonyms, TypeOperators, MultiParamTypeClasses, FlexibleInstances #-}

data Dict c where
  Dict :: c => Dict c

infixr |-
class    (a => b) => (a |- b)
instance (a => b) => (a |- b)

type a :- b = Dict (a |- b)

uncurryC :: forall a b c. (a |- b |- c) :- ((a, b) |- c)
uncurryC = Dict

$ ghci -ignore-dot-ghci Z.hs 
GHCi, version 8.5.20180128: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( Z.hs, interpreted )

Z.hs:13:12: error:
    • Could not deduce: c arising from a use of ‘Dict’
      from the context: a |- (b |- c)
        bound by a quantified context at Z.hs:1:1
      or from: (a, b) bound by a quantified context at Z.hs:1:1
    • In the expression: Dict
      In an equation for ‘uncurryC’: uncurryC = Dict
    • Relevant bindings include
        uncurryC :: (a |- (b |- c)) :- ((a, b) |- c) (bound at Z.hs:13:1)
   |
13 | uncurryC = Dict
   |            ^^^^
Failed, no modules loaded.
Prelude> 

Trac metadata

Trac field	Value
Version	8.5
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture