[GHC] #15507: Deriving with QuantifiedConstraints is unable to penetrate type families
GHC
ghc-devs at haskell.org
Sat Aug 11 20:31:32 UTC 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
More information about the ghc-tickets
mailing list