#14733 closed bug (fixed)
Won't use (forall xx. f xx) with -XQuantifiedConstraints
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
{-# Language QuantifiedConstraints #-} {-# Language GADTs #-} {-# Language ConstraintKinds #-} data D c where D :: c => D c proof :: (forall xx. f xx) => D (f a) proof = D
Running this program with wip/T2893 gives
GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( 174-quantifiedconstraints.hs, interpreted ) 174-quantifiedconstraints.hs:9:9: error: • Could not deduce: f a arising from a use of ‘D’ from the context: forall xx. f xx bound by the type signature for: proof :: forall (f :: * -> Constraint) a. (forall xx. f xx) => D (f a) at 174-quantifiedconstraints.hs:8:1-37 • In the expression: D In an equation for ‘proof’: proof = D • Relevant bindings include proof :: D (f a) (bound at 174-quantifiedconstraints.hs:9:1) | 9 | proof = D | ^
How can I instantiate xx
to a
?
Change History (13)
comment:1 Changed 2 years ago by
Keywords: | QuantifiedContexts added |
---|
comment:2 Changed 2 years ago by
Keywords: | wipT2893 added |
---|
comment:3 follow-up: 7 Changed 2 years ago by
comment:4 Changed 2 years ago by
Keywords: | QuantifiedConstraints added; QuantifiedContexts removed |
---|
comment:5 follow-up: 8 Changed 2 years ago by
How about adding the workaround internally? I.e. add
class c => SomeInteralClass c instance c => SomeInternalClass c
and translate (forall xx. f xx)
to (forall xx. SomeInternalClass (f xx))
comment:6 Changed 2 years ago by
Only moderate pain? ;-) Here are some use cases
- (Phab) Vocabulary of constraints:
constC :: a :- (b => a)
. In fact lifting this restriction lets us definea :- b
asDict (a => b)
pattern SubDict :: a => b => (a :- b) pattern SubDict = Dict
- (Phab)
newtype Free cls a = Free (forall xx. cls xx => (a -> xx) -> xx) instance (forall xx. cls (Free cls xx)) => Monad (Free cls)
- (Phab)
type cls ~=> cls' = forall xx. cls xx => cls' xx instance Monoid ~=> mon => Foldable (Free mon)
- (Phab by Ryan) The need for
Coercible1
has been discussed elsewhere, current design preventsCoercible
from being abstracted out.type Coercible1 m = forall xx yy. Coercible xx yy => Coercible (m xx) (m yy),
- We might similarly want to parameterize
Coercion
byCoercible
type Coercion = With Coercible type (:~:) = With (~) type (:~~:) = With (~~) data With cls a b where With :: cls a b => With cls a b
.. without losing that
Category
instance:-- Constraint-enriched category type Refl rel = forall a. () => rel a a type Trans rel = forall a b c. (rel a b, rel b c) => rel a c instance (Refl rel, Trans rel) => Category (With rel) where id :: With rel a a id = With (.) :: With rel b c -> With rel a b -> With rel a c With . With = With
Your class f a => C f a
solution didn't work for me (using latest version): here is my full code and error messages.
Echoing Sjoerd if there is a mechanical translation can't GHC do it?
comment:7 Changed 2 years ago by
Replying to simonpj:
Currently this is by-design, but we could change the design.
I'm +1 on change but that's easy to say, how big of a task is it
How bad is the restriction?
Hard to say. If it's a matter of encoding them as class aliases then it is a huge improvement over the current situation, otherwise may rule out a lot of fun examples.
comment:8 Changed 2 years ago by
Replying to sjoerd_visscher:
How about adding the workaround internally? I.e. add
class c => SomeInteralClass c instance c => SomeInternalClass cand translate
(forall xx. f xx)
to(forall xx. SomeInternalClass (f xx))
That's one idea. But does that idea even work if you write it out by hand? I tried:
{-# Language QuantifiedConstraints #-} {-# Language GADTs #-} {-# Language ConstraintKinds #-} {-# Language FlexibleInstances #-} {-# Language UndecidableInstances #-} {-# Language UndecidableSuperClasses #-} class c => SomeInternalClass c instance c => SomeInternalClass c data D c where D :: c => D c proof :: (forall xx. SomeInternalClass (f xx)) => D (f a) proof = D
But that fails with:
Bug.hs:15:9: error: • Could not deduce: f a arising from a use of ‘D’ from the context: forall xx. SomeInternalClass (f xx) bound by the type signature for: proof :: forall (f :: * -> Constraint) a. (forall xx. SomeInternalClass (f xx)) => D (f a) at Bug.hs:14:1-57 • In the expression: D In an equation for ‘proof’: proof = D • Relevant bindings include proof :: D (f a) (bound at Bug.hs:15:1) | 15 | proof = D | ^
Granted, it does work if you change the proof
to:
proof :: (forall xx. SomeInternalClass (f xx)) => D (SomeInternalClass (f a)) proof = D
But that would require pervasively inserting SomeInternalClass
everywhere in your program, and not just on the quantified constraints which lack an explicit type class constructor.
comment:9 Changed 2 years ago by
I have fixed this (on branch wip/TT2893
); and updated the proposal to reflect it
Would you like to try now?
comment:10 Changed 2 years ago by
Thank you! I played with it yesterday and it works great with a few kinks.
comment:12 Changed 2 years ago by
Resolution: | → fixed |
---|---|
Status: | new → closed |
This featurette was fixed in c477f53799deb46b4987ac788ad67d1bcbb8eb0c.
comment:13 Changed 20 months ago by
Keywords: | wipT2893 removed |
---|
Currently this is by-design, but we could change the design.
These forall-constraints currently behave just like a local version of a top-level instance declaration, and those are all for classes. You can't say
although it'd make sense to do so. So similarly you currently can't do that with the local-foralld constraints.
It'd be a moderate pain to generalise the facility, mainly because
InstEnv
(in which we look up instances) has class constraints as a deeply-baked-in assumption.