Test cases for #15772 and #17139.wip/T15772

6 files changed, 125 insertions, 0 deletions

diff --git a/testsuite/tests/typecheck/should_compile/T15772.hs b/testsuite/tests/typecheck/should_compile/T15772.hs
new file mode 100644
index 0000000000..5a81558bad
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T15772.hs
@@ -0,0 +1,29 @@
+{-# LANGUAGE DataKinds, TypeFamilies, TypeOperators, UndecidableInstances #-}
+module T15772 where
+
+import Data.Kind
+
+data NP (f :: Type -> Type) (xs :: [Type])
+
+type family Curry (f :: Type -> Type) (xs :: [Type]) (r :: Type) (a :: Type) :: Constraint where
+  Curry f xs r (f x -> a) = (xs ~ (x : Tail xs), Curry f (Tail xs) r a)
+  Curry f xs r a          = (xs ~ '[], r ~ a)
+
+type family Tail (a :: [Type]) :: [Type] where
+  Tail (_ : xs) = xs
+
+uncurry_NP :: (Curry f xs r a) => (NP f xs -> r) -> a
+uncurry_NP = undefined
+
+fun_NP :: NP Id xs -> ()
+fun_NP = undefined
+
+newtype Id a = MkId a
+
+-- Bizarrely: uncommenting this allows the program to type-check in GHC 8.8
+-- It should type-check without it.
+-- test1 :: ()
+-- test1 = uncurry_NP fun_NP (MkId 5)
+
+test2 :: ()
+test2 = uncurry_NP fun_NP (MkId True) (MkId 5) (MkId True)
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 3fc36839d8..ad3cebca86 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -690,6 +690,7 @@ test('UnlifNewUnify', normal, compile, [''])
 test('UnliftedNewtypesLPFamily', normal, compile, [''])
 test('UnliftedNewtypesDifficultUnification', normal, compile, [''])
 test('T16832', normal, ghci_script, ['T16832.script'])
+test('T15772', normal, compile, [''])
 test('T16995', normal, compile, [''])
 test('T17007', normal, compile, [''])
 test('T17067', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/T17139.hs b/testsuite/tests/typecheck/should_fail/T17139.hs
new file mode 100644
index 0000000000..b4025588dd
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T17139.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+
+module T17139 where
+
+import T17139a
+
+type family TypeFam f fun where
+  TypeFam f (a -> b) = f a -> TypeFam f b
+
+lift :: (a -> b) -> TypeFam f (a -> b)
+lift f = \x -> _ (f <*> x)
diff --git a/testsuite/tests/typecheck/should_fail/T17139.stderr b/testsuite/tests/typecheck/should_fail/T17139.stderr
new file mode 100644
index 0000000000..7da4635a61
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T17139.stderr
@@ -0,0 +1,49 @@
+
+T17139.hs:15:10: error:
+    • Couldn't match type ‘f’ with ‘(->) a’
+      Expected: TypeFam f (a -> b)
+        Actual: (a -> a) -> f a -> TypeFam f b0
+      ‘f’ is a rigid type variable bound by
+        the type signature for:
+          lift :: forall a b (f :: * -> *). (a -> b) -> TypeFam f (a -> b)
+        at T17139.hs:14:1-38
+    • The lambda expression ‘\ x -> _ (f <*> x)’
+      has one value argument,
+        but its type ‘TypeFam f (a -> b)’ has none
+      In the expression: \ x -> _ (f <*> x)
+      In an equation for ‘lift’: lift f = \ x -> _ (f <*> x)
+    • Relevant bindings include
+        f :: a -> b (bound at T17139.hs:15:6)
+        lift :: (a -> b) -> TypeFam f (a -> b) (bound at T17139.hs:15:1)
+
+T17139.hs:15:16: error:
+    • Found hole: _ :: (a -> b0) -> f a -> TypeFam f b0
+      Where: ‘b0’ is an ambiguous type variable
+             ‘a’, ‘f’ are rigid type variables bound by
+               the type signature for:
+                 lift :: forall a b (f :: * -> *). (a -> b) -> TypeFam f (a -> b)
+               at T17139.hs:14:1-38
+    • In the expression: _ (f <*> x)
+      The lambda expression ‘\ x -> _ (f <*> x)’ has one value argument,
+        but its type ‘TypeFam f (a -> b)’ has none
+      In the expression: \ x -> _ (f <*> x)
+    • Relevant bindings include
+        x :: a -> a (bound at T17139.hs:15:11)
+        f :: a -> b (bound at T17139.hs:15:6)
+        lift :: (a -> b) -> TypeFam f (a -> b) (bound at T17139.hs:15:1)
+
+T17139.hs:15:19: error:
+    • Couldn't match type ‘b’ with ‘a -> b0’
+      Expected: a -> a -> b0
+        Actual: a -> b
+      ‘b’ is a rigid type variable bound by
+        the type signature for:
+          lift :: forall a b (f :: * -> *). (a -> b) -> TypeFam f (a -> b)
+        at T17139.hs:14:1-38
+    • In the first argument of ‘(<*>)’, namely ‘f’
+      In the first argument of ‘_’, namely ‘(f <*> x)’
+      In the expression: _ (f <*> x)
+    • Relevant bindings include
+        x :: a -> a (bound at T17139.hs:15:11)
+        f :: a -> b (bound at T17139.hs:15:6)
+        lift :: (a -> b) -> TypeFam f (a -> b) (bound at T17139.hs:15:1)
diff --git a/testsuite/tests/typecheck/should_fail/T17139a.hs b/testsuite/tests/typecheck/should_fail/T17139a.hs
new file mode 100644
index 0000000000..4a025a801c
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T17139a.hs
@@ -0,0 +1,30 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilyDependencies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+-- A stripped-down version of singletons
+module T17139a where
+
+import Data.Kind (Type)
+import Data.Proxy (Proxy)
+
+data family Sing :: k -> Type
+class SingI a where
+  sing :: Sing a
+class SingKind k where
+  type Demote k = (r :: Type) | r -> k
+  toSing   :: Demote k -> Proxy k
+data TyFun :: Type -> Type -> Type
+type a ~> b = TyFun a b -> Type
+infixr 0 ~>
+type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
+newtype instance Sing (f :: k1 ~> k2) =
+  SLambda { applySing :: forall t. Sing t -> Sing (Apply f t) }
+instance (SingKind k1, SingKind k2) => SingKind (k1 ~> k2) where
+  type Demote (k1 ~> k2) = Demote k1 -> Demote k2
+  toSing = undefined
+withSing :: SingI a => (Sing a -> b) -> b
+withSing f = f sing
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index c55425ae3a..62d6e3b2ae 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -594,6 +594,7 @@ test('T10709b', normal, compile_fail, [''])
 test('GivenForallLoop', normal, compile_fail, [''])
 test('T18891a', normal, compile_fail, [''])
 test('T19109', normal, compile_fail, [''])
+test('T17139', [extra_files(['T17139a.hs'])], multimod_compile_fail, ['T17139', '-v0'])
 test('TyAppPat_ExistentialEscape', normal, compile_fail, [''])
 test('TyAppPat_MisplacedApplication', normal, compile_fail, [''])
 test('TyAppPat_NonlinearMultiAppPat', normal, compile_fail, [''])