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