diff options
author | Simon Peyton Jones <simonpj@microsoft.com> | 2020-07-15 23:50:42 +0100 |
---|---|---|
committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2020-09-24 13:16:32 -0400 |
commit | 97cff9190d346c3b51c32c88fd145fcf1e6678f1 (patch) | |
tree | bf5f482cb2efb3ed0396cbc76cf236f50bdc8ee1 /testsuite/tests/typecheck | |
parent | 04d6433158d95658684cf419c4ba5725d2aa539e (diff) | |
download | haskell-97cff9190d346c3b51c32c88fd145fcf1e6678f1.tar.gz |
Implement Quick Look impredicativity
This patch implements Quick Look impredicativity (#18126), sticking
very closely to the design in
A quick look at impredicativity, Serrano et al, ICFP 2020
The main change is that a big chunk of GHC.Tc.Gen.Expr has been
extracted to two new modules
GHC.Tc.Gen.App
GHC.Tc.Gen.Head
which deal with typechecking n-ary applications, and the head of
such applications, respectively. Both contain a good deal of
documentation.
Three other loosely-related changes are in this patch:
* I implemented (partly by accident) points (2,3)) of the accepted GHC
proposal "Clean up printing of foralls", namely
https://github.com/ghc-proposals/ghc-proposals/blob/
master/proposals/0179-printing-foralls.rst
(see #16320).
In particular, see Note [TcRnExprMode] in GHC.Tc.Module
- :type instantiates /inferred/, but not /specified/, quantifiers
- :type +d instantiates /all/ quantifiers
- :type +v is killed off
That completes the implementation of the proposal,
since point (1) was done in
commit df08468113ab46832b7ac0a7311b608d1b418c4d
Author: Krzysztof Gogolewski <krzysztof.gogolewski@tweag.io>
Date: Mon Feb 3 21:17:11 2020 +0100
Always display inferred variables using braces
* HsRecFld (which the renamer introduces for record field selectors),
is now preserved by the typechecker, rather than being rewritten
back to HsVar. This is more uniform, and turned out to be more
convenient in the new scheme of things.
* The GHCi debugger uses a non-standard unification that allows the
unification variables to unify with polytypes. We used to hack
this by using ImpredicativeTypes, but that doesn't work anymore
so I introduces RuntimeUnkTv. See Note [RuntimeUnkTv] in
GHC.Runtime.Heap.Inspect
Updates haddock submodule.
WARNING: this patch won't validate on its own. It was too
hard to fully disentangle it from the following patch, on
type errors and kind generalisation.
Changes to tests
* Fixes #9730 (test added)
* Fixes #7026 (test added)
* Fixes most of #8808, except function `g2'` which uses a
section (which doesn't play with QL yet -- see #18126)
Test added
* Fixes #1330. NB Church1.hs subsumes Church2.hs, which is now deleted
* Fixes #17332 (test added)
* Fixes #4295
* This patch makes typecheck/should_run/T7861 fail.
But that turns out to be a pre-existing bug: #18467.
So I have just made T7861 into expect_broken(18467)
Diffstat (limited to 'testsuite/tests/typecheck')
9 files changed, 30 insertions, 21 deletions
diff --git a/testsuite/tests/typecheck/should_fail/T11355.stderr b/testsuite/tests/typecheck/should_fail/T11355.stderr index 5310989327..c922e4db93 100644 --- a/testsuite/tests/typecheck/should_fail/T11355.stderr +++ b/testsuite/tests/typecheck/should_fail/T11355.stderr @@ -1,7 +1,7 @@ T11355.hs:5:7: error: • Illegal polymorphic type: forall a. a - GHC doesn't yet support impredicative polymorphism + Perhaps you intended to use ImpredicativeTypes • In the expression: const @_ @((forall a. a) -> forall a. a) () (id @(forall a. a)) In an equation for ‘foo’: diff --git a/testsuite/tests/typecheck/should_fail/T2538.stderr b/testsuite/tests/typecheck/should_fail/T2538.stderr index 18c82bd992..726ac8fd71 100644 --- a/testsuite/tests/typecheck/should_fail/T2538.stderr +++ b/testsuite/tests/typecheck/should_fail/T2538.stderr @@ -2,17 +2,14 @@ T2538.hs:6:6: error: • Illegal qualified type: Eq a => a -> a Perhaps you intended to use RankNTypes - • In the type signature: - f :: (Eq a => a -> a) -> Int + • In the type signature: f :: (Eq a => a -> a) -> Int T2538.hs:9:6: error: • Illegal qualified type: Eq a => a -> a - GHC doesn't yet support impredicative polymorphism - • In the type signature: - g :: [Eq a => a -> a] -> Int + Perhaps you intended to use ImpredicativeTypes + • In the type signature: g :: [Eq a => a -> a] -> Int T2538.hs:12:6: error: • Illegal qualified type: Eq a => a -> a - GHC doesn't yet support impredicative polymorphism - • In the type signature: - h :: Ix (Eq a => a -> a) => Int + Perhaps you intended to use ImpredicativeTypes + • In the type signature: h :: Ix (Eq a => a -> a) => Int diff --git a/testsuite/tests/typecheck/should_fail/T7809.stderr b/testsuite/tests/typecheck/should_fail/T7809.stderr index 9ec32b3ff6..0e0c867659 100644 --- a/testsuite/tests/typecheck/should_fail/T7809.stderr +++ b/testsuite/tests/typecheck/should_fail/T7809.stderr @@ -1,6 +1,6 @@ T7809.hs:8:8: error: • Illegal polymorphic type: forall a. a -> a - GHC doesn't yet support impredicative polymorphism + Perhaps you intended to use ImpredicativeTypes • In the expansion of type synonym ‘PolyId’ In the type signature: foo :: F PolyId diff --git a/testsuite/tests/typecheck/should_fail/tcfail127.stderr b/testsuite/tests/typecheck/should_fail/tcfail127.stderr index 6716724860..a262e0113e 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail127.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail127.stderr @@ -1,6 +1,5 @@ tcfail127.hs:3:8: error: • Illegal qualified type: Num a => a -> a - GHC doesn't yet support impredicative polymorphism - • In the type signature: - foo :: IO (Num a => a -> a) + Perhaps you intended to use ImpredicativeTypes + • In the type signature: foo :: IO (Num a => a -> a) diff --git a/testsuite/tests/typecheck/should_fail/tcfail196.stderr b/testsuite/tests/typecheck/should_fail/tcfail196.stderr index 57370d4014..313e7cbdd4 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail196.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail196.stderr @@ -1,6 +1,5 @@ tcfail196.hs:5:8: error: • Illegal polymorphic type: forall a. a - GHC doesn't yet support impredicative polymorphism - • In the type signature: - bar :: Num (forall a. a) => Int -> Int + Perhaps you intended to use ImpredicativeTypes + • In the type signature: bar :: Num (forall a. a) => Int -> Int diff --git a/testsuite/tests/typecheck/should_fail/tcfail197.stderr b/testsuite/tests/typecheck/should_fail/tcfail197.stderr index 1d5f455968..cfbc3fd0dd 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail197.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail197.stderr @@ -1,6 +1,5 @@ tcfail197.hs:5:8: error: • Illegal polymorphic type: forall a. a - GHC doesn't yet support impredicative polymorphism - • In the type signature: - foo :: [forall a. a] -> Int + Perhaps you intended to use ImpredicativeTypes + • In the type signature: foo :: [forall a. a] -> Int diff --git a/testsuite/tests/typecheck/should_run/all.T b/testsuite/tests/typecheck/should_run/all.T index f69cc71352..ef8ae9136d 100755 --- a/testsuite/tests/typecheck/should_run/all.T +++ b/testsuite/tests/typecheck/should_run/all.T @@ -58,7 +58,7 @@ test('tcrun038', [extra_files(['TcRun038_B.hs'])], multimod_compile_and_run, ['t test('tcrun039', normal, compile_and_run, ['']) test('tcrun040', normal, compile_and_run, ['']) test('tcrun041', omit_ways(['ghci']), compile_and_run, ['']) -test('tcrun042', normal, compile, ['']) +test('tcrun042', normal, compile_fail, ['']) test('tcrun043', normal, compile_and_run, ['']) test('tcrun044', normal, compile_and_run, ['']) test('tcrun045', normal, compile_fail, ['']) @@ -96,7 +96,7 @@ test('T6117', normal, compile_and_run, ['']) test('T5751', normal, compile_and_run, ['']) test('T5913', normal, compile_and_run, ['']) test('T7748', normal, compile_and_run, ['']) -test('T7861', [omit_ways(['debug']), exit_code(1)], compile_and_run, ['']) +test('T7861', [expect_broken(18467),omit_ways(['debug']), exit_code(1)], compile_and_run, ['']) test('TcTypeNatSimpleRun', normal, compile_and_run, ['']) test('TcTypeSymbolSimpleRun', normal, compile_and_run, ['']) test('T8119', normal, ghci_script, ['T8119.script']) diff --git a/testsuite/tests/typecheck/should_run/tcrun042.hs b/testsuite/tests/typecheck/should_run/tcrun042.hs index ba809a16ba..30c67601ed 100644 --- a/testsuite/tests/typecheck/should_run/tcrun042.hs +++ b/testsuite/tests/typecheck/should_run/tcrun042.hs @@ -7,6 +7,11 @@ -- -- Apr 20: Works again. NB: the ImpredicativeTypes flag -- +-- July 20: Fails again. Under Quick Look this now fails, because +-- we don't have a special typing rule for ExplicitTuples +-- We could, and it would improve the typing for tuple sections. +-- But for now I'm just letting it fail, until someone yells. +-- -- The test was added by Max in 5e8ff849, apparently to test tuple sections module Main where diff --git a/testsuite/tests/typecheck/should_run/tcrun042.stderr b/testsuite/tests/typecheck/should_run/tcrun042.stderr new file mode 100644 index 0000000000..dcf0854d47 --- /dev/null +++ b/testsuite/tests/typecheck/should_run/tcrun042.stderr @@ -0,0 +1,10 @@ + +tcrun042.hs:20:5: error: + • Couldn't match type ‘t0’ with ‘forall b. b -> b -> b’ + Expected: a + -> (forall b. b -> b -> b) -> (a, String, forall c. c -> c -> c) + Actual: a -> t0 -> (a, [Char], t0) + Cannot instantiate unification variable ‘t0’ + with a type involving polytypes: forall b. b -> b -> b + • In the expression: (, "Hello" ++ "World",) + In an equation for ‘e’: e = (, "Hello" ++ "World",) |