#15635: Implication introduction for quantified constraints -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: feature | Status: new request | Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.6.1-beta1 Keywords: | Operating System: Unknown/Multiple QuantifiedConstraints | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Now that we have `QuantifiedConstraints`, it seems we need some implication introduction form. The `constraints` package has these types: {{{#!hs data Dict a where Dict :: a => Dict a newtype a :- b = Sub (a => Dict b) }}} `QuantifiedConstraints` suggests another version of `:-`: {{{#!hs newtype Imp a b = Imp { unImp :: forall r. ((a => b) => r) -> r} }}} We can write {{{#!hs fromImp :: Imp a b -> a :- b fromImp (Imp f) = Sub (f Dict) }}} But ... there's no way to go the other way! Let's try it: {{{#!hs toImp :: a :- Dict b -> a :- b toImp (Sub ab) = Imp $ \r -> _ }}} We get {{{ * Found hole: _ :: r * Relevant bindings include r :: (a => b) => r ab :: a => Dict b }}} There's no way to put these things together. But there's no terribly obvious reason they ''can't'' be combined. `a => b` is a function from an `a` dictionary to a `b` dictionary. `a => Dict b` is a function from an `a` dictionary to a value that ''contains'' a `b` dictionary. We just need some way to plumb these things together: some sort of implication introduction. The simplest thing might be a bit of magic: {{{#!hs implIntro :: ((a => b) => q) -> (forall r. (b => r) -> (a => r)) -> q }}} In Core (modulo type abstraction and application), we could simply write {{{#!hs implIntro f g = f (g id) }}} Unfortunately, I doubt that `implIntro` is really general enough to do everything people will want in this space. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15635 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler