#2893: Implement "Quantified constraints" proposal -------------------------------------+------------------------------------- Reporter: porges | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: ⊥ Component: Compiler | Version: 6.10.1 Resolution: | Keywords: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #5927 | Differential Rev(s): Phab:D4353 Wiki Page: | -------------------------------------+------------------------------------- Comment (by AntC):

... superclass stufff ... Give it a whirl!

Terrific. I'd appreciate if someone could test my hypothesis of a use case [1]. Note this using QuantifiedConstraints purely as implications with nothing `forall`'d.:

Consider modelling the logic for somewhat-injective type functions. Take type-level Boolean `And` [5].

`And` is not fully injective but:

* If the result is True, the two arguments must be True.

* If the result is False and one argument is True, the other must be False.

{{{ class ( (b3 ~ True) => (b1 ~ True, b2 ~ True), (b3 ~ False, b1 ~ True) => b2 ~ False, (b3 ~ False, b2 ~ True) => b1 ~ False ) => And (b1 :: Bool) (b2 :: Bool) (b3 :: Bool) | b1 b2 -> b3 where {} instance And True b2 b2 instance And False b2 False x3 = undefined :: (And b1 b2 True) => (b1, b2) -- should infer x3's type as :: (True, True) }}} [https://mail.haskell.org/pipermail/glasgow-haskell- users/2018-February/026694.html [1]] [https://mail.haskell.org/pipermail/ghc-devs/2017-November/015073.html [5]] [https://mail.haskell.org/pipermail/glasgow-haskell- users/2017-November/026650.html continued] -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/2893#comment:35 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler