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/saks/should_fail | |
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/saks/should_fail')
13 files changed, 42 insertions, 11 deletions
diff --git a/testsuite/tests/saks/should_fail/T16758.stderr b/testsuite/tests/saks/should_fail/T16758.stderr index f74241a706..066a4f106a 100644 --- a/testsuite/tests/saks/should_fail/T16758.stderr +++ b/testsuite/tests/saks/should_fail/T16758.stderr @@ -3,6 +3,6 @@ T16758.hs:14:8: error: • Couldn't match expected kind ‘Int’ with actual kind ‘a’ ‘a’ is a rigid type variable bound by the class declaration for ‘C’ - at T16758.hs:12:19 + at T16758.hs:13:9 • In the type signature: f :: C a => a -> Int In the class declaration for ‘C’ diff --git a/testsuite/tests/saks/should_fail/T20916.hs b/testsuite/tests/saks/should_fail/T20916.hs new file mode 100644 index 0000000000..f62aa4caab --- /dev/null +++ b/testsuite/tests/saks/should_fail/T20916.hs @@ -0,0 +1,9 @@ +{-# LANGUAGE CUSKs, EmptyDataDecls, PolyKinds, KindSignatures, StandaloneKindSignatures #-} + +module T20916 where + +import Data.Kind + +type T3 :: k -> k -> Type +data T3 (a :: p) (b :: q) = MkT +-- Should fail because p and q are bound the same kind variable diff --git a/testsuite/tests/saks/should_fail/T20916.stderr b/testsuite/tests/saks/should_fail/T20916.stderr new file mode 100644 index 0000000000..aeef4ca438 --- /dev/null +++ b/testsuite/tests/saks/should_fail/T20916.stderr @@ -0,0 +1,4 @@ + +T20916.hs:8:10: error: + • Different names for the same type variable: ‘p’ and ‘q’ + • In the data type declaration for ‘T3’ diff --git a/testsuite/tests/saks/should_fail/all.T b/testsuite/tests/saks/should_fail/all.T index 7e2194a21f..98345aa2ca 100644 --- a/testsuite/tests/saks/should_fail/all.T +++ b/testsuite/tests/saks/should_fail/all.T @@ -24,6 +24,7 @@ test('saks_fail022', normal, compile_fail, ['']) test('saks_fail023', normal, compile_fail, ['']) test('saks_fail024', normal, compile_fail, ['']) test('saks_fail025', normal, compile_fail, ['']) +test('saks_fail026', normal, compile_fail, ['']) test('T16722', normal, compile_fail, ['']) test('T16727a', normal, compile_fail, ['']) test('T16727b', normal, compile_fail, ['']) @@ -33,3 +34,4 @@ test('T16756b', normal, compile_fail, ['']) test('T16758', normal, compile_fail, ['']) test('T18863a', normal, compile_fail, ['']) test('T18863b', normal, compile_fail, ['']) +test('T20916', normal, compile_fail, ['']) diff --git a/testsuite/tests/saks/should_fail/saks_fail009.hs b/testsuite/tests/saks/should_fail/saks_fail009.hs index 317c0e7644..21394ada56 100644 --- a/testsuite/tests/saks/should_fail/saks_fail009.hs +++ b/testsuite/tests/saks/should_fail/saks_fail009.hs @@ -5,5 +5,5 @@ module SAKS_Fail009 where import Data.Kind (Type) -type T :: forall k -> k -> Type +type T :: forall j -> j -> Type data T (k :: Type -> Type) (a :: k) diff --git a/testsuite/tests/saks/should_fail/saks_fail009.stderr b/testsuite/tests/saks/should_fail/saks_fail009.stderr index 8ce43f6d5d..22b66b421b 100644 --- a/testsuite/tests/saks/should_fail/saks_fail009.stderr +++ b/testsuite/tests/saks/should_fail/saks_fail009.stderr @@ -1,4 +1,5 @@ saks_fail009.hs:9:1: error: - • Expected kind ‘* -> *’, but ‘k’ has kind ‘*’ + • Expecting one more argument to ‘k’ + Expected a type, but ‘k’ has kind ‘* -> *’ • In the data type declaration for ‘T’ diff --git a/testsuite/tests/saks/should_fail/saks_fail019.hs b/testsuite/tests/saks/should_fail/saks_fail019.hs index 51cdd54ca2..ddd20d099c 100644 --- a/testsuite/tests/saks/should_fail/saks_fail019.hs +++ b/testsuite/tests/saks/should_fail/saks_fail019.hs @@ -6,6 +6,6 @@ module SAKS_Fail019 where import Data.Kind (Type) type T :: Type -> Type -> Type -data T a :: a -> Type +data T x :: x -> Type -- Should not panic with: - -- GHC internal error: ‘a’ is not in scope during type checking, but it passed the renamer + -- GHC internal error: ‘x’ is not in scope during type checking, but it passed the renamer diff --git a/testsuite/tests/saks/should_fail/saks_fail019.stderr b/testsuite/tests/saks/should_fail/saks_fail019.stderr index b34a7e1905..a824ab118c 100644 --- a/testsuite/tests/saks/should_fail/saks_fail019.stderr +++ b/testsuite/tests/saks/should_fail/saks_fail019.stderr @@ -1,9 +1,9 @@ saks_fail019.hs:9:1: error: - • Couldn't match kind ‘a’ with ‘*’ - Expected: a -> * + • Couldn't match kind ‘x’ with ‘*’ + Expected: x -> * Actual: * -> * - ‘a’ is a rigid type variable bound by + ‘x’ is a rigid type variable bound by the data type declaration for ‘T’ at saks_fail019.hs:9:8 • In the data type declaration for ‘T’ diff --git a/testsuite/tests/saks/should_fail/saks_fail021.stderr b/testsuite/tests/saks/should_fail/saks_fail021.stderr index 6128aff165..fa20ccc826 100644 --- a/testsuite/tests/saks/should_fail/saks_fail021.stderr +++ b/testsuite/tests/saks/should_fail/saks_fail021.stderr @@ -1,4 +1,4 @@ saks_fail021.hs:10:1: error: - • Expected kind ‘k’, but ‘a’ has kind ‘*’ + • Expected a type, but ‘a’ has kind ‘k’ • In the class declaration for ‘C’ diff --git a/testsuite/tests/saks/should_fail/saks_fail022.stderr b/testsuite/tests/saks/should_fail/saks_fail022.stderr index e0cc222344..0591eced95 100644 --- a/testsuite/tests/saks/should_fail/saks_fail022.stderr +++ b/testsuite/tests/saks/should_fail/saks_fail022.stderr @@ -1,4 +1,4 @@ saks_fail022.hs:10:1: error: - • Expected kind ‘k’, but ‘a’ has kind ‘(x, y)’ + • Expected kind ‘(x, y)’, but ‘a’ has kind ‘k’ • In the class declaration for ‘C’ diff --git a/testsuite/tests/saks/should_fail/saks_fail023.stderr b/testsuite/tests/saks/should_fail/saks_fail023.stderr index 3af24c7abb..36144f6d9d 100644 --- a/testsuite/tests/saks/should_fail/saks_fail023.stderr +++ b/testsuite/tests/saks/should_fail/saks_fail023.stderr @@ -1,4 +1,4 @@ saks_fail023.hs:10:1: error: - • Expected kind ‘k’, but ‘a’ has kind ‘*’ + • Expected a type, but ‘a’ has kind ‘k’ • In the class declaration for ‘C’ diff --git a/testsuite/tests/saks/should_fail/saks_fail026.hs b/testsuite/tests/saks/should_fail/saks_fail026.hs new file mode 100644 index 0000000000..1d47a06d6e --- /dev/null +++ b/testsuite/tests/saks/should_fail/saks_fail026.hs @@ -0,0 +1,8 @@ +{-# LANGUAGE TypeFamilies #-} + +module SAKS_Fail026 where + +import Data.Kind (Type) + +type F3 :: forall kx. kx -> Type +type family F3 (b :: Type) where diff --git a/testsuite/tests/saks/should_fail/saks_fail026.stderr b/testsuite/tests/saks/should_fail/saks_fail026.stderr new file mode 100644 index 0000000000..ceeeaa01c7 --- /dev/null +++ b/testsuite/tests/saks/should_fail/saks_fail026.stderr @@ -0,0 +1,7 @@ + +saks_fail026.hs:8:1: error: + • Expected kind ‘kx’, but ‘b’ has kind ‘*’ + ‘kx’ is a rigid type variable bound by + the type family declaration for ‘F3’ + at saks_fail026.hs:7:19-20 + • In the type family declaration for ‘F3’ |