#14861 closed bug (invalid)
QuantifiedConstraints: Can't use forall'd variable in context
Reported by: | RyanGlScott | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler (Type checker) | Version: | 8.5 |
Keywords: | QuantifiedConstraints | Cc: | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | GHC rejects valid program | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description
This fails to typecheck, to my surprise:
{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE UndecidableInstances #-} module Bug where import Data.Kind data ECC1 :: (Type -> Constraint) -> (Type -> Type) -> Type -> Type where ECC1 :: c p => f p -> ECC1 c f p class Foldable' f where foldMap' :: Monoid m => (a -> m) -> f a -> m instance (forall p. c p => Foldable' f) => Foldable' (ECC1 c f) where foldMap' f (ECC1 x) = foldMap' f x instance Foldable' [] where foldMap' = foldMap test :: ECC1 Show [] Ordering -> Ordering test = foldMap' id
$ ghc-cq/inplace/bin/ghc-stage2 --interactive Bug.hs GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) Bug.hs:18:25: error: • Could not deduce: c p0 arising from a use of ‘foldMap'’ from the context: forall p. c p => Foldable' f bound by the instance declaration at Bug.hs:17:10-63 or from: Monoid m bound by the type signature for: foldMap' :: forall m a. Monoid m => (a -> m) -> ECC1 c f a -> m at Bug.hs:18:3-10 or from: c a bound by a pattern with constructor: ECC1 :: forall (f :: * -> *) p (c :: * -> Constraint). c p => f p -> ECC1 c f p, in an equation for ‘foldMap'’ at Bug.hs:18:15-20 • In the expression: foldMap' f x In an equation for ‘foldMap'’: foldMap' f (ECC1 x) = foldMap' f x In the instance declaration for ‘Foldable' (ECC1 c f)’ • Relevant bindings include foldMap' :: (a -> m) -> ECC1 c f a -> m (bound at Bug.hs:18:3) | 18 | foldMap' f (ECC1 x) = foldMap' f x | ^^^^^^^^^^^^
I would have expected the (forall p. c p => Foldable' f)
quantified constraint to kick in there.
Change History (7)
comment:1 follow-up: 2 Changed 19 months ago by
comment:2 Changed 19 months ago by
Replying to simonpj:
Can you say why?
When we pattern-match on ECC1
, we bring into scope the given constraint c p0
, where p0
is a fresh type variable. We have as a constraint:
(forall p. c p => Foldable' f)
GHC should be able to use the given c p0
constraint to discharge the obligation and conclude Foldable' f
.
comment:3 Changed 19 months ago by
If I have
instance forall p. Show p => Show T
then when I invoke the instance declaration I get a Show beta
constraint with absolutely nothing telling the compiler what beta
should be. Yes, it could be solved with beta := Int
or a variety of other things. But GHC never guesses.
Same here. You have
instance (forall p. c p => Foldable' f) -- Yikes: nothing constrains p => Foldable' (ECC1 c f) where
When the quantified constraint fires, to solve Foldable' f
, it generates c beta
with no constraints whatsoever on beta
. The fact that we have in scope c p
does not help, because it requires quessing that beta := p
. Sorry!
comment:4 Changed 19 months ago by
I don't think we're talking about the same thing here. You're talking about solving beta := Int
, but I'm not asking for that! After, if you had:
instance forall p. Show p => Show T
Then that forces GHC to be parametric in p
(so trying to solve p := Int
would certainly be nonsense).
Similarly, in:
instance (forall p. c p => Foldable' f) -- Yikes: nothing constrains p => Foldable' (ECC1 c f) where
You put "Yikes: nothing constrains p
" here, but that is intentional! The whole point is that this constraint must be parametric in p
. Therefore, if we have a given constraint of the form c Int
, then this certainly couldn't be used to discharge that quantified constraint.
However, the code I wrote should work, since the given constraint we have is c p0
—this does not violate the parametricity of p
, as p0
is simply a skolem.
comment:5 Changed 19 months ago by
No, p is not a skolem. Think of the quantified constraint like a local instance decl. It says
local instance forall p. c p => Foldable' f
That means, if you want to solve Foldable' f
(where f
really is a skolem coming from the instance for Foldable' (ECC1 c f)
), then
- If you can solve
c beta
, where you are free to pick beta - then you can solve
Foldable' f
So we have to guess beta
. And we can't.
Try some top level instances with tyars on the left which don't appear on the right
instance C a => C [b]
comment:6 Changed 19 months ago by
Resolution: | → invalid |
---|---|
Status: | new → closed |
Hm. Your point about instance C a => C [b]
being wonky is a good one. In practice, such an instance would probably be OK if we could explicitly manipulate dictionaries and specify what exactly a
should be whenever we applied it. But alas, we cannot, and GHC is unwilling to do this for us, so I'm forced to agree that this is in the realm of the impossible for the time being.
comment:7 Changed 16 months ago by
Keywords: | wipT2893 removed |
---|
Can you say why? We are trying to solve
c beta
. How does the quantified constraint help with that? It tells how to solveFoldable
constraints.