Skip to content

Quantified constraints leads to type errors when deriving default class methods

Summary

When working with a GADT, ConstraintKinds, and QuantifiedConstraints, I can build a Show instance that fails to typecheck if any of the default methods (showList and show xor showsPrec) are missing. Copy-and-pasting these implementations from the typeclass’s definition makes them typecheck, so I think this is a bug in code generation.

Steps to reproduce

Define

data Some (c :: Type -> Constraint) where
  Some :: c a => a -> Some c

Then try to write a Show instance using QuantifiedConstraints:

instance (forall x . c x => Show x) => Show (Some c) where
  showsPrec n (Some a) = showsPrec n a

An error message is emitted about not being able to make a deduction when generating $dmshow and $dmshowList:

src/Data/Some.hs:45:10: error:
    • Could not deduce: c (Some c)
        arising from a use of ‘GHC.Show.$dmshow’
      from the context: forall x. c x => Show x
        bound by the instance declaration at src/Data/Some.hs:45:10-52
    • In the expression: GHC.Show.$dmshow @(Some c)
      In an equation for ‘show’: show = GHC.Show.$dmshow @(Some c)
      In the instance declaration for ‘Show (Some c)’
    • Relevant bindings include
        show :: Some c -> String (bound at src/Data/Some.hs:45:10)
   |
45 | instance (forall x . c x => Show x) => Show (Some c) where
   |          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

src/Data/Some.hs:45:10: error:
    • Could not deduce: c (Some c)
        arising from a use of ‘GHC.Show.$dmshowList’
      from the context: forall x. c x => Show x
        bound by the instance declaration at src/Data/Some.hs:45:10-52
    • In the expression: GHC.Show.$dmshowList @(Some c)
      In an equation for ‘showList’:
          showList = GHC.Show.$dmshowList @(Some c)
      In the instance declaration for ‘Show (Some c)’
    • Relevant bindings include
        showList :: [Some c] -> ShowS (bound at src/Data/Some.hs:45:10)
   |
45 | instance (forall x . c x => Show x) => Show (Some c) where
   |          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

If you copy-paste in a definition of showList and show, things will typecheck. Example:

instance (forall x . c x => Show x) => Show (Some c) where
  showsPrec n (Some a) = showsPrec n a
  show        (Some a) = show a
  showList ls s = showList__ shows' ls s

-- Not sure why this is necessary: defining it inline produces another error
-- about being unable to deduce c (Some c).
shows' :: (forall x . c x => Show x) => Some c -> ShowS
shows' (Some x) = shows x

Expected behavior

I expected the original definition (one expressed solely in terms of showsPrec) to typecheck.

Environment

  • GHC version used: 8.8.1

Optional:

  • Operating System: macOS
  • System Architecture: x86_64
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information