diff options
author | Matthew Pickering <matthewtpickering@gmail.com> | 2021-11-30 17:05:11 +0000 |
---|---|---|
committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2022-01-29 02:41:21 -0500 |
commit | 268efcc9a45da36458442d9203c66a415b48f2b3 (patch) | |
tree | 8d99c80c3ebf68cd91c4262573a1a8634863f90a /testsuite/tests/dependent | |
parent | bb15c34784a3143ef048807fd351667d6775e399 (diff) | |
download | haskell-268efcc9a45da36458442d9203c66a415b48f2b3.tar.gz |
Rework the handling of SkolemInfo
The main purpose of this patch is to attach a SkolemInfo directly to
each SkolemTv. This fixes the large number of bugs which have
accumulated over the years where we failed to report errors due to
having "no skolem info" for particular type variables. Now the origin of
each type varible is stored on the type variable we can always report
accurately where it cames from.
Fixes #20969 #20732 #20680 #19482 #20232 #19752 #10946
#19760 #20063 #13499 #14040
The main changes of this patch are:
* SkolemTv now contains a SkolemInfo field which tells us how the
SkolemTv was created. Used when reporting errors.
* Enforce invariants relating the SkolemInfoAnon and level of an implication (ic_info, ic_tclvl)
to the SkolemInfo and level of the type variables in ic_skols.
* All ic_skols are TcTyVars -- Check is currently disabled
* All ic_skols are SkolemTv
* The tv_lvl of the ic_skols agrees with the ic_tclvl
* The ic_info agrees with the SkolInfo of the implication.
These invariants are checked by a debug compiler by
checkImplicationInvariants.
* Completely refactor kcCheckDeclHeader_sig which kept
doing my head in. Plus, it wasn't right because it wasn't skolemising
the binders as it decomposed the kind signature.
The new story is described in Note [kcCheckDeclHeader_sig]. The code
is considerably shorter than before (roughly 240 lines turns into 150
lines).
It still has the same awkward complexity around computing arity as
before, but that is a language design issue.
See Note [Arity inference in kcCheckDeclHeader_sig]
* I added new type synonyms MonoTcTyCon and PolyTcTyCon, and used
them to be clear which TcTyCons have "finished" kinds etc, and
which are monomorphic. See Note [TcTyCon, MonoTcTyCon, and PolyTcTyCon]
* I renamed etaExpandAlgTyCon to splitTyConKind, becuase that's a
better name, and it is very useful in kcCheckDeclHeader_sig, where
eta-expansion isn't an issue.
* Kill off the nasty `ClassScopedTvEnv` entirely.
Co-authored-by: Simon Peyton Jones <simon.peytonjones@gmail.com>
Diffstat (limited to 'testsuite/tests/dependent')
8 files changed, 8 insertions, 8 deletions
diff --git a/testsuite/tests/dependent/should_compile/T14066a.stderr b/testsuite/tests/dependent/should_compile/T14066a.stderr index 889d51b1cf..3f3c88a3e6 100644 --- a/testsuite/tests/dependent/should_compile/T14066a.stderr +++ b/testsuite/tests/dependent/should_compile/T14066a.stderr @@ -1,5 +1,5 @@ T14066a.hs:14:3: warning: Type family instance equation is overlapped: - forall {c} {d} {x :: c} {y :: d}. + forall {c} {x :: c} {d} {y :: d}. Bar x y = Bool -- Defined at T14066a.hs:14:3 diff --git a/testsuite/tests/dependent/should_fail/BadTelescope2.stderr b/testsuite/tests/dependent/should_fail/BadTelescope2.stderr index 3637dece24..f5aee5a1eb 100644 --- a/testsuite/tests/dependent/should_fail/BadTelescope2.stderr +++ b/testsuite/tests/dependent/should_fail/BadTelescope2.stderr @@ -1,5 +1,5 @@ -BadTelescope2.hs:9:8: error: +BadTelescope2.hs:9:15: error: • These kind and type variables: a k (b :: k) are out of dependency order. Perhaps try this ordering: k (a :: k) (b :: k) diff --git a/testsuite/tests/dependent/should_fail/BadTelescope5.stderr b/testsuite/tests/dependent/should_fail/BadTelescope5.stderr index 02daf9d742..b5e4ce9c3a 100644 --- a/testsuite/tests/dependent/should_fail/BadTelescope5.stderr +++ b/testsuite/tests/dependent/should_fail/BadTelescope5.stderr @@ -2,7 +2,7 @@ BadTelescope5.hs:10:81: error: • Expected kind ‘k’, but ‘d’ has kind ‘Proxy a’ ‘k’ is a rigid type variable bound by - an explicit forall a k (b :: k) (c :: Proxy b) (d :: Proxy a) + the type signature for ‘bar’ at BadTelescope5.hs:10:17 • In the second argument of ‘SameKind’, namely ‘d’ In the type signature: diff --git a/testsuite/tests/dependent/should_fail/T13780a.stderr b/testsuite/tests/dependent/should_fail/T13780a.stderr index 3e3fa61a9b..6cdcf96369 100644 --- a/testsuite/tests/dependent/should_fail/T13780a.stderr +++ b/testsuite/tests/dependent/should_fail/T13780a.stderr @@ -3,7 +3,7 @@ T13780a.hs:9:40: error: • Couldn't match kind ‘a’ with ‘Bool’ Expected kind ‘Foo a’, but ‘MkFoo’ has kind ‘Foo Bool’ ‘a’ is a rigid type variable bound by - the data constructor ‘SMkFoo’ + a family instance declaration at T13780a.hs:9:20-31 • In the second argument of ‘(~)’, namely ‘MkFoo’ In the definition of data constructor ‘SMkFoo’ diff --git a/testsuite/tests/dependent/should_fail/T14066.stderr b/testsuite/tests/dependent/should_fail/T14066.stderr index 240108c296..20c82215ed 100644 --- a/testsuite/tests/dependent/should_fail/T14066.stderr +++ b/testsuite/tests/dependent/should_fail/T14066.stderr @@ -4,7 +4,7 @@ T14066.hs:15:59: error: because kind variable ‘k’ would escape its scope This (rigid, skolem) kind variable is bound by an explicit forall k (b :: k) - at T14066.hs:15:29-59 + at T14066.hs:15:36-45 • In the second argument of ‘SameKind’, namely ‘b’ In the type signature: g :: forall k (b :: k). SameKind a b In the expression: diff --git a/testsuite/tests/dependent/should_fail/T16344a.stderr b/testsuite/tests/dependent/should_fail/T16344a.stderr index 8325bf4169..ab3b991293 100644 --- a/testsuite/tests/dependent/should_fail/T16344a.stderr +++ b/testsuite/tests/dependent/should_fail/T16344a.stderr @@ -2,7 +2,7 @@ T16344a.hs:11:36: error: • Expected a type, but ‘a’ has kind ‘ka’ ‘ka’ is a rigid type variable bound by - the data constructor ‘MkT2’ + the data type declaration for ‘T2’ at T16344a.hs:11:9-10 • In the second argument of ‘T2’, namely ‘a’ In the type ‘(T2 Type a)’ diff --git a/testsuite/tests/dependent/should_fail/T16418.stderr b/testsuite/tests/dependent/should_fail/T16418.stderr index fa2263abd3..a286d77805 100644 --- a/testsuite/tests/dependent/should_fail/T16418.stderr +++ b/testsuite/tests/dependent/should_fail/T16418.stderr @@ -1,5 +1,5 @@ -T16418.hs:9:6: error: +T16418.hs:9:13: error: • These kind and type variables: a k (b :: k) are out of dependency order. Perhaps try this ordering: k (a :: k) (b :: k) diff --git a/testsuite/tests/dependent/should_fail/TypeSkolEscape.stderr b/testsuite/tests/dependent/should_fail/TypeSkolEscape.stderr index d642d6201c..b8ccbdfc9f 100644 --- a/testsuite/tests/dependent/should_fail/TypeSkolEscape.stderr +++ b/testsuite/tests/dependent/should_fail/TypeSkolEscape.stderr @@ -4,6 +4,6 @@ TypeSkolEscape.hs:9:52: error: because kind variable ‘v’ would escape its scope This (rigid, skolem) kind variable is bound by an explicit forall (v :: RuntimeRep) (a :: TYPE v) - at TypeSkolEscape.hs:9:12-52 + at TypeSkolEscape.hs:9:19-49 • In the type ‘forall (v :: RuntimeRep) (a :: TYPE v). a’ In the type declaration for ‘Bad’ |