Opened 18 months ago

Closed 18 months ago

Last modified 16 months ago

#14961 closed bug (invalid)

QuantifiedConstraints: introducing classes through equality constraints fails

Reported by: mrkgnao Owned by:
Priority: normal Milestone: 8.6.1
Component: Compiler Version: 8.5
Keywords: QuantifiedConstraints Cc: Iceland_jack
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case: quantified-constraints/T14961
Blocked By: Blocking:
Related Tickets: #14860 Differential Rev(s):
Wiki Page:

Description

The following doesn't typecheck with the wip/T2893 branch:

{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE TypeFamilies #-}

module Subst where

class (forall x. c x => d x) => c ~=> d
instance (forall x. c x => d x) => c ~=> d

foo :: forall c a. c ~=> Monoid => (c a => a) -- ok
foo = mempty

bar :: forall c a m. (m ~ Monoid, c ~=> m) => (c a => a) -- ok
bar = mempty

baz :: forall c a. (forall m. m ~ Monoid => c ~=> m) => (c a => a) -- fails
baz = mempty
Prelude> :reload
[1 of 1] Compiling Subst            ( src/Subst.hs, interpreted )

src/Subst.hs:21:7: error:
    • Could not deduce (Monoid a) arising from a use of ‘mempty’
      from the context: (forall (m :: * -> Constraint).
                         (m ~ Monoid) =>
                         c ~=> m,
                         c a)
        bound by the type signature for:
                   baz :: forall (c :: * -> Constraint) a.
                          (forall (m :: * -> Constraint). (m ~ Monoid) => c ~=> m, c a) =>
                          a
        at src/Subst.hs:20:1-66
      Possible fix:
        add (Monoid a) to the context of
          the type signature for:
            baz :: forall (c :: * -> Constraint) a.
                   (forall (m :: * -> Constraint). (m ~ Monoid) => c ~=> m, c a) =>
                   a
    • In the expression: mempty
      In an equation for ‘baz’: baz = mempty
   |
21 | baz = mempty
   |       ^^^^^^
Failed, no modules loaded.

Shouldn't the equality constraint be "substituted in"?

Attachments (1)

icelandjack-profunctor-optics.jpeg (110.0 KB) - added by mrkgnao 18 months ago.
Iceland_jack's encoding

Download all attachments as: .zip

Change History (11)

comment:1 Changed 18 months ago by mrkgnao

Summary: QuantifiedConstraints: class name introduced via an equality constraint does not reduceQuantifiedConstraints: introducing classes through equality constraints fails

comment:2 Changed 18 months ago 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.

Changed 18 months ago by mrkgnao

Iceland_jack's encoding

comment:3 Changed 18 months ago 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.

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

comment:4 Changed 18 months ago by simonpj

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.

comment:5 Changed 18 months ago 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.

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

comment:6 Changed 18 months ago by simonpj

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?

comment:7 Changed 18 months ago by mrkgnao

Yes, it does. Thanks for humouring me!

comment:8 Changed 18 months ago by mrkgnao

Resolution: invalid
Status: newclosed

comment:9 Changed 16 months ago by RyanGlScott

Keywords: wipT2893 removed

comment:10 Changed 16 months ago by RyanGlScott

Milestone: 8.6.1
Test Case: quantified-constraints/T14961
Note: See TracTickets for help on using tickets.