#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