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/tests/dependent | |
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/tests/dependent')
12 files changed, 52 insertions, 79 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’ |