diff options
| author | Simon Peyton Jones <simonpj@microsoft.com> | 2018-11-28 16:06:15 +0000 |
|---|---|---|
| committer | Simon Peyton Jones <simonpj@microsoft.com> | 2018-11-29 17:27:40 +0000 |
| commit | 2257a86daa72db382eb927df12a718669d5491f8 (patch) | |
| tree | 74bc33c17a5c898764be09eb6a9cb33572e91b2d /testsuite | |
| parent | 79d5427e1f9de02c0b171bf5db46b6b49c6f85e3 (diff) | |
| download | haskell-2257a86daa72db382eb927df12a718669d5491f8.tar.gz | |
Taming the Kind Inference Monster
My original goal was (Trac #15809) to move towards using level numbers
as the basis for deciding which type variables to generalise, rather
than searching for the free varaibles of the environment. However
it has turned into a truly major refactoring of the kind inference
engine.
Let's deal with the level-numbers part first:
* Augment quantifyTyVars to calculate the type variables to
quantify using level numbers, and compare the result with
the existing approach. That is; no change in behaviour,
just a WARNing if the two approaches give different answers.
* To do this I had to get the level number right when calling
quantifyTyVars, and this entailed a bit of care, especially
in the code for kind-checking type declarations.
* However, on the way I was able to eliminate or simplify
a number of calls to solveEqualities.
This work is incomplete: I'm not /using/ level numbers yet.
When I subsequently get rid of any remaining WARNings in
quantifyTyVars, that the level-number answers differ from
the current answers, then I can rip out the current
"free vars of the environment" stuff.
Anyway, this led me into deep dive into kind inference for type and
class declarations, which is an increasingly soggy part of GHC.
Richard already did some good work recently in
commit 5e45ad10ffca1ad175b10f6ef3327e1ed8ba25f3
Date: Thu Sep 13 09:56:02 2018 +0200
Finish fix for #14880.
The real change that fixes the ticket is described in
Note [Naughty quantification candidates] in TcMType.
but I kept turning over stones. So this patch has ended up
with a pretty significant refactoring of that code too.
Kind inference for types and classes
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
* Major refactoring in the way we generalise the inferred kind of
a TyCon, in kcTyClGroup. Indeed, I made it into a new top-level
function, generaliseTcTyCon. Plus a new Note to explain it
Note [Inferring kinds for type declarations].
* We decided (Trac #15592) not to treat class type variables specially
when dealing with Inferred/Specified/Required for associated types.
That simplifies things quite a bit. I also rewrote
Note [Required, Specified, and Inferred for types]
* Major refactoring of the crucial function kcLHsQTyVars:
I split it into
kcLHsQTyVars_Cusk and kcLHsQTyVars_NonCusk
because the two are really quite different. The CUSK case is
almost entirely rewritten, and is much easier because of our new
decision not to treat the class variables specially
* I moved all the error checks from tcTyClTyVars (which was a bizarre
place for it) into generaliseTcTyCon and/or the CUSK case of
kcLHsQTyVars. Now tcTyClTyVars is extremely simple.
* I got rid of all the all the subtleties in tcImplicitTKBndrs. Indeed
now there is no difference between tcImplicitTKBndrs and
kcImplicitTKBndrs; there is now a single bindImplicitTKBndrs.
Same for kc/tcExplicitTKBndrs. None of them monkey with level
numbers, nor build implication constraints. scopeTyVars is gone
entirely, as is kcLHsQTyVarBndrs. It's vastly simpler.
I found I could get rid of kcLHsQTyVarBndrs entirely, in favour of
the bnew bindExplicitTKBndrs.
Quantification
~~~~~~~~~~~~~~
* I now deal with the "naughty quantification candidates"
of the previous patch in candidateQTyVars, rather than in
quantifyTyVars; see Note [Naughty quantification candidates]
in TcMType.
I also killed off closeOverKindsCQTvs in favour of the same
strategy that we use for tyCoVarsOfType: namely, close over kinds
at the occurrences.
And candidateQTyVars no longer needs a gbl_tvs argument.
* Passing the ContextKind, rather than the expected kind itself,
to tc_hs_sig_type_and_gen makes it easy to allocate the expected
result kind (when we are in inference mode) at the right level.
Type families
~~~~~~~~~~~~~~
* I did a major rewrite of the impenetrable tcFamTyPats. The result
is vastly more comprehensible.
* I got rid of kcDataDefn entirely, quite a big function.
* I re-did the way that checkConsistentFamInst works, so
that it allows alpha-renaming of invisible arguments.
* The interaction of kind signatures and family instances is tricky.
Type families: see Note [Apparently-nullary families]
Data families: see Note [Result kind signature for a data family instance]
and Note [Eta-reduction for data families]
* The consistent instantation of an associated type family is tricky.
See Note [Checking consistent instantiation] and
Note [Matching in the consistent-instantation check]
in TcTyClsDecls. It's now checked in TcTyClsDecls because that is
when we have the relevant info to hand.
* I got tired of the compromises in etaExpandFamInst, so I did the
job properly by adding a field cab_eta_tvs to CoAxBranch.
See Coercion.etaExpandCoAxBranch.
tcInferApps and friends
~~~~~~~~~~~~~~~~~~~~~~~
* I got rid of the mysterious and horrible ClsInstInfo argument
to tcInferApps, checkExpectedKindX, and various checkValid
functions. It was horrible!
* I got rid of [Type] result of tcInferApps. This list was used
only in tcFamTyPats, when checking the LHS of a type instance;
and if there is a cast in the middle, the list is meaningless.
So I made tcInferApps simpler, and moved the complexity
(not much) to tcInferApps.
Result: tcInferApps is now pretty comprehensible again.
* I refactored the many function in TcMType that instantiate skolems.
Smaller things
* I rejigged the error message in checkValidTelescope; I think it's
quite a bit better now.
* checkValidType was not rejecting constraints in a kind signature
forall (a :: Eq b => blah). blah2
That led to further errors when we then do an ambiguity check.
So I make checkValidType reject it more aggressively.
* I killed off quantifyConDecl, instead calling kindGeneralize
directly.
* I fixed an outright bug in tyCoVarsOfImplic, where we were not
colleting the tyvar of the kind of the skolems
* Renamed ClsInstInfo to AssocInstInfo, and made it into its
own data type
* Some fiddling around with pretty-printing of family
instances which was trickier than I thought. I wanted
wildcards to print as plain "_" in user messages, although
they each need a unique identity in the CoAxBranch.
Some other oddments
* Refactoring around the trace messages from reportUnsolved.
* A bit of extra tc-tracing in TcHsSyn.commitFlexi
This patch fixes a raft of bugs, and includes tests for them.
* #14887
* #15740
* #15764
* #15789
* #15804
* #15817
* #15870
* #15874
* #15881
Diffstat (limited to 'testsuite')
106 files changed, 615 insertions, 322 deletions
diff --git a/testsuite/tests/dependent/should_compile/T15743.stderr b/testsuite/tests/dependent/should_compile/T15743.stderr index 7162a877a2..f44c430d8d 100644 --- a/testsuite/tests/dependent/should_compile/T15743.stderr +++ b/testsuite/tests/dependent/should_compile/T15743.stderr @@ -1,6 +1,6 @@ TYPE CONSTRUCTORS type role T nominal nominal nominal phantom phantom phantom - T :: forall {k1} k2 (k3 :: k2). Proxy k3 -> k1 -> k2 -> * + T{6} :: forall {k1} k2 (k3 :: k2). Proxy k3 -> k1 -> k2 -> * Dependent modules: [] Dependent packages: [base-4.12.0.0, ghc-prim-0.5.3, integer-gmp-1.0.2.0] diff --git a/testsuite/tests/dependent/should_compile/T15743e.stderr b/testsuite/tests/dependent/should_compile/T15743e.stderr index c77bf3849c..f96da68a7f 100644 --- a/testsuite/tests/dependent/should_compile/T15743e.stderr +++ b/testsuite/tests/dependent/should_compile/T15743e.stderr @@ -1,7 +1,7 @@ TYPE CONSTRUCTORS type role T nominal nominal nominal nominal nominal nominal phantom phantom representational nominal nominal phantom nominal phantom - T :: + T{14} :: forall {k1} {k2} {k3} (k4 :: k2) k5. forall k6 -> k6 -> Proxy k4 @@ -10,13 +10,13 @@ TYPE CONSTRUCTORS -> forall (k7 :: k1). Proxy k7 -> forall (k8 :: k5). Proxy k8 -> * type role T2 nominal nominal nominal nominal nominal phantom phantom representational nominal nominal phantom nominal nominal phantom - T2 :: - forall {k1} {k2} (k3 :: k1) k7. forall k4 -> + T2{14} :: + forall {k1} {k2} (k3 :: k2) k7. forall k4 -> k4 -> Proxy k3 -> (k7 -> *) -> k7 - -> forall (k5 :: k2). + -> forall (k5 :: k1). Proxy k5 -> forall k6 (k8 :: k6). Proxy k8 -> * DATA CONSTRUCTORS MkT2 :: forall {k7} {k1} {k2 :: k1} {k3} {k4 :: k3} {k5} {k6 :: k5} diff --git a/testsuite/tests/dependent/should_fail/BadTelescope.stderr b/testsuite/tests/dependent/should_fail/BadTelescope.stderr index 5fa8efd502..078d7377da 100644 --- a/testsuite/tests/dependent/should_fail/BadTelescope.stderr +++ b/testsuite/tests/dependent/should_fail/BadTelescope.stderr @@ -1,6 +1,7 @@ BadTelescope.hs:9:1: error: - • 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) + • The kind of ‘X’ is ill-scoped + Inferred kind: X :: forall (a :: k) k (b :: k) -> SameKind a b -> * + Perhaps try this order instead: + k (a :: k) (b :: k) (c :: SameKind a b) • In the data type declaration for ‘X’ diff --git a/testsuite/tests/dependent/should_fail/BadTelescope3.stderr b/testsuite/tests/dependent/should_fail/BadTelescope3.stderr index 1137f28c4d..c36ad07c42 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 (b :: k) - are out of dependency order. Perhaps try this ordering: - k (a :: k) (b :: k) + • The kind of ‘S’ is ill-scoped + Inferred kind: S :: k -> forall k -> k -> * + Perhaps try this order instead: 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 f7c281e983..039389bed0 100644 --- a/testsuite/tests/dependent/should_fail/BadTelescope4.stderr +++ b/testsuite/tests/dependent/should_fail/BadTelescope4.stderr @@ -1,15 +1,16 @@ BadTelescope4.hs:9:1: error: - • These kind and type variables: a - (c :: Proxy b) - (d :: Proxy a) - (x :: SameKind b d) - are out of dependency order. Perhaps try this ordering: + • The kind of ‘Bad’ is ill-scoped + Inferred kind: Bad :: forall k (b :: Proxy a). forall (a :: k) -> + Proxy b -> forall (d :: Proxy a) -> SameKind b d -> * + NB: Inferred variables + (namely: k) always come first + then Specified variables (namely: (b :: Proxy a)) + Perhaps try this order instead: k (a :: k) (b :: Proxy a) (c :: Proxy b) (d :: Proxy a) (x :: SameKind b d) - NB: Implicitly declared variables come before others. • In the data type declaration for ‘Bad’ diff --git a/testsuite/tests/dependent/should_fail/T13895.stderr b/testsuite/tests/dependent/should_fail/T13895.stderr index 3ced11a79d..adfebdd113 100644 --- a/testsuite/tests/dependent/should_fail/T13895.stderr +++ b/testsuite/tests/dependent/should_fail/T13895.stderr @@ -1,38 +1,7 @@ -T13895.hs:8:14: error: - • Could not deduce (Typeable (t dict)) - from the context: (Data a, Typeable (t dict)) - bound by the type signature for: - dataCast1 :: forall k1 a (c :: * -> *) (t :: forall k2. - Typeable k2 => - k2 -> *). - (Data a, Typeable (t dict)) => - (forall d. Data d => c (t dict1 d)) -> Maybe (c a) - at T13895.hs:(8,14)-(14,24) - The type variable ‘k0’ is ambiguous - • In the ambiguity check for ‘dataCast1’ - To defer the ambiguity check to use sites, enable AllowAmbiguousTypes - In the type signature: - dataCast1 :: forall (a :: Type). - Data a => - forall (c :: Type -> Type) - (t :: forall (k :: Type). Typeable k => k -> Type). - Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a) - -T13895.hs:12:23: error: - • Illegal constraint in a kind: Typeable k0 - • In the first argument of ‘Typeable’, namely ‘t’ - In the type signature: - dataCast1 :: forall (a :: Type). - Data a => - forall (c :: Type -> Type) - (t :: forall (k :: Type). Typeable k => k -> Type). - Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a) - -T13895.hs:13:38: error: - • Illegal constraint in a kind: Typeable k0 - • In the first argument of ‘c’, namely ‘(t d)’ - In the type signature: +T13895.hs:10:14: error: + • Illegal constraint in a kind: forall k. Typeable k => k -> * + • In the type signature: dataCast1 :: forall (a :: Type). Data a => forall (c :: Type -> Type) diff --git a/testsuite/tests/dependent/should_fail/T14066f.stderr b/testsuite/tests/dependent/should_fail/T14066f.stderr index 44c4ed293c..10aa1b9da4 100644 --- a/testsuite/tests/dependent/should_fail/T14066f.stderr +++ b/testsuite/tests/dependent/should_fail/T14066f.stderr @@ -1,6 +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) + • The kind of ‘P’ is ill-scoped + Inferred kind: P :: k -> forall k -> * + Perhaps try this order instead: k (a :: k) • In the type synonym declaration for ‘P’ diff --git a/testsuite/tests/dependent/should_fail/T14066g.stderr b/testsuite/tests/dependent/should_fail/T14066g.stderr index 22ca786343..23f0a4c9d0 100644 --- a/testsuite/tests/dependent/should_fail/T14066g.stderr +++ b/testsuite/tests/dependent/should_fail/T14066g.stderr @@ -1,7 +1,9 @@ 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: + • The kind of ‘Q’ is ill-scoped + Inferred kind: Q :: forall (c :: a). forall a (b :: a) -> + SameKind c b -> * + NB: Specified variables (namely: (c :: a)) always come first + Perhaps try this order instead: 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/T15591b.stderr b/testsuite/tests/dependent/should_fail/T15591b.stderr index 838ee51c8f..91d9a948f4 100644 --- a/testsuite/tests/dependent/should_fail/T15591b.stderr +++ b/testsuite/tests/dependent/should_fail/T15591b.stderr @@ -1,7 +1,8 @@ T15591b.hs:9:3: error: - • These kind and type variables: a c - are out of dependency order. Perhaps try this ordering: - a (b :: Proxy a) (c :: Proxy b) - NB: Implicitly declared variables come before others. + • The kind of ‘T4’ is ill-scoped + Inferred kind: T4 :: forall (b :: Proxy a). forall a -> + Proxy b -> * + NB: Inferred variables (namely: (b :: Proxy a)) always come first + Perhaps try this order instead: a (b :: Proxy a) (c :: Proxy b) • In the associated type family declaration for ‘T4’ diff --git a/testsuite/tests/dependent/should_fail/T15591c.stderr b/testsuite/tests/dependent/should_fail/T15591c.stderr index 2f2b47fc8d..ecaa66048c 100644 --- a/testsuite/tests/dependent/should_fail/T15591c.stderr +++ b/testsuite/tests/dependent/should_fail/T15591c.stderr @@ -1,7 +1,8 @@ T15591c.hs:9:3: error: - • These kind and type variables: c a - are out of dependency order. Perhaps try this ordering: - a (b :: Proxy a) (c :: Proxy b) - NB: Implicitly declared variables come before others. + • The kind of ‘T5’ is ill-scoped + Inferred kind: T5 :: forall (b :: Proxy a). + Proxy b -> forall a -> * + NB: Inferred variables (namely: (b :: Proxy a)) always come first + Perhaps try this order instead: a (b :: Proxy a) (c :: Proxy b) • In the associated type family declaration for ‘T5’ diff --git a/testsuite/tests/dependent/should_fail/T15743c.stderr b/testsuite/tests/dependent/should_fail/T15743c.stderr index 9d28b68998..8e3ad5077f 100644 --- a/testsuite/tests/dependent/should_fail/T15743c.stderr +++ b/testsuite/tests/dependent/should_fail/T15743c.stderr @@ -1,16 +1,15 @@ T15743c.hs:10:1: error: - • These kind and type variables: k - (c :: k) - (a :: Proxy c) - b - (x :: SimilarKind a b) - are out of dependency order. Perhaps try this ordering: + • The kind of ‘T’ is ill-scoped + Inferred kind: T :: forall (d :: k). + forall k (c :: k) (a :: Proxy c) (b :: Proxy d) -> + SimilarKind a b -> * + NB: Inferred variables (namely: (d :: k)) always come first + Perhaps try this order instead: k (d :: k) (c :: k) (a :: Proxy c) (b :: Proxy d) (x :: SimilarKind a b) - NB: Implicitly declared variables come before others. • In the data type declaration for ‘T’ diff --git a/testsuite/tests/dependent/should_fail/T15743d.stderr b/testsuite/tests/dependent/should_fail/T15743d.stderr index d982d16980..51d1fad66f 100644 --- a/testsuite/tests/dependent/should_fail/T15743d.stderr +++ b/testsuite/tests/dependent/should_fail/T15743d.stderr @@ -1,16 +1,15 @@ T15743d.hs:10:1: error: - • These kind and type variables: k - (c :: k) - (a :: Proxy c) - (b :: Proxy d) - (x :: SimilarKind a b) - are out of dependency order. Perhaps try this ordering: + • The kind of ‘T2’ is ill-scoped + Inferred kind: T2 :: forall (d :: k). + forall k (c :: k) (a :: Proxy c) (b :: Proxy d) -> + SimilarKind a b -> * + NB: Specified variables (namely: (d :: k)) always come first + Perhaps try this order instead: k (d :: k) (c :: k) (a :: Proxy c) (b :: Proxy d) (x :: SimilarKind a b) - NB: Implicitly declared variables come before others. • In the data type declaration for ‘T2’ diff --git a/testsuite/tests/ghci/scripts/T10059.stdout b/testsuite/tests/ghci/scripts/T10059.stdout index 92fbb45ef7..955c95a966 100644 --- a/testsuite/tests/ghci/scripts/T10059.stdout +++ b/testsuite/tests/ghci/scripts/T10059.stdout @@ -1,4 +1,4 @@ -class (a ~ b) => (~) (a :: k0) (b :: k0) -- Defined in ‘GHC.Types’ -(~) :: k0 -> k0 -> Constraint -class (a GHC.Prim.~# b) => (~) (a :: k0) (b :: k0) +class (a ~ b) => (~) (a :: k) (b :: k) -- Defined in ‘GHC.Types’ +(~) :: k -> k -> Constraint +class (a GHC.Prim.~# b) => (~) (a :: k) (b :: k) -- Defined in ‘GHC.Types’ diff --git a/testsuite/tests/ghci/scripts/T15591.hs b/testsuite/tests/ghci/scripts/T15591.hs index f333fe0194..a27f8f0269 100644 --- a/testsuite/tests/ghci/scripts/T15591.hs +++ b/testsuite/tests/ghci/scripts/T15591.hs @@ -13,11 +13,15 @@ class C (a :: Type) where type T2 (x :: f a) class C2 (a :: Type) (b :: Proxy a) (c :: Proxy b) where - type T3 (x :: Proxy '(a, c)) + type T3 (x :: Proxy '(a, (c :: Proxy b))) + -- NB: we have to put (c :: Proxy b) so that 'b' is Specified + -- in the kind of T3; else 'b' is Inferred and comes + -- first, which is ill-scoped -- no CUSK class C3 (a :: Type) (b :: Proxy a) (c :: Proxy b) d where - type T4 (x :: Proxy '(a, c)) + type T4 (x :: Proxy '(a, (c :: Proxy b))) + -- Ditto to T3 class C4 (a :: Type) b where type T5 (x :: f a) diff --git a/testsuite/tests/ghci/scripts/T15591.stdout b/testsuite/tests/ghci/scripts/T15591.stdout index b4673d5174..b0d4f8b34d 100644 --- a/testsuite/tests/ghci/scripts/T15591.stdout +++ b/testsuite/tests/ghci/scripts/T15591.stdout @@ -1,6 +1,6 @@ T1 :: forall (f :: * -> *) a. f a -> * -T2 :: forall a (f :: * -> *). f a -> * +T2 :: forall (f :: * -> *) a. f a -> * T3 :: forall a (b :: Proxy a) (c :: Proxy b). Proxy '(a, c) -> * T4 :: forall a (b :: Proxy a) (c :: Proxy b). Proxy '(a, c) -> * -T5 :: forall a (f :: * -> *). f a -> * -T6 :: forall {k} (a :: k) (f :: k -> *). f a -> * +T5 :: forall (f :: * -> *) a. f a -> * +T6 :: forall {k} (f :: k -> *) (a :: k). f a -> * diff --git a/testsuite/tests/ghci/scripts/T15743b.stdout b/testsuite/tests/ghci/scripts/T15743b.stdout index 03e593e5bd..2850a685fc 100644 --- a/testsuite/tests/ghci/scripts/T15743b.stdout +++ b/testsuite/tests/ghci/scripts/T15743b.stdout @@ -1 +1 @@ -F :: forall k k2. k -> k2 -> * +F :: forall {k} k2. k -> k2 -> * diff --git a/testsuite/tests/ghci/scripts/T6018ghcifail.stderr b/testsuite/tests/ghci/scripts/T6018ghcifail.stderr index 15e19cf105..c6698d2944 100644 --- a/testsuite/tests/ghci/scripts/T6018ghcifail.stderr +++ b/testsuite/tests/ghci/scripts/T6018ghcifail.stderr @@ -39,9 +39,9 @@ <interactive>:55:41: error: Type family equation violates injectivity annotation. - Kind variable ‘k2’ cannot be inferred from the right-hand side. + Kind variable ‘k1’ cannot be inferred from the right-hand side. In the type family equation: - PolyKindVarsF @{[k2]} @[k1] ('[] @k2) = '[] @k1 + PolyKindVarsF @{[k1]} @[k2] ('[] @k1) = '[] @k2 -- Defined at <interactive>:55:41 <interactive>:60:15: error: diff --git a/testsuite/tests/ghci/scripts/T7873.stderr b/testsuite/tests/ghci/scripts/T7873.stderr index 731a216a1a..b4759714c2 100644 --- a/testsuite/tests/ghci/scripts/T7873.stderr +++ b/testsuite/tests/ghci/scripts/T7873.stderr @@ -5,4 +5,4 @@ of its type variables. Perhaps you meant to bind it explicitly somewhere? Type variables with inferred kinds: (k :: *) - • In the data declaration for ‘D1’ + • In the data type declaration for ‘D1’ diff --git a/testsuite/tests/ghci/scripts/ghci059.stdout b/testsuite/tests/ghci/scripts/ghci059.stdout index 9e9adb9ff1..7e734f1ccc 100644 --- a/testsuite/tests/ghci/scripts/ghci059.stdout +++ b/testsuite/tests/ghci/scripts/ghci059.stdout @@ -4,6 +4,6 @@ It is not a class. Please see section 9.14.4 of the user's guide for details. -} type role Coercible representational representational -class Coercible a b => Coercible (a :: k0) (b :: k0) +class Coercible a b => Coercible (a :: k) (b :: k) -- Defined in ‘GHC.Types’ coerce :: Coercible a b => a -> b -- Defined in ‘GHC.Prim’ diff --git a/testsuite/tests/indexed-types/should_compile/T15711.stderr b/testsuite/tests/indexed-types/should_compile/T15711.stderr index 1d23612cfc..2a012489e7 100644 --- a/testsuite/tests/indexed-types/should_compile/T15711.stderr +++ b/testsuite/tests/indexed-types/should_compile/T15711.stderr @@ -1,7 +1,7 @@ TYPE CONSTRUCTORS - C :: * -> Constraint + C{1} :: * -> Constraint type role F nominal nominal - F :: forall a. Maybe a -> * + F{2} :: forall a. Maybe a -> * Dependent modules: [] Dependent packages: [base-4.12.0.0, ghc-prim-0.5.3, integer-gmp-1.0.2.0] diff --git a/testsuite/tests/indexed-types/should_compile/T15740a.hs b/testsuite/tests/indexed-types/should_compile/T15740a.hs new file mode 100644 index 0000000000..2d79a99878 --- /dev/null +++ b/testsuite/tests/indexed-types/should_compile/T15740a.hs @@ -0,0 +1,12 @@ +{-# LANGUAGE TypeInType, RankNTypes, TypeFamilies #-} + +module T15740a where + +import Data.Kind +import Data.Proxy + +type family F2 :: forall k. k -> Type + +-- This should succeed +type instance F2 = Proxy + diff --git a/testsuite/tests/indexed-types/should_compile/T15764a.hs b/testsuite/tests/indexed-types/should_compile/T15764a.hs new file mode 100644 index 0000000000..91d348bd96 --- /dev/null +++ b/testsuite/tests/indexed-types/should_compile/T15764a.hs @@ -0,0 +1,14 @@ +{-# Language PolyKinds #-} +{-# Language TypeFamilies #-} +{-# Language KindSignatures #-} +{-# Language DataKinds #-} +{-# Language MultiParamTypeClasses #-} + +module T15764a where + +import Data.Kind +import Data.Proxy +import GHC.TypeLits + +class C6 (k :: Type) (a :: k) (b :: Proxy (a :: k)) where + type T6 (proxy :: Proxy '(k, (b :: Proxy a))) diff --git a/testsuite/tests/indexed-types/should_compile/T15852.stderr b/testsuite/tests/indexed-types/should_compile/T15852.stderr index bc5fd2a72e..6908d000ab 100644 --- a/testsuite/tests/indexed-types/should_compile/T15852.stderr +++ b/testsuite/tests/indexed-types/should_compile/T15852.stderr @@ -1,13 +1,14 @@ TYPE CONSTRUCTORS type role DF nominal nominal nominal - DF :: forall k. * -> k -> * + DF{3} :: forall k. * -> k -> * COERCION AXIOMS axiom T15852.D:R:DFProxyProxy0 :: - forall k1 k2 (c :: k1) (j :: k2) (a :: Proxy j). - DF (Proxy c) a = T15852.R:DFProxyProxy k1 k2 c j a - -- Defined at T15852.hs:10:15 + forall k1 k2 (j :: k1) (c :: k2). + DF (Proxy c) = T15852.R:DFProxyProxy k1 k2 j c FAMILY INSTANCES - data instance DF (Proxy c) c j a + data instance forall k1 k2 (j :: k1) (c :: k2). + DF (Proxy c) = T15852.R:DFProxyProxy k1 k2 j c + -- Defined at T15852.hs:10:15 Dependent modules: [] Dependent packages: [base-4.12.0.0, ghc-prim-0.5.3, integer-gmp-1.0.2.0] diff --git a/testsuite/tests/indexed-types/should_compile/T3017.stderr b/testsuite/tests/indexed-types/should_compile/T3017.stderr index 3b4361a2a5..9cf31965a4 100644 --- a/testsuite/tests/indexed-types/should_compile/T3017.stderr +++ b/testsuite/tests/indexed-types/should_compile/T3017.stderr @@ -5,19 +5,18 @@ TYPE SIGNATURES test2 :: forall c a b. (Coll c, Num a, Num b, Elem c ~ (a, b)) => c -> c TYPE CONSTRUCTORS - Coll :: * -> Constraint + Coll{1} :: * -> Constraint type role Elem nominal - Elem :: * -> * - ListColl :: * -> * + Elem{1} :: * -> * + ListColl{1} :: * -> * COERCION AXIOMS - axiom Foo.D:R:ElemListColl :: - Elem (ListColl a) = a -- Defined at T3017.hs:13:9 + axiom Foo.D:R:ElemListColl :: Elem (ListColl a) = a DATA CONSTRUCTORS L :: forall a. [a] -> ListColl a CLASS INSTANCES instance Coll (ListColl a) -- Defined at T3017.hs:12:11 FAMILY INSTANCES - type Elem (ListColl a) + type instance Elem (ListColl a) = a -- Defined at T3017.hs:13:9 Dependent modules: [] Dependent packages: [base-4.12.0.0, ghc-prim-0.5.3, integer-gmp-1.0.2.0] diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T index 409e1efce1..484d843672 100644 --- a/testsuite/tests/indexed-types/should_compile/all.T +++ b/testsuite/tests/indexed-types/should_compile/all.T @@ -298,3 +298,5 @@ test('T15943', normal, compile, ['']) test('T15704', normal, compile, ['']) test('T15711', normal, compile, ['-ddump-types']) test('T15852', normal, compile, ['-ddump-types']) +test('T15764a', normal, compile, ['']) +test('T15740a', normal, compile, ['']) diff --git a/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4a.stderr b/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4a.stderr index ecbd7d9e79..776ee19592 100644 --- a/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4a.stderr +++ b/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4a.stderr @@ -1,8 +1,12 @@ ExplicitForAllFams4a.hs:7:12: error: - • Explicitly quantified but not used in LHS pattern: type variable ‘b’ - • In the type family declaration for ‘H’ + • Type variable ‘b’ is bound by a forall, + but not used in the family instance + • In the equations for closed type family ‘H’ + In the type family declaration for ‘H’ ExplicitForAllFams4a.hs:8:10: error: - • Explicitly quantified but not used in LHS pattern: type variable ‘b’ - • In the type family declaration for ‘H’ + • Type variable ‘b’ is mentioned in the RHS, + but not bound on the LHS of the family instance + • In the equations for closed type family ‘H’ + In the type family declaration for ‘H’ diff --git a/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.hs b/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.hs index cb5665401b..c488f45a65 100644 --- a/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.hs +++ b/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.hs @@ -22,5 +22,6 @@ class C a where instance C Int where type forall a b. CT [a] (a,a) = Float type forall b. CT _ _ = Maybe b + data forall a b. CD [a] (a,a) = CD5 Float data forall b. CD _ _ = CD6 (Maybe b) diff --git a/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.stderr b/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.stderr index 0861a8a756..8e268d6301 100644 --- a/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.stderr +++ b/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.stderr @@ -1,44 +1,107 @@ ExplicitForAllFams4b.hs:7:24: error: - • Explicitly quantified but not used in LHS pattern: type variable ‘b’ + • Type variable ‘b’ is bound by a forall, + but not used in the family instance • In the type instance declaration for ‘J’ +ExplicitForAllFams4b.hs:7:27: error: + Conflicting family instance declarations: + J [a] = Float -- Defined at ExplicitForAllFams4b.hs:7:27 + J _ = Maybe b -- Defined at ExplicitForAllFams4b.hs:8:27 + ExplicitForAllFams4b.hs:8:22: error: - • Explicitly quantified but not used in LHS pattern: type variable ‘b’ + • Type variable ‘b’ is mentioned in the RHS, + but not bound on the LHS of the family instance • In the type instance declaration for ‘J’ ExplicitForAllFams4b.hs:11:24: error: - • Explicitly quantified but not used in LHS pattern: type variable ‘b’ + • Type variable ‘b’ is mentioned in the RHS, + but not bound on the LHS of the family instance • In the data instance declaration for ‘K’ +ExplicitForAllFams4b.hs:11:27: error: + Conflicting family instance declarations: + K (a, Bool) -- Defined at ExplicitForAllFams4b.hs:11:27 + K _ -- Defined at ExplicitForAllFams4b.hs:12:27 + ExplicitForAllFams4b.hs:12:22: error: - • Explicitly quantified but not used in LHS pattern: type variable ‘b’ + • Type variable ‘b’ is mentioned in the RHS, + but not bound on the LHS of the family instance • In the data instance declaration for ‘K’ ExplicitForAllFams4b.hs:15:27: error: - • Explicitly quantified but not used in LHS pattern: type variable ‘b’ + • Type variable ‘b’ is mentioned in the RHS, + but not bound on the LHS of the family instance • In the newtype instance declaration for ‘L’ +ExplicitForAllFams4b.hs:15:30: error: + Conflicting family instance declarations: + L (a, Bool) -- Defined at ExplicitForAllFams4b.hs:15:30 + L _ -- Defined at ExplicitForAllFams4b.hs:16:30 + ExplicitForAllFams4b.hs:16:25: error: - • Explicitly quantified but not used in LHS pattern: type variable ‘b’ + • Type variable ‘b’ is mentioned in the RHS, + but not bound on the LHS of the family instance • In the newtype instance declaration for ‘L’ +ExplicitForAllFams4b.hs:23:3: error: + • Type indexes must match class instance head + Expected: CT Int _ + Actual: CT [a] (a, a) -- Defined at ExplicitForAllFams4b.hs:23:20 + • In the type instance declaration for ‘CT’ + In the instance declaration for ‘C Int’ + ExplicitForAllFams4b.hs:23:17: error: - • Explicitly quantified but not used in LHS pattern: type variable ‘b’ + • Type variable ‘b’ is bound by a forall, + but not used in the family instance + • In the type instance declaration for ‘CT’ + In the instance declaration for ‘C Int’ + +ExplicitForAllFams4b.hs:23:20: error: + Conflicting family instance declarations: + CT [a] (a, a) = Float -- Defined at ExplicitForAllFams4b.hs:23:20 + CT _ _ = Maybe b -- Defined at ExplicitForAllFams4b.hs:24:20 + +ExplicitForAllFams4b.hs:24:3: error: + • Type indexes must match class instance head + Expected: CT Int _ + Actual: CT _ _ -- Defined at ExplicitForAllFams4b.hs:24:20 • In the type instance declaration for ‘CT’ In the instance declaration for ‘C Int’ ExplicitForAllFams4b.hs:24:15: error: - • Explicitly quantified but not used in LHS pattern: type variable ‘b’ + • Type variable ‘b’ is mentioned in the RHS, + but not bound on the LHS of the family instance • In the type instance declaration for ‘CT’ In the instance declaration for ‘C Int’ -ExplicitForAllFams4b.hs:25:17: error: - • Explicitly quantified but not used in LHS pattern: type variable ‘b’ +ExplicitForAllFams4b.hs:26:3: error: + • Type indexes must match class instance head + Expected: CD Int _ + Actual: CD [a] (a, a) -- Defined at ExplicitForAllFams4b.hs:26:20 + • In the data instance declaration for ‘CD’ + In the instance declaration for ‘C Int’ + +ExplicitForAllFams4b.hs:26:17: error: + • Type variable ‘b’ is mentioned in the RHS, + but not bound on the LHS of the family instance + • In the data instance declaration for ‘CD’ + In the instance declaration for ‘C Int’ + +ExplicitForAllFams4b.hs:26:20: error: + Conflicting family instance declarations: + CD [a] (a, a) -- Defined at ExplicitForAllFams4b.hs:26:20 + CD _ _ -- Defined at ExplicitForAllFams4b.hs:27:20 + +ExplicitForAllFams4b.hs:27:3: error: + • Type indexes must match class instance head + Expected: CD Int _ + Actual: CD _ _ -- Defined at ExplicitForAllFams4b.hs:27:20 • In the data instance declaration for ‘CD’ In the instance declaration for ‘C Int’ -ExplicitForAllFams4b.hs:26:15: error: - • Explicitly quantified but not used in LHS pattern: type variable ‘b’ +ExplicitForAllFams4b.hs:27:15: error: + • Type variable ‘b’ is mentioned in the RHS, + but not bound on the LHS of the family instance • In the data instance declaration for ‘CD’ In the instance declaration for ‘C Int’ diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail13.stderr b/testsuite/tests/indexed-types/should_fail/SimpleFail13.stderr index cfbab576b9..eb54cf2e11 100644 --- a/testsuite/tests/indexed-types/should_fail/SimpleFail13.stderr +++ b/testsuite/tests/indexed-types/should_fail/SimpleFail13.stderr @@ -1,5 +1,5 @@ -SimpleFail13.hs:9:1: error: +SimpleFail13.hs:9:15: error: • Illegal type synonym family application ‘C a’ in instance: D [C a] • In the data instance declaration for ‘D’ diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail2a.hs b/testsuite/tests/indexed-types/should_fail/SimpleFail2a.hs index fc773af0ff..7d78a15baa 100644 --- a/testsuite/tests/indexed-types/should_fail/SimpleFail2a.hs +++ b/testsuite/tests/indexed-types/should_fail/SimpleFail2a.hs @@ -8,7 +8,7 @@ class C a where type St a :: * instance C Int where - data Sd a :: * -- Looks like a nullary data instance decl + data Sd a = MkSd -- :: * -- Looks like a nullary data instance decl data Sd Int = SdC Char newtype Sn Int = SnC Char type St Int = Char diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail2a.stderr b/testsuite/tests/indexed-types/should_fail/SimpleFail2a.stderr index 9bd571e2b9..b21375ceb2 100644 --- a/testsuite/tests/indexed-types/should_fail/SimpleFail2a.stderr +++ b/testsuite/tests/indexed-types/should_fail/SimpleFail2a.stderr @@ -2,6 +2,11 @@ SimpleFail2a.hs:11:3: error: • Type indexes must match class instance head Expected: Sd Int - Actual: Sd a :: * + Actual: Sd a -- Defined at SimpleFail2a.hs:11:11 • In the data instance declaration for ‘Sd’ In the instance declaration for ‘C Int’ + +SimpleFail2a.hs:11:11: error: + Conflicting family instance declarations: + Sd a -- Defined at SimpleFail2a.hs:11:11 + Sd Int -- Defined at SimpleFail2a.hs:12:11 diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail9.hs b/testsuite/tests/indexed-types/should_fail/SimpleFail9.hs index 9c1c4a82d2..0f20f78e95 100644 --- a/testsuite/tests/indexed-types/should_fail/SimpleFail9.hs +++ b/testsuite/tests/indexed-types/should_fail/SimpleFail9.hs @@ -2,8 +2,10 @@ module ShouldFail where +import Data.Kind + class C7 a b where - data S7 b :: * + data S7 b :: Type instance C7 Char (a, Bool) where data S7 (a, Bool) = S7_1 diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail9.stderr b/testsuite/tests/indexed-types/should_fail/SimpleFail9.stderr index b0c421fce8..b3dd8ef839 100644 --- a/testsuite/tests/indexed-types/should_fail/SimpleFail9.stderr +++ b/testsuite/tests/indexed-types/should_fail/SimpleFail9.stderr @@ -1,7 +1,7 @@ -SimpleFail9.hs:14:3: error: +SimpleFail9.hs:16:3: error: • Type indexes must match class instance head Expected: S7 (a, Int) - Actual: S7 (b, Int) + Actual: S7 (b, Int) -- Defined at SimpleFail9.hs:16:8 • In the data instance declaration for ‘S7’ In the instance declaration for ‘C7 Char (a, Int)’ diff --git a/testsuite/tests/indexed-types/should_fail/T10817.stderr b/testsuite/tests/indexed-types/should_fail/T10817.stderr index 715febdc25..af8acae33a 100644 --- a/testsuite/tests/indexed-types/should_fail/T10817.stderr +++ b/testsuite/tests/indexed-types/should_fail/T10817.stderr @@ -1,6 +1,7 @@ T10817.hs:9:3: error: - The type family application ‘F a’ - is no smaller than the instance head ‘F a’ - (Use UndecidableInstances to permit this) - In the class declaration for ‘C’ + • The type family application ‘F a’ + is no smaller than the instance head ‘F a’ + (Use UndecidableInstances to permit this) + • In the default type instance declaration for ‘F’ + In the class declaration for ‘C’ diff --git a/testsuite/tests/indexed-types/should_fail/T10899.stderr b/testsuite/tests/indexed-types/should_fail/T10899.stderr index 925e4348fe..0dd92ef9bf 100644 --- a/testsuite/tests/indexed-types/should_fail/T10899.stderr +++ b/testsuite/tests/indexed-types/should_fail/T10899.stderr @@ -1,4 +1,5 @@ T10899.hs:7:3: error: • Illegal polymorphic type: forall (m :: * -> *). m a - • In the class declaration for ‘C’ + • In the default type instance declaration for ‘F’ + In the class declaration for ‘C’ diff --git a/testsuite/tests/indexed-types/should_fail/T11450.stderr b/testsuite/tests/indexed-types/should_fail/T11450.stderr index a6fe961fcf..f5be9d48c3 100644 --- a/testsuite/tests/indexed-types/should_fail/T11450.stderr +++ b/testsuite/tests/indexed-types/should_fail/T11450.stderr @@ -1,7 +1,7 @@ -T11450.hs:9:8: error: +T11450.hs:9:3: error: • Type indexes must match class instance head Expected: T (Either a b) - Actual: T (Either b a) + Actual: T (Either b a) -- Defined at T11450.hs:9:8 • In the type instance declaration for ‘T’ In the instance declaration for ‘C (Either a b)’ diff --git a/testsuite/tests/indexed-types/should_fail/T12041.stderr b/testsuite/tests/indexed-types/should_fail/T12041.stderr index 006ca37bae..d16a9cc49c 100644 --- a/testsuite/tests/indexed-types/should_fail/T12041.stderr +++ b/testsuite/tests/indexed-types/should_fail/T12041.stderr @@ -1,7 +1,7 @@ -T12041.hs:12:15: error: - • Expected kind ‘i -> Constraint’, - but ‘(~) Int’ has kind ‘* -> Constraint’ - • In the type ‘(~) Int’ - In the type instance declaration for ‘Ob’ +T12041.hs:12:3: error: + • Type indexes must match class instance head + Expected: Ob @i (I @{i} @{i}) + Actual: Ob @* (I @{*} @{*}) -- Defined at T12041.hs:12:8 + • In the type instance declaration for ‘Ob’ In the instance declaration for ‘Category I’ diff --git a/testsuite/tests/indexed-types/should_fail/T13092/T13092.stderr b/testsuite/tests/indexed-types/should_fail/T13092/T13092.stderr index 9df66e7cd1..c13bde5ad8 100644 --- a/testsuite/tests/indexed-types/should_fail/T13092/T13092.stderr +++ b/testsuite/tests/indexed-types/should_fail/T13092/T13092.stderr @@ -2,4 +2,4 @@ Main.hs:10:15: error: Conflicting family instance declarations: A (a, Y) = Bool -- Defined at Main.hs:10:15 - A (B.X, b) = () -- Defined in ‘B’ + A (B.X, b) = () -- Defined in module B diff --git a/testsuite/tests/indexed-types/should_fail/T13092c/T13092c.stderr b/testsuite/tests/indexed-types/should_fail/T13092c/T13092c.stderr index 6676684ec1..ab714e3ecc 100644 --- a/testsuite/tests/indexed-types/should_fail/T13092c/T13092c.stderr +++ b/testsuite/tests/indexed-types/should_fail/T13092c/T13092c.stderr @@ -2,4 +2,4 @@ T13092c_4.hs:7:15: error: Conflicting family instance declarations: F (a, Char) = String -- Defined at T13092c_4.hs:7:15 - F (T13092c_2.X, b) = Bool -- Defined in ‘T13092c_2’ + F (T13092c_2.X, b) = Bool -- Defined in module T13092c_2 diff --git a/testsuite/tests/indexed-types/should_fail/T13972.hs b/testsuite/tests/indexed-types/should_fail/T13972.hs index a0a203d30a..9a5af411e2 100644 --- a/testsuite/tests/indexed-types/should_fail/T13972.hs +++ b/testsuite/tests/indexed-types/should_fail/T13972.hs @@ -8,5 +8,11 @@ import Data.Kind class C (a :: k) where type T k :: Type +-- This used to fail, with a mysterious error messate +-- Type indexes must match class instance head +-- Expected: T (a1 -> Either a1 b1) +-- Actual: T (a -> Either a b) +-- but now it succeeds fine + instance C Left where type T (a -> Either a b) = Int diff --git a/testsuite/tests/indexed-types/should_fail/T13972.stderr b/testsuite/tests/indexed-types/should_fail/T13972.stderr deleted file mode 100644 index b1f05b3105..0000000000 --- a/testsuite/tests/indexed-types/should_fail/T13972.stderr +++ /dev/null @@ -1,7 +0,0 @@ - -T13972.hs:12:8: error: - • Type indexes must match class instance head - Expected: T (a1 -> Either a1 b1) - Actual: T (a -> Either a b) - • In the type instance declaration for ‘T’ - In the instance declaration for ‘C Left’ diff --git a/testsuite/tests/indexed-types/should_fail/T14045a.hs b/testsuite/tests/indexed-types/should_fail/T14045a.hs index fc545a8d41..985220c472 100644 --- a/testsuite/tests/indexed-types/should_fail/T14045a.hs +++ b/testsuite/tests/indexed-types/should_fail/T14045a.hs @@ -7,6 +7,11 @@ import Data.Kind class C (a :: k) where data S (a :: k) +-- This used to fail with the mysterious error +-- Type indexes must match class instance head +-- Expected: S z +-- Actual: S a +-- But now it is fine instance C (z :: Bool) where data S :: Bool -> Type where SF :: S False diff --git a/testsuite/tests/indexed-types/should_fail/T14045a.stderr b/testsuite/tests/indexed-types/should_fail/T14045a.stderr deleted file mode 100644 index 0306bd2a07..0000000000 --- a/testsuite/tests/indexed-types/should_fail/T14045a.stderr +++ /dev/null @@ -1,7 +0,0 @@ - -T14045a.hs:11:3: error: - • Type indexes must match class instance head - Expected: S z - Actual: S :: Bool -> Type - • In the data instance declaration for ‘S’ - In the instance declaration for ‘C (z :: Bool)’ diff --git a/testsuite/tests/indexed-types/should_fail/T14179.stderr b/testsuite/tests/indexed-types/should_fail/T14179.stderr index 38d77f1cca..bb956c7b51 100644 --- a/testsuite/tests/indexed-types/should_fail/T14179.stderr +++ b/testsuite/tests/indexed-types/should_fail/T14179.stderr @@ -6,8 +6,8 @@ T14179.hs:7:15: error: T14179.hs:11:15: error: Conflicting family instance declarations: - Foo2 a -- Defined at T14179.hs:11:15 - Foo2 a -- Defined at T14179.hs:12:15 + Foo2 -- Defined at T14179.hs:11:15 + Foo2 -- Defined at T14179.hs:12:15 T14179.hs:15:15: error: Conflicting family instance declarations: diff --git a/testsuite/tests/indexed-types/should_fail/T14887.hs b/testsuite/tests/indexed-types/should_fail/T14887.hs new file mode 100644 index 0000000000..63fbbd3943 --- /dev/null +++ b/testsuite/tests/indexed-types/should_fail/T14887.hs @@ -0,0 +1,14 @@ +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeInType #-} +{-# LANGUAGE TypeOperators #-} +{-# OPTIONS_GHC -fprint-explicit-kinds #-} +module T14887 where + +import Data.Kind +import Data.Type.Equality + +type family Foo1 (e :: (a :: k) :~: (a :: k)) :: Type where + Foo1 (e :: a :~: a) = a :~: a + +type family Foo2 (k :: Type) (e :: (a :: k) :~: (a :: k)) :: Type where + Foo2 k (e :: a :~: a) = a :~: a diff --git a/testsuite/tests/indexed-types/should_fail/T14887.stderr b/testsuite/tests/indexed-types/should_fail/T14887.stderr new file mode 100644 index 0000000000..56875a7628 --- /dev/null +++ b/testsuite/tests/indexed-types/should_fail/T14887.stderr @@ -0,0 +1,12 @@ + +T14887.hs:13:1: error: + • The kind of ‘Foo2’ is ill-scoped + Inferred kind: Foo2 :: forall (a :: k). forall k -> (a :~: a) -> * + NB: Specified variables (namely: (a :: k)) always come first + Perhaps try this order instead: k (a :: k) (e :: a :~: a) + • In the type family declaration for ‘Foo2’ + +T14887.hs:14:11: error: + • Expected kind ‘a0 :~: a0’, but ‘e :: a :~: a’ has kind ‘a :~: a’ + • In the second argument of ‘Foo2’, namely ‘(e :: a :~: a)’ + In the type family declaration for ‘Foo2’ diff --git a/testsuite/tests/indexed-types/should_fail/T15740.hs b/testsuite/tests/indexed-types/should_fail/T15740.hs new file mode 100644 index 0000000000..e564a87509 --- /dev/null +++ b/testsuite/tests/indexed-types/should_fail/T15740.hs @@ -0,0 +1,12 @@ +{-# LANGUAGE TypeInType, TypeFamilies, KindSignatures, RankNTypes #-} + +module T15740 where + +import Data.Kind + +type family F2 :: forall k. k -> Type +data SBool :: Bool -> Type +data Nat +data SNat :: Nat -> Type +type instance F2 = SBool +type instance F2 = SNat diff --git a/testsuite/tests/indexed-types/should_fail/T15740.stderr b/testsuite/tests/indexed-types/should_fail/T15740.stderr new file mode 100644 index 0000000000..9d7cdcfee7 --- /dev/null +++ b/testsuite/tests/indexed-types/should_fail/T15740.stderr @@ -0,0 +1,11 @@ + +T15740.hs:11:20: error: + • Expected kind ‘forall k. k -> *’, + but ‘SBool’ has kind ‘Bool -> *’ + • In the type ‘SBool’ + In the type instance declaration for ‘F2’ + +T15740.hs:12:20: error: + • Expected kind ‘forall k. k -> *’, but ‘SNat’ has kind ‘Nat -> *’ + • In the type ‘SNat’ + In the type instance declaration for ‘F2’ diff --git a/testsuite/tests/indexed-types/should_fail/T15764.hs b/testsuite/tests/indexed-types/should_fail/T15764.hs new file mode 100644 index 0000000000..f4c164cd05 --- /dev/null +++ b/testsuite/tests/indexed-types/should_fail/T15764.hs @@ -0,0 +1,14 @@ +{-# Language PolyKinds #-} +{-# Language TypeFamilies #-} +{-# Language KindSignatures #-} +{-# Language DataKinds #-} +{-# Language MultiParamTypeClasses #-} + +module T15764 where + +import Data.Kind +import Data.Proxy +import GHC.TypeLits + +class C6 (k :: Type) (a :: k) (b :: Proxy (a :: k)) where + type T6 (proxy :: Proxy '(k, b)) diff --git a/testsuite/tests/indexed-types/should_fail/T15764.stderr b/testsuite/tests/indexed-types/should_fail/T15764.stderr new file mode 100644 index 0000000000..5c04427841 --- /dev/null +++ b/testsuite/tests/indexed-types/should_fail/T15764.stderr @@ -0,0 +1,11 @@ + +T15764.hs:14:2: error: + • The kind of ‘T6’ is ill-scoped + Inferred kind: T6 :: forall (a :: k) k (b :: Proxy a). + Proxy '(k, b) -> * + NB: Inferred variables + (namely: (a :: k)) always come first + then Specified variables (namely: k (b :: Proxy a)) + Perhaps try this order instead: + k (a :: k) (b :: Proxy a) (proxy :: Proxy '(k, b)) + • In the associated type family declaration for ‘T6’ diff --git a/testsuite/tests/indexed-types/should_fail/T15870.hs b/testsuite/tests/indexed-types/should_fail/T15870.hs new file mode 100644 index 0000000000..0a07c3e5e5 --- /dev/null +++ b/testsuite/tests/indexed-types/should_fail/T15870.hs @@ -0,0 +1,32 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} + +module T15870 where + +data Optic a where + --Index :: Nat -> Optic a + --Name :: Symbol -> Optic a + (:.:) :: Optic a -> Optic b -> Optic a -- composition + +class Gettable a (optic :: Optic a) where + type Get a (optic :: Optic a) + +{- +some basic instances, e.g. +instance Gettable (a,b) (Index 0) where + type Get (a,b) (Index 0) = a +... +-} + +instance forall a b (g1 :: Optic a) (g2 :: Optic b). + ( Gettable a g1 + , b ~ Get a g1 + , Gettable b g2 + ) => Gettable a (g1 :.: g2) where + type Get a (g1 :.: g2) = Get a g2 diff --git a/testsuite/tests/indexed-types/should_fail/T15870.stderr b/testsuite/tests/indexed-types/should_fail/T15870.stderr new file mode 100644 index 0000000000..4acacbab50 --- /dev/null +++ b/testsuite/tests/indexed-types/should_fail/T15870.stderr @@ -0,0 +1,6 @@ + +T15870.hs:32:34: error: + • Expected kind ‘Optic a’, but ‘g2’ has kind ‘Optic b’ + • In the second argument of ‘Get’, namely ‘g2’ + In the type ‘Get a g2’ + In the type instance declaration for ‘Get’ diff --git a/testsuite/tests/indexed-types/should_fail/T7536.stderr b/testsuite/tests/indexed-types/should_fail/T7536.stderr index 9e7ed3010e..22c565be62 100644 --- a/testsuite/tests/indexed-types/should_fail/T7536.stderr +++ b/testsuite/tests/indexed-types/should_fail/T7536.stderr @@ -1,5 +1,6 @@ -T7536.hs:8:15: - Family instance purports to bind type variable ‘a’ - but the real LHS (expanding synonyms) is: TF Int = ... - In the type instance declaration for ‘TF’ +T7536.hs:8:21: error: + • Type variable ‘a’ is mentioned in the RHS, + but not bound on the LHS of the family instance + The real LHS (expanding synonyms) is: TF Int + • In the type instance declaration for ‘TF’ diff --git a/testsuite/tests/indexed-types/should_fail/T7938.hs b/testsuite/tests/indexed-types/should_fail/T7938.hs index 405a7e54d0..246015ddf7 100644 --- a/testsuite/tests/indexed-types/should_fail/T7938.hs +++ b/testsuite/tests/indexed-types/should_fail/T7938.hs @@ -9,4 +9,4 @@ class Foo (a :: k1) (b :: k2) where type Bar a instance Foo (a :: k1) (b :: k2) where - type Bar a = (KP :: KProxy k2)
\ No newline at end of file + type Bar a = (KP :: KProxy k2) diff --git a/testsuite/tests/indexed-types/should_fail/T7938.stderr b/testsuite/tests/indexed-types/should_fail/T7938.stderr index 890be7b7b8..5751c4e992 100644 --- a/testsuite/tests/indexed-types/should_fail/T7938.stderr +++ b/testsuite/tests/indexed-types/should_fail/T7938.stderr @@ -1,6 +1,6 @@ T7938.hs:12:17: error: - • Expected a type, but ‘KP :: KProxy k2’ has kind ‘KProxy k4’ + • Expected a type, but ‘KP :: KProxy k2’ has kind ‘KProxy k2’ • In the type ‘(KP :: KProxy k2)’ In the type instance declaration for ‘Bar’ In the instance declaration for ‘Foo (a :: k1) (b :: k2)’ diff --git a/testsuite/tests/indexed-types/should_fail/T9160.stderr b/testsuite/tests/indexed-types/should_fail/T9160.stderr index 4ed166cfdb..36a1cb6767 100644 --- a/testsuite/tests/indexed-types/should_fail/T9160.stderr +++ b/testsuite/tests/indexed-types/should_fail/T9160.stderr @@ -1,7 +1,7 @@ -T9160.hs:19:12: error: - Expecting one more argument to ‘Maybe’ - Expected a type, but ‘Maybe’ has kind ‘* -> *’ - In the type ‘Maybe’ - In the type instance declaration for ‘F’ - In the instance declaration for ‘C (a :: *)’ +T9160.hs:19:3: error: + • Type indexes must match class instance head + Expected: F @* + Actual: F @(* -> *) -- Defined at T9160.hs:19:8 + • In the type instance declaration for ‘F’ + In the instance declaration for ‘C (a :: *)’ diff --git a/testsuite/tests/indexed-types/should_fail/all.T b/testsuite/tests/indexed-types/should_fail/all.T index 12fa999a9f..6273f595b0 100644 --- a/testsuite/tests/indexed-types/should_fail/all.T +++ b/testsuite/tests/indexed-types/should_fail/all.T @@ -139,12 +139,16 @@ test('T13271', normal, compile_fail, ['']) test('T13674', normal, compile_fail, ['']) test('T13784', normal, compile_fail, ['']) test('T13877', normal, compile_fail, ['']) -test('T13972', normal, compile_fail, ['']) +test('T13972', normal, compile, ['']) test('T14033', normal, compile_fail, ['']) -test('T14045a', normal, compile_fail, ['']) +test('T14045a', normal, compile, ['']) test('T14175', normal, compile_fail, ['']) test('T14179', normal, compile_fail, ['']) test('T14246', normal, compile_fail, ['']) test('T14369', normal, compile_fail, ['']) test('T15172', normal, compile_fail, ['']) test('T14904', normal, compile_fail, ['']) +test('T15740', normal, compile_fail, ['']) +test('T15764', normal, compile_fail, ['']) +test('T15870', normal, compile_fail, ['']) +test('T14887', normal, compile_fail, ['']) diff --git a/testsuite/tests/partial-sigs/should_compile/ADT.stderr b/testsuite/tests/partial-sigs/should_compile/ADT.stderr index 0569722f24..385a44b737 100644 --- a/testsuite/tests/partial-sigs/should_compile/ADT.stderr +++ b/testsuite/tests/partial-sigs/should_compile/ADT.stderr @@ -1,7 +1,7 @@ TYPE SIGNATURES bar :: Int -> Foo Bool () Int TYPE CONSTRUCTORS - Foo :: * -> * -> * -> * + Foo{3} :: * -> * -> * -> * DATA CONSTRUCTORS Foo :: forall x y z. x -> y -> z -> Foo x y z Dependent modules: [] diff --git a/testsuite/tests/partial-sigs/should_compile/DataFamilyInstanceLHS.stderr b/testsuite/tests/partial-sigs/should_compile/DataFamilyInstanceLHS.stderr index 12982a740c..6f68f3cd66 100644 --- a/testsuite/tests/partial-sigs/should_compile/DataFamilyInstanceLHS.stderr +++ b/testsuite/tests/partial-sigs/should_compile/DataFamilyInstanceLHS.stderr @@ -1,20 +1,20 @@ TYPE SIGNATURES foo :: Sing 'A TYPE CONSTRUCTORS - MyKind :: * + MyKind{0} :: * type role Sing nominal nominal - Sing :: forall k. k -> * + Sing{2} :: forall k. k -> * COERCION AXIOMS axiom DataFamilyInstanceLHS.D:R:SingMyKind_0 :: - Sing _1 = DataFamilyInstanceLHS.R:SingMyKind_ _1 - -- Defined at DataFamilyInstanceLHS.hs:8:15 + Sing = DataFamilyInstanceLHS.R:SingMyKind_ DATA CONSTRUCTORS A :: MyKind B :: MyKind SingA :: Sing 'A SingB :: Sing 'B FAMILY INSTANCES - data instance Sing + data instance Sing _ = DataFamilyInstanceLHS.R:SingMyKind_ _ + -- Defined at DataFamilyInstanceLHS.hs:8:15 Dependent modules: [] Dependent packages: [base-4.12.0.0, ghc-prim-0.5.3, integer-gmp-1.0.2.0] diff --git a/testsuite/tests/partial-sigs/should_compile/Meltdown.stderr b/testsuite/tests/partial-sigs/should_compile/Meltdown.stderr index 750a951222..a40ecfeee0 100644 --- a/testsuite/tests/partial-sigs/should_compile/Meltdown.stderr +++ b/testsuite/tests/partial-sigs/should_compile/Meltdown.stderr @@ -5,7 +5,7 @@ TYPE SIGNATURES NukeMonad param1 param2 () -> NukeMonad param1 param2 () TYPE CONSTRUCTORS type role NukeMonad phantom phantom phantom - NukeMonad :: * -> * -> * -> * + NukeMonad{3} :: * -> * -> * -> * CLASS INSTANCES instance Functor (NukeMonad a b) -- Defined at Meltdown.hs:8:10 instance Applicative (NukeMonad a b) diff --git a/testsuite/tests/partial-sigs/should_compile/NamedWildcardInDataFamilyInstanceLHS.stderr b/testsuite/tests/partial-sigs/should_compile/NamedWildcardInDataFamilyInstanceLHS.stderr index 1cd0417e54..94245d6aa2 100644 --- a/testsuite/tests/partial-sigs/should_compile/NamedWildcardInDataFamilyInstanceLHS.stderr +++ b/testsuite/tests/partial-sigs/should_compile/NamedWildcardInDataFamilyInstanceLHS.stderr @@ -1,11 +1,10 @@ TYPE CONSTRUCTORS - MyKind :: * + MyKind{0} :: * type role Sing nominal nominal - Sing :: forall k. k -> * + Sing{2} :: forall k. k -> * COERCION AXIOMS axiom NamedWildcardInDataFamilyInstanceLHS.D:R:SingMyKind_a0 :: - Sing _a = NamedWildcardInDataFamilyInstanceLHS.R:SingMyKind_a _a - -- Defined at NamedWildcardInDataFamilyInstanceLHS.hs:8:15 + Sing = NamedWildcardInDataFamilyInstanceLHS.R:SingMyKind_a DATA CONSTRUCTORS A :: MyKind B :: MyKind @@ -13,6 +12,8 @@ DATA CONSTRUCTORS SingB :: Sing 'B FAMILY INSTANCES data instance Sing + _a = NamedWildcardInDataFamilyInstanceLHS.R:SingMyKind_a _a + -- Defined at NamedWildcardInDataFamilyInstanceLHS.hs:8:15 Dependent modules: [] Dependent packages: [base-4.12.0.0, ghc-prim-0.5.3, integer-gmp-1.0.2.0] diff --git a/testsuite/tests/partial-sigs/should_compile/NamedWildcardInTypeFamilyInstanceLHS.stderr b/testsuite/tests/partial-sigs/should_compile/NamedWildcardInTypeFamilyInstanceLHS.stderr index 0554f0a6e7..5a709fff9d 100644 --- a/testsuite/tests/partial-sigs/should_compile/NamedWildcardInTypeFamilyInstanceLHS.stderr +++ b/testsuite/tests/partial-sigs/should_compile/NamedWildcardInTypeFamilyInstanceLHS.stderr @@ -1,10 +1,8 @@ TYPE CONSTRUCTORS type role F nominal - F :: * -> * + F{1} :: * -> * COERCION AXIOMS - axiom NamedWildcardInTypeFamilyInstanceLHS.D:R:F :: - F _t = Int - -- Defined at NamedWildcardInTypeFamilyInstanceLHS.hs:5:3 + axiom NamedWildcardInTypeFamilyInstanceLHS.D:R:F :: F _t = Int Dependent modules: [] Dependent packages: [base-4.12.0.0, ghc-prim-0.5.3, integer-gmp-1.0.2.0] diff --git a/testsuite/tests/partial-sigs/should_compile/SkipMany.stderr b/testsuite/tests/partial-sigs/should_compile/SkipMany.stderr index a821a6970a..0ee0a34564 100644 --- a/testsuite/tests/partial-sigs/should_compile/SkipMany.stderr +++ b/testsuite/tests/partial-sigs/should_compile/SkipMany.stderr @@ -4,7 +4,7 @@ TYPE SIGNATURES skipMany' :: forall tok st a. GenParser tok st a -> GenParser tok st () TYPE CONSTRUCTORS - GenParser :: * -> * -> * -> * + GenParser{3} :: * -> * -> * -> * DATA CONSTRUCTORS GenParser :: forall tok st a. tok -> st -> a -> GenParser tok st a Dependent modules: [] diff --git a/testsuite/tests/partial-sigs/should_compile/TypeFamilyInstanceLHS.stderr b/testsuite/tests/partial-sigs/should_compile/TypeFamilyInstanceLHS.stderr index ae82437e1d..8f24ba1384 100644 --- a/testsuite/tests/partial-sigs/should_compile/TypeFamilyInstanceLHS.stderr +++ b/testsuite/tests/partial-sigs/should_compile/TypeFamilyInstanceLHS.stderr @@ -2,15 +2,15 @@ TYPE SIGNATURES foo :: F Int Char -> Int TYPE CONSTRUCTORS type role F nominal nominal - F :: * -> * -> * + F{2} :: * -> * -> * COERCION AXIOMS - axiom TypeFamilyInstanceLHS.D:R:FBool_1 :: - F Bool _1 = Bool -- Defined at TypeFamilyInstanceLHS.hs:8:15 - axiom TypeFamilyInstanceLHS.D:R:FInt_1 :: - F Int _1 = Int -- Defined at TypeFamilyInstanceLHS.hs:7:15 + axiom TypeFamilyInstanceLHS.D:R:FBool_1 :: F Bool _1 = Bool + axiom TypeFamilyInstanceLHS.D:R:FInt_1 :: F Int _1 = Int FAMILY INSTANCES - type instance F Int _1 - type instance F Bool _1 + type instance F Int _ = Int + -- Defined at TypeFamilyInstanceLHS.hs:7:15 + type instance F Bool _ = Bool + -- Defined at TypeFamilyInstanceLHS.hs:8:15 Dependent modules: [] Dependent packages: [base-4.12.0.0, ghc-prim-0.5.3, integer-gmp-1.0.2.0] diff --git a/testsuite/tests/partial-sigs/should_fail/T14040a.stderr b/testsuite/tests/partial-sigs/should_fail/T14040a.stderr index 20a0fa51ca..67fae7b31e 100644 --- a/testsuite/tests/partial-sigs/should_fail/T14040a.stderr +++ b/testsuite/tests/partial-sigs/should_fail/T14040a.stderr @@ -1,10 +1,10 @@ T14040a.hs:34:8: error: - • Cannot apply expression of type ‘Sing wl - -> (forall y. p w0 'WeirdNil) + • Cannot apply expression of type ‘Sing wl0 + -> (forall y. p0 w0 'WeirdNil) -> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList z1)). - Sing x -> Sing xs -> p w1 xs -> p w2 ('WeirdCons x xs)) - -> p w3 wl’ + Sing x -> Sing xs -> p0 w1 xs -> p0 w2 ('WeirdCons x xs)) + -> p0 w3 wl0’ to a visible type argument ‘(WeirdList z)’ • In the sixth argument of ‘pWeirdCons’, namely ‘(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)’ diff --git a/testsuite/tests/polykinds/T11203.stderr b/testsuite/tests/polykinds/T11203.stderr index 5d62e00304..f5c72133ae 100644 --- a/testsuite/tests/polykinds/T11203.stderr +++ b/testsuite/tests/polykinds/T11203.stderr @@ -1,4 +1,4 @@ T11203.hs:7:24: error: • Couldn't match ‘k1’ with ‘k2’ - • In the data declaration for ‘Q’ + • In the data type declaration for ‘Q’ diff --git a/testsuite/tests/polykinds/T11821a.stderr b/testsuite/tests/polykinds/T11821a.stderr index 2e443e637b..f55c703524 100644 --- a/testsuite/tests/polykinds/T11821a.stderr +++ b/testsuite/tests/polykinds/T11821a.stderr @@ -1,4 +1,4 @@ T11821a.hs:4:31: error: • Couldn't match ‘k1’ with ‘k2’ - • In the type declaration for ‘SameKind’ + • In the type synonym declaration for ‘SameKind’ diff --git a/testsuite/tests/polykinds/T12593.stderr b/testsuite/tests/polykinds/T12593.stderr index 27123a8bc8..e150299ea1 100644 --- a/testsuite/tests/polykinds/T12593.stderr +++ b/testsuite/tests/polykinds/T12593.stderr @@ -92,8 +92,8 @@ T12593.hs:14:6: error: • In the pattern: Free cat In an equation for ‘run’: run (Free cat) = cat • Relevant bindings include - run :: Free k6 k7 k8 p a b - -> (forall (c :: k6) (d :: k7). p c d -> q c d) -> q a b + run :: Free k k4 k8 p a b + -> (forall (c :: k) (d :: k4). p c d -> q c d) -> q a b (bound at T12593.hs:14:1) T12593.hs:14:18: error: @@ -111,6 +111,6 @@ T12593.hs:14:18: error: k2 q => (forall (c :: k0) (d :: k1). p0 c d -> q c d) -> q a b (bound at T12593.hs:14:11) - run :: Free k6 k7 k8 p a b - -> (forall (c :: k6) (d :: k7). p c d -> q c d) -> q a b + run :: Free k k4 k8 p a b + -> (forall (c :: k) (d :: k4). p c d -> q c d) -> q a b (bound at T12593.hs:14:1) diff --git a/testsuite/tests/polykinds/T13985.hs b/testsuite/tests/polykinds/T13985.hs index c0555d8f69..6a844b366e 100644 --- a/testsuite/tests/polykinds/T13985.hs +++ b/testsuite/tests/polykinds/T13985.hs @@ -1,5 +1,6 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeFamilies #-} diff --git a/testsuite/tests/polykinds/T13985.stderr b/testsuite/tests/polykinds/T13985.stderr index f60314a443..2df92c34da 100644 --- a/testsuite/tests/polykinds/T13985.stderr +++ b/testsuite/tests/polykinds/T13985.stderr @@ -1,39 +1,28 @@ -T13985.hs:12:1: error: - • Kind variable ‘k’ is implicitly bound in data family - ‘Fam’, but does not appear as the kind of any - of its type variables. Perhaps you meant - to bind it explicitly somewhere? +T13985.hs:13:41: error: + • Type variable ‘k’ is mentioned in the RHS, + but not bound on the LHS of the family instance • In the data instance declaration for ‘Fam’ -T13985.hs:15:15: error: - • Kind variable ‘a’ is implicitly bound in type family - ‘T’, but does not appear as the kind of any - of its type variables. Perhaps you meant - to bind it explicitly somewhere? +T13985.hs:16:43: error: + • Type variable ‘a’ is mentioned in the RHS, + but not bound on the LHS of the family instance • In the type instance declaration for ‘T’ -T13985.hs:22:3: error: - • Kind variable ‘k’ is implicitly bound in associated data family - ‘CD’, but does not appear as the kind of any - of its type variables. Perhaps you meant - to bind it explicitly somewhere? +T13985.hs:23:26: error: + • Type variable ‘k’ is mentioned in the RHS, + but not bound on the LHS of the family instance • In the data instance declaration for ‘CD’ In the instance declaration for ‘C Type’ -T13985.hs:23:8: error: - • Kind variable ‘a’ is implicitly bound in associated type family - ‘CT’, but does not appear as the kind of any - of its type variables. Perhaps you meant - to bind it explicitly somewhere? +T13985.hs:24:37: error: + • Type variable ‘a’ is mentioned in the RHS, + but not bound on the LHS of the family instance • In the type instance declaration for ‘CT’ In the instance declaration for ‘C Type’ -T13985.hs:27:3: error: - • Kind variable ‘x’ is implicitly bound in associated type family - ‘ZT’, but does not appear as the kind of any - of its type variables. Perhaps you meant - to bind it explicitly somewhere? - Type variables with inferred kinds: (k :: *) (a :: k) +T13985.hs:28:39: error: + • Type variable ‘x’ is mentioned in the RHS, + but not bound on the LHS of the family instance • In the default type instance declaration for ‘ZT’ In the class declaration for ‘Z’ diff --git a/testsuite/tests/polykinds/T14450.stderr b/testsuite/tests/polykinds/T14450.stderr index 8a987b7a56..107f4aa2ce 100644 --- a/testsuite/tests/polykinds/T14450.stderr +++ b/testsuite/tests/polykinds/T14450.stderr @@ -1,8 +1,7 @@ -T14450.hs:33:13: error: - • Expected kind ‘k ~> k’, - but ‘IddSym0 :: Type ~> Type’ has kind ‘* ~> *’ - • In the first argument of ‘Dom’, namely - ‘(IddSym0 :: Type ~> Type)’ - In the type instance declaration for ‘Dom’ +T14450.hs:33:3: error: + • Type indexes must match class instance head + Expected: Dom @k @k (IddSym0 @k) + Actual: Dom @* @* (IddSym0 @*) -- Defined at T14450.hs:33:8 + • In the type instance declaration for ‘Dom’ In the instance declaration for ‘Varpi (IddSym0 :: k ~> k)’ diff --git a/testsuite/tests/polykinds/T14846.stderr b/testsuite/tests/polykinds/T14846.stderr index 062dc49e1f..43d81c5e1e 100644 --- a/testsuite/tests/polykinds/T14846.stderr +++ b/testsuite/tests/polykinds/T14846.stderr @@ -3,12 +3,8 @@ T14846.hs:38:8: error: • Couldn't match type ‘ríki’ with ‘Hom riki’ ‘ríki’ is a rigid type variable bound by the type signature for: - i :: forall k5 k6 (cls2 :: k6 - -> Constraint) (xx :: k5) (a :: Struct cls2) (ríki :: Struct - cls2 - -> Struct - cls2 - -> *). + i :: forall k5 k6 (cls2 :: k6 -> Constraint) (xx :: k5) + (a :: Struct cls2) (ríki :: Struct cls2 -> Struct cls2 -> *). StructI xx a => ríki a a at T14846.hs:38:8-48 @@ -16,21 +12,31 @@ T14846.hs:38:8: error: Actual type: Hom riki a a • When checking that instance signature for ‘i’ is more general than its signature in the class - Instance sig: forall k1 k2 (cls :: k2 - -> Constraint) (xx :: k1) (a :: Struct cls). + Instance sig: forall k1 k2 (cls :: k2 -> Constraint) (xx :: k1) + (a :: Struct cls). StructI xx a => Hom riki a a - Class sig: forall k1 k2 (cls :: k2 - -> Constraint) (xx :: k1) (a :: Struct - cls) (ríki :: Struct - cls - -> Struct - cls - -> *). + Class sig: forall k1 k2 (cls :: k2 -> Constraint) (xx :: k1) + (a :: Struct cls) (ríki :: Struct cls -> Struct cls -> *). StructI xx a => ríki a a In the instance declaration for ‘Category (Hom riki)’ +T14846.hs:39:12: error: + • Couldn't match kind ‘k3’ with ‘Struct cls2’ + ‘k3’ is a rigid type variable bound by + the instance declaration + at T14846.hs:37:10-65 + When matching kinds + cls0 :: Struct cls -> Constraint + cls1 :: k3 -> Constraint + • In the expression: struct :: AStruct (Structured a cls) + In the expression: case struct :: AStruct (Structured a cls) of + In an equation for ‘i’: + i = case struct :: AStruct (Structured a cls) of + • Relevant bindings include + i :: Hom riki a a (bound at T14846.hs:39:3) + T14846.hs:39:31: error: • Couldn't match kind ‘k3’ with ‘Struct cls2’ ‘k3’ is a rigid type variable bound by diff --git a/testsuite/tests/polykinds/T14887a.hs b/testsuite/tests/polykinds/T14887a.hs new file mode 100644 index 0000000000..2e5cf02212 --- /dev/null +++ b/testsuite/tests/polykinds/T14887a.hs @@ -0,0 +1,16 @@ +{-# LANGUAGE PartialTypeSignatures #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeInType #-} +{-# OPTIONS_GHC -Wno-partial-type-signatures -Wno-implicit-kind-vars #-} +module Bug where + +import Data.Proxy + +f1 :: forall (x :: a). Proxy (x :: _) +-- This one has an implicitly-quantified kind var 'a', which +-- we will stop accepting in the future, under the forall-or-nothing +-- rule. Hence -Wno-implicit-kind-vars +f1 = Proxy + +f2 :: forall a (x :: a). Proxy (x :: _) +f2 = Proxy diff --git a/testsuite/tests/polykinds/T14887a.stderr b/testsuite/tests/polykinds/T14887a.stderr new file mode 100644 index 0000000000..0519ecba6e --- /dev/null +++ b/testsuite/tests/polykinds/T14887a.stderr @@ -0,0 +1 @@ +
\ No newline at end of file diff --git a/testsuite/tests/polykinds/T15592.stderr b/testsuite/tests/polykinds/T15592.stderr index c1b823e738..4086c12bf6 100644 --- a/testsuite/tests/polykinds/T15592.stderr +++ b/testsuite/tests/polykinds/T15592.stderr @@ -1,6 +1,6 @@ TYPE CONSTRUCTORS type role T nominal nominal representational nominal nominal - T :: forall {k} k1. (k1 -> k -> *) -> k1 -> k -> * + T{5} :: forall {k} k1. (k1 -> k -> *) -> k1 -> k -> * DATA CONSTRUCTORS MkT :: forall {k} k1 (f :: k1 -> k -> *) (a :: k1) (b :: k). f a b -> T f a b -> T f a b diff --git a/testsuite/tests/polykinds/T15592b.stderr b/testsuite/tests/polykinds/T15592b.stderr index c51416f4c5..d07b3a1ac7 100644 --- a/testsuite/tests/polykinds/T15592b.stderr +++ b/testsuite/tests/polykinds/T15592b.stderr @@ -1,7 +1,7 @@ TYPE CONSTRUCTORS - C :: forall {k}. k -> Constraint + C{2} :: forall {k}. k -> Constraint type role T nominal nominal nominal nominal - T :: forall {k} (a :: k) (f :: k -> *). f a -> * + T{4} :: forall k (f :: k -> *) (a :: k). f a -> * Dependent modules: [] Dependent packages: [base-4.12.0.0, ghc-prim-0.5.3, integer-gmp-1.0.2.0] diff --git a/testsuite/tests/polykinds/T15789.hs b/testsuite/tests/polykinds/T15789.hs new file mode 100644 index 0000000000..6465da2a9b --- /dev/null +++ b/testsuite/tests/polykinds/T15789.hs @@ -0,0 +1,10 @@ +{-# Language LiberalTypeSynonyms #-} +{-# Language PolyKinds #-} +{-# Language RankNTypes #-} +{-# Language DataKinds #-} + +import Data.Kind + +type Cat ob = ob -> ob -> Type + +data Zero :: forall (cat :: forall xx. xx -> Type) a. forall b. Cat (forall b. cat b u) diff --git a/testsuite/tests/polykinds/T15789.stderr b/testsuite/tests/polykinds/T15789.stderr new file mode 100644 index 0000000000..c0fd4eab34 --- /dev/null +++ b/testsuite/tests/polykinds/T15789.stderr @@ -0,0 +1,6 @@ + +T15789.hs:10:80: error: + • Expected kind ‘k2 -> *’, but ‘cat b’ has kind ‘*’ + • In the first argument of ‘Cat’, namely ‘(forall b. cat b u)’ + In the kind ‘forall (cat :: forall xx. xx -> Type) a. + forall b. Cat (forall b. cat b u)’ diff --git a/testsuite/tests/polykinds/T15804.hs b/testsuite/tests/polykinds/T15804.hs new file mode 100644 index 0000000000..be5fa165a3 --- /dev/null +++ b/testsuite/tests/polykinds/T15804.hs @@ -0,0 +1,5 @@ +{-# Language PolyKinds #-} + +module T15804 where + +data T :: (a :: k) -> * diff --git a/testsuite/tests/polykinds/T15804.stderr b/testsuite/tests/polykinds/T15804.stderr new file mode 100644 index 0000000000..52262b675f --- /dev/null +++ b/testsuite/tests/polykinds/T15804.stderr @@ -0,0 +1,4 @@ + +T15804.hs:5:12: error: + • Expected a type, but ‘a :: k’ has kind ‘k’ + • In the kind ‘(a :: k) -> *’ diff --git a/testsuite/tests/polykinds/T15817.hs b/testsuite/tests/polykinds/T15817.hs new file mode 100644 index 0000000000..a5f3eb78db --- /dev/null +++ b/testsuite/tests/polykinds/T15817.hs @@ -0,0 +1,10 @@ +{-# Language RankNTypes #-} +{-# Language PolyKinds #-} +{-# Language TypeFamilies #-} + +module T15817 where + +import Data.Kind + +data family X :: forall (a :: Type). Type +data instance X = MkX diff --git a/testsuite/tests/polykinds/T15874.hs b/testsuite/tests/polykinds/T15874.hs new file mode 100644 index 0000000000..fd560db095 --- /dev/null +++ b/testsuite/tests/polykinds/T15874.hs @@ -0,0 +1,18 @@ +{-# Language RankNTypes #-} +{-# Language DataKinds #-} +{-# Language PolyKinds #-} +{-# Language GADTs #-} +{-# Language TypeFamilies #-} + +module T15874 where + +import Data.Kind + +data Var where + Op :: Var + Id :: Var + +type Varianced = (forall (var :: Var). Type) + +data family Parser :: Varianced +data instance Parser = P diff --git a/testsuite/tests/polykinds/T15881.hs b/testsuite/tests/polykinds/T15881.hs new file mode 100644 index 0000000000..a49b7fd436 --- /dev/null +++ b/testsuite/tests/polykinds/T15881.hs @@ -0,0 +1,8 @@ +{-# Language KindSignatures #-} +{-# Language PolyKinds #-} + +module T15881 where + +import Data.Kind + +data A n (a :: n n) :: Type diff --git a/testsuite/tests/polykinds/T15881.stderr b/testsuite/tests/polykinds/T15881.stderr new file mode 100644 index 0000000000..4fde71dab7 --- /dev/null +++ b/testsuite/tests/polykinds/T15881.stderr @@ -0,0 +1,5 @@ + +T15881.hs:8:18: error: + • Occurs check: cannot construct the infinite kind: k0 ~ k0 -> * + • In the first argument of ‘n’, namely ‘n’ + In the kind ‘n n’ diff --git a/testsuite/tests/polykinds/T15881a.hs b/testsuite/tests/polykinds/T15881a.hs new file mode 100644 index 0000000000..a29c63f706 --- /dev/null +++ b/testsuite/tests/polykinds/T15881a.hs @@ -0,0 +1,8 @@ +{-# Language KindSignatures #-} +{-# Language PolyKinds #-} + +module T15881a where + +import Data.Kind + +data A n (a :: n) :: a -> Type diff --git a/testsuite/tests/polykinds/T15881a.stderr b/testsuite/tests/polykinds/T15881a.stderr new file mode 100644 index 0000000000..84014c7abc --- /dev/null +++ b/testsuite/tests/polykinds/T15881a.stderr @@ -0,0 +1,4 @@ + +T15881a.hs:8:22: error: + • Expected a type, but ‘a’ has kind ‘n’ + • In the kind ‘a -> Type’ diff --git a/testsuite/tests/polykinds/T8616.stderr b/testsuite/tests/polykinds/T8616.stderr index 9aa4ab50d9..f9e5132a34 100644 --- a/testsuite/tests/polykinds/T8616.stderr +++ b/testsuite/tests/polykinds/T8616.stderr @@ -13,3 +13,12 @@ T8616.hs:8:16: error: withSomeSing = undefined :: (Any :: k) • Relevant bindings include withSomeSing :: Proxy kproxy (bound at T8616.hs:8:1) + +T8616.hs:8:30: error: + • Expected a type, but ‘Any :: k’ has kind ‘k’ + • In an expression type signature: (Any :: k) + In the expression: undefined :: (Any :: k) + In an equation for ‘withSomeSing’: + withSomeSing = undefined :: (Any :: k) + • Relevant bindings include + withSomeSing :: Proxy kproxy (bound at T8616.hs:8:1) diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T index 6ffb3181ce..8be2c59bf0 100644 --- a/testsuite/tests/polykinds/all.T +++ b/testsuite/tests/polykinds/all.T @@ -196,3 +196,10 @@ test('T15577', normal, compile_fail, ['-O']) test('T15592', normal, compile, ['']) test('T15592b', normal, compile, ['-ddump-types -fprint-explicit-foralls']) test('T15787', normal, compile_fail, ['']) +test('T15789', normal, compile_fail, ['']) +test('T15804', normal, compile_fail, ['']) +test('T15881', normal, compile_fail, ['']) +test('T15881a', normal, compile_fail, ['']) +test('T15817', normal, compile, ['']) +test('T15874', normal, compile, ['']) +test('T14887a', normal, compile, ['']) diff --git a/testsuite/tests/roles/should_compile/Roles1.stderr b/testsuite/tests/roles/should_compile/Roles1.stderr index 3278701048..c2678b71d7 100644 --- a/testsuite/tests/roles/should_compile/Roles1.stderr +++ b/testsuite/tests/roles/should_compile/Roles1.stderr @@ -1,16 +1,16 @@ TYPE CONSTRUCTORS type role T1 nominal - T1 :: * -> * - T2 :: * -> * + T1{1} :: * -> * + T2{1} :: * -> * type role T3 nominal phantom - T3 :: forall k. k -> * + T3{2} :: forall k. k -> * type role T4 nominal nominal - T4 :: (* -> *) -> * -> * - T5 :: * -> * + T4{2} :: (* -> *) -> * -> * + T5{1} :: * -> * type role T6 nominal phantom - T6 :: forall {k}. k -> * + T6{2} :: forall {k}. k -> * type role T7 nominal phantom representational - T7 :: forall {k}. k -> * -> * + T7{3} :: forall {k}. k -> * -> * DATA CONSTRUCTORS K7 :: forall {k} (a :: k) b. b -> T7 a b K6 :: forall {k} (a :: k). T6 a diff --git a/testsuite/tests/roles/should_compile/Roles14.stderr b/testsuite/tests/roles/should_compile/Roles14.stderr index 57899142d9..1745332a6b 100644 --- a/testsuite/tests/roles/should_compile/Roles14.stderr +++ b/testsuite/tests/roles/should_compile/Roles14.stderr @@ -2,9 +2,9 @@ TYPE SIGNATURES meth2 :: forall a. C2 a => a -> a TYPE CONSTRUCTORS type role C2 representational - C2 :: * -> Constraint + C2{1} :: * -> Constraint COERCION AXIOMS - axiom Roles12.N:C2 :: C2 a = a -> a -- Defined at Roles14.hs:6:1 + axiom Roles12.N:C2 :: C2 a = a -> a Dependent modules: [] Dependent packages: [base-4.12.0.0, ghc-prim-0.5.3, integer-gmp-1.0.2.0] diff --git a/testsuite/tests/roles/should_compile/Roles2.stderr b/testsuite/tests/roles/should_compile/Roles2.stderr index 4cb55ec063..170315111d 100644 --- a/testsuite/tests/roles/should_compile/Roles2.stderr +++ b/testsuite/tests/roles/should_compile/Roles2.stderr @@ -1,7 +1,7 @@ TYPE CONSTRUCTORS - T1 :: * -> * + T1{1} :: * -> * type role T2 phantom - T2 :: * -> * + T2{1} :: * -> * DATA CONSTRUCTORS K2 :: forall a. FunPtr a -> T2 a K1 :: forall a. IO a -> T1 a diff --git a/testsuite/tests/roles/should_compile/Roles3.stderr b/testsuite/tests/roles/should_compile/Roles3.stderr index b3507b0564..bf76b72987 100644 --- a/testsuite/tests/roles/should_compile/Roles3.stderr +++ b/testsuite/tests/roles/should_compile/Roles3.stderr @@ -4,25 +4,22 @@ TYPE SIGNATURES meth3 :: forall a b. C3 a b => a -> F3 b -> F3 b meth4 :: forall a b. C4 a b => a -> F4 b -> F4 b TYPE CONSTRUCTORS - C1 :: * -> Constraint - C2 :: * -> * -> Constraint - C3 :: * -> * -> Constraint - C4 :: * -> * -> Constraint + C1{1} :: * -> Constraint + C2{2} :: * -> * -> Constraint + C3{2} :: * -> * -> Constraint + C4{2} :: * -> * -> Constraint type role F3 nominal - F3 :: * -> * + F3{1} :: * -> * type role F4 nominal - F4 :: * -> * + F4{1} :: * -> * type role Syn1 nominal - Syn1 :: * -> * - Syn2 :: * -> * + Syn1{1} :: * -> * + Syn2{1} :: * -> * COERCION AXIOMS - axiom Roles3.N:C1 :: C1 a = a -> a -- Defined at Roles3.hs:6:1 - axiom Roles3.N:C2 :: - C2 a b = (a ~ b) => a -> b -- Defined at Roles3.hs:9:1 - axiom Roles3.N:C3 :: - C3 a b = a -> F3 b -> F3 b -- Defined at Roles3.hs:12:1 - axiom Roles3.N:C4 :: - C4 a b = a -> F4 b -> F4 b -- Defined at Roles3.hs:18:1 + axiom Roles3.N:C1 :: C1 a = a -> a + axiom Roles3.N:C2 :: C2 a b = (a ~ b) => a -> b + axiom Roles3.N:C3 :: C3 a b = a -> F3 b -> F3 b + axiom Roles3.N:C4 :: C4 a b = a -> F4 b -> F4 b Dependent modules: [] Dependent packages: [base-4.12.0.0, ghc-prim-0.5.3, integer-gmp-1.0.2.0] diff --git a/testsuite/tests/roles/should_compile/Roles4.stderr b/testsuite/tests/roles/should_compile/Roles4.stderr index 93a86a514c..dbca015edb 100644 --- a/testsuite/tests/roles/should_compile/Roles4.stderr +++ b/testsuite/tests/roles/should_compile/Roles4.stderr @@ -2,13 +2,12 @@ TYPE SIGNATURES meth1 :: forall a. C1 a => a -> a meth3 :: forall a. C3 a => a -> Syn1 a TYPE CONSTRUCTORS - C1 :: * -> Constraint - C3 :: * -> Constraint - Syn1 :: * -> * + C1{1} :: * -> Constraint + C3{1} :: * -> Constraint + Syn1{1} :: * -> * COERCION AXIOMS - axiom Roles4.N:C1 :: C1 a = a -> a -- Defined at Roles4.hs:6:1 - axiom Roles4.N:C3 :: - C3 a = a -> Syn1 a -- Defined at Roles4.hs:11:1 + axiom Roles4.N:C1 :: C1 a = a -> a + axiom Roles4.N:C3 :: C3 a = a -> Syn1 a Dependent modules: [] Dependent packages: [base-4.12.0.0, ghc-prim-0.5.3, integer-gmp-1.0.2.0] diff --git a/testsuite/tests/roles/should_compile/T8958.stderr b/testsuite/tests/roles/should_compile/T8958.stderr index eaad63859d..4e2fe00e87 100644 --- a/testsuite/tests/roles/should_compile/T8958.stderr +++ b/testsuite/tests/roles/should_compile/T8958.stderr @@ -3,12 +3,12 @@ T8958.hs:1:31: warning: -XDatatypeContexts is deprecated: It was widely considered a misfeature, and has been removed from the Haskell language. TYPE CONSTRUCTORS type role Map nominal representational - Map :: * -> * -> * - Nominal :: * -> Constraint + Map{2} :: * -> * -> * + Nominal{1} :: * -> Constraint type role Representational representational - Representational :: * -> Constraint + Representational{1} :: * -> Constraint COERCION AXIOMS - axiom T8958.N:Map :: Map k v = [(k, v)] -- Defined at T8958.hs:13:1 + axiom T8958.N:Map :: Map k v = [(k, v)] DATA CONSTRUCTORS MkMap :: forall k v. [(k, v)] -> Map k v CLASS INSTANCES diff --git a/testsuite/tests/showIface/Orphans.stdout b/testsuite/tests/showIface/Orphans.stdout index 63fcd79a19..38e4066d9e 100644 --- a/testsuite/tests/showIface/Orphans.stdout +++ b/testsuite/tests/showIface/Orphans.stdout @@ -2,5 +2,5 @@ instance [orphan] GHC.Exts.IsList [GHC.Types.Bool] = $fIsListBool instance GHC.Exts.IsList [X] = $fIsListX family instance GHC.Exts.Item [X] = D:R:ItemX family instance [orphan] GHC.Exts.Item [GHC.Types.Bool] -"myrule1" [orphan] forall @ a -"myrule2" forall GHC.Base.id @ (X -> X) f = f +"myrule1" [orphan] forall @ a. +"myrule2" GHC.Base.id @ (X -> X) f = f diff --git a/testsuite/tests/th/TH_Roles2.stderr b/testsuite/tests/th/TH_Roles2.stderr index c988015622..3807609678 100644 --- a/testsuite/tests/th/TH_Roles2.stderr +++ b/testsuite/tests/th/TH_Roles2.stderr @@ -1,6 +1,6 @@ TYPE CONSTRUCTORS type role T nominal representational - T :: forall k. k -> * + T{2} :: forall k. k -> * Dependent modules: [] Dependent packages: [array-0.5.2.0, base-4.12.0.0, deepseq-1.4.4.0, ghc-boot-th-8.7, ghc-prim-0.5.3, integer-gmp-1.0.2.0, diff --git a/testsuite/tests/th/TH_reifyExplicitForAllFams.stderr b/testsuite/tests/th/TH_reifyExplicitForAllFams.stderr index 6205547873..673f09e2e0 100644 --- a/testsuite/tests/th/TH_reifyExplicitForAllFams.stderr +++ b/testsuite/tests/th/TH_reifyExplicitForAllFams.stderr @@ -13,4 +13,4 @@ type family TH_reifyExplicitForAllFams.H (a_0 :: *) (b_1 :: *) :: * where (Data.Proxy.Proxy y_3) = Data.Either.Either x_2 y_3 forall (z_4 :: *). TH_reifyExplicitForAllFams.H z_4 - z_4 = GHC.Maybe.Maybe z_4
\ No newline at end of file + z_4 = GHC.Maybe.Maybe z_4 diff --git a/testsuite/tests/typecheck/should_compile/T12763.stderr b/testsuite/tests/typecheck/should_compile/T12763.stderr index ad3460c2da..99a66bd59e 100644 --- a/testsuite/tests/typecheck/should_compile/T12763.stderr +++ b/testsuite/tests/typecheck/should_compile/T12763.stderr @@ -2,9 +2,9 @@ TYPE SIGNATURES f :: Int -> () m :: forall a. C a => a -> () TYPE CONSTRUCTORS - C :: * -> Constraint + C{1} :: * -> Constraint COERCION AXIOMS - axiom T12763.N:C :: C a = a -> () -- Defined at T12763.hs:6:1 + axiom T12763.N:C :: C a = a -> () CLASS INSTANCES instance C Int -- Defined at T12763.hs:9:10 Dependent modules: [] diff --git a/testsuite/tests/typecheck/should_compile/tc231.stderr b/testsuite/tests/typecheck/should_compile/tc231.stderr index 6c785b4a40..18beabd3a1 100644 --- a/testsuite/tests/typecheck/should_compile/tc231.stderr +++ b/testsuite/tests/typecheck/should_compile/tc231.stderr @@ -6,13 +6,11 @@ TYPE SIGNATURES huh :: forall s a b chain. Zork s a b => Q s a chain -> ST s () s :: forall t t1. Q t (Z [Char]) t1 -> Q t (Z [Char]) t1 TYPE CONSTRUCTORS - Q :: * -> * -> * -> * - Z :: * -> * - Zork :: * -> * -> * -> Constraint + Q{3} :: * -> * -> * -> * + Z{1} :: * -> * + Zork{3} :: * -> * -> * -> Constraint COERCION AXIOMS - axiom N:Zork :: - Zork s a b = forall chain. Q s a chain -> ST s () - -- Defined at tc231.hs:25:1 + axiom N:Zork :: Zork s a b = forall chain. Q s a chain -> ST s () DATA CONSTRUCTORS Z :: forall a. a -> Z a Node :: forall s a chain. s -> a -> chain -> Q s a chain diff --git a/testsuite/tests/typecheck/should_fail/LevPolyBounded.stderr b/testsuite/tests/typecheck/should_fail/LevPolyBounded.stderr index 21ae68ab85..afa8330765 100644 --- a/testsuite/tests/typecheck/should_fail/LevPolyBounded.stderr +++ b/testsuite/tests/typecheck/should_fail/LevPolyBounded.stderr @@ -3,3 +3,8 @@ LevPolyBounded.hs:10:15: error: • Expected a type, but ‘a’ has kind ‘TYPE r’ • In the type signature: LevPolyBounded.minBound :: a In the class declaration for ‘XBounded’ + +LevPolyBounded.hs:11:15: error: + • Expected a type, but ‘a’ has kind ‘TYPE r’ + • In the type signature: LevPolyBounded.maxBound :: a + In the class declaration for ‘XBounded’ diff --git a/testsuite/tests/typecheck/should_fail/T13983.stderr b/testsuite/tests/typecheck/should_fail/T13983.stderr index 5c7a031654..d1b2fe067b 100644 --- a/testsuite/tests/typecheck/should_fail/T13983.stderr +++ b/testsuite/tests/typecheck/should_fail/T13983.stderr @@ -5,4 +5,4 @@ T13983.hs:7:1: error: of its type variables. Perhaps you meant to bind it explicitly somewhere? Type variables with inferred kinds: (k :: *) - • In the type declaration for ‘Wat’ + • In the type synonym declaration for ‘Wat’ diff --git a/testsuite/tests/typecheck/should_fail/T14607.hs b/testsuite/tests/typecheck/should_fail/T14607.hs index 86c738dc19..af2e1c7677 100644 --- a/testsuite/tests/typecheck/should_fail/T14607.hs +++ b/testsuite/tests/typecheck/should_fail/T14607.hs @@ -31,4 +31,4 @@ instance Mk a where -- So now the kind error can be deferred. -- Consequence of a fast-path for tcImplicitTKBndrsX I think. - +-- Later (Nov 18) we are back to a kind error, which is fine diff --git a/testsuite/tests/typecheck/should_fail/T14607.stderr b/testsuite/tests/typecheck/should_fail/T14607.stderr index 5e0b66a340..b7d60593e1 100644 --- a/testsuite/tests/typecheck/should_fail/T14607.stderr +++ b/testsuite/tests/typecheck/should_fail/T14607.stderr @@ -1,21 +1,12 @@ -T14607.hs:22:9: warning: [-Wdeferred-type-errors (in -Wdefault)] +T14607.hs:22:9: error: • Expecting one more argument to ‘LamCons a '()’ - Expected a type, but ‘LamCons a '()’ has kind ‘() -> *’ - • In the type signature: mk :: LamCons a '() + Expected a type, but ‘LamCons a '()’ has kind ‘() -> *’ + • In the type signature: mk :: LamCons a '() In the instance declaration for ‘Mk a’ -T14607.hs:22:19: warning: [-Wdeferred-type-errors (in -Wdefault)] +T14607.hs:22:19: error: • Expected a type, but ‘'()’ has kind ‘()’ • In the second argument of ‘LamCons’, namely ‘'()’ In the type signature: mk :: LamCons a '() In the instance declaration for ‘Mk a’ - -T14607.hs:23:8: warning: [-Wdeferred-type-errors (in -Wdefault)] - • Couldn't match expected type ‘LamCons a '()’ - with actual type ‘LamCons a0 a0 '()’ - • In the expression: mk - In an equation for ‘mk’: mk = mk - In the instance declaration for ‘Mk a’ - • Relevant bindings include - mk :: LamCons a '() (bound at T14607.hs:23:3) diff --git a/testsuite/tests/typecheck/should_fail/T2688.stderr b/testsuite/tests/typecheck/should_fail/T2688.stderr index 2b2ca0d22a..63379a03b9 100644 --- a/testsuite/tests/typecheck/should_fail/T2688.stderr +++ b/testsuite/tests/typecheck/should_fail/T2688.stderr @@ -2,9 +2,11 @@ T2688.hs:8:14: error: • Couldn't match expected type ‘v’ with actual type ‘s’ ‘s’ is a rigid type variable bound by - the class declaration for ‘VectorSpace’ at T2688.hs:5:21 + the class declaration for ‘VectorSpace’ + at T2688.hs:(5,1)-(8,23) ‘v’ is a rigid type variable bound by - the class declaration for ‘VectorSpace’ at T2688.hs:5:19 + the class declaration for ‘VectorSpace’ + at T2688.hs:(5,1)-(8,23) • In the expression: v *^ (1 / s) In an equation for ‘^/’: v ^/ s = v *^ (1 / s) • Relevant bindings include diff --git a/testsuite/tests/typecheck/should_fail/T6018fail.stderr b/testsuite/tests/typecheck/should_fail/T6018fail.stderr index 0e230e62c8..84af180b20 100644 --- a/testsuite/tests/typecheck/should_fail/T6018fail.stderr +++ b/testsuite/tests/typecheck/should_fail/T6018fail.stderr @@ -59,9 +59,9 @@ T6018fail.hs:53:15: error: T6018fail.hs:61:10: error: Type family equation violates injectivity annotation. - Kind variable ‘k2’ cannot be inferred from the right-hand side. + Kind variable ‘k1’ cannot be inferred from the right-hand side. In the type family equation: - PolyKindVarsF @{[k2]} @[k1] ('[] @k2) = '[] @k1 + PolyKindVarsF @{[k1]} @[k2] ('[] @k1) = '[] @k2 -- Defined at T6018fail.hs:61:10 T6018fail.hs:64:15: error: diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T index 3805315398..7dca65b499 100644 --- a/testsuite/tests/typecheck/should_fail/all.T +++ b/testsuite/tests/typecheck/should_fail/all.T @@ -469,7 +469,7 @@ test('T14350', normal, compile_fail, ['']) test('T14390', normal, compile_fail, ['']) test('MissingExportList03', normal, compile_fail, ['']) test('T14618', normal, compile_fail, ['']) -test('T14607', normal, compile, ['']) +test('T14607', normal, compile_fail, ['']) test('T14605', normal, compile_fail, ['']) test('T14761a', normal, compile_fail, ['']) test('T14761b', normal, compile_fail, ['']) |