summaryrefslogtreecommitdiff
path: root/testsuite/tests/dependent
diff options
context:
space:
mode:
Diffstat (limited to 'testsuite/tests/dependent')
-rw-r--r--testsuite/tests/dependent/should_compile/InferDependency.hs6
-rw-r--r--testsuite/tests/dependent/should_compile/T11635.hs2
-rw-r--r--testsuite/tests/dependent/should_compile/T14066a.hs82
-rw-r--r--testsuite/tests/dependent/should_compile/T14066a.stderr5
-rw-r--r--testsuite/tests/dependent/should_compile/T14749.hs27
-rw-r--r--testsuite/tests/dependent/should_compile/all.T2
-rw-r--r--testsuite/tests/dependent/should_fail/BadTelescope.stderr5
-rw-r--r--testsuite/tests/dependent/should_fail/BadTelescope2.stderr13
-rw-r--r--testsuite/tests/dependent/should_fail/BadTelescope3.stderr2
-rw-r--r--testsuite/tests/dependent/should_fail/BadTelescope4.stderr4
-rw-r--r--testsuite/tests/dependent/should_fail/InferDependency.stderr10
-rw-r--r--testsuite/tests/dependent/should_fail/T13601.stderr3
-rw-r--r--testsuite/tests/dependent/should_fail/T13780c.stderr2
-rw-r--r--testsuite/tests/dependent/should_fail/T14066.hs17
-rw-r--r--testsuite/tests/dependent/should_fail/T14066.stderr11
-rw-r--r--testsuite/tests/dependent/should_fail/T14066c.hs9
-rw-r--r--testsuite/tests/dependent/should_fail/T14066c.stderr6
-rw-r--r--testsuite/tests/dependent/should_fail/T14066d.hs17
-rw-r--r--testsuite/tests/dependent/should_fail/T14066d.stderr21
-rw-r--r--testsuite/tests/dependent/should_fail/T14066e.hs13
-rw-r--r--testsuite/tests/dependent/should_fail/T14066e.stderr11
-rw-r--r--testsuite/tests/dependent/should_fail/T14066f.hs8
-rw-r--r--testsuite/tests/dependent/should_fail/T14066f.stderr6
-rw-r--r--testsuite/tests/dependent/should_fail/T14066g.hs9
-rw-r--r--testsuite/tests/dependent/should_fail/T14066g.stderr7
-rw-r--r--testsuite/tests/dependent/should_fail/T14066h.hs11
-rw-r--r--testsuite/tests/dependent/should_fail/T14066h.stderr16
-rw-r--r--testsuite/tests/dependent/should_fail/TypeSkolEscape.hs1
-rw-r--r--testsuite/tests/dependent/should_fail/TypeSkolEscape.stderr10
-rw-r--r--testsuite/tests/dependent/should_fail/all.T11
30 files changed, 316 insertions, 31 deletions
diff --git a/testsuite/tests/dependent/should_compile/InferDependency.hs b/testsuite/tests/dependent/should_compile/InferDependency.hs
new file mode 100644
index 0000000000..47957d47d6
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/InferDependency.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE TypeInType #-}
+
+module InferDependency where
+
+data Proxy k (a :: k)
+data Proxy2 k a = P (Proxy k a)
diff --git a/testsuite/tests/dependent/should_compile/T11635.hs b/testsuite/tests/dependent/should_compile/T11635.hs
index 1cbdbafb90..2292def966 100644
--- a/testsuite/tests/dependent/should_compile/T11635.hs
+++ b/testsuite/tests/dependent/should_compile/T11635.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeInType, KindSignatures, ExplicitForAll #-}
+{-# LANGUAGE TypeInType, KindSignatures, ExplicitForAll, RankNTypes #-}
module T11635 where
diff --git a/testsuite/tests/dependent/should_compile/T14066a.hs b/testsuite/tests/dependent/should_compile/T14066a.hs
new file mode 100644
index 0000000000..e1a6255520
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T14066a.hs
@@ -0,0 +1,82 @@
+{-# LANGUAGE TypeFamilies, TypeInType, ExplicitForAll, GADTs,
+ UndecidableInstances, RankNTypes, ScopedTypeVariables #-}
+
+module T14066a where
+
+import Data.Proxy
+import Data.Kind
+import Data.Type.Bool
+
+
+type family Bar x y where
+ Bar (x :: a) (y :: b) = Int
+ Bar (x :: c) (y :: d) = Bool -- a,b,c,d should be SigTvs and unify appropriately
+
+
+ -- the two k's, even though they have different scopes, should unify in the
+ -- kind-check and then work in the type-check because Prox3 has been generalized
+
+data Prox3 a where
+ MkProx3a :: Prox3 (a :: k1)
+ MkProx3b :: Prox3 (a :: k2)
+
+ -- This probably should be rejected, as it's polymorphic recursion without a CUSK.
+ -- But GHC accepts it because the polymorphic occurrence is at a type variable.
+data T0 a = forall k (b :: k). MkT0 (T0 b) Int
+
+ -- k and j should unify
+type family G x a where
+ G Int (b :: k) = Int
+ G Bool (c :: j) = Bool
+
+-- this last example just checks that GADT pattern-matching on kinds still works.
+-- nothing new here.
+data T (a :: k) where
+ MkT :: T (a :: Type -> Type)
+
+data S (a :: Type -> Type) where
+ MkS :: S a
+
+f :: forall k (a :: k). Proxy a -> T a -> ()
+f _ MkT = let y :: S a
+ y = MkS
+ in ()
+
+-- This is questionable. Should we use the RHS to determine dependency? It works
+-- now, but if it stops working in the future, that's not a deal-breaker.
+type P k a = Proxy (a :: k)
+
+
+-- This is a challenge. It should be accepted, but only because c's kind is learned
+-- to be Proxy True, allowing b to be assigned kind `a`. If we don't know c's kind,
+-- then GHC would need to be convinced that If (c's kind) b d always has kind `a`.
+-- Naively, we don't know about c's kind early enough.
+
+data SameKind :: forall k. k -> k -> Type
+type family IfK (e :: Proxy (j :: Bool)) (f :: m) (g :: n) :: If j m n where
+ IfK (_ :: Proxy True) f _ = f
+ IfK (_ :: Proxy False) _ g = g
+x :: forall c. (forall a b (d :: a). SameKind (IfK c b d) d) -> (Proxy (c :: Proxy True))
+x _ = Proxy
+
+
+f2 :: forall b. b -> Proxy Maybe
+f2 x = fstOf3 y :: Proxy Maybe
+ where
+ y :: (Proxy a, Proxy c, b)
+ y = (Proxy, Proxy, x)
+
+fstOf3 (x, _, _) = x
+
+f3 :: forall b. b -> Proxy Maybe
+f3 x = fst y :: Proxy Maybe
+ where
+ y :: (Proxy a, b)
+ y = (Proxy, x)
+
+-- cf. dependent/should_fail/T14066h. Here, y's type does *not* capture any variables,
+-- so it is generalized, even with MonoLocalBinds.
+f4 x = (fst y :: Proxy Int, fst y :: Proxy Maybe)
+ where
+ y :: (Proxy a, Int)
+ y = (Proxy, x)
diff --git a/testsuite/tests/dependent/should_compile/T14066a.stderr b/testsuite/tests/dependent/should_compile/T14066a.stderr
new file mode 100644
index 0000000000..906695f3f7
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T14066a.stderr
@@ -0,0 +1,5 @@
+
+T14066a.hs:13:3: warning:
+ Type family instance equation is overlapped:
+ forall c d (x :: c) (y :: d).
+ Bar x y = Bool -- Defined at T14066a.hs:13:3
diff --git a/testsuite/tests/dependent/should_compile/T14749.hs b/testsuite/tests/dependent/should_compile/T14749.hs
new file mode 100644
index 0000000000..79bcce66ff
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T14749.hs
@@ -0,0 +1,27 @@
+{-# LANGUAGE GADTs, TypeOperators, DataKinds, TypeFamilies, TypeInType #-}
+
+module T14749 where
+
+import Data.Kind
+
+data KIND = STAR | KIND :> KIND
+
+data Ty :: KIND -> Type where
+ TMaybe :: Ty (STAR :> STAR)
+ TApp :: Ty (a :> b) -> (Ty a -> Ty b)
+
+type family IK (k :: KIND) = (res :: Type) where
+ IK STAR = Type
+ IK (a:>b) = IK a -> IK b
+
+type family I (t :: Ty k) = (res :: IK k) where
+ I TMaybe = Maybe
+ I (TApp f a) = (I f) (I a)
+
+data TyRep (k :: KIND) (t :: Ty k) where
+ TyMaybe :: TyRep (STAR:>STAR) TMaybe
+ TyApp :: TyRep (a:>b) f -> TyRep a x -> TyRep b (TApp f x)
+
+zero :: TyRep STAR a -> I a
+zero x = case x of
+ TyApp TyMaybe _ -> Nothing
diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index da25b22799..070e1203f8 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -32,3 +32,5 @@ test('T13938', [extra_files(['T13938a.hs'])], run_command,
['$MAKE -s --no-print-directory T13938'])
test('T14556', normal, compile, [''])
test('T14720', normal, compile, [''])
+test('T14066a', normal, compile, [''])
+test('T14749', normal, compile, [''])
diff --git a/testsuite/tests/dependent/should_fail/BadTelescope.stderr b/testsuite/tests/dependent/should_fail/BadTelescope.stderr
index 2fbc35a9ba..5fa8efd502 100644
--- a/testsuite/tests/dependent/should_fail/BadTelescope.stderr
+++ b/testsuite/tests/dependent/should_fail/BadTelescope.stderr
@@ -1,9 +1,6 @@
BadTelescope.hs:9:1: error:
- • These kind and type variables: (a :: k)
- k
- (b :: k)
- (c :: SameKind a b)
+ • These kind and type variables: a k (b :: k) (c :: SameKind a b)
are out of dependency order. Perhaps try this ordering:
k (a :: k) (b :: k) (c :: SameKind a b)
• In the data type declaration for ‘X’
diff --git a/testsuite/tests/dependent/should_fail/BadTelescope2.stderr b/testsuite/tests/dependent/should_fail/BadTelescope2.stderr
index 2a9dc76310..55a484910c 100644
--- a/testsuite/tests/dependent/should_fail/BadTelescope2.stderr
+++ b/testsuite/tests/dependent/should_fail/BadTelescope2.stderr
@@ -3,14 +3,11 @@ BadTelescope2.hs:10:8: error:
• These kind and type variables: a k (b :: k)
are out of dependency order. Perhaps try this ordering:
k (a :: k) (b :: k)
- • In the type signature:
- foo :: forall a k (b :: k). SameKind a b
+ • In the type signature: foo :: forall a k (b :: k). SameKind a b
-BadTelescope2.hs:13:8: error:
- • The kind of variable ‘b’, namely ‘Proxy a’,
- depends on variable ‘a’ from an inner scope
- Perhaps bind ‘b’ sometime after binding ‘a’
- NB: Implicitly-bound variables always come before other ones.
- • In the type signature:
+BadTelescope2.hs:13:70: error:
+ • Expected kind ‘k0’, but ‘d’ has kind ‘Proxy a’
+ • In the second argument of ‘SameKind’, namely ‘d’
+ In the type signature:
bar :: forall a (c :: Proxy b) (d :: Proxy a).
Proxy c -> SameKind b d
diff --git a/testsuite/tests/dependent/should_fail/BadTelescope3.stderr b/testsuite/tests/dependent/should_fail/BadTelescope3.stderr
index 4ea7458bb2..1137f28c4d 100644
--- a/testsuite/tests/dependent/should_fail/BadTelescope3.stderr
+++ b/testsuite/tests/dependent/should_fail/BadTelescope3.stderr
@@ -1,6 +1,6 @@
BadTelescope3.hs:9:1: error:
- • These kind and type variables: (a :: k) k (b :: k)
+ • These kind and type variables: a k (b :: k)
are out of dependency order. Perhaps try this ordering:
k (a :: k) (b :: k)
• In the type synonym declaration for ‘S’
diff --git a/testsuite/tests/dependent/should_fail/BadTelescope4.stderr b/testsuite/tests/dependent/should_fail/BadTelescope4.stderr
index 2394f896ad..f7c281e983 100644
--- a/testsuite/tests/dependent/should_fail/BadTelescope4.stderr
+++ b/testsuite/tests/dependent/should_fail/BadTelescope4.stderr
@@ -1,6 +1,6 @@
BadTelescope4.hs:9:1: error:
- • These kind and type variables: (a :: k)
+ • These kind and type variables: a
(c :: Proxy b)
(d :: Proxy a)
(x :: SameKind b d)
@@ -11,5 +11,5 @@ BadTelescope4.hs:9:1: error:
(c :: Proxy b)
(d :: Proxy a)
(x :: SameKind b d)
- NB: Implicitly declared kind variables are put first.
+ NB: Implicitly declared variables come before others.
• In the data type declaration for ‘Bad’
diff --git a/testsuite/tests/dependent/should_fail/InferDependency.stderr b/testsuite/tests/dependent/should_fail/InferDependency.stderr
index 7fa900a889..cc852ee58c 100644
--- a/testsuite/tests/dependent/should_fail/InferDependency.stderr
+++ b/testsuite/tests/dependent/should_fail/InferDependency.stderr
@@ -1,8 +1,10 @@
-InferDependency.hs:6:1: error:
- • Invalid declaration for ‘Proxy2’; you must explicitly
- declare which variables are dependent on which others.
- Inferred variable kinds:
+InferDependency.hs:6:13: error:
+ • Type constructor argument ‘k’ is used dependently.
+ Any dependent arguments must be obviously so, not inferred
+ by the type-checker.
+ Inferred argument kinds:
k :: *
a :: k
+ Suggestion: use ‘k’ in a kind to make the dependency clearer.
• In the data type declaration for ‘Proxy2’
diff --git a/testsuite/tests/dependent/should_fail/T13601.stderr b/testsuite/tests/dependent/should_fail/T13601.stderr
index c1c9803e5a..bc2877c3e6 100644
--- a/testsuite/tests/dependent/should_fail/T13601.stderr
+++ b/testsuite/tests/dependent/should_fail/T13601.stderr
@@ -1,6 +1,5 @@
T13601.hs:18:16: error:
- • Expected kind ‘TYPE (Rep 'LiftedRep)’,
- but ‘Logic a’ has kind ‘TYPE (Rep rep)’
+ • Expected a type, but ‘Logic a’ has kind ‘TYPE (Rep rep)’
• In the first argument of ‘Boolean’, namely ‘(Logic a)’
In the class declaration for ‘Eq’
diff --git a/testsuite/tests/dependent/should_fail/T13780c.stderr b/testsuite/tests/dependent/should_fail/T13780c.stderr
index f91d7a3236..065c700dfc 100644
--- a/testsuite/tests/dependent/should_fail/T13780c.stderr
+++ b/testsuite/tests/dependent/should_fail/T13780c.stderr
@@ -2,7 +2,7 @@
[2 of 2] Compiling T13780c ( T13780c.hs, T13780c.o )
T13780c.hs:11:16: error:
- • Expected kind ‘Sing _’, but ‘SFalse’ has kind ‘Sing 'False’
+ • Expected kind ‘Sing _1’, but ‘SFalse’ has kind ‘Sing 'False’
• In the third argument of ‘ElimBool’, namely ‘SFalse’
In the type family declaration for ‘ElimBool’
diff --git a/testsuite/tests/dependent/should_fail/T14066.hs b/testsuite/tests/dependent/should_fail/T14066.hs
new file mode 100644
index 0000000000..58396df591
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14066.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE KindSignatures #-}
+
+module T14066 where
+
+import Data.Kind ( Type )
+import Data.Type.Equality
+import Data.Proxy
+import GHC.Exts
+
+data SameKind :: k -> k -> Type
+
+f (x :: Proxy a) = let g :: forall k (b :: k). SameKind a b
+ g = undefined
+ in ()
diff --git a/testsuite/tests/dependent/should_fail/T14066.stderr b/testsuite/tests/dependent/should_fail/T14066.stderr
new file mode 100644
index 0000000000..cd0142f5c1
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14066.stderr
@@ -0,0 +1,11 @@
+
+T14066.hs:15:59: error:
+ • Expected kind ‘k0’, but ‘b’ has kind ‘k’
+ • In the second argument of ‘SameKind’, namely ‘b’
+ In the type signature: g :: forall k (b :: k). SameKind a b
+ In the expression:
+ let
+ g :: forall k (b :: k). SameKind a b
+ g = undefined
+ in ()
+ • Relevant bindings include x :: Proxy a (bound at T14066.hs:15:4)
diff --git a/testsuite/tests/dependent/should_fail/T14066c.hs b/testsuite/tests/dependent/should_fail/T14066c.hs
new file mode 100644
index 0000000000..b4597d2cec
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14066c.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE TypeFamilies, TypeInType, UndecidableInstances #-}
+
+module T14066c where
+
+type family H a b where
+ H a b = H b a
+
+type X = H True Nothing -- this should fail to kind-check.
+ -- if it's accepted, then we've inferred polymorphic recursion for H
diff --git a/testsuite/tests/dependent/should_fail/T14066c.stderr b/testsuite/tests/dependent/should_fail/T14066c.stderr
new file mode 100644
index 0000000000..dc5ba30a4f
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14066c.stderr
@@ -0,0 +1,6 @@
+
+T14066c.hs:8:17: error:
+ • Expected kind ‘Bool’, but ‘Nothing’ has kind ‘Maybe a0’
+ • In the second argument of ‘H’, namely ‘Nothing’
+ In the type ‘H True Nothing’
+ In the type declaration for ‘X’
diff --git a/testsuite/tests/dependent/should_fail/T14066d.hs b/testsuite/tests/dependent/should_fail/T14066d.hs
new file mode 100644
index 0000000000..ea47644688
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14066d.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE RankNTypes, ScopedTypeVariables, TypeInType #-}
+
+module T14066d where
+
+import Data.Proxy
+
+g :: (forall c b (a :: c). (Proxy a, Proxy c, b)) -> ()
+g _ = ()
+
+f :: forall b. b -> (Proxy Maybe, ())
+f x = (fstOf3 y :: Proxy Maybe, g y)
+ where
+ y :: (Proxy a, Proxy c, b) -- this should NOT generalize over b
+ -- meaning the call to g is ill-typed
+ y = (Proxy, Proxy, x)
+
+fstOf3 (x, _, _) = x
diff --git a/testsuite/tests/dependent/should_fail/T14066d.stderr b/testsuite/tests/dependent/should_fail/T14066d.stderr
new file mode 100644
index 0000000000..3a8b90edce
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14066d.stderr
@@ -0,0 +1,21 @@
+
+T14066d.hs:11:35: error:
+ • Couldn't match type ‘b’ with ‘b1’
+ ‘b’ is a rigid type variable bound by
+ the type signature for:
+ f :: forall b. b -> (Proxy Maybe, ())
+ at T14066d.hs:10:1-37
+ ‘b1’ is a rigid type variable bound by
+ a type expected by the context:
+ forall c b1 (a :: c). (Proxy a, Proxy c, b1)
+ at T14066d.hs:11:33-35
+ Expected type: (Proxy a, Proxy c, b1)
+ Actual type: (Proxy a, Proxy c, b)
+ • In the first argument of ‘g’, namely ‘y’
+ In the expression: g y
+ In the expression: (fstOf3 y :: Proxy Maybe, g y)
+ • Relevant bindings include
+ y :: forall k1 k2 (a :: k2) (c :: k1). (Proxy a, Proxy c, b)
+ (bound at T14066d.hs:15:5)
+ x :: b (bound at T14066d.hs:11:3)
+ f :: b -> (Proxy Maybe, ()) (bound at T14066d.hs:11:1)
diff --git a/testsuite/tests/dependent/should_fail/T14066e.hs b/testsuite/tests/dependent/should_fail/T14066e.hs
new file mode 100644
index 0000000000..9b799e542c
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14066e.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE MonoLocalBinds, TypeInType, ScopedTypeVariables #-}
+
+module T14066e where
+
+import Data.Proxy
+
+-- this should fail because the dependency between b and c can't be
+-- determined in the type signature
+h :: forall a. a -> ()
+h x = ()
+ where
+ j :: forall c b. Proxy a -> Proxy b -> Proxy c -> Proxy b
+ j _ (p1 :: Proxy b') (p2 :: Proxy c') = (p1 :: Proxy (b' :: c'))
diff --git a/testsuite/tests/dependent/should_fail/T14066e.stderr b/testsuite/tests/dependent/should_fail/T14066e.stderr
new file mode 100644
index 0000000000..504ca5a80e
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14066e.stderr
@@ -0,0 +1,11 @@
+
+T14066e.hs:13:59: error:
+ • Expected kind ‘c’, but ‘b'’ has kind ‘k0’
+ • In the first argument of ‘Proxy’, namely ‘(b' :: c')’
+ In an expression type signature: Proxy (b' :: c')
+ In the expression: (p1 :: Proxy (b' :: c'))
+ • Relevant bindings include
+ p2 :: Proxy c (bound at T14066e.hs:13:27)
+ p1 :: Proxy b (bound at T14066e.hs:13:10)
+ j :: Proxy a -> Proxy b -> Proxy c -> Proxy b
+ (bound at T14066e.hs:13:5)
diff --git a/testsuite/tests/dependent/should_fail/T14066f.hs b/testsuite/tests/dependent/should_fail/T14066f.hs
new file mode 100644
index 0000000000..ccb7ceac0e
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14066f.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE TypeInType #-}
+
+module T14066f where
+
+import Data.Proxy
+
+-- a can't come before k.
+type P a k = Proxy (a :: k)
diff --git a/testsuite/tests/dependent/should_fail/T14066f.stderr b/testsuite/tests/dependent/should_fail/T14066f.stderr
new file mode 100644
index 0000000000..44c4ed293c
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14066f.stderr
@@ -0,0 +1,6 @@
+
+T14066f.hs:8:1: error:
+ • These kind and type variables: a k
+ are out of dependency order. Perhaps try this ordering:
+ k (a :: k)
+ • In the type synonym declaration for ‘P’
diff --git a/testsuite/tests/dependent/should_fail/T14066g.hs b/testsuite/tests/dependent/should_fail/T14066g.hs
new file mode 100644
index 0000000000..df0e03b173
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14066g.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE TypeInType #-}
+
+module T14066g where
+
+import Data.Kind
+
+data SameKind :: k -> k -> Type
+
+data Q a (b :: a) (d :: SameKind c b)
diff --git a/testsuite/tests/dependent/should_fail/T14066g.stderr b/testsuite/tests/dependent/should_fail/T14066g.stderr
new file mode 100644
index 0000000000..22ca786343
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14066g.stderr
@@ -0,0 +1,7 @@
+
+T14066g.hs:9:1: error:
+ • These kind and type variables: a (b :: a) (d :: SameKind c b)
+ are out of dependency order. Perhaps try this ordering:
+ a (c :: a) (b :: a) (d :: SameKind c b)
+ NB: Implicitly declared variables come before others.
+ • In the data type declaration for ‘Q’
diff --git a/testsuite/tests/dependent/should_fail/T14066h.hs b/testsuite/tests/dependent/should_fail/T14066h.hs
new file mode 100644
index 0000000000..7e7ecd31c9
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14066h.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE ScopedTypeVariables, TypeInType, MonoLocalBinds #-}
+
+module T14066h where
+
+import Data.Proxy
+
+f :: forall b. b -> (Proxy Int, Proxy Maybe)
+f x = (fst y :: Proxy Int, fst y :: Proxy Maybe)
+ where
+ y :: (Proxy a, b) -- MonoLocalBinds means this won't generalize over the kind of a
+ y = (Proxy, x)
diff --git a/testsuite/tests/dependent/should_fail/T14066h.stderr b/testsuite/tests/dependent/should_fail/T14066h.stderr
new file mode 100644
index 0000000000..bfd33693b6
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14066h.stderr
@@ -0,0 +1,16 @@
+
+T14066h.hs:8:28: error:
+ • Couldn't match kind ‘* -> *’ with ‘*’
+ When matching types
+ a0 :: *
+ Maybe :: * -> *
+ Expected type: Proxy Maybe
+ Actual type: Proxy a0
+ • In the expression: fst y :: Proxy Maybe
+ In the expression: (fst y :: Proxy Int, fst y :: Proxy Maybe)
+ In an equation for ‘f’:
+ f x
+ = (fst y :: Proxy Int, fst y :: Proxy Maybe)
+ where
+ y :: (Proxy a, b)
+ y = (Proxy, x)
diff --git a/testsuite/tests/dependent/should_fail/TypeSkolEscape.hs b/testsuite/tests/dependent/should_fail/TypeSkolEscape.hs
index bbec037487..02b7737499 100644
--- a/testsuite/tests/dependent/should_fail/TypeSkolEscape.hs
+++ b/testsuite/tests/dependent/should_fail/TypeSkolEscape.hs
@@ -1,4 +1,5 @@
{-# LANGUAGE RankNTypes, PolyKinds, TypeInType #-}
+-- NB: -fprint-explicit-runtime-reps enabled in all.T
module TypeSkolEscape where
diff --git a/testsuite/tests/dependent/should_fail/TypeSkolEscape.stderr b/testsuite/tests/dependent/should_fail/TypeSkolEscape.stderr
index 88539858cf..e2ef266914 100644
--- a/testsuite/tests/dependent/should_fail/TypeSkolEscape.stderr
+++ b/testsuite/tests/dependent/should_fail/TypeSkolEscape.stderr
@@ -1,7 +1,5 @@
-TypeSkolEscape.hs:8:1: error:
- • Quantified type's kind mentions quantified type variable
- (skolem escape)
- type: forall (a1 :: TYPE v1). a1
- of kind: TYPE v
- • In the type synonym declaration for ‘Bad’
+TypeSkolEscape.hs:9:52: error:
+ • Expected kind ‘k0’, but ‘a’ has kind ‘TYPE v’
+ • In the type ‘forall (v :: RuntimeRep) (a :: TYPE v). a’
+ In the type declaration for ‘Bad’
diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T
index e28b2df5cd..7273445548 100644
--- a/testsuite/tests/dependent/should_fail/all.T
+++ b/testsuite/tests/dependent/should_fail/all.T
@@ -1,6 +1,6 @@
test('DepFail1', normal, compile_fail, [''])
test('RAE_T32a', normal, compile_fail, [''])
-test('TypeSkolEscape', normal, compile_fail, [''])
+test('TypeSkolEscape', normal, compile_fail, ['-fprint-explicit-runtime-reps'])
test('BadTelescope', normal, compile_fail, [''])
test('BadTelescope2', normal, compile_fail, [''])
test('BadTelescope3', normal, compile_fail, [''])
@@ -10,7 +10,6 @@ test('BadTelescope4', normal, compile_fail, [''])
test('RenamingStar', normal, compile_fail, [''])
test('T11407', normal, compile_fail, [''])
test('T11334b', normal, compile_fail, [''])
-test('InferDependency', normal, compile_fail, [''])
test('KindLevelsB', normal, compile_fail, [''])
test('T11473', normal, compile_fail, [''])
test('T11471', normal, compile_fail, [''])
@@ -21,3 +20,11 @@ test('T13601', normal, compile_fail, [''])
test('T13780a', normal, compile_fail, [''])
test('T13780c', [extra_files(['T13780b.hs'])],
multimod_compile_fail, ['T13780c', ''])
+test('T14066', normal, compile_fail, [''])
+test('T14066c', normal, compile_fail, [''])
+test('T14066d', normal, compile_fail, [''])
+test('T14066e', normal, compile_fail, [''])
+test('T14066f', normal, compile_fail, [''])
+test('T14066g', normal, compile_fail, [''])
+test('T14066h', normal, compile_fail, [''])
+test('InferDependency', normal, compile_fail, [''])