diff options
author | Richard Eisenberg <rae@richarde.dev> | 2019-12-05 10:59:54 +0000 |
---|---|---|
committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2020-02-11 05:08:10 -0500 |
commit | de32beffde82eec954691703541a2d4081799453 (patch) | |
tree | b97109ac5b28a077f95bb057c0a3f7d5af371239 /testsuite/tests/typecheck | |
parent | 375b3c45be0e5de673d03097ebbad442c85c89eb (diff) | |
download | haskell-de32beffde82eec954691703541a2d4081799453.tar.gz |
Do not create nested quantified constraints
Previously, we would accidentally make constraints like
forall a. C a => forall b. D b => E a b c as we traversed
superclasses. No longer!
This patch also expands Note [Eagerly expand given superclasses]
to work over quantified constraints; necessary for T16502b.
Close #17202 and #16502.
test cases: typecheck/should_compile/T{17202,16502{,b}}
Diffstat (limited to 'testsuite/tests/typecheck')
-rw-r--r-- | testsuite/tests/typecheck/should_compile/T16502b.hs | 35 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_compile/T17202.hs | 4 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_compile/all.T | 3 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_fail/T16502.hs | 31 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_fail/all.T | 1 |
5 files changed, 72 insertions, 2 deletions
diff --git a/testsuite/tests/typecheck/should_compile/T16502b.hs b/testsuite/tests/typecheck/should_compile/T16502b.hs new file mode 100644 index 0000000000..03855c4557 --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/T16502b.hs @@ -0,0 +1,35 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UndecidableInstances #-} +module T16502b where + +import Data.Kind + +type family Sing :: k -> Type + +class (forall (sing :: k -> Type). sing ~ Sing => Show (sing z)) + => ShowSing' (z :: k) +instance Show (Sing z) => ShowSing' (z :: k) + +class (forall (z :: k). ShowSing' z) => ShowSing k +instance (forall (z :: k). ShowSing' z) => ShowSing k + +newtype Foo a = MkFoo a +data SFoo :: forall a. Foo a -> Type where + SMkFoo :: Sing x -> SFoo (MkFoo x) +type instance Sing = SFoo +deriving instance ShowSing a => Show (SFoo (z :: Foo a)) + +newtype Bar a = MkBar (Foo a) +data SBar :: forall a. Bar a -> Type where + SMkBar :: forall a (x :: Foo a). Sing x -> SBar (MkBar x) +type instance Sing = SBar +deriving instance ShowSing (Foo a) => Show (SBar (z :: Bar a)) diff --git a/testsuite/tests/typecheck/should_compile/T17202.hs b/testsuite/tests/typecheck/should_compile/T17202.hs index d9d6ec281f..9f28ccc753 100644 --- a/testsuite/tests/typecheck/should_compile/T17202.hs +++ b/testsuite/tests/typecheck/should_compile/T17202.hs @@ -1,6 +1,7 @@ {-# LANGUAGE GADTs #-} {-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE ConstraintKinds #-} module T17202 where @@ -15,6 +16,7 @@ data Dict c = c => Dict foo :: forall a. C3 a => Dict (C1 a) foo = Dict +{- is rejected due to #17719 bar :: forall a. C3 a => Dict (C1 a) bar = Dict :: C2 a => Dict (C1 a) - +-} diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T index 54a0c4f4c7..8eb6f17b57 100644 --- a/testsuite/tests/typecheck/should_compile/all.T +++ b/testsuite/tests/typecheck/should_compile/all.T @@ -688,9 +688,10 @@ test('T16832', normal, ghci_script, ['T16832.script']) test('T16995', normal, compile, ['']) test('T17007', normal, compile, ['']) test('T17067', normal, compile, ['']) -test('T17202', expect_broken(17202), compile, ['']) +test('T17202', normal, compile, ['']) test('T15839a', normal, compile, ['']) test('T15839b', normal, compile, ['']) +test('T16502b', normal, compile, ['']) test('T17343', exit_code(1), compile_and_run, ['']) test('T17566', [extra_files(['T17566a.hs'])], makefile_test, []) test('T12760', unless(compiler_debugged(), skip), compile, ['-O']) diff --git a/testsuite/tests/typecheck/should_fail/T16502.hs b/testsuite/tests/typecheck/should_fail/T16502.hs new file mode 100644 index 0000000000..5fac062d85 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T16502.hs @@ -0,0 +1,31 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE InstanceSigs #-} +module T16502 where + +import Data.Kind + +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 :: Type -> Type + +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) + +-- This is rejected because we cannot derive (Show (D a)) from (C a) +-- due to troublesome quantified constraints. And then the error +-- message mentions the internal name of the default method for show. +-- Simon thinks that we should accept the fact that this doesn't get +-- accepted, given that a quantified constraint for (Show (c b)) is far +-- too applicable to be useful. So we're left with the suboptimal +-- error message. diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T index e2496562e1..31b1fb3333 100644 --- a/testsuite/tests/typecheck/should_fail/all.T +++ b/testsuite/tests/typecheck/should_fail/all.T @@ -551,6 +551,7 @@ test('T17355', normal, compile_fail, ['']) test('T17360', normal, compile_fail, ['']) test('T17563', normal, compile_fail, ['']) test('T16946', normal, compile_fail, ['']) +test('T16502', expect_broken(12854), compile, ['']) test('T17566b', normal, compile_fail, ['']) test('T17566c', normal, compile_fail, ['']) test('T17773', normal, compile_fail, ['']) |