#2893: Implement "Quantified contexts" proposal -------------------------------------+------------------------------------- Reporter: porges | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: ⊥ Component: Compiler | Version: 6.10.1 Resolution: | Keywords: proposal Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by dfeuer): Replying to [comment:12 heisenbug]:

Copying a use-case from #9196:

My point is that I'd like to have polymorphic (multiparameter) constraints, where the param universally abstracted over is a non-`*` kind, that is an ADT.

See: {{{ class Foo a where ... data Bar (b :: Bool) x = ... instance Foo (Bar True x) where ... instance Foo (Bar False x) where ...

test :: (forall b. Foo (Bar b x)) =>... }}} Here the `forall` condition is satisfiable, as all `Bool` alternatives are covered with `instance` declarations.

Actually, the `forall` condition is ''not'' satisfiable. The smaller problem is that stuck type families like `Any` can inhabit `Bool` without being `'True` or `'False`. The bigger problem is that Haskell's "logic" is inherently constructive. The claim that for any type `b :: Bool` there exists some instance `Foo b x` does not translate to a way to actually get the dictionary representing that instance. So I think your beautiful dream is, sadly, almost certainly unrealizable. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/2893#comment:24 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler