Commit 97cff919 authored by Simon Peyton Jones's avatar Simon Peyton Jones Committed by Marge Bot

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 df084681
    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)
parent 04d64331
......@@ -40,6 +40,7 @@ import GHC.Hs.Binds
-- others:
import GHC.Tc.Types.Evidence
import GHC.Core
import GHC.Types.Id( Id )
import GHC.Types.Name
import GHC.Types.Name.Set
import GHC.Types.Basic
......@@ -251,8 +252,8 @@ data HsExpr p
-- Turned from HsVar to HsUnboundVar by the
-- renamer, when it finds an out-of-scope
-- variable or hole.
-- Turned into HsVar by type checker, to support
-- deferred type errors.
-- The (XUnboundVar p) field becomes Id
-- after typechecking
| HsConLikeOut (XConLikeOut p)
ConLike -- ^ After typechecker only; must be different
......@@ -260,7 +261,9 @@ data HsExpr p
| HsRecFld (XRecFld p)
(AmbiguousFieldOcc p) -- ^ Variable pointing to record selector
-- Not in use after typechecking
-- The parser produces HsVars
-- The renamer renames record-field selectors to HsRecFld
-- The typechecker preserves HsRecFld
| HsOverLabel (XOverLabel p)
(Maybe (IdP p)) FastString
......@@ -592,7 +595,6 @@ deriving instance (Data (hs_syn GhcTc), Typeable hs_syn) => Data (HsWrap hs_syn)
-- ---------------------------------------------------------------------
type instance XVar (GhcPass _) = NoExtField
type instance XUnboundVar (GhcPass _) = NoExtField
type instance XConLikeOut (GhcPass _) = NoExtField
type instance XRecFld (GhcPass _) = NoExtField
type instance XOverLabel (GhcPass _) = NoExtField
......@@ -603,6 +605,10 @@ type instance XLam (GhcPass _) = NoExtField
type instance XLamCase (GhcPass _) = NoExtField
type instance XApp (GhcPass _) = NoExtField
type instance XUnboundVar GhcPs = NoExtField
type instance XUnboundVar GhcRn = NoExtField
type instance XUnboundVar GhcTc = Id
type instance XAppTypeE GhcPs = NoExtField
type instance XAppTypeE GhcRn = NoExtField
type instance XAppTypeE GhcTc = Type
......@@ -1049,14 +1055,15 @@ ppr_lexpr e = ppr_expr (unLoc e)
ppr_expr :: forall p. (OutputableBndrId p)
=> HsExpr (GhcPass p) -> SDoc
ppr_expr (HsVar _ (L _ v)) = pprPrefixOcc v
ppr_expr (HsUnboundVar _ uv)= pprPrefixOcc uv
ppr_expr (HsConLikeOut _ c) = pprPrefixOcc c
ppr_expr (HsIPVar _ v) = ppr v
ppr_expr (HsOverLabel _ _ l)= char '#' <> ppr l
ppr_expr (HsLit _ lit) = ppr lit
ppr_expr (HsOverLit _ lit) = ppr lit
ppr_expr (HsPar _ e) = parens (ppr_lexpr e)
ppr_expr (HsVar _ (L _ v)) = pprPrefixOcc v
ppr_expr (HsUnboundVar _ uv) = pprPrefixOcc uv
ppr_expr (HsConLikeOut _ c) = pprPrefixOcc c
ppr_expr (HsRecFld _ f) = pprPrefixOcc f
ppr_expr (HsIPVar _ v) = ppr v
ppr_expr (HsOverLabel _ _ l) = char '#' <> ppr l
ppr_expr (HsLit _ lit) = ppr lit
ppr_expr (HsOverLit _ lit) = ppr lit
ppr_expr (HsPar _ e) = parens (ppr_lexpr e)
ppr_expr (HsPragE _ prag e) = sep [ppr prag, ppr_lexpr e]
......@@ -1212,7 +1219,6 @@ ppr_expr (HsBinTick _ tickIdTrue tickIdFalse exp)
text ">(",
ppr exp, text ")"]
ppr_expr (HsRecFld _ f) = ppr f
ppr_expr (XExpr x) = case ghcPass @p of
#if __GLASGOW_HASKELL__ < 811
GhcPs -> ppr x
......@@ -1377,7 +1383,6 @@ isAtomicHsExpr (HsOverLit {}) = True
isAtomicHsExpr (HsIPVar {}) = True
isAtomicHsExpr (HsOverLabel {}) = True
isAtomicHsExpr (HsUnboundVar {}) = True
isAtomicHsExpr (HsPar _ e) = isAtomicHsExpr (unLoc e)
isAtomicHsExpr (HsRecFld{}) = True
isAtomicHsExpr (XExpr x)
| GhcTc <- ghcPass @p = case x of
......
......@@ -478,7 +478,7 @@ data HsRecField' id arg = HsRecField {
--
-- hsRecFieldLbl = Unambiguous "x" $sel:x:MkS :: AmbiguousFieldOcc Id
--
-- See also Note [Disambiguating record fields] in GHC.Tc.Gen.Expr.
-- See also Note [Disambiguating record fields] in GHC.Tc.Gen.Head.
hsRecFields :: HsRecFields p arg -> [XCFieldOcc p]
hsRecFields rbinds = map (unLoc . hsRecFieldSel . unLoc) (rec_flds rbinds)
......
......@@ -348,7 +348,7 @@ data HsForAllTelescope pass
{ hsf_xvis :: XHsForAllVis pass
, hsf_vis_bndrs :: [LHsTyVarBndr () pass]
}
| HsForAllInvis -- ^ An invisible @forall@ (e.g., @forall a {b} c -> {...}@),
| HsForAllInvis -- ^ An invisible @forall@ (e.g., @forall a {b} c. {...}@),
-- where each binder has a 'Specificity'.
{ hsf_xinvis :: XHsForAllInvis pass
, hsf_invis_bndrs :: [LHsTyVarBndr Specificity pass]
......@@ -1712,7 +1712,7 @@ mkFieldOcc rdr = FieldOcc noExtField rdr
-- occurrences).
--
-- See Note [HsRecField and HsRecUpdField] in "GHC.Hs.Pat" and
-- Note [Disambiguating record fields] in "GHC.Tc.Gen.Expr".
-- Note [Disambiguating record fields] in "GHC.Tc.Gen.Head".
-- See Note [Located RdrNames] in "GHC.Hs.Expr"
data AmbiguousFieldOcc pass
= Unambiguous (XUnambiguous pass) (Located RdrName)
......
......@@ -505,23 +505,25 @@ addBinTickLHsExpr boxLabel (L pos e0)
-- in the addTickLHsExpr family of functions.)
addTickHsExpr :: HsExpr GhcTc -> TM (HsExpr GhcTc)
addTickHsExpr e@(HsVar _ (L _ id)) = do freeVar id; return e
addTickHsExpr (HsUnboundVar {}) = panic "addTickHsExpr.HsUnboundVar"
addTickHsExpr e@(HsVar _ (L _ id)) = do freeVar id; return e
addTickHsExpr e@(HsUnboundVar id _) = do freeVar id; return e
addTickHsExpr e@(HsRecFld _ (Ambiguous id _)) = do freeVar id; return e
addTickHsExpr e@(HsRecFld _ (Unambiguous id _)) = do freeVar id; return e
addTickHsExpr e@(HsConLikeOut _ con)
| Just id <- conLikeWrapId_maybe con = do freeVar id; return e
addTickHsExpr e@(HsIPVar {}) = return e
addTickHsExpr e@(HsOverLit {}) = return e
addTickHsExpr e@(HsOverLabel{}) = return e
addTickHsExpr e@(HsLit {}) = return e
addTickHsExpr (HsLam x matchgroup) = liftM (HsLam x)
(addTickMatchGroup True matchgroup)
addTickHsExpr (HsLamCase x mgs) = liftM (HsLamCase x)
(addTickMatchGroup True mgs)
addTickHsExpr (HsApp x e1 e2) = liftM2 (HsApp x) (addTickLHsExprNever e1)
(addTickLHsExpr e2)
addTickHsExpr (HsAppType x e ty) = liftM3 HsAppType (return x)
(addTickLHsExprNever e)
(return ty)
addTickHsExpr e@(HsIPVar {}) = return e
addTickHsExpr e@(HsOverLit {}) = return e
addTickHsExpr e@(HsOverLabel{}) = return e
addTickHsExpr e@(HsLit {}) = return e
addTickHsExpr (HsLam x mg) = liftM (HsLam x)
(addTickMatchGroup True mg)
addTickHsExpr (HsLamCase x mgs) = liftM (HsLamCase x)
(addTickMatchGroup True mgs)
addTickHsExpr (HsApp x e1 e2) = liftM2 (HsApp x) (addTickLHsExprNever e1)
(addTickLHsExpr e2)
addTickHsExpr (HsAppType x e ty) = liftM3 HsAppType (return x)
(addTickLHsExprNever e)
(return ty)
addTickHsExpr (OpApp fix e1 e2 e3) =
liftM4 OpApp
......
......@@ -261,10 +261,14 @@ dsLExprNoLP (L loc e)
; return e' }
dsExpr :: HsExpr GhcTc -> DsM CoreExpr
dsExpr (HsVar _ (L _ id)) = dsHsVar id
dsExpr (HsRecFld _ (Unambiguous id _)) = dsHsVar id
dsExpr (HsRecFld _ (Ambiguous id _)) = dsHsVar id
dsExpr (HsUnboundVar id _) = dsHsVar id
dsExpr (HsPar _ e) = dsLExpr e
dsExpr (ExprWithTySig _ e _) = dsLExpr e
dsExpr (HsVar _ (L _ var)) = dsHsVar var
dsExpr (HsUnboundVar {}) = panic "dsExpr: HsUnboundVar" -- Typechecker eliminates them
dsExpr (HsConLikeOut _ con) = dsConLike con
dsExpr (HsIPVar {}) = panic "dsExpr: HsIPVar"
dsExpr (HsOverLabel{}) = panic "dsExpr: HsOverLabel"
......@@ -806,7 +810,6 @@ dsExpr (HsBinTick _ ixT ixF e) = do
-- HsSyn constructs that just shouldn't be here:
dsExpr (HsBracket {}) = panic "dsExpr:HsBracket"
dsExpr (HsDo {}) = panic "dsExpr:HsDo"
dsExpr (HsRecFld {}) = panic "dsExpr:HsRecFld"
ds_prag_expr :: HsPragE GhcTc -> LHsExpr GhcTc -> DsM CoreExpr
ds_prag_expr (HsPragSCC _ _ cc) expr = do
......
......@@ -785,6 +785,7 @@ class ( IsPass p
, Data (HsTupArg (GhcPass p))
, Data (IPBind (GhcPass p))
, ToHie (Context (Located (IdGhcP p)))
, ToHie (Context (Located (XUnboundVar (GhcPass p))))
, ToHie (RFContext (Located (AmbiguousFieldOcc (GhcPass p))))
, ToHie (RFContext (Located (FieldOcc (GhcPass p))))
, ToHie (TScoped (LHsWcType (GhcPass (NoGhcTcPass p))))
......@@ -799,6 +800,9 @@ instance HiePass 'Renamed where
instance HiePass 'Typechecked where
hiePass = HieTc
instance ToHie (Context (Located NoExtField)) where
toHie _ = pure []
instance HiePass p => ToHie (BindContext (Located (HsBind (GhcPass p)))) where
toHie (BC context scope b@(L span bind)) =
concatM $ getTypeNode b : case bind of
......@@ -1042,8 +1046,8 @@ instance HiePass p => ToHie (Located (HsExpr (GhcPass p))) where
[ toHie $ C Use (L mspan var)
-- Patch up var location since typechecker removes it
]
HsUnboundVar _ _ ->
[]
HsUnboundVar var _ ->
[ toHie $ C Use (L mspan var) ]
HsConLikeOut _ con ->
[ toHie $ C Use $ L mspan $ conLikeName con
]
......
......@@ -1634,7 +1634,7 @@ patSynErr item l e explanation =
explanation
; return (L l hsHoleExpr) }
hsHoleExpr :: HsExpr (GhcPass id)
hsHoleExpr :: HsExpr GhcPs
hsHoleExpr = HsUnboundVar noExtField (mkVarOcc "_")
-- | See Note [Ambiguous syntactic categories] and Note [PatBuilder]
......
......@@ -749,7 +749,7 @@ rnHsRecUpdFields flds
= do { let lbl = rdrNameAmbiguousFieldOcc f
; sel <- setSrcSpan loc $
-- Defer renaming of overloaded fields to the typechecker
-- See Note [Disambiguating record fields] in GHC.Tc.Gen.Expr
-- See Note [Disambiguating record fields] in GHC.Tc.Gen.Head
if overload_ok
then do { mb <- lookupGlobalOccRn_overloaded
overload_ok lbl
......
......@@ -81,7 +81,6 @@ import GHC.ByteCode.Types
import GHC.Runtime.Linker as Linker
import GHC.Driver.Session
import GHC.Driver.Ppr
import GHC.LanguageExtensions
import GHC.Types.Unique
import GHC.Types.Unique.Supply
import GHC.Utils.Monad
......@@ -1283,10 +1282,7 @@ obtainTermFromVal hsc_env _bound _force _ty _x = withInterp hsc_env $ \case
obtainTermFromId :: HscEnv -> Int -> Bool -> Id -> IO Term
obtainTermFromId hsc_env bound force id = do
hv <- Linker.getHValue hsc_env (varName id)
cvObtainTerm (updEnv hsc_env) bound force (idType id) hv
where updEnv env = env {hsc_dflags = -- #14828
xopt_set (hsc_dflags env) ImpredicativeTypes}
-- See Note [Setting ImpredicativeTypes for :print command]
cvObtainTerm hsc_env bound force (idType id) hv
-- Uses RTTI to reconstruct the type of an Id, making it less polymorphic
reconstructType :: HscEnv -> Int -> Id -> IO (Maybe Type)
......@@ -1296,39 +1292,3 @@ reconstructType hsc_env bound id = do
mkRuntimeUnkTyVar :: Name -> Kind -> TyVar
mkRuntimeUnkTyVar name kind = mkTcTyVar name kind RuntimeUnk
{-
Note [Setting ImpredicativeTypes for :print command]
If ImpredicativeTypes is not enabled, then `:print <term>` will fail if the
type of <term> has nested `forall`s or `=>`s.
This is because the GHCi debugger's internals will attempt to unify a
metavariable with the type of <term> and then display the result, but if the
type has nested `forall`s or `=>`s, then unification will fail.
As a result, `:print` will bail out and the unhelpful result will be
`<term> = (_t1::t1)` (where `t1` is a metavariable).
Beware: <term> can have nested `forall`s even if its definition doesn't use
RankNTypes! Here is an example from #14828:
class Functor f where
fmap :: (a -> b) -> f a -> f b
Somewhat surprisingly, `:print fmap` considers the type of fmap to have
nested foralls. This is because the GHCi debugger sees the type
`fmap :: forall f. Functor f => forall a b. (a -> b) -> f a -> f b`.
We could envision deeply instantiating this type to get the type
`forall f a b. Functor f => (a -> b) -> f a -> f b`,
but this trick wouldn't work for higher-rank types.
Instead, we adopt a simpler fix: enable `ImpredicativeTypes` when using
`:print` and friends in the GHCi debugger. This allows metavariables
to unify with types that have nested (or higher-rank) `forall`s/`=>`s,
which makes `:print fmap` display as
`fmap = (_t1::forall a b. Functor f => (a -> b) -> f a -> f b)`, as expected.
Although ImpredicativeTypes is a somewhat unpredictable from a type inference
perspective, there is no danger in using it in the GHCi debugger, since all
of the terms that the GHCi debugger deals with have already been typechecked.
-}
......@@ -559,11 +559,52 @@ trIO = liftTcM . liftIO
liftTcM :: TcM a -> TR a
liftTcM = id
-- When we make new unification variables in the GHCi debugger,
-- we use RuntimeUnkTvs. See Note [RuntimeUnkTv].
newVar :: Kind -> TR TcType
newVar = liftTcM . newFlexiTyVarTy
newVar kind = liftTcM (do { tv <- newAnonMetaTyVar RuntimeUnkTv kind
; return (mkTyVarTy tv) })
newOpenVar :: TR TcType
newOpenVar = liftTcM newOpenFlexiTyVarTy
newOpenVar = liftTcM (do { kind <- newOpenTypeKind
; newVar kind })
{- Note [RuntimeUnkTv]
~~~~~~~~~~~~~~~~~~~~~~
In the GHCi debugger we use unification variables whose MetaInfo is
RuntimeUnkTv. The special property of a RuntimeUnkTv is that it can
unify with a polytype (see GHC.Tc.Utils.Unify.metaTyVarUpdateOK).
If we don't do this `:print <term>` will fail if the type of <term>
has nested `forall`s or `=>`s.
This is because the GHCi debugger's internals will attempt to unify a
metavariable with the type of <term> and then display the result, but
if the type has nested `forall`s or `=>`s, then unification will fail
unless we do something special. As a result, `:print` will bail out
and the unhelpful result will be `<term> = (_t1::t1)` (where `t1` is a
metavariable).
Beware: <term> can have nested `forall`s even if its definition doesn't use
RankNTypes! Here is an example from #14828:
class Functor f where
fmap :: (a -> b) -> f a -> f b
Somewhat surprisingly, `:print fmap` considers the type of fmap to have
nested foralls. This is because the GHCi debugger sees the type
`fmap :: forall f. Functor f => forall a b. (a -> b) -> f a -> f b`.
We could envision deeply instantiating this type to get the type
`forall f a b. Functor f => (a -> b) -> f a -> f b`,
but this trick wouldn't work for higher-rank types.
Instead, we adopt a simpler fix: allow RuntimeUnkTv to unify with a
polytype (specifically, see ghci_tv in GHC.Tc.Utils.Unify.preCheck).
This allows metavariables to unify with types that have
nested (or higher-rank) `forall`s/`=>`s, which makes `:print fmap`
display as
`fmap = (_t1::forall a b. Functor f => (a -> b) -> f a -> f b)`, as expected.
-}
instTyVars :: [TyVar] -> TR (TCvSubst, [TcTyVar])
-- Instantiate fresh mutable type variables from some TyVars
......@@ -578,6 +619,10 @@ type RttiInstantiation = [(TcTyVar, TyVar)]
-- If the TcTyVar has not been refined by the runtime type
-- elaboration, then we want to turn it back into the
-- original RuntimeUnk
--
-- July 20: I'm not convinced that the little dance from
-- RuntimeUnkTv unification variables to RuntimeUnk skolems
-- is buying us anything. ToDo: get rid of it.
-- | Returns the instantiated type scheme ty', and the
-- mapping from new (instantiated) -to- old (skolem) type variables
......@@ -585,6 +630,7 @@ instScheme :: QuantifiedType -> TR (TcType, RttiInstantiation)
instScheme (tvs, ty)
= do { (subst, tvs') <- instTyVars tvs
; let rtti_inst = [(tv',tv) | (tv',tv) <- tvs' `zip` tvs]
; traceTR (text "instScheme" <+> (ppr tvs $$ ppr ty $$ ppr tvs'))
; return (substTy subst ty, rtti_inst) }
applyRevSubst :: RttiInstantiation -> TR ()
......
......@@ -1691,19 +1691,14 @@ a polytype. E.g.
@(T x -> forall b. b -> b)
op
The use of type applications is crucial here. If we had tried using only
explicit type signatures, like so:
The use of type applications is crucial here. We have to instantiate
both type args of (coerce :: Coercible a b => a -> b) to polytypes,
and we can only do that with VTA or Quick Look. Here VTA seems more
appropriate for machine generated code: it's simple and robust.
instance C <rep-ty> => C (T x) where
op :: T x -> forall b. b -> b
op = coerce (op :: <rep-ty> -> forall b. b -> b)
Then GHC will attempt to deeply skolemize the two type signatures, which will
wreak havoc with the Coercible solver. Therefore, we instead use type
applications, which do not deeply skolemize and thus avoid this issue.
The downside is that we currently require -XImpredicativeTypes to permit this
polymorphic type instantiation, so we have to switch that flag on locally in
GHC.Tc.Deriv.genInst. See #8503 for more discussion.
However, to allow VTA with polytypes we must switch on
-XImpredicativeTypes locally in GHC.Tc.Deriv.genInst.
See #8503 for more discussion.
Note [Newtype-deriving trickiness]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......@@ -1807,9 +1802,8 @@ break this example (from the T15290d test case):
c = coerce @(Int -> forall b. b -> Int)
c
That is because the instance signature deeply skolemizes the forall-bound
`b`, which wreaks havoc with the `Coercible` solver. An additional visible type
argument of @(Int -> forall b. b -> Age) is enough to prevent this.
That is because we still need to instantiate the second argument of
coerce with a polytype, and we can only do that with VTA or QuickLook.
Be aware that the use of an instance signature doesn't /solve/ this
problem; it just makes it less likely to occur. For example, if a class has
......
This diff is collapsed.
......@@ -15,10 +15,11 @@ module GHC.Tc.Gen.Arrow ( tcProc ) where
import GHC.Prelude
import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcCheckMonoExpr, tcInferRho, tcSyntaxOp
, tcCheckId, tcCheckPolyExpr )
, tcCheckPolyExpr )
import GHC.Hs
import GHC.Tc.Gen.Match
import GHC.Tc.Gen.Head( tcCheckId )
import GHC.Tc.Utils.Zonk( hsLPatType )
import GHC.Tc.Utils.TcType
import GHC.Tc.Utils.TcMType
......
This diff is collapsed.
module GHC.Tc.Gen.Expr where
import GHC.Types.Name
import GHC.Hs ( HsExpr, LHsExpr, SyntaxExprRn, SyntaxExprTc )
import GHC.Hs ( HsExpr, LHsExpr, SyntaxExprRn
, SyntaxExprTc )
import GHC.Tc.Utils.TcType ( TcRhoType, TcSigmaType, SyntaxOpType, ExpType, ExpRhoType )
import GHC.Tc.Types ( TcM )
import GHC.Tc.Types.Origin ( CtOrigin )
import GHC.Core.Type ( Mult )
import GHC.Hs.Extension ( GhcRn, GhcTc )
tcCheckPolyExpr ::
tcCheckPolyExpr, tcCheckPolyExprNC ::
LHsExpr GhcRn
-> TcSigmaType
-> TcM (LHsExpr GhcTc)
......@@ -23,8 +23,6 @@ tcCheckMonoExpr, tcCheckMonoExprNC ::
tcExpr :: HsExpr GhcRn -> ExpRhoType -> TcM (HsExpr GhcTc)
tcInferSigma :: LHsExpr GhcRn -> TcM (LHsExpr GhcTc, TcSigmaType)
tcInferRho, tcInferRhoNC ::
LHsExpr GhcRn -> TcM (LHsExpr GhcTc, TcRhoType)
......@@ -42,5 +40,3 @@ tcSyntaxOpGen :: CtOrigin
-> ([TcSigmaType] -> [Mult] -> TcM a)
-> TcM (a, SyntaxExprTc)
tcCheckId :: Name -> ExpRhoType -> TcM (HsExpr GhcTc)
This diff is collapsed.
......@@ -39,13 +39,14 @@ import GHC.Prelude
import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcSyntaxOp, tcInferRho, tcInferRhoNC
, tcMonoExpr, tcMonoExprNC, tcExpr
, tcCheckMonoExpr, tcCheckMonoExprNC
, tcCheckPolyExpr, tcCheckId )
, tcCheckPolyExpr )
import GHC.Types.Basic (LexicalFixity(..))
import GHC.Hs
import GHC.Tc.Utils.Monad
import GHC.Tc.Utils.Env
import GHC.Tc.Gen.Pat
import GHC.Tc.Gen.Head( tcCheckId )
import GHC.Tc.Utils.TcMType
import GHC.Tc.Utils.TcType
import GHC.Tc.Gen.Bind
......
......@@ -426,10 +426,9 @@ tc_pat pat_ty penv ps_pat thing_inside = case ps_pat of
-- Note [View patterns and polymorphism]
-- Expression must be a function
; let expr_orig = lexprCtOrigin expr
herald = text "A view pattern expression expects"
; let herald = text "A view pattern expression expects"
; (expr_wrap1, Scaled _mult inf_arg_ty, inf_res_sigma)
<- matchActualFunTySigma herald expr_orig (Just (unLoc expr)) (1,[]) expr_ty
<- matchActualFunTySigma herald (Just (ppr expr)) (1,[]) expr_ty
-- See Note [View patterns and polymorphism]
-- expr_wrap1 :: expr_ty "->" (inf_arg_ty -> inf_res_sigma)
......
......@@ -74,6 +74,8 @@ import GHC.Builtin.Utils
import GHC.Types.Name.Reader
import GHC.Tc.Utils.Zonk
import GHC.Tc.Gen.Expr
import GHC.Tc.Errors( reportAllUnsolved )
import GHC.Tc.Gen.App( tcInferSigma )
import GHC.Tc.Utils.Monad
import GHC.Tc.Gen.Export
import GHC.Tc.Types.Evidence
......@@ -99,6 +101,7 @@ import GHC.Tc.TyCl.Instance
import GHC.IfaceToCore
import GHC.Tc.Utils.TcMType
import GHC.Tc.Utils.TcType
import GHC.Tc.Utils.Instantiate (tcGetInsts)
import GHC.Tc.Solver
import GHC.Tc.TyCl
import GHC.Tc.Instance.Typeable ( mkTypeableBinds )
......@@ -136,7 +139,6 @@ import GHC.Data.FastString
import GHC.Data.Maybe
import GHC.Utils.Misc
import GHC.Data.Bag
import GHC.Tc.Utils.Instantiate (tcGetInsts)
import qualified GHC.LanguageExtensions as LangExt
import Data.Data ( Data )
import GHC.Hs.Dump
......@@ -2478,9 +2480,9 @@ isGHCiMonad hsc_env ty
Nothing -> failWithTc $ text ("Can't find type:" ++ ty)
-- | How should we infer a type? See Note [TcRnExprMode]
data TcRnExprMode = TM_Inst -- ^ Instantiate the type fully (:type)
| TM_NoInst -- ^ Do not instantiate the type (:type +v)
| TM_Default -- ^ Default the type eagerly (:type +d)
data TcRnExprMode = TM_Inst -- ^ Instantiate inferred quantifiers only (:type)
| TM_Default -- ^ Instantiate all quantifiers,
-- and do eager defaulting (:type +d)
-- | tcRnExpr just finds the type of an expression
-- for :type
......@@ -2495,16 +2497,15 @@ tcRnExpr hsc_env mode rdr_expr
(rn_expr, _fvs) <- rnLExpr rdr_expr ;
failIfErrsM ;
-- 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, (_tc_expr, res_ty)), lie)
-- Typecheck the expression
((tclvl, res_ty), lie)
<- captureTopConstraints $
pushTcLevelM $
tc_infer rn_expr ;
tcInferSigma inst rn_expr ;
-- Generalise
uniq <- newUnique ;
let { fresh_it = itName uniq (getLoc rdr_expr) } ;
(qtvs, dicts, _, residual, _)
<- simplifyInfer tclvl infer_mode
[] {- No sig vars -}
......@@ -2528,14 +2529,10 @@ tcRnExpr hsc_env mode rdr_expr
return (snd (normaliseType fam_envs Nominal ty))
}
where
tc_infer expr | inst = tcInferRho expr
| otherwise = tcInferSigma expr
-- tcInferSigma: see Note [Implementing :type]
-- Optionally instantiate the type of the expression
-- See Note [TcRnExprMode]
(inst, infer_mode, perhaps_disable_default_warnings) = case mode of
TM_Inst -> (True, NoRestrictions, id)
TM_NoInst -> (False, NoRestrictions, id)
TM_Inst -> (False, NoRestrictions, id)
TM_Default -> (True, EagerDefaulting, unsetWOptM Opt_WarnTypeDefaults)
{- Note [Implementing :type]
......@@ -2621,32 +2618,20 @@ tcRnType hsc_env flexi normalise rdr_type
{- Note [TcRnExprMode]
~~~~~~~~~~~~~~~~~~~~~~
How should we infer a type when a user asks for the type of an expression e
at the GHCi prompt? We offer 3 different possibilities, described below. Each
considers this example, with -fprint-explicit-foralls enabled:
foo :: forall a f b. (Show a, Num b, Foldable f) => a -> f b -> String
:type{,-spec,-def} foo @Int
at the GHCi prompt? We offer 2 different possibilities, described below. Each
considers this example, with -fprint-explicit-foralls enabled. See also
https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0179-printing-foralls.rst
:type / TM_Inst
In this mode, we report the type that would be inferred if a variable
were assigned to expression e, without applying the monomorphism restriction.
This means we instantiate the type and then regeneralize, as discussed
in #11376.
In this mode, we report the type obained by instantiating only the
/inferred/ quantifiers of e's type, solving constraints, and
re-generalising, as discussed in #11376.
> :type foo @Int
forall {b} {f :: * -> *}. (Foldable f, Num b) => Int -> f b -> String
Note that the variables and constraints are reordered here, because this
is possible during regeneralization. Also note that the variables are
reported as Inferred instead of Specified.
:type +v / TM_NoInst
This mode is for the benefit of users using TypeApplications. It does no
instantiation whatsoever, sometimes meaning that class constraints are not
solved.
> :type reverse
reverse :: forall a. [a] -> [a]
-- foo :: forall a f b. (Show a, Num b, Foldable f) => a -> f b -> String
> :type +v foo @Int