Re: [GHC] #15507: Deriving with QuantifiedConstraints is unable to penetrate type families

11 Aug 2018

      #15507: Deriving with QuantifiedConstraints is unable to penetrate type families
-------------------------------------+-------------------------------------
        Reporter:  isovector         |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.6.1
       Component:  Compiler          |              Version:
      Resolution:                    |             Keywords:
                                     |  QuantifiedConstraints
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Description changed by isovector:

Old description:
...
I'd expect the following code to successfully derive a usable `Eq`
instance for `Foo`.

...
{{{#!hs
{-# LANGUAGE QuantifiedConstraints      #-}
{-# LANGUAGE StandaloneDeriving         #-}
{-# LANGUAGE TypeFamilies               #-}
{-# LANGUAGE UndecidableInstances       #-}
module QuantifiedConstraints where
import Data.Functor.Identity
type family HKD f a where
  HKD Identity a = a
  HKD f a = f a

...
data Foo f = Foo
  { zoo :: HKD f Int
  , zum :: HKD f Bool
  }
deriving instance (forall a. Eq (HKD f a)) => Eq (Foo f)
}}}
However, it complains:

...
{{{
    • Could not deduce (Eq (HKD f a))
      from the context: forall a. Eq (HKD f a)
        bound by an instance declaration:
                   forall (f :: * -> *). (forall a. Eq (HKD f a)) => Eq
(Foo f)
        at /home/sandy/prj/book-of-
types/code/QuantifiedConstraints.hs:20:19-56
    • In the ambiguity check for an instance declaration
      To defer the ambiguity check to use sites, enable
AllowAmbiguousTypes
      In the stand-alone deriving instance for
        ‘(forall a. Eq (HKD f a)) => Eq (Foo f)’
}}}
Adding -XAllowAmbiguousTypes doesn't fix the situation:
{{{
    • Could not deduce (Eq (HKD f a))
        arising from a use of ‘GHC.Classes.$dm/=’
      from the context: forall a. Eq (HKD f a)
        bound by the instance declaration
        at /home/sandy/prj/book-of-
types/code/QuantifiedConstraints.hs:21:1-56
    • In the expression: GHC.Classes.$dm/= @(Foo f)
      In an equation for ‘/=’: (/=) = GHC.Classes.$dm/= @(Foo f)
      When typechecking the code for ‘/=’
        in a derived instance for ‘Eq (Foo f)’:
        To see the code I am typechecking, use -ddump-deriv
      In the instance declaration for ‘Eq (Foo f)’
}}}
and the result of -ddump-deriv:
{{{
==================== Derived instances ====================
Derived class instances:
  instance (forall a.
            GHC.Classes.Eq (QuantifiedConstraints.HKD f a)) =>
           GHC.Classes.Eq (QuantifiedConstraints.Foo f) where
    (GHC.Classes.==)
      (QuantifiedConstraints.Foo a1_a6MW a2_a6MX)
      (QuantifiedConstraints.Foo b1_a6MY b2_a6MZ)
      = (((a1_a6MW GHC.Classes.== b1_a6MY))
           GHC.Classes.&& ((a2_a6MX GHC.Classes.== b2_a6MZ)))

...
Derived type family instances:

...
==================== Filling in method body ====================
GHC.Classes.Eq [QuantifiedConstraints.Foo f_a6N0[ssk:1]]
  GHC.Classes./= = GHC.Classes.$dm/=
                     @(QuantifiedConstraints.Foo f_a6N0[ssk:1])
}}}
New description:

 I'd expect the following code to successfully derive a usable `Eq`
 instance for `Foo`.

 {{{#!hs
 {-# LANGUAGE QuantifiedConstraints      #-}
 {-# LANGUAGE StandaloneDeriving         #-}
 {-# LANGUAGE TypeFamilies               #-}
 {-# LANGUAGE UndecidableInstances       #-}

 module QuantifiedConstraints where

 import Data.Functor.Identity

 type family HKD f a where
   HKD Identity a = a
   HKD f a = f a

 data Foo f = Foo
   { zoo :: HKD f Int
   , zum :: HKD f Bool
   }

 deriving instance (forall a. Eq a => Eq (HKD f a)) => Eq (Foo f)
 }}}

 However, it complains:

 {{{
     • Could not deduce (Eq (HKD f a))
       from the context: forall a. Eq a => Eq (HKD f a)
         bound by an instance declaration:
                    forall (f :: * -> *).
                    (forall a. Eq a => Eq (HKD f a)) =>
                    Eq (Foo f)
         at /home/sandy/prj/book-of-
 types/code/QuantifiedConstraints.hs:20:19-64
       or from: Eq a
         bound by a quantified context
         at /home/sandy/prj/book-of-
 types/code/QuantifiedConstraints.hs:20:19-64
     • In the ambiguity check for an instance declaration
       To defer the ambiguity check to use sites, enable
 AllowAmbiguousTypes
       In the stand-alone deriving instance for
         ‘(forall a. Eq a => Eq (HKD f a)) => Eq (Foo f)’
 }}}

 Adding -XAllowAmbiguousTypes doesn't fix the situation:

 {{{
     • Could not deduce (Eq (HKD f Int)) arising from a use of ‘==’
       from the context: forall a. Eq a => Eq (HKD f a)
         bound by the instance declaration
         at /home/sandy/prj/book-of-
 types/code/QuantifiedConstraints.hs:21:1-64
     • In the first argument of ‘(&&)’, namely ‘((a1 == b1))’
       In the expression: (((a1 == b1)) && ((a2 == b2)))
       In an equation for ‘==’:
           (==) (Foo a1 a2) (Foo b1 b2) = (((a1 == b1)) && ((a2 == b2)))
       When typechecking the code for ‘==’
         in a derived instance for ‘Eq (Foo f)’:
         To see the code I am typechecking, use -ddump-deriv
    |
 21 | deriving instance (forall a. Eq a => Eq (HKD f a)) => Eq (Foo f)
    | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

 /home/sandy/prj/book-of-types/code/QuantifiedConstraints.hs:21:1: error:
     • Could not deduce (Eq (HKD f a))
         arising from a use of ‘GHC.Classes.$dm/=’
       from the context: forall a. Eq a => Eq (HKD f a)
         bound by the instance declaration
         at /home/sandy/prj/book-of-
 types/code/QuantifiedConstraints.hs:21:1-64
       or from: Eq a
         bound by a quantified context
         at /home/sandy/prj/book-of-types/code/QuantifiedConstraints.hs:1:1
     • In the expression: GHC.Classes.$dm/= @(Foo f)
       In an equation for ‘/=’: (/=) = GHC.Classes.$dm/= @(Foo f)
       When typechecking the code for ‘/=’
         in a derived instance for ‘Eq (Foo f)’:
         To see the code I am typechecking, use -ddump-deriv
       In the instance declaration for ‘Eq (Foo f)’
    |
 21 | deriving instance (forall a. Eq a => Eq (HKD f a)) => Eq (Foo f)
    | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

 }}}

 and the result of -ddump-deriv:

 {{{
 ==================== Derived instances ====================
 Derived class instances:
   instance (forall a.
             GHC.Classes.Eq a =>
             GHC.Classes.Eq (QuantifiedConstraints.HKD f a)) =>
            GHC.Classes.Eq (QuantifiedConstraints.Foo f) where
     (GHC.Classes.==)
       (QuantifiedConstraints.Foo a1_a74s a2_a74t)
       (QuantifiedConstraints.Foo b1_a74u b2_a74v)
       = (((a1_a74s GHC.Classes.== b1_a74u))
            GHC.Classes.&& ((a2_a74t GHC.Classes.== b2_a74v)))

 Derived type family instances:

 ==================== Filling in method body ====================
 GHC.Classes.Eq [QuantifiedConstraints.Foo f_a74w[ssk:1]]
   GHC.Classes./= = GHC.Classes.$dm/=
                      @(QuantifiedConstraints.Foo f_a74w[ssk:1])
 }}}

--

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15507#comment:1
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler