Nested quantified constraints don't work
Consider this, spun off from #14860:
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE InstanceSigs #-}
module Foo where
class (forall c. c ~ T a => Show (c b)) => ShowT a b
instance Show (T a b) => ShowT a b
class (forall b. Show b => ShowT a b) => C a where
type family T a :: * -> *
data D a = MkD (T a Int)
instance C a => Show (D a) where
showsPrec p (MkD x)
= (showParen (p > 10) $ showString "MkD " . showsPrec 11 x)
When typechecking the final instance
decl we get
T14860a.hs:22:49: error:
• Could not deduce (Show (T a Int))
arising from a use of ‘showsPrec’
from the context: C a
bound by the instance declaration at T14860a.hs:20:10-26
but this is bogus. We have
g1: [G] C a -- Given by the instance
g2: [G] forall b. Show b => ShowT a b -- Superclass of g1
g3: [G] forall b c. (Show b, c ~ T a) => Show (c b) -- Superclass of g2
w1: [W] Show (T a Int) -- Wanted by the rhs of showsPrec
Well, that wanted should match g3
! But it doesn't because g3
ends up with a funny type
g3: [G] forall b. Show b => forall c. (Show b, c ~ T a) => Show (c b)
and that doens't work well at all.
Should not be hard to fix this.
EDIT: In the end, we don't think we really should accept this program, because it purports to solve Show (a b)
for any a
and b
-- an unlikely proposition. But the current (now that !2283 (closed) has landed) error message complains about default methods, which is poor form. We should fix the error message.