#14937: QuantifiedConstraints: Reify implication constraints from terms lacking them -------------------------------------+------------------------------------- Reporter: Bj0rn | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #14822, #15635 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by dfeuer): The magical built-in function doesn't seem like strong enough medicine. Today, you asked for {{{#!hs reifyImplication :: forall a b. (forall r. a => (b => r) -> r) -> (forall r. ((a => b) => r) -> r) }}} But tomorrow, you might need {{{#!hs reifyImplication1 :: forall a b. (forall r x. a x => (b x => r) -> r) -> (forall r. ((forall x. a x => b x) => r) -> r) reifyImplication2 :: forall a b. (forall r x y. a x y => (b x y => r) -> r) -> (forall r. ((forall x y. a x y => b x y) => r) -> r) }}} and the day after that, you may want {{{#!hs reifyImplicationQ :: forall a b y. (forall r x. a x y => (b x y => r) -> r) -> (forall r. ((forall x. a x y => b x y) => r) -> r) }}} and so on. It would be possible to offer a whole set of these primitives, but it would be a bit of a mess and never complete. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14937#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler