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 |