QuantifiedConstraints: Doesn't apply implication for existential?

This fails

{-# Language GADTs, RankNTypes, ConstraintKinds, QuantifiedConstraints, AllowAmbiguousTypes #-}

data Foo where
  Foo :: (forall x. ((forall y. cls y => Num y), cls x) => x) -> Foo

a :: Foo
a = Foo 10

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

/tmp/Optic.hs:7:9: error:
    • Could not deduce (Num x) arising from the literal ‘10’
      from the context: (forall y. cls0 y => Num y, cls0 x)
        bound by a type expected by the context:
                   forall x. (forall y. cls0 y => Num y, cls0 x) => x
        at /tmp/Optic.hs:7:5-10
      Possible fix:
        add (Num x) to the context of
          a type expected by the context:
            forall x. (forall y. cls0 y => Num y, cls0 x) => x
    • In the first argument of ‘Foo’, namely ‘10’
      In the expression: Foo 10
      In an equation for ‘a’: a = Foo 10
  |
7 | a = Foo 10
  |         ^^
Failed, no modules loaded.
Prelude> 

GHC knows that cls ~=> Num but still GHC cannot deduce Num x from cls x.

---

The reason for trying this is creating a newtype for optics where we still get subsumption

{-# Language GADTs, RankNTypes, ConstraintKinds, QuantifiedConstraints, AllowAmbiguousTypes, ApplicativeDo, TypeOperators, MultiParamTypeClasses, FlexibleInstances, UndecidableInstances, PolyKinds, FlexibleContexts #-}

data Optic cls s a where
  Optic :: (forall f. cls f => (a -> f a) -> (s -> f s)) -> Optic cls s a

class    (forall x. f x => g x) => (f ~=> g)
instance (forall x. f x => g x) => (f ~=> g)

_1 :: cls ~=> Functor => Optic cls (a, b) a
_1 = Optic $ \f (a, b) -> do
  a' <- f a
  pure (a', b)

lens_1 :: Optic Functor (a, b) a
lens_1 = _1

trav_1 :: Optic Applicative (a, b) a
trav_1 = _1

and I wanted to move cls ~=> Functor into the Optic type itself.

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