[commit: ghc] wip/T2893: Add regression test for Trac #14961 (3c66034)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : wip/T2893
Link       : http://ghc.haskell.org/trac/ghc/changeset/3c660341647cb78db461cf80a34880d84b00092f/ghc

>---------------------------------------------------------------

commit 3c660341647cb78db461cf80a34880d84b00092f
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Thu Mar 22 14:37:35 2018 +0000

    Add regression test for Trac #14961
    
    More precisely, for the code in comment:3


>---------------------------------------------------------------

3c660341647cb78db461cf80a34880d84b00092f
 testsuite/tests/quantified-constraints/T14961.hs | 98 ++++++++++++++++++++++++
 testsuite/tests/quantified-constraints/T9123a.hs |  2 +-
 testsuite/tests/quantified-constraints/all.T     |  1 +
 3 files changed, 100 insertions(+), 1 deletion(-)

diff --git a/testsuite/tests/quantified-constraints/T14961.hs b/testsuite/tests/quantified-constraints/T14961.hs
new file mode 100644
index 0000000..6f15ceb
--- /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/T9123a.hs b/testsuite/tests/quantified-constraints/T9123a.hs
index 4e84479..53f09b9 100644
--- a/testsuite/tests/quantified-constraints/T9123a.hs
+++ b/testsuite/tests/quantified-constraints/T9123a.hs
@@ -3,7 +3,7 @@
            , UndecidableInstances
            , GeneralizedNewtypeDeriving #-}
 
-module T9123 where
+module T9123a where
 
 import Data.Coerce
 
diff --git a/testsuite/tests/quantified-constraints/all.T b/testsuite/tests/quantified-constraints/all.T
index 4f63911..fe1f091 100644
--- a/testsuite/tests/quantified-constraints/all.T
+++ b/testsuite/tests/quantified-constraints/all.T
@@ -6,6 +6,7 @@ test('T2893a', normal, compile, [''])
 test('T2893c', normal, compile, [''])
 test('T9123', normal, compile, [''])
 test('T14863', normal, compile, [''])
+test('T14961', normal, compile, [''])
 
 # Not yet
 # test('T9123a', normal, compile, [''])