Commit 7c0c76fb authored by Roland Senn's avatar Roland Senn Committed by Marge Bot

Set `ImpredicativeTypes` during :print command. (#14828)

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 is 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.
parent dbea7e9d
Pipeline #16382 passed with stages
in 519 minutes and 54 seconds
......@@ -79,6 +79,7 @@ import VarEnv
import GHC.ByteCode.Types
import GHC.Runtime.Linker as Linker
import GHC.Driver.Session
import GHC.LanguageExtensions
import Unique
import UniqSupply
import MonadUtils
......@@ -1256,7 +1257,10 @@ 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 hsc_env bound force (idType id) hv
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]
-- Uses RTTI to reconstruct the type of an Id, making it less polymorphic
reconstructType :: HscEnv -> Int -> Id -> IO (Maybe Type)
......@@ -1266,3 +1270,39 @@ 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.
-}
+ = (_t1::t1)
print = (_t2::t1)
log = (_t3::t1)
head = (_t4::[a] -> a)
tail = (_t5::[a1] -> [a1])
fst = (_t6::(a2, b) -> a2)
+ = (_t1::Num a => a -> a -> a)
print = (_t2::Show a1 => a1 -> IO ())
log = (_t3::Floating a2 => a2 -> a2)
head = (_t4::[a4] -> a4)
tail = (_t5::[a7] -> [a7])
fst = (_t6::(a11, b) -> a11)
foldl :: Foldable t => (b -> a -> b) -> b -> t a -> b
foldl = (_t1::t1)
foldl = (_t1::forall b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b)
fmap :: Functor f => (a -> b) -> f a -> f b
fmap = (_t2::t1)
fmap = (_t2::forall a b. Functor f => (a -> b) -> f a -> f b)
return :: Monad m => a -> m a
return = (_t3::t1)
return = (_t3::forall a. Monad m => a -> m a)
pure :: Applicative f => a -> f a
pure = (_t4::t1)
mempty = (_t5::t1)
mappend = (_t6::t1)
foldl' = (_t7::t1)
f = (_t8::t1)
pure = (_t4::forall a. Applicative f1 => a -> f1 a)
mempty = (_t5::Monoid a => a)
mappend = (_t6::Monoid a => a -> a -> a)
foldl' = (_t7::forall b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b)
f = (_t8::(forall a. a -> a) -> b -> b)
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