[GHC] #14861: QuantifiedConstraints: Can't use forall'd variable in context
#14861: QuantifiedConstraints: Can't use forall'd variable in context -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 (Type checker) | Keywords: | Operating System: Unknown/Multiple QuantifiedConstraints wipT2893 | Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- This fails to typecheck, to my surprise: {{{#!hs {-# 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14861 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14861: QuantifiedConstraints: Can't use forall'd variable in context -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints wipT2893 Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
I would have expected the (forall p. c p => Foldable' f) quantified constraint to kick in there.
Can you say why? We are trying to solve `c beta`. How does the quantified constraint help with that? It tells how to solve `Foldable` constraints. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14861#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14861: QuantifiedConstraints: Can't use forall'd variable in context -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints wipT2893 Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Replying to [comment:1 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: {{{#!hs (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`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14861#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14861: QuantifiedConstraints: Can't use forall'd variable in context -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints wipT2893 Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): 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! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14861#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14861: QuantifiedConstraints: Can't use forall'd variable in context -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints wipT2893 Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): 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: {{{#!hs 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: {{{#!hs 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14861#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14861: QuantifiedConstraints: Can't use forall'd variable in context -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints wipT2893 Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): 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] }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14861#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14861: QuantifiedConstraints: Can't use forall'd variable in context -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: invalid | QuantifiedConstraints wipT2893 Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => closed * resolution: => invalid Comment: 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14861#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC