Deriving with QuantifiedConstraints is unable to penetrate type families
I'd expect the following code to successfully derive a usable Eq
instance for Foo
.
{-# 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])