
#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