I’m looking at the flurry of activity around Quantified Constraints [1, 2, 3], suggestion of uses for implication logic [4], and comments in the hs2017 paper “raise the expressive power of type classes … to first-order logic. … more expressive modelling …”[Abstract]. 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 ) -- etc => And (b1 :: Bool) (b2 :: Bool) (b3 :: Bool) | b1 b2 -> b3 where … None of this is relying on `Bool` being a closed type AFAICT. (That’s the usual downfall of trying to capture application logic in constraints.) Come to that, can we capture the logic of the FunDep? (The hs2017 paper hints we might.) class ( {- as before -}, ( forall b3’. And b1 b2 b3’ => b3’ ~ b3 ) ) => And (b1 :: Bool) (b2 :: Bool) (b3 :: Bool) | b1 b2 -> b3 where … This might come closer to the logic of FunDeps as originally specified by Mark P Jones, which ghc doesn’t quite reach to [6]. OTOH we now have a cyclical superclass constraint, which ain’t allowed. [1] https://github.com/ghc-proposals/ghc-proposals/pull/109 [2] https://ghc.haskell.org/trac/ghc/wiki/QuantifiedConstraints [3] https://ghc.haskell.org/trac/ghc/ticket/2893 [4] https://mail.haskell.org/pipermail/libraries/2017-December/028377.html [5] https://mail.haskell.org/pipermail/ghc-devs/2017-November/015073.html, continued at https://mail.haskell.org/pipermail/glasgow-haskell-users/2017-November/02665... [6] https://ghc.haskell.org/trac/ghc/ticket/10675 AntC