Commit f2a2b79f authored by Simon Peyton Jones's avatar Simon Peyton Jones

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.
parent 72bd7f7b
......@@ -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.
......
......@@ -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
test('T11549',
normal,
[ expect_broken( 11787 ),
expect_broken( 11786 ) ],
ghci_script, ['T11549.script'])
:set -XTypeApplications
let { bar :: Show a => a -> b -> a; bar = error "urk" }
:type bar @Int
:set -fprint-explicit-foralls
:type bar @Int
bar @Int :: Int -> b -> Int
bar @Int :: forall {b}. Int -> b -> Int
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
......@@ -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'])
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment