#14961 closed bug (invalid)
QuantifiedConstraints: introducing classes through equality constraints fails
Reported by: | mrkgnao | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | 8.6.1 |
Component: | Compiler | Version: | 8.5 |
Keywords: | QuantifiedConstraints | Cc: | Iceland_jack |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | GHC rejects valid program | Test Case: | quantified-constraints/T14961 |
Blocked By: | Blocking: | ||
Related Tickets: | #14860 | Differential Rev(s): | |
Wiki Page: |
Description
The following doesn't typecheck with the wip/T2893
branch:
{-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE TypeFamilies #-} module Subst where class (forall x. c x => d x) => c ~=> d instance (forall x. c x => d x) => c ~=> d foo :: forall c a. c ~=> Monoid => (c a => a) -- ok foo = mempty bar :: forall c a m. (m ~ Monoid, c ~=> m) => (c a => a) -- ok bar = mempty baz :: forall c a. (forall m. m ~ Monoid => c ~=> m) => (c a => a) -- fails baz = mempty
Prelude> :reload [1 of 1] Compiling Subst ( src/Subst.hs, interpreted ) src/Subst.hs:21:7: error: • Could not deduce (Monoid a) arising from a use of ‘mempty’ from the context: (forall (m :: * -> Constraint). (m ~ Monoid) => c ~=> m, c a) bound by the type signature for: baz :: forall (c :: * -> Constraint) a. (forall (m :: * -> Constraint). (m ~ Monoid) => c ~=> m, c a) => a at src/Subst.hs:20:1-66 Possible fix: add (Monoid a) to the context of the type signature for: baz :: forall (c :: * -> Constraint) a. (forall (m :: * -> Constraint). (m ~ Monoid) => c ~=> m, c a) => a • In the expression: mempty In an equation for ‘baz’: baz = mempty | 21 | baz = mempty | ^^^^^^ Failed, no modules loaded.
Shouldn't the equality constraint be "substituted in"?
Attachments (1)
Change History (11)
comment:1 Changed 18 months ago by
Summary: | QuantifiedConstraints: class name introduced via an equality constraint does not reduce → QuantifiedConstraints: introducing classes through equality constraints fails |
---|
comment:2 Changed 18 months ago by
Changed 18 months ago by
Attachment: | icelandjack-profunctor-optics.jpeg added |
---|
Iceland_jack's encoding
comment:3 Changed 18 months ago by
Sorry for the trouble! I truly don't understand what happened when I made the report: when I check it now, all the definitions fail, just as you said.
And, worse, I just rewrote the code that I tried to "simplify" into the example in the original bug report, and it works now!
Perhaps it might give you an idea of what I was trying to achieve.
{-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE InstanceSigs #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeFamilyDependencies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE QuantifiedConstraints #-} module QC where import Data.Kind import Control.Arrow (left, right, (&&&), (|||)) import Control.Category import Prelude hiding (id, (.)) import Data.Coerce class (forall x. f x => g x) => f ~=> g instance (forall x. f x => g x) => f ~=> g type family (#) (p :: Type -> Type -> Type) (ab :: (Type, Type)) = (r :: Type) | r -> p ab where p # '(a, b) = p a b newtype Glass :: ((Type -> Type -> Type) -> Constraint) -> (Type, Type) -> (Type, Type) -> Type where Glass :: (forall p. z p => p # ab -> p # st) -> Glass z st ab data A_Prism type family ConstraintOf (tag :: Type) = (r :: (Type -> Type -> Type) -> Constraint) where ConstraintOf A_Prism = Choice _Left0 :: Glass Choice '(Either a x, Either b x) '(a, b) _Left0 = Glass left' _Left1 :: c ~=> Choice => Glass c '(Either a x, Either b x) '(a, b) _Left1 = Glass left' -- fails with -- • Could not deduce (Choice p) -- _Left2 -- :: (forall p. c p => ConstraintOf A_Prism p) -- => Glass c '(Either a x, Either b x) '(a, b) -- _Left2 = Glass left' _Left3 :: d ~ ConstraintOf A_Prism => (forall p . c p => d p) => Glass c '(Either a x, Either b x) '(a, b) _Left3 = Glass left' -- fails to typecheck unless at least a partial type signature is provided -- l :: c ~=> Choice => Glass c _ _ -- l = _Left1 . _Left1 newtype Optic o st ab where Optic :: (forall c d. (d ~ ConstraintOf o, c ~=> d) => Glass c st ab) -> Optic o st ab _Left :: Optic A_Prism '(Either a x, Either b x) '(a, b) _Left = Optic _Left1 instance Category (Glass z) where id :: Glass z a a id = Glass id (.) :: Glass z uv ab -> Glass z st uv -> Glass z st ab Glass abuv . Glass uvst = Glass (uvst . abuv) class Profunctor (p :: Type -> Type -> Type) where dimap :: (a -> b) -> (c -> d) -> p b c -> p a d lmap :: (a -> b) -> p b c -> p a c rmap :: (b -> c) -> p a b -> p a c class Profunctor p => Choice (p :: Type -> Type -> Type) where left' :: p a b -> p (Either a c) (Either b c) right' :: p a b -> p (Either c a) (Either c b)
Iceland_jack suggested an interesting encoding of profunctor optics (https://pbs.twimg.com/media/DY1y3voX4AAh1Jj.jpg:large) where, instead of specifying the constraint c
like is usually done in an encoding like
type Optic c s t a b = forall p. c p => p a b -> p s t
we just put a bound on it, to get something like
type QOptic c s t a b = forall p d. d ~=> c => Optic d s t a b
Then we can make optics where the profunctor satisfies _at least_ such-and-such constraint, but the quantified constraint lets you take it to satisfy something stronger (hence making it less general). This would mean that one could define a class whose instances would have to define something that was at least as good as a Prism
, say, but the instances were free to define something better like a Lens
or an Iso
. Kmett has a sketch of this idea: https://gist.github.com/ekmett/af1c460582b1de467c8461abdf134b6f.
I found that interesting, but for the fact that bindings with quantified constraints don't seem very friendly to inference, as I expected (e.g. :type
doesn't work without +v
, and, as shown above for the l
binding, you can't write _Left1 . _Left1
because the quantified c
is ambiguous).
So I thought of trying to encode things as newtypes: we could have a type tag o
(like A_Prism
) above that would, through a type family ConstraintOf
, give us a constraint that we could then use as a minimum bound. This makes things much less fragile by wrapping the polymorphism inside a constructor, which I found appealing.
Now, as in ticket:14860, this would mean trying to quantify a constraint involving a type family, which is not going to work directly. Hence the introduction of the d
variable, which it seems does get substituted in, as one can check with :type +v
:
*QC> :t +v _Left1 _Left1 :: (c ~=> Choice) => Glass c '(Either a x, Either b x) '(a, b)
Now, this is weird, but I could swear that the trick with the d
type variable didn't work when I submitted the bug report (likely a result of me reloading the wrong file in GHCi or something silly like that), and I "simplified" it down, poorly, to what I gave you.
Apologies :)
comment:4 Changed 18 months ago by
It's fine; did not take long. If the code above reflects something you want to do, I could just add it to our regression tests. It seems to be a relatively sophisticated use of QuantifiedConstraints
!
I'm not following the details but I'm sure that you and Iceland Jack will tell us if any further infelicities show up.
comment:5 Changed 18 months ago by
I think it would be good to add it as a regression test. Optics seem like an area where QuantifiedConstraints
could simplify many things a lot!
Also, is the incompatibility of QuantifiedConstraints
-using bindings with :type
in GHCi, or the inability to write, e.g.
_Left1 :: c ~=> Choice => Glass c '(Either a x, Either b x) '(a, b) _Left1 = Glass left' _Left4 = _Left1 {- src/Main.hs:73:10: error: • Could not deduce (Choice x1) arising from a use of ‘_Left1’ from the context: c x1 bound by a quantified context at src/Main.hs:73:1-15 Possible fix: add (Choice x1) to the context of a quantified context • In the expression: _Left1 In an equation for ‘_Left4’: _Left4 = _Left1 -}
expected? (I have -XNoMonomorphismRestriction
on if that's relevant.)
comment:6 Changed 18 months ago by
You want GHC to infer a type with a quantified constraint. In general that is hard, and quite probably not what you wanted, so GHC doesn't even try.
In short: no inferred type has a quantified constraint, only declared types.
In GHCi, :type <expression>
infers the type of <expression>
so you have the same issue. On the other hand :info <identifier>
will work just fine.
Does that make sense?
comment:8 Changed 18 months ago by
Resolution: | → invalid |
---|---|
Status: | new → closed |
comment:9 Changed 16 months ago by
Keywords: | wipT2893 removed |
---|
comment:10 Changed 16 months ago by
Milestone: | → 8.6.1 |
---|---|
Test Case: | → quantified-constraints/T14961 |
I get different results for
wip/T2893
branch. First I needFlexibleContexts
. Second, all the definitions fail. For the first one I getAnd the same happens if I simplify the type a bit more to
Sure enough, this is an ambiguous type! In a call, how do you expect
c
to be instantiated??I'm at a loss for what you are trying to achieve here. Before we can look at substituting equalities, we need to work out these simpler questions.