diff options
Diffstat (limited to 'testsuite/tests/quantified-constraints')
27 files changed, 642 insertions, 0 deletions
diff --git a/testsuite/tests/quantified-constraints/Makefile b/testsuite/tests/quantified-constraints/Makefile new file mode 100644 index 0000000000..9a36a1c5fe --- /dev/null +++ b/testsuite/tests/quantified-constraints/Makefile @@ -0,0 +1,3 @@ +TOP=../.. +include $(TOP)/mk/boilerplate.mk +include $(TOP)/mk/test.mk diff --git a/testsuite/tests/quantified-constraints/T14833.hs b/testsuite/tests/quantified-constraints/T14833.hs new file mode 100644 index 0000000000..43b6491def --- /dev/null +++ b/testsuite/tests/quantified-constraints/T14833.hs @@ -0,0 +1,28 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE UndecidableInstances #-} +module T14833 where + +data Dict c where + Dict :: c => Dict c + +class (a => b) => Implies a b +instance (a => b) => Implies a b + +-- Works ok +iota1 :: (() => a) => Dict a +iota1 = Dict + +iota2 :: Implies () a => Dict a +iota2 = Dict + +{- +[G] Implies () a +[G] (() => a) -- By superclass + +[W] a +-} diff --git a/testsuite/tests/quantified-constraints/T14835.hs b/testsuite/tests/quantified-constraints/T14835.hs new file mode 100644 index 0000000000..de9b450b7c --- /dev/null +++ b/testsuite/tests/quantified-constraints/T14835.hs @@ -0,0 +1,20 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE UndecidableInstances #-} +module Bug where + +data Dict c where + Dict :: c => Dict c + +class (a => b) => Implies a b +instance (a => b) => Implies a b + +curryC1 :: ((a, b) => c) => Dict (Implies a (Implies b c)) +curryC1 = Dict + +curryC2 :: Implies (a, b) c => Dict (Implies a (Implies b c)) +curryC2 = Dict diff --git a/testsuite/tests/quantified-constraints/T14863.hs b/testsuite/tests/quantified-constraints/T14863.hs new file mode 100644 index 0000000000..35e1a14b42 --- /dev/null +++ b/testsuite/tests/quantified-constraints/T14863.hs @@ -0,0 +1,27 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE ImpredicativeTypes #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE UndecidableInstances #-} +module T14863 where + +data Dict c where + Dict :: c => Dict c + +class (a => b) => Implies a b +instance (a => b) => Implies a b + +uncurryCImpredic1 :: forall a b c. Implies a (b => c) => Dict (Implies (a, b) c) +uncurryCImpredic1 = Dict + +uncurryCImpredic2 :: forall a b c. a => Implies b c => Dict (Implies (a, b) c) +uncurryCImpredic2 = Dict + +uncurryC1 :: forall a b c. (a => b => c) => Dict (Implies (a, b) c) +uncurryC1 = Dict + +uncurryC2 :: forall a b c. Implies a (Implies b c) => Dict (Implies (a, b) c) +uncurryC2 = Dict diff --git a/testsuite/tests/quantified-constraints/T14961.hs b/testsuite/tests/quantified-constraints/T14961.hs new file mode 100644 index 0000000000..6f15ceb572 --- /dev/null +++ b/testsuite/tests/quantified-constraints/T14961.hs @@ -0,0 +1,98 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE InstanceSigs #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeFamilyDependencies #-} +{-# LANGUAGE TypeInType #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE QuantifiedConstraints #-} + +module T14961 where + +import Data.Kind + +import Control.Arrow (left, right, (&&&), (|||)) +import Control.Category +import Prelude hiding (id, (.)) + +import Data.Coerce + +class (forall x. f x => g x) => f ~=> g +instance (forall x. f x => g x) => f ~=> g + +type family (#) (p :: Type -> Type -> Type) (ab :: (Type, Type)) + = (r :: Type) | r -> p ab where + p # '(a, b) = p a b + +newtype Glass + :: ((Type -> Type -> Type) -> Constraint) + -> (Type, Type) -> (Type, Type) -> Type where + Glass :: (forall p. z p => p # ab -> p # st) -> Glass z st ab + +data A_Prism + +type family ConstraintOf (tag :: Type) + = (r :: (Type -> Type -> Type) -> Constraint) where + ConstraintOf A_Prism = Choice + +_Left0 + :: Glass Choice + '(Either a x, Either b x) + '(a, b) +_Left0 = Glass left' + +_Left1 + :: c ~=> Choice + => Glass c '(Either a x, Either b x) '(a, b) +_Left1 = Glass left' + +-- fails with +-- • Could not deduce (Choice p) +-- _Left2 +-- :: (forall p. c p => ConstraintOf A_Prism p) +-- => Glass c '(Either a x, Either b x) '(a, b) +-- _Left2 = Glass left' + +_Left3 + :: d ~ ConstraintOf A_Prism + => (forall p . c p => d p) + => Glass c + '(Either a x, Either b x) + '(a, b) +_Left3 = Glass left' + +-- fails to typecheck unless at least a partial type signature is provided +-- l :: c ~=> Choice => Glass c _ _ +-- l = _Left1 . _Left1 + +newtype Optic o st ab where + Optic + :: (forall c d. (d ~ ConstraintOf o, c ~=> d) => Glass c st ab) + -> Optic o st ab + +_Left + :: Optic A_Prism + '(Either a x, Either b x) + '(a, b) +_Left = Optic _Left1 + +instance Category (Glass z) where + id :: Glass z a a + id = Glass id + + (.) :: Glass z uv ab -> Glass z st uv -> Glass z st ab + Glass abuv . Glass uvst = Glass (uvst . abuv) + +class Profunctor (p :: Type -> Type -> Type) where + dimap :: (a -> b) -> (c -> d) -> p b c -> p a d + lmap :: (a -> b) -> p b c -> p a c + rmap :: (b -> c) -> p a b -> p a c + +class Profunctor p => Choice (p :: Type -> Type -> Type) where + left' :: p a b -> p (Either a c) (Either b c) + right' :: p a b -> p (Either c a) (Either c b) diff --git a/testsuite/tests/quantified-constraints/T15231.hs b/testsuite/tests/quantified-constraints/T15231.hs new file mode 100644 index 0000000000..7b7834d1f2 --- /dev/null +++ b/testsuite/tests/quantified-constraints/T15231.hs @@ -0,0 +1,15 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE QuantifiedConstraints #-} +module Bug where + +import Data.Kind + +data ECC :: Constraint -> Type -> Type + +class Y a +class Z a + +instance c => Y (ECC c a) +instance (c => Z a) => Z (ECC c a) diff --git a/testsuite/tests/quantified-constraints/T15231.stderr b/testsuite/tests/quantified-constraints/T15231.stderr new file mode 100644 index 0000000000..afb7ac3a25 --- /dev/null +++ b/testsuite/tests/quantified-constraints/T15231.stderr @@ -0,0 +1,7 @@ + +T15231.hs:15:10: error: + • Variable ‘c’ occurs more often + in the constraint ‘c’ than in the instance head ‘Z a’ + (Use UndecidableInstances to permit this) + • In the quantified constraint ‘c => Z a’ + In the instance declaration for ‘Z (ECC c a)’ diff --git a/testsuite/tests/quantified-constraints/T15244.hs b/testsuite/tests/quantified-constraints/T15244.hs new file mode 100644 index 0000000000..16d2b65d53 --- /dev/null +++ b/testsuite/tests/quantified-constraints/T15244.hs @@ -0,0 +1,69 @@ +{-# LANGUAGE QuantifiedConstraints, TypeFamilies #-} + +module T15244 where +class (forall t . Eq (c t)) => Blah c + +-- Unquantified works +foo :: (Eq (a t), Eq (b t), a ~ b) => a t -> b t -> Bool +foo a b = a == b +-- Works + +-- Two quantified instances fail with double ambiguity check errors +bar :: (forall t . Eq (a t), forall t . Eq (b t), a ~ b) => a t -> b t -> Bool +bar a b = a == b +-- Minimal.hs:11:8: error: +-- • Could not deduce (Eq (b t1)) +-- from the context: (forall t1. Eq (a t1), forall t1. Eq (b t1), +-- a ~ b) +-- bound by the type signature for: +-- bar :: forall (a :: * -> *) (b :: * -> *) t. +-- (forall t1. Eq (a t1), forall t1. Eq (b t1), a ~ b) => +-- a t -> b t -> Bool +-- at Minimal.hs:11:8-78 +-- • In the ambiguity check for ‘bar’ +-- To defer the ambiguity check to use sites, enable AllowAmbiguousTypes +-- In the type signature: +-- bar :: (forall t. Eq (a t), forall t. Eq (b t), a ~ b) => +-- a t -> b t -> Bool +-- | +-- 11 | bar :: (forall t . Eq (a t), forall t . Eq (b t), a ~ b) => a t -> b t -> Bool +-- | +-- [And then another copy of the same error] + +-- Two copies from superclass instances fail +baz :: (Blah a, Blah b, a ~ b) => a t -> b t -> Bool +baz a b = a == b +-- Minimal.hs:34:11: error: +-- • Could not deduce (Eq (b t)) arising from a use of ‘==’ +-- from the context: (Blah a, Blah b, a ~ b) +-- bound by the type signature for: +-- baz :: forall (a :: * -> *) (b :: * -> *) t. +-- (Blah a, Blah b, a ~ b) => +-- a t -> b t -> Bool +-- at Minimal.hs:33:1-52 +-- • In the expression: a == b +-- In an equation for ‘baz’: baz a b = a == b +-- | +-- 34 | baz a b = a == b +-- | + +-- Two copies from superclass from same declaration also fail +mugga :: (Blah a, Blah a) => a t -> a t -> Bool +mugga a b = a == b +-- • Could not deduce (Eq (a t)) arising from a use of ‘==’ +-- from the context: (Blah a, Blah a) +-- bound by the type signature for: +-- mugga :: forall (a :: * -> *) t. +-- (Blah a, Blah a) => +-- a t -> a t -> Bool +-- at Minimal.hs:50:1-47 +-- • In the expression: a == b +-- In an equation for ‘mugga’: mugga a b = a == b +-- | +-- 51 | mugga a b = a == b +-- | + +-- One copy works +quux :: (Blah a, a ~ b) => a t -> b t -> Bool +quux a b = a == b +-- Works diff --git a/testsuite/tests/quantified-constraints/T15290.hs b/testsuite/tests/quantified-constraints/T15290.hs new file mode 100644 index 0000000000..8a0c3d989f --- /dev/null +++ b/testsuite/tests/quantified-constraints/T15290.hs @@ -0,0 +1,35 @@ +{-# LANGUAGE TypeApplications, ImpredicativeTypes, ScopedTypeVariables, + QuantifiedConstraints, StandaloneDeriving, GeneralizedNewtypeDeriving #-} + +module T15290 where + +import Prelude hiding ( Monad(..) ) +import Data.Coerce ( Coercible, coerce ) + +class Monad m where + join :: m (m a) -> m a + +newtype StateT s m a = StateT { runStateT :: s -> m (s, a) } + +newtype IntStateT m a = IntStateT { runIntStateT :: StateT Int m a } + +instance Monad m => Monad (StateT s m) where + join = error "urk" + +instance (Monad m, forall p q. Coercible p q => Coercible (m p) (m q)) + => Monad (IntStateT m) where + +-- Fails with the impredicative instantiation of coerce, succeeds without + +-- Impredicative version (fails) +-- join = coerce +-- @(forall a. StateT Int m (StateT Int m a) -> StateT Int m a) +-- @(forall a. IntStateT m (IntStateT m a) -> IntStateT m a) +-- join + + +-- Predicative version (succeeds) + join = (coerce + @(StateT Int m (StateT Int m a) -> StateT Int m a) + @(IntStateT m (IntStateT m a) -> IntStateT m a) + join) :: forall a. IntStateT m (IntStateT m a) -> IntStateT m a diff --git a/testsuite/tests/quantified-constraints/T15290a.hs b/testsuite/tests/quantified-constraints/T15290a.hs new file mode 100644 index 0000000000..bfb5b2a069 --- /dev/null +++ b/testsuite/tests/quantified-constraints/T15290a.hs @@ -0,0 +1,35 @@ +{-# LANGUAGE TypeApplications, ImpredicativeTypes, ScopedTypeVariables, + QuantifiedConstraints, StandaloneDeriving, GeneralizedNewtypeDeriving #-} + +module T15290a where + +import Prelude hiding ( Monad(..) ) +import Data.Coerce ( Coercible, coerce ) + +class Monad m where + join :: m (m a) -> m a + +newtype StateT s m a = StateT { runStateT :: s -> m (s, a) } + +newtype IntStateT m a = IntStateT { runIntStateT :: StateT Int m a } + +instance Monad m => Monad (StateT s m) where + join = error "urk" + +instance (Monad m, forall p q. Coercible p q => Coercible (m p) (m q)) + => Monad (IntStateT m) where + +-- Fails with the impredicative instantiation of coerce, succeeds without + +-- Impredicative version (fails) + join = coerce + @(forall a. StateT Int m (StateT Int m a) -> StateT Int m a) + @(forall a. IntStateT m (IntStateT m a) -> IntStateT m a) + join + + +-- Predicative version (succeeds) +-- join = (coerce +-- @(StateT Int m (StateT Int m a) -> StateT Int m a) +-- @(IntStateT m (IntStateT m a) -> IntStateT m a) +-- join) :: forall a. IntStateT m (IntStateT m a) -> IntStateT m a diff --git a/testsuite/tests/quantified-constraints/T15290a.stderr b/testsuite/tests/quantified-constraints/T15290a.stderr new file mode 100644 index 0000000000..2efd784f31 --- /dev/null +++ b/testsuite/tests/quantified-constraints/T15290a.stderr @@ -0,0 +1,22 @@ + +T15290a.hs:25:12: error: + • Couldn't match representation of type ‘m (Int, IntStateT m a1)’ + with that of ‘m (Int, StateT Int m a1)’ + arising from a use of ‘coerce’ + NB: We cannot know what roles the parameters to ‘m’ have; + we must assume that the role is nominal + • In the expression: + coerce + @(forall a. StateT Int m (StateT Int m a) -> StateT Int m a) + @(forall a. IntStateT m (IntStateT m a) -> IntStateT m a) + join + In an equation for ‘join’: + join + = coerce + @(forall a. StateT Int m (StateT Int m a) -> StateT Int m a) + @(forall a. IntStateT m (IntStateT m a) -> IntStateT m a) + join + In the instance declaration for ‘Monad (IntStateT m)’ + • Relevant bindings include + join :: IntStateT m (IntStateT m a) -> IntStateT m a + (bound at T15290a.hs:25:5) diff --git a/testsuite/tests/quantified-constraints/T15290b.hs b/testsuite/tests/quantified-constraints/T15290b.hs new file mode 100644 index 0000000000..ce99aa9454 --- /dev/null +++ b/testsuite/tests/quantified-constraints/T15290b.hs @@ -0,0 +1,28 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE ImpredicativeTypes #-} +{-# LANGUAGE InstanceSigs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +module T15290b where + +import Data.Coerce +import Data.Kind + +type Representational1 m = (forall a b. Coercible a b => Coercible (m a) (m b) :: Constraint) + +class Representational1 f => Functor' f where + fmap' :: (a -> b) -> f a -> f b + +class Functor' f => Applicative' f where + pure' :: a -> f a + (<*>@) :: f (a -> b) -> f a -> f b + +class Functor' t => Traversable' t where + traverse' :: Applicative' f => (a -> f b) -> t a -> f (t b) + +-- Typechecks +newtype T1 m a = MkT1 (m a) deriving (Functor', Traversable') diff --git a/testsuite/tests/quantified-constraints/T15290b.stderr b/testsuite/tests/quantified-constraints/T15290b.stderr new file mode 100644 index 0000000000..7dc1852c6d --- /dev/null +++ b/testsuite/tests/quantified-constraints/T15290b.stderr @@ -0,0 +1,14 @@ + +T15290b.hs:28:49: error: + • Couldn't match representation of type ‘f (m b)’ + with that of ‘f (T1 m b)’ + arising from the coercion of the method ‘traverse'’ + from type ‘forall (f :: * -> *) a b. + Applicative' f => + (a -> f b) -> m a -> f (m b)’ + to type ‘forall (f :: * -> *) a b. + Applicative' f => + (a -> f b) -> T1 m a -> f (T1 m b)’ + NB: We cannot know what roles the parameters to ‘f’ have; + we must assume that the role is nominal + • When deriving the instance for (Traversable' (T1 m)) diff --git a/testsuite/tests/quantified-constraints/T15316.hs b/testsuite/tests/quantified-constraints/T15316.hs new file mode 100644 index 0000000000..07539e3183 --- /dev/null +++ b/testsuite/tests/quantified-constraints/T15316.hs @@ -0,0 +1,21 @@ +{-# LANGUAGE RankNTypes, QuantifiedConstraints, ConstraintKinds #-} +-- NB: disabling these if enabled: +{-# LANGUAGE NoUndecidableInstances, NoUndecidableSuperClasses #-} + +module T15316 where + +import Data.Proxy + +{- +class Class a where + method :: a + +subsume :: (Class a => Class b) => Proxy a -> Proxy b -> ((Class a => Class b) => r) -> r +subsume _ _ x = x + +value :: Proxy a -> a +value p = subsume p p method +-} + +subsume' :: Proxy c -> ((c => c) => r) -> r +subsume' _ x = x diff --git a/testsuite/tests/quantified-constraints/T15316.stderr b/testsuite/tests/quantified-constraints/T15316.stderr new file mode 100644 index 0000000000..4444c2c453 --- /dev/null +++ b/testsuite/tests/quantified-constraints/T15316.stderr @@ -0,0 +1,6 @@ + +T15316.hs:20:13: error: + • The constraint ‘c’ is no smaller than the instance head ‘c’ + (Use UndecidableInstances to permit this) + • In the quantified constraint ‘c => c’ + In the type signature: subsume' :: Proxy c -> ((c => c) => r) -> r diff --git a/testsuite/tests/quantified-constraints/T15334.hs b/testsuite/tests/quantified-constraints/T15334.hs new file mode 100644 index 0000000000..88d7c3f376 --- /dev/null +++ b/testsuite/tests/quantified-constraints/T15334.hs @@ -0,0 +1,9 @@ +{-# LANGUAGE MultiParamTypeClasses, PolyKinds, QuantifiedConstraints, RankNTypes #-} + +module T15334 where + +class C m a +class D m a + +f :: (forall a. Eq a => (C m a, D m a)) => m a +f = undefined diff --git a/testsuite/tests/quantified-constraints/T15334.stderr b/testsuite/tests/quantified-constraints/T15334.stderr new file mode 100644 index 0000000000..902d7a71e5 --- /dev/null +++ b/testsuite/tests/quantified-constraints/T15334.stderr @@ -0,0 +1,6 @@ + +T15334.hs:8:6: error: + • You can't specify an instance for a tuple constraint + • In the quantified constraint ‘forall a. Eq a => (C m a, D m a)’ + In the type signature: + f :: (forall a. Eq a => (C m a, D m a)) => m a diff --git a/testsuite/tests/quantified-constraints/T15359.hs b/testsuite/tests/quantified-constraints/T15359.hs new file mode 100644 index 0000000000..7ef1cc5572 --- /dev/null +++ b/testsuite/tests/quantified-constraints/T15359.hs @@ -0,0 +1,12 @@ +{-# LANGUAGE MultiParamTypeClasses, GADTs, RankNTypes, + ConstraintKinds, QuantifiedConstraints #-} + +module T15359 where + +class C a b + +data Dict c where + Dict :: c => Dict c + +foo :: (forall a b. C a b => a ~ b) => Dict (C a b) -> a -> b +foo Dict x = x diff --git a/testsuite/tests/quantified-constraints/T15359a.hs b/testsuite/tests/quantified-constraints/T15359a.hs new file mode 100644 index 0000000000..6ec5f861a8 --- /dev/null +++ b/testsuite/tests/quantified-constraints/T15359a.hs @@ -0,0 +1,14 @@ +{-# LANGUAGE MultiParamTypeClasses, GADTs, RankNTypes, + ConstraintKinds, QuantifiedConstraints, + UndecidableInstances #-} + +module T15359a where + +class C a b +class a ~ b => D a b + +data Dict c where + Dict :: c => Dict c + +foo :: (forall a b. C a b => D a b) => Dict (C a b) -> a -> b +foo Dict x = x diff --git a/testsuite/tests/quantified-constraints/T15625.hs b/testsuite/tests/quantified-constraints/T15625.hs new file mode 100644 index 0000000000..8fe092da98 --- /dev/null +++ b/testsuite/tests/quantified-constraints/T15625.hs @@ -0,0 +1,16 @@ +{-# Language GADTs, MultiParamTypeClasses, QuantifiedConstraints #-} + +module T15625 where + +import Data.Coerce + +class a ~ b => Equal a b + +test1 :: (forall b. a ~ b) => a +test1 = False + +test2 :: (forall b. Equal a b) => a +test2 = False + +test3 :: (forall b. Coercible a b) => a +test3 = coerce False diff --git a/testsuite/tests/quantified-constraints/T15625a.hs b/testsuite/tests/quantified-constraints/T15625a.hs new file mode 100644 index 0000000000..ca049cb19d --- /dev/null +++ b/testsuite/tests/quantified-constraints/T15625a.hs @@ -0,0 +1,20 @@ +{-# Language RankNTypes, ConstraintKinds, QuantifiedConstraints, + PolyKinds, GADTs, MultiParamTypeClasses, + DataKinds, FlexibleInstances #-} + +module T15625a where + +import Data.Kind + +type Cat ob = ob -> ob -> Type + +data KLEISLI (m :: Type -> Type) :: Cat (KL_kind m) where + MkKLEISLI :: (a -> m b) -> KLEISLI(m) (KL a) (KL b) + +data KL_kind (m :: Type -> Type) = KL Type + +class (a ~ KL xx) => AsKL a xx +instance (a ~ KL xx) => AsKL a xx + +ekki__ :: Monad m => (forall xx. AsKL a xx) => KLEISLI m a a +ekki__ = MkKLEISLI undefined diff --git a/testsuite/tests/quantified-constraints/T2893.hs b/testsuite/tests/quantified-constraints/T2893.hs new file mode 100644 index 0000000000..ffec2cf72d --- /dev/null +++ b/testsuite/tests/quantified-constraints/T2893.hs @@ -0,0 +1,18 @@ +{-# LANGUAGE QuantifiedConstraints #-} + +-- Two simple examples that should work + +module T2893 where + +f :: forall b c. (Eq b, forall a. Eq a => Eq (c a)) => c b -> Bool +{-# NOINLINE f #-} +f x = x==x + +g x = f [x] + +data Rose f x = Rose x (f (Rose f x)) + +instance (Eq a, forall b. Eq b => Eq (f b)) + => Eq (Rose f a) where + (Rose x1 rs1) == (Rose x2 rs2) + = x1==x2 && rs1 == rs2 diff --git a/testsuite/tests/quantified-constraints/T2893a.hs b/testsuite/tests/quantified-constraints/T2893a.hs new file mode 100644 index 0000000000..187029fdd5 --- /dev/null +++ b/testsuite/tests/quantified-constraints/T2893a.hs @@ -0,0 +1,27 @@ +{-# LANGUAGE + GADTs + , FlexibleContexts + , RankNTypes + , ScopedTypeVariables + , QuantifiedConstraints #-} + +module T2893a where + +import Control.Monad.ST +import Data.Array.ST + +sortM + :: forall a s. + (Ord a, MArray (STUArray s) a (ST s)) + => [a] + -> ST s [a] +sortM xs = do + arr <- newListArray (1, length xs) xs + :: ST s (STUArray s Int a) + -- do some in-place sorting here + getElems arr + +sortP_3 + :: (Ord a, forall s. MArray (STUArray s) a (ST s)) + => [a] -> [a] +sortP_3 xs = runST (sortM xs) diff --git a/testsuite/tests/quantified-constraints/T2893c.hs b/testsuite/tests/quantified-constraints/T2893c.hs new file mode 100644 index 0000000000..832d0f8428 --- /dev/null +++ b/testsuite/tests/quantified-constraints/T2893c.hs @@ -0,0 +1,15 @@ +{-# LANGUAGE QuantifiedConstraints #-} + +module T2893c where + +data Rose f x = Rose x (f (Rose f x)) + +instance Eq a => Eq (Rose f a) where + (Rose x1 _) == (Rose x2 _) = x1==x2 + +-- Needs superclasses +instance (Ord a, forall b. Ord b => Ord (f b)) + => Ord (Rose f a) where + (Rose x1 rs1) >= (Rose x2 rs2) + = x1 >= x2 && rs1 == rs2 + a <= b = False -- Just to suppress the warning diff --git a/testsuite/tests/quantified-constraints/T9123.hs b/testsuite/tests/quantified-constraints/T9123.hs new file mode 100644 index 0000000000..130312b150 --- /dev/null +++ b/testsuite/tests/quantified-constraints/T9123.hs @@ -0,0 +1,25 @@ +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE InstanceSigs, RoleAnnotations #-} + +module T9123 where + +import Data.Coerce + +type role Wrap representational nominal +newtype Wrap m a = Wrap (m a) + +class Monad' m where + join' :: forall a. m (m a) -> m a + +-- Tests the superclass stuff +instance (forall p q. Coercible p q => Coercible (m p) (m q), Monad' m) => Monad' (Wrap m) where + join' :: forall a. Wrap m (Wrap m a) -> Wrap m a + join' = coerce @(m (m a) -> m a) + @(Wrap m (Wrap m a) -> Wrap m a) + join' + diff --git a/testsuite/tests/quantified-constraints/T9123a.hs b/testsuite/tests/quantified-constraints/T9123a.hs new file mode 100644 index 0000000000..76379b6c00 --- /dev/null +++ b/testsuite/tests/quantified-constraints/T9123a.hs @@ -0,0 +1,30 @@ +{-# LANGUAGE QuantifiedConstraints, PolyKinds, ScopedTypeVariables + , StandaloneDeriving, RoleAnnotations, TypeApplications + , UndecidableInstances, InstanceSigs + , GeneralizedNewtypeDeriving #-} + +module T9123a where + +import Data.Coerce + +class MyMonad m where + join :: m (m a) -> m a + +newtype StateT s m a = StateT (s -> m (a, s)) + +type role StateT nominal representational nominal -- as inferred + +instance MyMonad m => MyMonad (StateT s m) where + join = error "urk" -- A good impl exists, but is not + -- of interest for this test case + +newtype IntStateT m a = IntStateT (StateT Int m a) + +type role IntStateT representational nominal -- as inferred + +instance (MyMonad m, forall p q. Coercible p q => Coercible (m p) (m q)) + => MyMonad (IntStateT m) where + join :: forall a. IntStateT m (IntStateT m a) -> IntStateT m a + join = coerce @(StateT Int m (StateT Int m a) -> StateT Int m a) + @(IntStateT m (IntStateT m a) -> IntStateT m a) + join diff --git a/testsuite/tests/quantified-constraints/all.T b/testsuite/tests/quantified-constraints/all.T new file mode 100644 index 0000000000..1e2eca8358 --- /dev/null +++ b/testsuite/tests/quantified-constraints/all.T @@ -0,0 +1,22 @@ + +test('T14833', normal, compile, ['']) +test('T14835', normal, compile, ['']) +test('T2893', normal, compile, ['']) +test('T2893a', normal, compile, ['']) +test('T2893c', normal, compile, ['']) +test('T9123', normal, compile, ['']) +test('T14863', normal, compile, ['']) +test('T14961', normal, compile, ['']) +test('T9123a', normal, compile, ['']) +test('T15244', normal, compile, ['']) +test('T15231', normal, compile_fail, ['']) + +test('T15290', normal, compile, ['']) +test('T15290a', normal, compile_fail, ['']) +test('T15290b', normal, compile_fail, ['']) +test('T15316', normal, compile_fail, ['']) +test('T15334', normal, compile_fail, ['']) +test('T15359', normal, compile, ['']) +test('T15359a', normal, compile, ['']) +test('T15625', normal, compile, ['']) +test('T15625a', normal, compile, ['']) |