diff options
Diffstat (limited to 'testsuite/tests')
24 files changed, 173 insertions, 74 deletions
diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T index 823244ebca..6cc9f12bca 100644 --- a/testsuite/tests/dependent/should_compile/all.T +++ b/testsuite/tests/dependent/should_compile/all.T @@ -54,13 +54,9 @@ test('T15419', normal, compile, ['']) test('T14066h', normal, compile, ['']) test('T15666', normal, compile, ['']) test('T15725', normal, compile, ['']) -test('T14880', normal, compile, ['']) -test('T14880-2', normal, compile, ['']) test('T15743', normal, compile, ['-ddump-types -fprint-explicit-foralls']) test('InferDependency', normal, compile, ['']) test('T15743e', normal, compile, ['-ddump-types -fprint-explicit-foralls']) -test('T15076', normal, compile, ['']) -test('T15076b', normal, compile, ['']) test('T15076c', normal, compile, ['']) test('T15829', normal, compile, ['']) test('T14729', normal, compile, ['-ddump-types -fprint-typechecker-elaboration -fprint-explicit-coercions']) diff --git a/testsuite/tests/dependent/should_compile/T14880-2.hs b/testsuite/tests/dependent/should_fail/T14880-2.hs index e7057a3f00..e7057a3f00 100644 --- a/testsuite/tests/dependent/should_compile/T14880-2.hs +++ b/testsuite/tests/dependent/should_fail/T14880-2.hs diff --git a/testsuite/tests/dependent/should_fail/T14880-2.stderr b/testsuite/tests/dependent/should_fail/T14880-2.stderr new file mode 100644 index 0000000000..2082ca6c34 --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T14880-2.stderr @@ -0,0 +1,8 @@ + +T14880-2.hs:12:9: error: + • Cannot generalise type; skolem ‘arg’ would escape its scope + if I tried to quantify (a0 :: arg) in this type: + forall arg. Proxy @{Proxy @{arg} a0 -> *} (Foo arg @a0) -> () + (Indeed, I sometimes struggle even printing this correctly, + due to its ill-scoped nature.) + • In the type signature: quux :: forall arg. Proxy (Foo arg) -> () diff --git a/testsuite/tests/dependent/should_compile/T14880.hs b/testsuite/tests/dependent/should_fail/T14880.hs index 91cfb20a4a..91cfb20a4a 100644 --- a/testsuite/tests/dependent/should_compile/T14880.hs +++ b/testsuite/tests/dependent/should_fail/T14880.hs diff --git a/testsuite/tests/dependent/should_fail/T14880.stderr b/testsuite/tests/dependent/should_fail/T14880.stderr new file mode 100644 index 0000000000..a5aa1df8d2 --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T14880.stderr @@ -0,0 +1,12 @@ + +T14880.hs:12:5: error: + • Cannot generalise type; skolem ‘arg’ would escape its scope + if I tried to quantify (a0 :: arg) in this type: + forall x arg. + ((Foo arg @a0 :: (Proxy @{arg} a0 -> *)) + ~ (Foo arg @a0 :: (Proxy @{arg} a0 -> *))) => + Bar x + (Indeed, I sometimes struggle even printing this correctly, + due to its ill-scoped nature.) + • In the definition of data constructor ‘MkBar’ + In the data declaration for ‘Bar’ diff --git a/testsuite/tests/dependent/should_compile/T15076.hs b/testsuite/tests/dependent/should_fail/T15076.hs index 0890cf9eab..0890cf9eab 100644 --- a/testsuite/tests/dependent/should_compile/T15076.hs +++ b/testsuite/tests/dependent/should_fail/T15076.hs diff --git a/testsuite/tests/dependent/should_fail/T15076.stderr b/testsuite/tests/dependent/should_fail/T15076.stderr new file mode 100644 index 0000000000..814d459c3c --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T15076.stderr @@ -0,0 +1,11 @@ + +T15076.hs:10:8: error: + • Cannot generalise type; skolem ‘a’ would escape its scope + if I tried to quantify (x0 :: a) in this type: + forall a (f :: forall (x :: a). Proxy @{a} x -> *). + Proxy @{Proxy @{a} x0 -> *} (f @x0) -> () + (Indeed, I sometimes struggle even printing this correctly, + due to its ill-scoped nature.) + • In the type signature: + foo :: forall (a :: Type) (f :: forall (x :: a). Proxy x -> Type). + Proxy f -> () diff --git a/testsuite/tests/dependent/should_compile/T15076b.hs b/testsuite/tests/dependent/should_fail/T15076b.hs index 15fce826c0..15fce826c0 100644 --- a/testsuite/tests/dependent/should_compile/T15076b.hs +++ b/testsuite/tests/dependent/should_fail/T15076b.hs diff --git a/testsuite/tests/dependent/should_fail/T15076b.stderr b/testsuite/tests/dependent/should_fail/T15076b.stderr new file mode 100644 index 0000000000..3ee27a82b3 --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T15076b.stderr @@ -0,0 +1,11 @@ + +T15076b.hs:8:8: error: + • Cannot generalise type; skolem ‘a’ would escape its scope + if I tried to quantify (x0 :: a) in this type: + forall a (f :: forall (x :: a). Proxy @{a} x -> *). + Proxy @{Proxy @{a} x0 -> *} (f @x0) -> () + (Indeed, I sometimes struggle even printing this correctly, + due to its ill-scoped nature.) + • In the type signature: + foo :: forall (a :: Type) (f :: forall (x :: a). Proxy x -> Type). + Proxy f -> () diff --git a/testsuite/tests/dependent/should_fail/T15825.stderr b/testsuite/tests/dependent/should_fail/T15825.stderr index 97582ba952..5d989303a6 100644 --- a/testsuite/tests/dependent/should_fail/T15825.stderr +++ b/testsuite/tests/dependent/should_fail/T15825.stderr @@ -1,6 +1,8 @@ -T15825.hs:14:31: error: - • Illegal type synonym family application ‘GHC.Types.Any - @k’ in instance: - X (a @(GHC.Types.Any @k)) +T15825.hs:14:10: error: + • Cannot generalise type; skolem ‘k’ would escape its scope + if I tried to quantify (x0 :: k) in this type: + forall k (a :: C k). X (a @x0) + (Indeed, I sometimes struggle even printing this correctly, + due to its ill-scoped nature.) • In the instance declaration for ‘X (a :: *)’ diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T index 8ff5a88961..dde686af7a 100644 --- a/testsuite/tests/dependent/should_fail/all.T +++ b/testsuite/tests/dependent/should_fail/all.T @@ -60,3 +60,7 @@ test('T16418', normal, compile_fail, ['']) test('T17541', normal, compile_fail, ['']) test('T17541b', normal, compile_fail, ['']) test('T17131', normal, compile_fail, ['']) +test('T14880', normal, compile_fail, ['']) +test('T14880-2', normal, compile_fail, ['']) +test('T15076', normal, compile_fail, ['']) +test('T15076b', normal, compile_fail, ['']) diff --git a/testsuite/tests/partial-sigs/should_fail/T14040a.stderr b/testsuite/tests/partial-sigs/should_fail/T14040a.stderr index d03d0dc32b..1d122cf590 100644 --- a/testsuite/tests/partial-sigs/should_fail/T14040a.stderr +++ b/testsuite/tests/partial-sigs/should_fail/T14040a.stderr @@ -1,34 +1,25 @@ -T14040a.hs:34:8: error: - • Cannot apply expression of type ‘Sing wl - -> (forall y. p _0 'WeirdNil) - -> (forall z (x :: z) (xs :: WeirdList (WeirdList z)). - Sing x - -> Sing xs - -> p GHC.Types.Any xs - -> p GHC.Types.Any ('WeirdCons x xs)) - -> p _1 wl’ - to a visible type argument ‘(WeirdList z)’ - • In the sixth argument of ‘pWeirdCons’, namely - ‘(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)’ - In the expression: - pWeirdCons - @z - @x - @xs - x - xs - (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons) - In an equation for ‘elimWeirdList’: - elimWeirdList - (SWeirdCons (x :: Sing (x :: z)) - (xs :: Sing (xs :: WeirdList (WeirdList z)))) - pWeirdNil - pWeirdCons - = pWeirdCons - @z - @x - @xs - x - xs - (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons) +T14040a.hs:21:18: error: + • Cannot generalise type; skolem ‘z’ would escape its scope + if I tried to quantify (_1 :: WeirdList z) in this type: + forall a1 (wl :: WeirdList a1) + (p :: forall x. x -> WeirdList x -> *). + Sing @(WeirdList a1) wl + -> (forall y. p @x0 _0 ('WeirdNil @x0)) + -> (forall z (x :: z) (xs :: WeirdList (WeirdList z)). + Sing @z x + -> Sing @(WeirdList (WeirdList z)) xs + -> p @(WeirdList z) _1 xs + -> p @z _2 ('WeirdCons @z x xs)) + -> p @a1 _3 wl + (Indeed, I sometimes struggle even printing this correctly, + due to its ill-scoped nature.) + • In the type signature: + elimWeirdList :: forall (a :: Type) + (wl :: WeirdList a) + (p :: forall (x :: Type). x -> WeirdList x -> Type). + Sing wl + -> (forall (y :: Type). p _ WeirdNil) + -> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)). + Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs)) + -> p _ wl diff --git a/testsuite/tests/patsyn/should_compile/all.T b/testsuite/tests/patsyn/should_compile/all.T index 2ac343f635..6ef1928768 100644 --- a/testsuite/tests/patsyn/should_compile/all.T +++ b/testsuite/tests/patsyn/should_compile/all.T @@ -75,7 +75,6 @@ test('T14058', [extra_files(['T14058.hs', 'T14058a.hs'])], multimod_compile, ['T14058', '-v0']) test('T14326', normal, compile, ['']) test('T14394', normal, ghci_script, ['T14394.script']) -test('T14552', normal, compile, ['']) test('T14498', normal, compile, ['']) test('T16682', [extra_files(['T16682.hs', 'T16682a.hs'])], multimod_compile, ['T16682', '-v0 -fwarn-incomplete-patterns -fno-code']) diff --git a/testsuite/tests/patsyn/should_compile/T14552.hs b/testsuite/tests/patsyn/should_fail/T14552.hs index a4a7493530..a4a7493530 100644 --- a/testsuite/tests/patsyn/should_compile/T14552.hs +++ b/testsuite/tests/patsyn/should_fail/T14552.hs diff --git a/testsuite/tests/patsyn/should_fail/T14552.stderr b/testsuite/tests/patsyn/should_fail/T14552.stderr new file mode 100644 index 0000000000..b9b6b8448b --- /dev/null +++ b/testsuite/tests/patsyn/should_fail/T14552.stderr @@ -0,0 +1,8 @@ + +T14552.hs:22:9: error: + • Cannot generalise type; skolem ‘k’ would escape its scope + if I tried to quantify (aa0 :: k) in this type: + forall k (w :: k --> *). Exp a0 (F @k @(*) w aa0) + (Indeed, I sometimes struggle even printing this correctly, + due to its ill-scoped nature.) + • In the declaration for pattern synonym ‘FOO’ diff --git a/testsuite/tests/patsyn/should_fail/all.T b/testsuite/tests/patsyn/should_fail/all.T index 27ebc8bdd4..02cc2cec2c 100644 --- a/testsuite/tests/patsyn/should_fail/all.T +++ b/testsuite/tests/patsyn/should_fail/all.T @@ -46,3 +46,4 @@ test('T15685', normal, compile_fail, ['']) test('T15692', normal, compile, ['']) # It has -fdefer-type-errors inside test('T15694', normal, compile_fail, ['']) test('T16900', normal, compile_fail, ['-fdiagnostics-show-caret']) +test('T14552', normal, compile_fail, ['']) diff --git a/testsuite/tests/polykinds/T15795.stderr b/testsuite/tests/polykinds/T15795.stderr new file mode 100644 index 0000000000..65bfdddecc --- /dev/null +++ b/testsuite/tests/polykinds/T15795.stderr @@ -0,0 +1,9 @@ + +T15795.hs:12:3: error: + • Cannot generalise type; skolem ‘k’ would escape its scope + if I tried to quantify (a0 :: k) in this type: + forall k (b :: k). T @k @a0 b + (Indeed, I sometimes struggle even printing this correctly, + due to its ill-scoped nature.) + • In the definition of data constructor ‘MkT’ + In the data declaration for ‘T’ diff --git a/testsuite/tests/polykinds/T15795a.stderr b/testsuite/tests/polykinds/T15795a.stderr new file mode 100644 index 0000000000..f4757137ce --- /dev/null +++ b/testsuite/tests/polykinds/T15795a.stderr @@ -0,0 +1,9 @@ + +T15795a.hs:9:3: error: + • Cannot generalise type; skolem ‘u’ would escape its scope + if I tried to quantify (cat10 :: u) in this type: + forall u (a :: u). F @u @cat10 a + (Indeed, I sometimes struggle even printing this correctly, + due to its ill-scoped nature.) + • In the definition of data constructor ‘Prod’ + In the data declaration for ‘F’ diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T index 74ab266308..4312691755 100644 --- a/testsuite/tests/polykinds/all.T +++ b/testsuite/tests/polykinds/all.T @@ -204,8 +204,8 @@ test('T15817', normal, compile, ['']) test('T15874', normal, compile, ['']) test('T14887a', normal, compile, ['']) test('T14847', normal, compile, ['']) -test('T15795', normal, compile, ['']) -test('T15795a', normal, compile, ['']) +test('T15795', normal, compile_fail, ['']) +test('T15795a', normal, compile_fail, ['']) test('T16247', normal, compile_fail, ['']) test('T16247a', normal, compile_fail, ['']) test('KindVarOrder', normal, ghci_script, ['KindVarOrder.script']) diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T index c51ff0b36b..80b11ca851 100644 --- a/testsuite/tests/typecheck/should_compile/all.T +++ b/testsuite/tests/typecheck/should_compile/all.T @@ -685,7 +685,6 @@ test('UnlifNewUnify', normal, compile, ['']) test('UnliftedNewtypesLPFamily', normal, compile, ['']) test('UnliftedNewtypesDifficultUnification', normal, compile, ['']) test('T16832', normal, ghci_script, ['T16832.script']) -test('T16946', normal, compile, ['']) test('T16995', normal, compile, ['']) test('T17007', normal, compile, ['']) test('T17067', normal, compile, ['']) diff --git a/testsuite/tests/typecheck/should_fail/T14350.stderr b/testsuite/tests/typecheck/should_fail/T14350.stderr index eb80d3ec80..955554ab8d 100644 --- a/testsuite/tests/typecheck/should_fail/T14350.stderr +++ b/testsuite/tests/typecheck/should_fail/T14350.stderr @@ -1,30 +1,52 @@ -T14350.hs:59:15: error: - • Couldn't match expected type ‘Proxy a1 - -> Apply (Apply c 'Proxy) (Apply g 'Proxy)’ - with actual type ‘Sing (f @@ t0)’ - • The function ‘applySing’ is applied to three arguments, - but its type ‘Sing f -> Sing t0 -> Sing (f @@ t0)’ has only two - In the expression: applySing f Proxy Proxy - In an equation for ‘dcomp’: dcomp f g x = applySing f Proxy Proxy - • Relevant bindings include - x :: Sing x (bound at T14350.hs:59:11) - g :: Sing g (bound at T14350.hs:59:9) - f :: Sing f (bound at T14350.hs:59:7) - dcomp :: Sing f - -> Sing g -> Sing x -> (c @@ 'Proxy) @@ (g @@ 'Proxy) - (bound at T14350.hs:59:1) - -T14350.hs:59:27: error: - • Couldn't match expected type ‘Sing t0’ - with actual type ‘Proxy a0’ - • In the second argument of ‘applySing’, namely ‘Proxy’ - In the expression: applySing f Proxy Proxy - In an equation for ‘dcomp’: dcomp f g x = applySing f Proxy Proxy - • Relevant bindings include - x :: Sing x (bound at T14350.hs:59:11) - g :: Sing g (bound at T14350.hs:59:9) - f :: Sing f (bound at T14350.hs:59:7) - dcomp :: Sing f - -> Sing g -> Sing x -> (c @@ 'Proxy) @@ (g @@ 'Proxy) - (bound at T14350.hs:59:1) +T14350.hs:49:10: error: + • Cannot generalise type; skolem ‘a’ would escape its scope + if I tried to quantify (x0 :: a) in this type: + forall a (b1 :: a ~> *) + (c :: forall (x :: a). Proxy @{a} x ~> ((@@) @{*} @{a} b1 x ~> *)) + (f :: forall (x :: a) (y :: (@@) @{*} @{a} b1 x). + Proxy @{a} x + ~> (Proxy @{Apply @a @(*) b1 x} y + ~> (@@) + @{*} + @{Apply @a @(*) b1 x} + ((@@) + @{Apply @a @(*) b1 x ~> *} @{Proxy @{a} x} (c @x) ('Proxy @{a} @x)) + y)) + (g :: forall (x :: a). Proxy @{a} x ~> (@@) @{*} @{a} b1 x) + (x :: a). + Sing + @(Proxy @{a} x0 + ~> (Proxy @{Apply @a @(*) b1 x0} y0 + ~> Apply + @(Apply @a @(*) b1 x0) + @(*) + (Apply + @(Proxy @{a} x0) + @(Apply @a @(*) b1 x0 ~> *) + (c @x0) + ('Proxy @{a} @x0)) + y0)) + (f @x0 @y0) + -> Sing @(Proxy @{a} x1 ~> Apply @a @(*) b1 x1) (g @x1) + -> Sing @a x + -> (@@) + @{*} + @{Apply @a @(*) b1 x} + ((@@) + @{Apply @a @(*) b1 x ~> *} @{Proxy @{a} x} (c @x) ('Proxy @{a} @x)) + ((@@) + @{Apply @a @(*) b1 x} @{Proxy @{a} x} (g @x) ('Proxy @{a} @x)) + (Indeed, I sometimes struggle even printing this correctly, + due to its ill-scoped nature.) + • In the type signature: + dcomp :: forall (a :: Type) + (b :: a ~> Type) + (c :: forall (x :: a). Proxy x ~> b @@ x ~> Type) + (f :: forall (x :: a) (y :: b @@ x). + Proxy x ~> Proxy y ~> c @@ ('Proxy :: Proxy x) @@ y) + (g :: forall (x :: a). Proxy x ~> b @@ x) + (x :: a). + Sing f + -> Sing g + -> Sing x -> c @@ ('Proxy :: Proxy x) @@ (g @@ ('Proxy :: Proxy x)) diff --git a/testsuite/tests/typecheck/should_compile/T16946.hs b/testsuite/tests/typecheck/should_fail/T16946.hs index e824f7cec8..e824f7cec8 100644 --- a/testsuite/tests/typecheck/should_compile/T16946.hs +++ b/testsuite/tests/typecheck/should_fail/T16946.hs diff --git a/testsuite/tests/typecheck/should_fail/T16946.stderr b/testsuite/tests/typecheck/should_fail/T16946.stderr new file mode 100644 index 0000000000..a923fe778e --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T16946.stderr @@ -0,0 +1,16 @@ + +T16946.hs:11:9: error: + • Cannot generalise type; skolem ‘k’ would escape its scope + if I tried to quantify (y0 :: k) in this type: + forall k (c :: k -> k -> *) + (m :: forall (x :: k) (y :: k). c x y -> * -> *) a. + CatMonad @k c m => + a -> m @y0 @y0 (Id @{k} @y0 c) a + (Indeed, I sometimes struggle even printing this correctly, + due to its ill-scoped nature.) + • In the type signature: + boom :: forall k + (c :: k -> k -> Type) + (m :: forall (x :: k) (y :: k). c x y -> Type -> Type) + a. + CatMonad c m => a -> m (Id c) a diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T index e46f694dd3..e11c239742 100644 --- a/testsuite/tests/typecheck/should_fail/all.T +++ b/testsuite/tests/typecheck/should_fail/all.T @@ -549,3 +549,4 @@ test('T17213', [extra_files(['T17213a.hs'])], multimod_compile_fail, ['T17213', test('T17355', normal, compile_fail, ['']) test('T17360', normal, compile_fail, ['']) test('T17563', normal, compile_fail, ['']) +test('T16946', normal, compile_fail, ['']) |