#14961: QuantifiedConstraints: introducing classes through equality constraints fails -------------------------------------+------------------------------------- Reporter: mrkgnao | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints wipT2893 Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #14860 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): I get different results for `wip/T2893` branch. First I need `FlexibleContexts`. Second, all the definitions fail. For the first one I get {{{ T14961.hs:16:8: error: • Could not deduce: c0 a from the context: (c ~=> Monoid, c a) bound by the type signature for: foo :: forall (c :: * -> Constraint) a. (c ~=> Monoid, c a) => a at T14961.hs:16:8-45 • In the ambiguity check for ‘foo’ To defer the ambiguity check to use sites, enable AllowAmbiguousTypes In the type signature: foo :: forall c a. c ~=> Monoid => (c a => a) | 16 | foo :: forall c a. c ~=> Monoid => (c a => a) -- ok | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ }}} And the same happens if I simplify the type a bit more to {{{ foo :: forall c a. (forall x. c x => Monoid x) => (c a => a) -- ok }}} Sure enough, this is an ambiguous type! In a call, how do you expect `c` to be instantiated?? I'm at a loss for what you are trying to achieve here. Before we can look at substituting equalities, we need to work out these simpler questions. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14961#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14961: QuantifiedConstraints: introducing classes through equality constraints fails -------------------------------------+------------------------------------- Reporter: mrkgnao | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints wipT2893 Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #14860 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by mrkgnao): Sorry for the trouble! I truly don't understand what happened when I made the report: when I check it now, all the definitions fail, just as you said. And, worse, I just rewrote the code that I tried to "simplify" into the example in the original bug report, and it works now! Perhaps it might give you an idea of what I was trying to achieve. {{{#!hs {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE InstanceSigs #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeFamilyDependencies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE QuantifiedConstraints #-} module QC where import Data.Kind import Control.Arrow (left, right, (&&&), (|||)) import Control.Category import Prelude hiding (id, (.)) import Data.Coerce class (forall x. f x => g x) => f ~=> g instance (forall x. f x => g x) => f ~=> g type family (#) (p :: Type -> Type -> Type) (ab :: (Type, Type)) = (r :: Type) | r -> p ab where p # '(a, b) = p a b newtype Glass :: ((Type -> Type -> Type) -> Constraint) -> (Type, Type) -> (Type, Type) -> Type where Glass :: (forall p. z p => p # ab -> p # st) -> Glass z st ab data A_Prism type family ConstraintOf (tag :: Type) = (r :: (Type -> Type -> Type) -> Constraint) where ConstraintOf A_Prism = Choice _Left0 :: Glass Choice '(Either a x, Either b x) '(a, b) _Left0 = Glass left' _Left1 :: c ~=> Choice => Glass c '(Either a x, Either b x) '(a, b) _Left1 = Glass left' -- fails with -- • Could not deduce (Choice p) -- _Left2 -- :: (forall p. c p => ConstraintOf A_Prism p) -- => Glass c '(Either a x, Either b x) '(a, b) -- _Left2 = Glass left' _Left3 :: d ~ ConstraintOf A_Prism => (forall p . c p => d p) => Glass c '(Either a x, Either b x) '(a, b) _Left3 = Glass left' -- fails to typecheck unless at least a partial type signature is provided -- l :: c ~=> Choice => Glass c _ _ -- l = _Left1 . _Left1 newtype Optic o st ab where Optic :: (forall c d. (d ~ ConstraintOf o, c ~=> d) => Glass c st ab) -> Optic o st ab _Left :: Optic A_Prism '(Either a x, Either b x) '(a, b) _Left = Optic _Left1 instance Category (Glass z) where id :: Glass z a a id = Glass id (.) :: Glass z uv ab -> Glass z st uv -> Glass z st ab Glass abuv . Glass uvst = Glass (uvst . abuv) class Profunctor (p :: Type -> Type -> Type) where dimap :: (a -> b) -> (c -> d) -> p b c -> p a d lmap :: (a -> b) -> p b c -> p a c rmap :: (b -> c) -> p a b -> p a c class Profunctor p => Choice (p :: Type -> Type -> Type) where left' :: p a b -> p (Either a c) (Either b c) right' :: p a b -> p (Either c a) (Either c b) }}} Iceland_jack suggested an interesting encoding of profunctor optics (https://pbs.twimg.com/media/DY1y3voX4AAh1Jj.jpg:large) where, instead of specifying the constraint `c` like is usually done in an encoding like {{{ type Optic c s t a b = forall p. c p => p a b -> p s t }}} we just put a bound on it, to get something like {{{ type QOptic c s t a b = forall p d. d ~=> c => Optic d s t a b }}} Then we can make optics where the profunctor satisfies _at least_ such- and-such constraint, but the quantified constraint lets you take it to satisfy something stronger (hence making it less general). This would mean that one could define a class whose instances would have to define something that was at least as good as a `Prism`, say, but the instances were free to define something better like a `Lens` or an `Iso`. Kmett has a sketch of this idea: https://gist.github.com/ekmett/af1c460582b1de467c8461abdf134b6f. I found that interesting, but for the fact that bindings with quantified constraints don't seem very friendly to inference, as I expected (e.g. `:type` doesn't work without `+v`, and, as shown above for the `l` binding, you can't write `_Left1 . _Left1` because the quantified `c` is ambiguous). So I thought of trying to encode things as newtypes: we could have a type tag `o` (like `A_Prism`) above that would, through a type family `ConstraintOf`, give us a constraint that we could then use as a minimum bound. This makes things much less fragile by wrapping the polymorphism inside a constructor, which I found appealing. Now, as in ticket:14860, this would mean trying to quantify a constraint involving a type family, which is not going to work directly. Hence the introduction of the `d` variable, which it seems does get substituted in, as one can check with `:type +v`: {{{ *QC> :t +v _Left1 _Left1 :: (c ~=> Choice) => Glass c '(Either a x, Either b x) '(a, b) }}} Now, this is weird, but I could swear that the trick with the `d` type variable didn't work when I submitted the bug report (likely a result of me reloading the wrong file in GHCi or something silly like that), and I "simplified" it down, poorly, to what I gave you. Apologies :) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14961#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14961: QuantifiedConstraints: introducing classes through equality constraints fails -------------------------------------+------------------------------------- Reporter: mrkgnao | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints wipT2893 Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #14860 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by mrkgnao): I think it would be good to add it as a regression test. Optics seem like an area where `QuantifiedConstraints` could simplify many things a lot! Also, is the incompatibility of `QuantifiedConstraints`-using bindings with `:type` in GHCi, or the inability to write, e.g. {{{#!hs _Left1 :: c ~=> Choice => Glass c '(Either a x, Either b x) '(a, b) _Left1 = Glass left' _Left4 = _Left1 {- src/Main.hs:73:10: error: • Could not deduce (Choice x1) arising from a use of ‘_Left1’ from the context: c x1 bound by a quantified context at src/Main.hs:73:1-15 Possible fix: add (Choice x1) to the context of a quantified context • In the expression: _Left1 In an equation for ‘_Left4’: _Left4 = _Left1 -} }}} expected? (I have `-XNoMonomorphismRestriction` on if that's relevant.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14961#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14961: QuantifiedConstraints: introducing classes through equality constraints fails -------------------------------------+------------------------------------- Reporter: mrkgnao | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints wipT2893 Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #14860 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by mrkgnao): Yes, it does. Thanks for humouring me! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14961#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14961: QuantifiedConstraints: introducing classes through equality constraints fails -------------------------------------+------------------------------------- Reporter: mrkgnao | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 Resolution: invalid | Keywords: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: quantified- valid program | constraints/T14961 Blocked By: | Blocking: Related Tickets: #14860 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * testcase: => quantified-constraints/T14961 * milestone: => 8.6.1 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14961#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler