#15507 closed bug (duplicate)

Deriving with QuantifiedConstraints is unable to penetrate type families

Reported by: isovector Owned by:
Priority: normal Milestone: 8.6.1
Component: Compiler Version:
Keywords: QuantifiedConstraints Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: #14860 Differential Rev(s):
Wiki Page:

Description (last modified by isovector)

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])    

Change History (2)

comment:1 Changed 13 months ago by isovector

Description: modified (diff)

comment:2 Changed 13 months ago by RyanGlScott

Resolution: duplicate
Status: newclosed

Alas, this is expected behavior. See #14860.

On GHC HEAD, you'll get a more informative error message, at least:

GHCi, version 8.7.20180806: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling QuantifiedConstraints ( Bug.hs, interpreted )

Bug.hs:20:19: error:
    • Illegal type synonym family application in instance: HKD f a
    • In the quantified constraint ‘forall a. Eq a => Eq (HKD f a)’
      In the stand-alone deriving instance for
        ‘(forall a. Eq a => Eq (HKD f a)) => Eq (Foo f)’
   |
20 | deriving instance (forall a. Eq a => Eq (HKD f a)) => Eq (Foo f)
   |                   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Note: See TracTickets for help on using tickets.