Opened 18 months ago
Last modified 16 months ago
#14958 new bug
QuantifiedConstraints: Doesn't apply implication for existential?
Reported by: | Iceland_jack | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler | Version: | 8.5 |
Keywords: | QuantifiedConstraints | Cc: | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description
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.
Change History (6)
comment:1 Changed 18 months ago by
comment:2 Changed 18 months ago by
Ah! That makes perfect sense, we can specify a Proxy cls
and not change the kind of Foo
data Foo where Foo :: Proxy cls -> (forall x. ((forall y. cls y => Num y), cls x) => x) -> Foo a :: Foo a = Foo (Proxy :: Proxy Num) 10 b :: Foo b = Foo (Proxy :: Proxy Fractional) 10.0
(it's maybe not as clear as I thought: is it possible to convert Foo
to data Foo2 = Foo2 (forall x. Num x => x)
?)
I have a draft ready for an overview of this extension from ticket:14840#comment:6, should I email it to you?
comment:3 Changed 18 months ago by
I have a draft ready for an overview of this extension from ticket:14840#comment:6, should I email it to you?
A draft of what? A blog post? If so, I suggest you just post it!
comment:6 Changed 16 months ago by
Keywords: | wipT2893 removed |
---|
This is to do with overlapping instances. We have
So from the expression
Foo 10
we have: Given:Here
cls0
is a unification variable; we don't yet know what it'll tur out to be, and indeed (given the type ofFoo
) it's ambiguous.When trying to solve
Num x
GHC doesn't want to used1
, because that make a commitment to solve its sub-goals. Ifcls0
turned out to beNum
, an alternative would be to pickd2
. So it simply refrains from choosing. (The error message doesn't make this clear, I know.)If you fix
cls0
all is well. For example: