From f2a2b79fa8d1c702b17e195a70734b06625e0153 Mon Sep 17 00:00:00 2001 From: Simon Peyton Jones Date: Mon, 4 Apr 2016 10:18:43 +0100 Subject: Deeply instantiate in :type See Trac #11376 and Note [Deeply instantiate in :type] in TcRnDriver Sadly this showed up one new problem (Trac #11786) and one opportunity (Trac #11787), so test T11549 is now marked expect-broken on these two. --- compiler/typecheck/TcRnDriver.hs | 31 +++++++++++++++++++++---- testsuite/tests/dependent/ghci/T11549.script | 8 +++---- testsuite/tests/dependent/ghci/all.T | 3 ++- testsuite/tests/ghci/scripts/T11376.script | 6 +++++ testsuite/tests/ghci/scripts/T11376.stdout | 2 ++ testsuite/tests/ghci/scripts/TypeAppData.stdout | 28 +++++++++++----------- testsuite/tests/ghci/scripts/all.T | 1 + 7 files changed, 56 insertions(+), 23 deletions(-) create mode 100644 testsuite/tests/ghci/scripts/T11376.script create mode 100644 testsuite/tests/ghci/scripts/T11376.stdout diff --git a/compiler/typecheck/TcRnDriver.hs b/compiler/typecheck/TcRnDriver.hs index 550f84fe7d..640d74dfc8 100644 --- a/compiler/typecheck/TcRnDriver.hs +++ b/compiler/typecheck/TcRnDriver.hs @@ -33,6 +33,7 @@ import RnSplice ( rnTopSpliceDecls, traceSplice, SpliceInfo(..) ) import IfaceEnv( externaliseName ) import TcHsType import TcMatches +import Inst( deeplyInstantiate ) import RnTypes import RnExpr import MkId @@ -1977,9 +1978,16 @@ tcRnExpr hsc_env rdr_expr -- Now typecheck the expression, and generalise its type -- it might have a rank-2 type (e.g. :t runST) uniq <- newUnique ; - let { fresh_it = itName uniq (getLoc rdr_expr) } ; - (tclvl, lie, (_tc_expr, res_ty)) <- pushLevelAndCaptureConstraints $ - tcInferSigma rn_expr ; + let { fresh_it = itName uniq (getLoc rdr_expr) + ; orig = OccurrenceOf fresh_it } ; -- Not a very satisfactory origin + (tclvl, lie, res_ty) + <- pushLevelAndCaptureConstraints $ + do { (_tc_expr, expr_ty) <- tcInferSigma rn_expr + ; (_wrap, res_ty) <- deeplyInstantiate orig expr_ty + -- See [Note Deeply instantiate in :type] + ; return res_ty } ; + + -- Generalise ((qtvs, dicts, _), lie_top) <- captureConstraints $ {-# SCC "simplifyInfer" #-} simplifyInfer tclvl @@ -2055,7 +2063,22 @@ tcRnType hsc_env normalise rdr_type ; return (ty', mkInvForAllTys kvs (typeKind ty')) } -{- Note [Kind-generalise in tcRnType] +{- Note [Deeply instantiate in :type] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Suppose (Trac #11376) + bar :: forall a b. Show a => a -> b -> a +What should `:t bar @Int` show? + + 1. forall b. Show Int => Int -> b -> Int + 2. forall b. Int -> b -> Int + 3. forall {b}. Int -> b -> Int + 4. Int -> b -> Int + +We choose (3), which is the effect of deeply instantiating and +re-generalising. All the others seem deeply confusing. That is +why we deeply instantiate here. + +Note [Kind-generalise in tcRnType] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ We switch on PolyKinds when kind-checking a user type, so that we will kind-generalise the type, even when PolyKinds is not otherwise on. diff --git a/testsuite/tests/dependent/ghci/T11549.script b/testsuite/tests/dependent/ghci/T11549.script index 5f8c500519..bb35589671 100644 --- a/testsuite/tests/dependent/ghci/T11549.script +++ b/testsuite/tests/dependent/ghci/T11549.script @@ -3,12 +3,12 @@ import GHC.Exts putStrLn "-fno-print-explicit-runtime-reps" :set -fno-print-explicit-runtime-reps -:ty ($) +:info ($) :kind TYPE -:ty error +:info error putStrLn "\n-fprint-explicit-runtime-reps" :set -fprint-explicit-runtime-reps -:ty ($) +:info ($) :kind TYPE -:ty error +:info error diff --git a/testsuite/tests/dependent/ghci/all.T b/testsuite/tests/dependent/ghci/all.T index 6d9332adaa..956272fa55 100644 --- a/testsuite/tests/dependent/ghci/all.T +++ b/testsuite/tests/dependent/ghci/all.T @@ -1,3 +1,4 @@ test('T11549', - normal, + [ expect_broken( 11787 ), + expect_broken( 11786 ) ], ghci_script, ['T11549.script']) diff --git a/testsuite/tests/ghci/scripts/T11376.script b/testsuite/tests/ghci/scripts/T11376.script new file mode 100644 index 0000000000..780db3c088 --- /dev/null +++ b/testsuite/tests/ghci/scripts/T11376.script @@ -0,0 +1,6 @@ +:set -XTypeApplications +let { bar :: Show a => a -> b -> a; bar = error "urk" } +:type bar @Int +:set -fprint-explicit-foralls +:type bar @Int + diff --git a/testsuite/tests/ghci/scripts/T11376.stdout b/testsuite/tests/ghci/scripts/T11376.stdout new file mode 100644 index 0000000000..0b0b95922f --- /dev/null +++ b/testsuite/tests/ghci/scripts/T11376.stdout @@ -0,0 +1,2 @@ +bar @Int :: Int -> b -> Int +bar @Int :: forall {b}. Int -> b -> Int diff --git a/testsuite/tests/ghci/scripts/TypeAppData.stdout b/testsuite/tests/ghci/scripts/TypeAppData.stdout index 5a4880a6df..0fd5506638 100644 --- a/testsuite/tests/ghci/scripts/TypeAppData.stdout +++ b/testsuite/tests/ghci/scripts/TypeAppData.stdout @@ -1,14 +1,14 @@ -P1 :: forall {k} (a :: k). P1 a -P2 :: forall k (a :: k). P2 a -P3 :: forall k (a :: k). P3 k a -P4 :: forall {k} (a :: k). P1 a -> P4 a -P5 :: forall {k} (a :: k). P1 a -> P5 -P6 :: forall k (a :: k). P1 a -> P6 -P7 :: forall {k} (a :: k). P1 a -P8 :: forall {k} (a :: k). P1 a -P9 :: forall k (a :: k). P1 a -P10 :: forall k (a :: k). P1 a -P11 :: forall {k} (a :: k). P1 a -> P5 -P12 :: forall {k} (a :: k). P1 a -> P5 -P13 :: forall k (a :: k). P1 a -> P5 -P14 :: forall k (a :: k). P1 a -> P5 +P1 :: forall {k} {a :: k}. P1 a +P2 :: forall {k} {a :: k}. P2 a +P3 :: forall {k} {a :: k}. P3 k a +P4 :: forall {k} {a :: k}. P1 a -> P4 a +P5 :: forall {k} {a :: k}. P1 a -> P5 +P6 :: forall {k} {a :: k}. P1 a -> P6 +P7 :: forall {k} {a :: k}. P1 a +P8 :: forall {k} {a :: k}. P1 a +P9 :: forall {k} {a :: k}. P1 a +P10 :: forall {k} {a :: k}. P1 a +P11 :: forall {k} {a :: k}. P1 a -> P5 +P12 :: forall {k} {a :: k}. P1 a -> P5 +P13 :: forall {k} {a :: k}. P1 a -> P5 +P14 :: forall {k} {a :: k}. P1 a -> P5 diff --git a/testsuite/tests/ghci/scripts/all.T b/testsuite/tests/ghci/scripts/all.T index 8fab9566a2..2d21772434 100755 --- a/testsuite/tests/ghci/scripts/all.T +++ b/testsuite/tests/ghci/scripts/all.T @@ -248,3 +248,4 @@ test('T11524a', normal, ghci_script, ['T11524a.script']) test('T11456', normal, ghci_script, ['T11456.script']) test('TypeAppData', normal, ghci_script, ['TypeAppData.script']) test('T11728', normal, ghci_script, ['T11728.script']) +test('T11376', normal, ghci_script, ['T11376.script']) -- cgit v1.2.1