[GHC] #14958: QuantifiedConstraints: Doesn't apply implication for existential?

21 Mar 2018

      #14958: QuantifiedConstraints: Doesn't apply implication for existential?
-------------------------------------+-------------------------------------
           Reporter:  Iceland_jack   |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.5
           Keywords:                 |  Operating System:  Unknown/Multiple
  QuantifiedConstraints, wipT2893    |
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 This fails

 {{{#!hs
 {-# 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

 {{{#!hs
 {-# 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.

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14958
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler