
#14863: QuantifiedConstraints: Can't deduce `c' from `(a, b)' and `a |- b |- c' -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: fixed | Keywords: | QuantifiedConstraints wipT2893 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 Iceland_jack): This is great work thanks! For those interested these examples came from [https://www.reddit.com/r/haskell/comments/6k86je/constraint_unions_bringing_... Edward Kmett's encoding of sums of Constraints]. This may be a milestone, since `curryC` / `uncurryC` mean that the "category of entailment" `(:-)` is a Cartesian closed `Constraint` category (which means we could get [https://www.reddit.com/r/haskell/comments/73lp4m/higherorder_abstract_syntax... HOAS syntax for constraints]?). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14863#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler