QuantifiedConstraints: introducing classes through equality constraints fails

changed weight to 5

changed title from QuantifiedConstraints: class name introduced via an equality constraint does not reduce to QuantifiedConstraints: introducing classes through equality constraints fails

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.

Attached file icelandjack-profunctor-optics.jpeg (download).

Iceland_jack's encoding

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.

{-# 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 #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 :)

It's fine; did not take long. If the code above reflects something you want to do, I could just add it to our regression tests. It seems to be a relatively sophisticated use of QuantifiedConstraints!

I'm not following the details but I'm sure that you and Iceland Jack will tell us if any further infelicities show up.

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.

_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.)

You want GHC to infer a type with a quantified constraint. In general that is hard, and quite probably not what you wanted, so GHC doesn't even try.

In short: no inferred type has a quantified constraint, only declared types.

In GHCi, :type <expression> infers the type of <expression> so you have the same issue. On the other hand :info <identifier> will work just fine.

Does that make sense?

Yes, it does. Thanks for humouring me!

closed

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedInvalid

changed milestone to %8.6.1

Trac metadata

Trac field	Value
Test case	- → quantified-constraints/T14961

added 1 deleted label

added Pnormal label

Trac field	Value
Version	8.5
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC	Iceland_jack
Operating system
Architecture

QuantifiedConstraints: introducing classes through equality constraints fails

Child items ...

Activity