[GHC] #14961: QuantifiedConstraints: introducing classes through equality constraints fails

[GHC]

#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