Commit 26c95f46 authored by Matthías Páll Gissurarson's avatar Matthías Páll Gissurarson Committed by Ben Gamari

Show valid substitutions for typed holes

The idea is to implement a mechanism similar to PureScript, where they
suggest which identifiers in scope would fit the given hole. In
PureScript, they use subsumption (which is what we would like here as
well). For subsumption, we would have to check each type in scope
whether the hole is a subtype of the given type, but that would require
`tcSubType` and constraint satisfiability checking. Currently,
`TcSimplify` uses a lot of functions from `TcErrors`, so that would
require more of a rewrite, I will hold on with that for now, and submit
the more simpler type equality version.

As an example, consider

```
ps :: String -> IO ()
ps = putStrLn

ps2 :: a -> IO ()
ps2 _ = putStrLn "hello, world"

main :: IO ()
main = _ "hello, world"
```

The results would be something like

```
    • Found hole: _ :: [Char] -> IO ()
    • In the expression: _
      In a stmt of a 'do' block: _ "hello, world"
      In the expression:
        do _ "hello, world"
    • Relevant bindings include
        main :: IO () (bound at test.hs:13:1)
        ps :: String -> IO () (bound at test.hs:7:1)
        ps2 :: forall a. a  -> IO () (bound at test.hs:10:1)
      Valid substitutions include
        putStrLn :: String
                    -> IO () (imported from ‘Prelude’ at
test.hs:1:1-14
                              (and originally defined in
‘System.IO’))
        putStr :: String
                  -> IO () (imported from ‘Prelude’ at
test.hs:1:1-14
                            (and originally defined in ‘System.IO’))
```

We'd like here for ps2 to be suggested as well, but for that we require
subsumption.

Reviewers: austin, bgamari, dfeuer, mpickering

Reviewed By: dfeuer, mpickering

Subscribers: mpickering, Wizek, dfeuer, rwbarton, thomie

Differential Revision: https://phabricator.haskell.org/D3361
parent 924a65fc
......@@ -708,6 +708,8 @@ data DynFlags = DynFlags {
maxRelevantBinds :: Maybe Int, -- ^ Maximum number of bindings from the type envt
-- to show in type error messages
maxValidSubstitutions :: Maybe Int, -- ^ Maximum number of substitutions
-- to show in type error messages
maxUncoveredPatterns :: Int, -- ^ Maximum number of unmatched patterns to show
-- in non-exhaustiveness warnings
simplTickFactor :: Int, -- ^ Multiplier for simplifier ticks
......@@ -1539,6 +1541,7 @@ defaultDynFlags mySettings =
maxPmCheckIterations = 2000000,
ruleCheck = Nothing,
maxRelevantBinds = Just 6,
maxValidSubstitutions = Just 6,
maxUncoveredPatterns = 4,
simplTickFactor = 100,
specConstrThreshold = Just 2000,
......@@ -3134,6 +3137,10 @@ dynamic_flags_deps = [
(intSuffix (\n d -> d { maxRelevantBinds = Just n }))
, make_ord_flag defFlag "fno-max-relevant-binds"
(noArg (\d -> d { maxRelevantBinds = Nothing }))
, make_ord_flag defFlag "fmax-valid-substitutions"
(intSuffix (\n d -> d { maxValidSubstitutions = Just n }))
, make_ord_flag defFlag "fno-max-valid-substitutions"
(noArg (\d -> d { maxValidSubstitutions = Nothing }))
, make_ord_flag defFlag "fmax-uncovered-patterns"
(intSuffix (\n d -> d { maxUncoveredPatterns = n }))
, make_ord_flag defFlag "fsimplifier-phases"
......
......@@ -32,7 +32,8 @@ import HsExpr ( UnboundVar(..) )
import HsBinds ( PatSynBind(..) )
import Name
import RdrName ( lookupGlobalRdrEnv, lookupGRE_Name, GlobalRdrEnv
, mkRdrUnqual, isLocalGRE, greSrcSpan )
, mkRdrUnqual, isLocalGRE, greSrcSpan, pprNameProvenance
, GlobalRdrElt (..), globalRdrEnvElts )
import PrelNames ( typeableClassName, hasKey, liftedRepDataConKey )
import Id
import Var
......@@ -42,8 +43,10 @@ import NameSet
import Bag
import ErrUtils ( ErrMsg, errDoc, pprLocErrMsg )
import BasicTypes
import ConLike ( ConLike(..) )
import ConLike ( ConLike(..), conLikeWrapId_maybe )
import Util
import HscTypes (HscEnv, lookupTypeHscEnv, TypeEnv, lookupTypeEnv )
import NameEnv (lookupNameEnv)
import FastString
import Outputable
import SrcLoc
......@@ -219,12 +222,16 @@ report_unsolved mb_binds_var err_as_warn type_errors expr_holes
data Report
= Report { report_important :: [SDoc]
, report_relevant_bindings :: [SDoc]
, report_valid_substitutions :: [SDoc]
}
instance Outputable Report where -- Debugging only
ppr (Report { report_important = imp, report_relevant_bindings = rel })
ppr (Report { report_important = imp
, report_relevant_bindings = rel
, report_valid_substitutions = val })
= vcat [ text "important:" <+> vcat imp
, text "relevant:" <+> vcat rel ]
, text "relevant:" <+> vcat rel
, text "valid:" <+> vcat val ]
{- Note [Error report]
The idea is that error msgs are divided into three parts: the main msg, the
......@@ -241,12 +248,13 @@ multiple places so they have to be in the Report.
#if __GLASGOW_HASKELL__ > 710
instance Semigroup Report where
Report a1 b1 <> Report a2 b2 = Report (a1 ++ a2) (b1 ++ b2)
Report a1 b1 c1 <> Report a2 b2 c2 = Report (a1 ++ a2) (b1 ++ b2) (c1 ++ c2)
#endif
instance Monoid Report where
mempty = Report [] []
mappend (Report a1 b1) (Report a2 b2) = Report (a1 ++ a2) (b1 ++ b2)
mempty = Report [] [] []
mappend (Report a1 b1 c1) (Report a2 b2 c2)
= Report (a1 ++ a2) (b1 ++ b2) (c1 ++ c2)
-- | Put a doc into the important msgs block.
important :: SDoc -> Report
......@@ -256,6 +264,10 @@ important doc = mempty { report_important = [doc] }
relevant_bindings :: SDoc -> Report
relevant_bindings doc = mempty { report_relevant_bindings = [doc] }
-- | Put a doc into the valid substitutions block.
valid_substitutions :: SDoc -> Report
valid_substitutions docs = mempty { report_valid_substitutions = [docs] }
data TypeErrorChoice -- What to do for type errors found by the type checker
= TypeError -- A type error aborts compilation with an error message
| TypeWarn -- A type error is deferred to runtime, plus a compile-time warning
......@@ -865,10 +877,10 @@ mkErrorMsgFromCt ctxt ct report
= mkErrorReport ctxt (ctLocEnv (ctLoc ct)) report
mkErrorReport :: ReportErrCtxt -> TcLclEnv -> Report -> TcM ErrMsg
mkErrorReport ctxt tcl_env (Report important relevant_bindings)
mkErrorReport ctxt tcl_env (Report important relevant_bindings valid_subs)
= do { context <- mkErrInfo (cec_tidy ctxt) (tcl_ctxt tcl_env)
; mkErrDocAt (RealSrcSpan (tcl_loc tcl_env))
(errDoc important [context] relevant_bindings)
(errDoc important [context] (relevant_bindings ++ valid_subs))
}
type UserGiven = Implication
......@@ -1051,9 +1063,11 @@ mkHoleError ctxt ct@(CHoleCan { cc_hole = hole })
= givenConstraintsMsg ctxt
| otherwise = empty
; sub_msg <- validSubstitutions ct
; mkErrorMsgFromCt ctxt ct $
important hole_msg `mappend`
relevant_bindings (binds_msg $$ constraints_msg) }
relevant_bindings (binds_msg $$ constraints_msg) `mappend`
valid_substitutions sub_msg}
where
occ = holeOcc hole
......@@ -1100,6 +1114,98 @@ mkHoleError ctxt ct@(CHoleCan { cc_hole = hole })
mkHoleError _ ct = pprPanic "mkHoleError" (ppr ct)
-- See Note [Valid substitutions include ...]
validSubstitutions :: Ct -> TcM SDoc
validSubstitutions ct | isExprHoleCt ct =
do { top_env <- getTopEnv
; rdr_env <- getGlobalRdrEnv
; gbl_env <- tcg_type_env <$> getGblEnv
; lcl_env <- getLclTypeEnv
; dflags <- getDynFlags
; (discards, substitutions) <-
go (gbl_env, lcl_env, top_env) (maxValidSubstitutions dflags)
$ localsFirst $ globalRdrEnvElts rdr_env
; return $ ppUnless (null substitutions) $
hang (text "Valid substitutions include")
2 (vcat (map (ppr_sub rdr_env) substitutions)
$$ ppWhen discards subsDiscardMsg) }
where
hole_ty :: TcPredType
hole_ty = ctEvPred (ctEvidence ct)
hole_env = ctLocEnv $ ctEvLoc $ ctEvidence ct
localsFirst :: [GlobalRdrElt] -> [GlobalRdrElt]
localsFirst elts = lcl ++ gbl
where (lcl, gbl) = partition gre_lcl elts
getBndrOcc :: TcIdBinder -> OccName
getBndrOcc (TcIdBndr id _) = occName $ getName id
getBndrOcc (TcIdBndr_ExpType name _ _) = occName $ getName name
relBindSet = mkOccSet $ map getBndrOcc $ tcl_bndrs hole_env
shouldBeSkipped :: GlobalRdrElt -> Bool
shouldBeSkipped el = (occName $ gre_name el) `elemOccSet` relBindSet
ppr_sub :: GlobalRdrEnv -> Id -> SDoc
ppr_sub rdr_env id = case lookupGRE_Name rdr_env (idName id) of
Just elt -> sep [ idAndTy, nest 2 (parens $ pprNameProvenance elt)]
_ -> idAndTy
where name = idName id
ty = varType id
idAndTy = (pprPrefixOcc name <+> dcolon <+> pprType ty)
tyToId :: TyThing -> Maybe Id
tyToId (AnId i) = Just i
tyToId (AConLike c) = conLikeWrapId_maybe c
tyToId _ = Nothing
tcTyToId :: TcTyThing -> Maybe Id
tcTyToId (AGlobal id) = tyToId id
tcTyToId (ATcId id _) = Just id
tcTyToId _ = Nothing
substituteable :: Id -> Bool
substituteable = tcEqType hole_ty . varType
lookupTopId :: HscEnv -> Name -> IO (Maybe Id)
lookupTopId env name =
maybe Nothing tyToId <$> lookupTypeHscEnv env name
lookupGblId :: TypeEnv -> Name -> Maybe Id
lookupGblId env name = maybe Nothing tyToId $ lookupTypeEnv env name
lookupLclId :: TcTypeEnv -> Name -> Maybe Id
lookupLclId env name = maybe Nothing tcTyToId $ lookupNameEnv env name
go :: (TypeEnv, TcTypeEnv, HscEnv) -> Maybe Int -> [GlobalRdrElt]
-> TcM (Bool, [Id])
go = go_ []
go_ :: [Id] -> (TypeEnv, TcTypeEnv, HscEnv) -> Maybe Int -> [GlobalRdrElt]
-> TcM (Bool, [Id])
go_ subs _ _ [] = return (False, reverse subs)
go_ subs _ (Just 0) _ = return (True, reverse subs)
go_ subs envs@(gbl,lcl,top) maxleft (el:elts) =
if shouldBeSkipped el then discard_it
else do { maybeId <- liftIO lookupId
; case maybeId of
Just id | substituteable id ->
go_ (id:subs) envs ((\n -> n - 1) <$> maxleft) elts
_ -> discard_it }
where name = gre_name el
discard_it = go_ subs envs maxleft elts
getTopId = lookupTopId top name
gbl_id = lookupGblId gbl name
lcl_id = lookupLclId lcl name
lookupId = if (isJust lcl_id) then return lcl_id
else if (isJust gbl_id) then return gbl_id else getTopId
validSubstitutions _ = return empty
-- See Note [Constraints include ...]
givenConstraintsMsg :: ReportErrCtxt -> SDoc
givenConstraintsMsg ctxt =
......@@ -1139,6 +1245,45 @@ mkIPErr ctxt cts
(ct1:_) = cts
{-
Note [Valid substitutions include ...]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
`validSubstitutions` returns the "Valid substitutions include ..." message.
For example, look at the following definitions in a file called test.hs:
ps :: String -> IO ()
ps = putStrLn
ps2 :: a -> IO ()
ps2 _ = putStrLn "hello, world"
main :: IO ()
main = _ "hello, world"
The hole in `main` would generate the message:
Valid substitutions include
ps :: String -> IO () ((defined at test.hs:2:1)
putStrLn :: String -> IO ()
(imported from ‘Prelude’ at test.hs:1:1
(and originally defined in ‘System.IO’))
putStr :: String -> IO ()
(imported from ‘Prelude’ at test.hs:1:1
(and originally defined in ‘System.IO’))
Valid substitutions are found by checking names in scope.
Currently the implementation only looks at exact type matches, as given by
`tcEqType`, so we DO NOT report `ps2` as a valid substitution in the example,
even though it fits in the hole. To determine that `ps2` fits in the hole,
we would need to check ids for subsumption, i.e. that the type of the hole is
a subtype of the id. This can be done using `tcSubType` from `TcUnify` and
`tcCheckSatisfiability` in `TcSimplify`. Unfortunately, `TcSimplify` uses
`TcErrors` to report errors found during constraint checking, so checking for
subsumption in holes would involve shuffling some code around in `TcSimplify`,
to make a non-error reporting constraint satisfiability checker which could
then be used for checking whether a given id satisfies the constraints imposed
by the hole.
Note [Constraints include ...]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
'givenConstraintsMsg' returns the "Constraints include ..." message enabled by
......@@ -2787,6 +2932,11 @@ discardMsg :: SDoc
discardMsg = text "(Some bindings suppressed;" <+>
text "use -fmax-relevant-binds=N or -fno-max-relevant-binds)"
subsDiscardMsg :: SDoc
subsDiscardMsg =
text "(Some substitutions suppressed;" <+>
text "use -fmax-valid-substitutions=N or -fno-max-valid-substitutions)"
-----------------------
warnDefaulting :: [Ct] -> Type -> TcM ()
warnDefaulting wanteds default_ty
......
......@@ -395,6 +395,16 @@ list.
they may be numerous), but ``-fno-max-relevant-bindings`` includes
them too.
.. ghc-flag:: -fmax-valid-substitutions=<n>
-fno-max-valid-substitutions
:default: 6
The type checker sometimes displays a list of valid substitutions
for typed holes in error messages, but only up to some maximum number,
set by this flag. Turning it off with
``-fno-max-valid-substitutions`` gives an unlimited number.
.. ghc-flag:: -fmax-uncovered-patterns=<n>
:default: 4
......
......@@ -9,6 +9,7 @@ Defer03.hs:7:5: warning: [-Wtyped-holes (in -Wdefault)]
• In the expression: _
In an equation for ‘f’: f = _
• Relevant bindings include f :: Int (bound at Defer03.hs:7:1)
Valid substitutions include a :: Int (defined at Defer03.hs:4:1)
Defer03.hs:4:5: error:
• Couldn't match expected type ‘Int’ with actual type ‘Char’
......@@ -20,6 +21,7 @@ Defer03.hs:7:5: error:
• In the expression: _
In an equation for ‘f’: f = _
• Relevant bindings include f :: Int (bound at Defer03.hs:7:1)
Valid substitutions include a :: Int (defined at Defer03.hs:4:1)
Defer03.hs:4:5: warning: [-Wdeferred-type-errors (in -Wdefault)]
• Couldn't match expected type ‘Int’ with actual type ‘Char’
......@@ -31,6 +33,7 @@ Defer03.hs:7:5: warning: [-Wtyped-holes (in -Wdefault)]
• In the expression: _
In an equation for ‘f’: f = _
• Relevant bindings include f :: Int (bound at Defer03.hs:7:1)
Valid substitutions include a :: Int (defined at Defer03.hs:4:1)
Defer03.hs:4:5: error:
• Couldn't match expected type ‘Int’ with actual type ‘Char’
......@@ -42,6 +45,7 @@ Defer03.hs:7:5: error:
• In the expression: _
In an equation for ‘f’: f = _
• Relevant bindings include f :: Int (bound at Defer03.hs:7:1)
Valid substitutions include a :: Int (defined at Defer03.hs:4:1)
Defer03.hs:4:5: warning: [-Wdeferred-type-errors (in -Wdefault)]
• Couldn't match expected type ‘Int’ with actual type ‘Char’
......@@ -53,3 +57,4 @@ Defer03.hs:7:5: warning: [-Wtyped-holes (in -Wdefault)]
• In the expression: _
In an equation for ‘f’: f = _
• Relevant bindings include f :: Int (bound at Defer03.hs:7:1)
Valid substitutions include a :: Int (defined at Defer03.hs:4:1)
......@@ -18,6 +18,8 @@ T13050.hs:5:11: warning: [-Wtyped-holes (in -Wdefault)]
y :: Int (bound at T13050.hs:5:5)
x :: Int (bound at T13050.hs:5:3)
g :: Int -> Int -> Int (bound at T13050.hs:5:1)
Valid substitutions include
f :: Int -> Int -> Int (defined at T13050.hs:4:1)
T13050.hs:6:11: warning: [-Wtyped-holes (in -Wdefault)]
• Found hole: _a :: Int -> Int -> Int
......@@ -29,3 +31,6 @@ T13050.hs:6:11: warning: [-Wtyped-holes (in -Wdefault)]
y :: Int (bound at T13050.hs:6:5)
x :: Int (bound at T13050.hs:6:3)
q :: Int -> Int -> Int (bound at T13050.hs:6:1)
Valid substitutions include
f :: Int -> Int -> Int (defined at T13050.hs:4:1)
g :: Int -> Int -> Int (defined at T13050.hs:5:1)
module ValidSubs where
data Moo = Moo Integer
......@@ -388,6 +388,8 @@ test('holes2', normal, compile, ['-fdefer-type-errors'])
test('holes3', normal, compile_fail, [''])
test('hole_constraints', normal, compile, ['-fdefer-type-errors'])
test('hole_constraints_nested', normal, compile, ['-fdefer-type-errors'])
test('valid_substitutions', [extra_files(['ValidSubs.hs'])],
multimod_compile, ['valid_substitutions','-fdefer-type-errors'])
test('T7408', normal, compile, [''])
test('UnboxStrictPrimitiveFields', normal, compile, [''])
test('T7541', normal, compile, [''])
......
module Foo where
import Prelude hiding (putStr)
import qualified System.IO
import Data.Maybe
import qualified ValidSubs
ps :: String -> IO ()
ps = putStrLn
test :: [Maybe a] -> [a]
test = _
test2 :: Integer -> ValidSubs.Moo
test2 = _
main :: IO ()
main = _ "hello, world"
[1 of 2] Compiling ValidSubs ( ValidSubs.hs, ValidSubs.o )
[2 of 2] Compiling Foo ( valid_substitutions.hs, valid_substitutions.o )
valid_substitutions.hs:13:8: warning: [-Wtyped-holes (in -Wdefault)]
• Found hole: _ :: [Maybe a] -> [a]
Where: ‘a’ is a rigid type variable bound by
the type signature for:
test :: forall a. [Maybe a] -> [a]
at valid_substitutions.hs:12:1-24
• In the expression: _
In an equation for ‘test’: test = _
• Relevant bindings include
test :: [Maybe a] -> [a] (bound at valid_substitutions.hs:13:1)
valid_substitutions.hs:16:9: warning: [-Wtyped-holes (in -Wdefault)]
• Found hole: _ :: Integer -> ValidSubs.Moo
• In the expression: _
In an equation for ‘test2’: test2 = _
• Relevant bindings include
test2 :: Integer -> ValidSubs.Moo
(bound at valid_substitutions.hs:16:1)
Valid substitutions include
ValidSubs.Moo :: Integer -> ValidSubs.Moo
valid_substitutions.hs:19:8: warning: [-Wtyped-holes (in -Wdefault)]
• Found hole: _ :: [Char] -> IO ()
• In the expression: _
In the expression: _ "hello, world"
In an equation for ‘main’: main = _ "hello, world"
• Relevant bindings include
main :: IO () (bound at valid_substitutions.hs:19:1)
Valid substitutions include
ps :: String -> IO () (defined at valid_substitutions.hs:9:1)
System.IO.putStr :: String -> IO ()
(imported qualified from ‘System.IO’ at valid_substitutions.hs:4:1-26)
putStrLn :: String -> IO ()
(imported qualified from ‘System.IO’ at valid_substitutions.hs:4:1-26)
......@@ -183,6 +183,13 @@ optimizationsOptions =
, flagType = DynamicFlag
, flagReverse = "-fno-max-relevant-bindings"
}
, flag { flagName = "-fmax-valid-substitutions=⟨n⟩"
, flagDescription =
"*default: 6.* Set the maximum number of valid substitutions for"++
"typed holes to display in type error messages."
, flagType = DynamicFlag
, flagReverse = "-fno-max-valid-substitutions"
}
, flag { flagName = "-fmax-uncovered-patterns=⟨n⟩"
, flagDescription =
"*default: 4.* Set the maximum number of patterns to display in "++
......
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