From 97cff9190d346c3b51c32c88fd145fcf1e6678f1 Mon Sep 17 00:00:00 2001 From: Simon Peyton Jones Date: Wed, 15 Jul 2020 23:50:42 +0100 Subject: 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 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) --- testsuite/tests/ghci/scripts/T11975.script | 4 ---- 1 file changed, 4 deletions(-) (limited to 'testsuite/tests/ghci/scripts/T11975.script') diff --git a/testsuite/tests/ghci/scripts/T11975.script b/testsuite/tests/ghci/scripts/T11975.script index 80061ef97b..72b1a5caff 100644 --- a/testsuite/tests/ghci/scripts/T11975.script +++ b/testsuite/tests/ghci/scripts/T11975.script @@ -1,9 +1,5 @@ :set -fprint-explicit-foralls :type mapM -:type +v mapM -:t +v mapM let foo :: (Show a, Num b) => a -> b; foo = undefined :set -XTypeApplications :type foo @Int -:type +v foo @Int -:t +v foo @Int -- cgit v1.2.1