Commit 4927117c authored by Simon Peyton Jones's avatar Simon Peyton Jones Committed by Marge Bot

Improve error recovery in the typechecker

Issue #16418 showed that we were carrying on too eagerly after a bogus
type signature was identified (a bad telescope in fact), leading to a
subsequent crash.

This led me in to a maze of twisty little passages in the typechecker's
error recovery, and I ended up doing some refactoring in TcRnMonad.
Some specfifics

* TcRnMonad.try_m is now called attemptM.

* I switched the order of the result pair in tryTc,
  to make it consistent with other similar functions.

* The actual exception used in the Tc monad is irrelevant so,
  to avoid polluting type signatures, I made tcTryM, a simple
  wrapper around tryM, and used it.

The more important changes are in

* TcSimplify.captureTopConstraints, where we should have been calling
  simplifyTop rather than reportUnsolved, so that levity defaulting
  takes place properly.

* TcUnify.emitResidualTvConstraint, where we need to set the correct
  status for a new implication constraint.  (Previously we ended up
  with an Insoluble constraint wrapped in an Unsolved implication,
  which meant that insolubleWC gave the wrong answer.
parent 57201beb
...@@ -765,7 +765,7 @@ cvObtainTerm hsc_env max_depth force old_ty hval = runTR hsc_env $ do ...@@ -765,7 +765,7 @@ cvObtainTerm hsc_env max_depth force old_ty hval = runTR hsc_env $ do
then parens (text "already monomorphic: " <> ppr my_ty) then parens (text "already monomorphic: " <> ppr my_ty)
else Ppr.empty) else Ppr.empty)
Right dcname <- liftIO $ constrClosToName hsc_env clos Right dcname <- liftIO $ constrClosToName hsc_env clos
(_,mb_dc) <- tryTc (tcLookupDataCon dcname) (mb_dc, _) <- tryTc (tcLookupDataCon dcname)
case mb_dc of case mb_dc of
Nothing -> do -- This can happen for private constructors compiled -O0 Nothing -> do -- This can happen for private constructors compiled -O0
-- where the .hi descriptor does not export them -- where the .hi descriptor does not export them
...@@ -981,7 +981,7 @@ cvReconstructType hsc_env max_depth old_ty hval = runTR_maybe hsc_env $ do ...@@ -981,7 +981,7 @@ cvReconstructType hsc_env max_depth old_ty hval = runTR_maybe hsc_env $ do
ConstrClosure{ptrArgs=pArgs} -> do ConstrClosure{ptrArgs=pArgs} -> do
Right dcname <- liftIO $ constrClosToName hsc_env clos Right dcname <- liftIO $ constrClosToName hsc_env clos
traceTR (text "Constr1" <+> ppr dcname) traceTR (text "Constr1" <+> ppr dcname)
(_,mb_dc) <- tryTc (tcLookupDataCon dcname) (mb_dc, _) <- tryTc (tcLookupDataCon dcname)
case mb_dc of case mb_dc of
Nothing-> do Nothing-> do
forM pArgs $ \x -> do forM pArgs $ \x -> do
......
...@@ -582,7 +582,7 @@ mergeSignatures ...@@ -582,7 +582,7 @@ mergeSignatures
-- signatures that are merged in, we will discover this -- signatures that are merged in, we will discover this
-- when we run exports_from_avail on the final merged -- when we run exports_from_avail on the final merged
-- export list. -- export list.
(msgs, mb_r) <- tryTc $ do (mb_r, msgs) <- tryTc $ do
-- Suppose that we have written in a signature: -- Suppose that we have written in a signature:
-- signature A ( module A ) where {- empty -} -- signature A ( module A ) where {- empty -}
-- If I am also inheriting a signature from a -- If I am also inheriting a signature from a
......
...@@ -392,14 +392,13 @@ tcValBinds :: TopLevelFlag ...@@ -392,14 +392,13 @@ tcValBinds :: TopLevelFlag
-> TcM ([(RecFlag, LHsBinds GhcTcId)], thing) -> TcM ([(RecFlag, LHsBinds GhcTcId)], thing)
tcValBinds top_lvl binds sigs thing_inside tcValBinds top_lvl binds sigs thing_inside
= do { let patsyns = getPatSynBinds binds = do { -- Typecheck the signatures
-- It's easier to do so now, once for all the SCCs together
-- Typecheck the signature -- because a single signature f,g :: <type>
-- might relate to more than one SCC
; (poly_ids, sig_fn) <- tcAddPatSynPlaceholders patsyns $ ; (poly_ids, sig_fn) <- tcAddPatSynPlaceholders patsyns $
tcTySigs sigs tcTySigs sigs
; let prag_fn = mkPragEnv sigs (foldr (unionBags . snd) emptyBag binds)
-- Extend the envt right away with all the Ids -- Extend the envt right away with all the Ids
-- declared with complete type signatures -- declared with complete type signatures
-- Do not extend the TcBinderStack; instead -- Do not extend the TcBinderStack; instead
...@@ -413,6 +412,9 @@ tcValBinds top_lvl binds sigs thing_inside ...@@ -413,6 +412,9 @@ tcValBinds top_lvl binds sigs thing_inside
; let extra_binds = [ (NonRecursive, builder) | builder <- patsyn_builders ] ; let extra_binds = [ (NonRecursive, builder) | builder <- patsyn_builders ]
; return (extra_binds, thing) } ; return (extra_binds, thing) }
; return (binds' ++ extra_binds', thing) }} ; return (binds' ++ extra_binds', thing) }}
where
patsyns = getPatSynBinds binds
prag_fn = mkPragEnv sigs (foldr (unionBags . snd) emptyBag binds)
------------------------ ------------------------
tcBindGroups :: TopLevelFlag -> TcSigFun -> TcPragEnv tcBindGroups :: TopLevelFlag -> TcSigFun -> TcPragEnv
......
...@@ -140,10 +140,10 @@ accumExports :: (ExportAccum -> x -> TcRn (Maybe (ExportAccum, y))) ...@@ -140,10 +140,10 @@ accumExports :: (ExportAccum -> x -> TcRn (Maybe (ExportAccum, y)))
-> TcRn [y] -> TcRn [y]
accumExports f = fmap (catMaybes . snd) . mapAccumLM f' emptyExportAccum accumExports f = fmap (catMaybes . snd) . mapAccumLM f' emptyExportAccum
where f' acc x = do where f' acc x = do
m <- try_m (f acc x) m <- attemptM (f acc x)
pure $ case m of pure $ case m of
Right (Just (acc', y)) -> (acc', Just y) Just (Just (acc', y)) -> (acc', Just y)
_ -> (acc, Nothing) _ -> (acc, Nothing)
type ExportOccMap = OccEnv (Name, IE GhcPs) type ExportOccMap = OccEnv (Name, IE GhcPs)
-- Tracks what a particular exported OccName -- Tracks what a particular exported OccName
...@@ -192,7 +192,7 @@ tcRnExports explicit_mod exports ...@@ -192,7 +192,7 @@ tcRnExports explicit_mod exports
; let do_it = exports_from_avail real_exports rdr_env imports this_mod ; let do_it = exports_from_avail real_exports rdr_env imports this_mod
; (rn_exports, final_avails) ; (rn_exports, final_avails)
<- if hsc_src == HsigFile <- if hsc_src == HsigFile
then do (msgs, mb_r) <- tryTc do_it then do (mb_r, msgs) <- tryTc do_it
case mb_r of case mb_r of
Just r -> return r Just r -> return r
Nothing -> addMessages msgs >> failM Nothing -> addMessages msgs >> failM
......
This diff is collapsed.
...@@ -168,14 +168,19 @@ completeSigPolyId_maybe sig ...@@ -168,14 +168,19 @@ completeSigPolyId_maybe sig
tcTySigs :: [LSig GhcRn] -> TcM ([TcId], TcSigFun) tcTySigs :: [LSig GhcRn] -> TcM ([TcId], TcSigFun)
tcTySigs hs_sigs tcTySigs hs_sigs
= checkNoErrs $ -- See Note [Fail eagerly on bad signatures] = checkNoErrs $
do { ty_sigs_s <- mapAndRecoverM tcTySig hs_sigs do { -- Fail if any of the signatures is duff
; let ty_sigs = concat ty_sigs_s -- Hence mapAndReportM
-- See Note [Fail eagerly on bad signatures]
ty_sigs_s <- mapAndReportM tcTySig hs_sigs
; let ty_sigs = concat ty_sigs_s
poly_ids = mapMaybe completeSigPolyId_maybe ty_sigs poly_ids = mapMaybe completeSigPolyId_maybe ty_sigs
-- The returned [TcId] are the ones for which we have -- The returned [TcId] are the ones for which we have
-- a complete type signature. -- a complete type signature.
-- See Note [Complete and partial type signatures] -- See Note [Complete and partial type signatures]
env = mkNameEnv [(tcSigInfoName sig, sig) | sig <- ty_sigs] env = mkNameEnv [(tcSigInfoName sig, sig) | sig <- ty_sigs]
; return (poly_ids, lookupNameEnv env) } ; return (poly_ids, lookupNameEnv env) }
tcTySig :: LSig GhcRn -> TcM [TcSigInfo] tcTySig :: LSig GhcRn -> TcM [TcSigInfo]
...@@ -308,9 +313,15 @@ If a type signature is wrong, fail immediately: ...@@ -308,9 +313,15 @@ If a type signature is wrong, fail immediately:
the code against the signature will give a very similar error the code against the signature will give a very similar error
to the ambiguity error. to the ambiguity error.
ToDo: this means we fall over if any type sig ToDo: this means we fall over if any top-level type signature in the
is wrong (eg at the top level of the module), module is wrong, because we typecheck all the signatures together
which is over-conservative (see TcBinds.tcValBinds). Moreover, because of top-level
captureTopConstraints, only insoluble constraints will be reported.
We typecheck all signatures at the same time because a signature
like f,g :: blah might have f and g from different SCCs.
So it's a bit awkward to get better error recovery, and no one
has complained!
-} -}
{- ********************************************************************* {- *********************************************************************
......
...@@ -107,10 +107,12 @@ captureTopConstraints thing_inside ...@@ -107,10 +107,12 @@ captureTopConstraints thing_inside
-- constraints, report the latter before propagating the exception -- constraints, report the latter before propagating the exception
-- Otherwise they will be lost altogether -- Otherwise they will be lost altogether
; case mb_res of ; case mb_res of
Right res -> return (res, lie `andWC` stWC) Just res -> return (res, lie `andWC` stWC)
Left {} -> do { _ <- reportUnsolved lie; failM } } Nothing -> do { _ <- simplifyTop lie; failM } }
-- This call to reportUnsolved is the reason -- This call to simplifyTop is the reason
-- this function is here instead of TcRnMonad -- this function is here instead of TcRnMonad
-- We call simplifyTop so that it does defaulting
-- (esp of runtime-reps) before reporting errors
simplifyTopImplic :: Bag Implication -> TcM () simplifyTopImplic :: Bag Implication -> TcM ()
simplifyTopImplic implics simplifyTopImplic implics
......
...@@ -1179,8 +1179,15 @@ emitResidualTvConstraint skol_info m_telescope skol_tvs tclvl wanted ...@@ -1179,8 +1179,15 @@ emitResidualTvConstraint skol_info m_telescope skol_tvs tclvl wanted
| otherwise | otherwise
= do { ev_binds <- newNoTcEvBinds = do { ev_binds <- newNoTcEvBinds
; implic <- newImplication ; implic <- newImplication
; let status | insolubleWC wanted = IC_Insoluble
| otherwise = IC_Unsolved
-- If the inner constraints are insoluble,
-- we should mark the outer one similarly,
-- so that insolubleWC works on the outer one
; emitImplication $ ; emitImplication $
implic { ic_tclvl = tclvl implic { ic_status = status
, ic_tclvl = tclvl
, ic_skols = skol_tvs , ic_skols = skol_tvs
, ic_no_eqs = True , ic_no_eqs = True
, ic_telescope = m_telescope , ic_telescope = m_telescope
......
...@@ -3,12 +3,9 @@ ...@@ -3,12 +3,9 @@
module BadTelescope2 where module BadTelescope2 where
import Data.Kind import Data.Kind
import Data.Proxy
data SameKind :: k -> k -> * data SameKind :: k -> k -> *
foo :: forall a k (b :: k). SameKind a b foo :: forall a k (b :: k). SameKind a b
foo = undefined foo = undefined
bar :: forall a k (b :: k) (c :: Proxy b) (d :: Proxy a). Proxy c -> SameKind b d
bar = undefined
BadTelescope2.hs:10:8: error: BadTelescope2.hs:9:8: error:
• These kind and type variables: a k (b :: k) • These kind and type variables: a k (b :: k)
are out of dependency order. Perhaps try this ordering: are out of dependency order. Perhaps try this ordering:
k (a :: k) (b :: k) k (a :: k) (b :: k)
• In the type signature: foo :: forall a k (b :: k). SameKind a b • In the type signature: foo :: forall a k (b :: k). SameKind a b
BadTelescope2.hs:13:81: error:
• Expected kind ‘k’, but ‘d’ has kind ‘Proxy a’
• In the second argument of ‘SameKind’, namely ‘d’
In the type signature:
bar :: forall a k (b :: k) (c :: Proxy b) (d :: Proxy a).
Proxy c -> SameKind b d
{-# LANGUAGE DataKinds, PolyKinds, ExplicitForAll #-}
module BadTelescope5 where
import Data.Kind
import Data.Proxy
data SameKind :: k -> k -> *
bar :: forall a k (b :: k) (c :: Proxy b) (d :: Proxy a). Proxy c -> SameKind b d
bar = undefined
BadTelescope5.hs:10:81: error:
• Expected kind ‘k’, but ‘d’ has kind ‘Proxy a’
• In the second argument of ‘SameKind’, namely ‘d’
In the type signature:
bar :: forall a k (b :: k) (c :: Proxy b) (d :: Proxy a).
Proxy c -> SameKind b d
...@@ -13,3 +13,18 @@ T15743c.hs:10:1: error: ...@@ -13,3 +13,18 @@ T15743c.hs:10:1: error:
(b :: Proxy d) (b :: Proxy d)
(x :: SimilarKind a b) (x :: SimilarKind a b)
• In the data type declaration for ‘T’ • In the data type declaration for ‘T’
T15743c.hs:11:1: error:
• The kind of ‘T2’ is ill-scoped
Inferred kind: T2 :: forall (d :: k).
forall k (c :: k) (a :: Proxy c) (b :: Proxy d) ->
SimilarKind a b -> *
NB: Specified variables (namely: (d :: k)) always come first
Perhaps try this order instead:
k
(d :: k)
(c :: k)
(a :: Proxy c)
(b :: Proxy d)
(x :: SimilarKind a b)
• In the data type declaration for ‘T2’
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
module T16418 where
import Data.Kind
data SameKind :: forall k. k -> k -> Type
f :: forall a k (b :: k). SameKind a b -> ()
f = g
where
g :: SameKind a b -> ()
g _ = ()
T16418.hs:9:6: error:
• These kind and type variables: a k (b :: k)
are out of dependency order. Perhaps try this ordering:
k (a :: k) (b :: k)
• In the type signature:
f :: forall a k (b :: k). SameKind a b -> ()
...@@ -4,9 +4,10 @@ test('TypeSkolEscape', normal, compile_fail, ['-fprint-explicit-runtime-reps']) ...@@ -4,9 +4,10 @@ test('TypeSkolEscape', normal, compile_fail, ['-fprint-explicit-runtime-reps'])
test('BadTelescope', normal, compile_fail, ['']) test('BadTelescope', normal, compile_fail, [''])
test('BadTelescope2', normal, compile_fail, ['']) test('BadTelescope2', normal, compile_fail, [''])
test('BadTelescope3', normal, compile_fail, ['']) test('BadTelescope3', normal, compile_fail, [''])
test('BadTelescope4', normal, compile_fail, [''])
test('BadTelescope5', normal, compile_fail, [''])
test('PromotedClass', normal, compile_fail, ['']) test('PromotedClass', normal, compile_fail, [''])
test('SelfDep', normal, compile_fail, ['']) test('SelfDep', normal, compile_fail, [''])
test('BadTelescope4', normal, compile_fail, [''])
test('RenamingStar', normal, compile_fail, ['']) test('RenamingStar', normal, compile_fail, [''])
test('T11407', normal, compile_fail, ['']) test('T11407', normal, compile_fail, [''])
test('T11334b', normal, compile_fail, ['']) test('T11334b', normal, compile_fail, [''])
...@@ -55,3 +56,4 @@ test('T16326_Fail12', normal, compile_fail, ['']) ...@@ -55,3 +56,4 @@ test('T16326_Fail12', normal, compile_fail, [''])
test('T16391b', normal, compile_fail, ['-fprint-explicit-runtime-reps']) test('T16391b', normal, compile_fail, ['-fprint-explicit-runtime-reps'])
test('T16344', normal, compile_fail, ['']) test('T16344', normal, compile_fail, [''])
test('T16344a', normal, compile_fail, ['']) test('T16344a', normal, compile_fail, [''])
test('T16418', normal, compile_fail, [''])
{-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE DataKinds #-} {-# LANGUAGE DataKinds #-}
module Bug where
pattern PATTERN = () pattern PATTERN = ()
wrongLift :: PATTERN wrongLift :: PATTERN
......
T9161-1.hs:6:14: error: T9161-1.hs:8:14: error:
• Pattern synonym ‘PATTERN’ cannot be used here • Pattern synonym ‘PATTERN’ cannot be used here
(pattern synonyms cannot be promoted) (pattern synonyms cannot be promoted)
• In the type signature: wrongLift :: PATTERN • In the type signature: wrongLift :: PATTERN
{-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE DataKinds, KindSignatures, PolyKinds #-} {-# LANGUAGE DataKinds, KindSignatures, PolyKinds #-}
module Bug where
pattern PATTERN = () pattern PATTERN = ()
data Proxy (tag :: k) (a :: *) data Proxy (tag :: k) (a :: *)
......
T9161-2.hs:8:20: error: T9161-2.hs:10:20: error:
• Pattern synonym ‘PATTERN’ cannot be used here • Pattern synonym ‘PATTERN’ cannot be used here
(pattern synonyms cannot be promoted) (pattern synonyms cannot be promoted)
• In the first argument of ‘Proxy’, namely ‘PATTERN’ • In the first argument of ‘Proxy’, namely ‘PATTERN’
......
...@@ -16,25 +16,3 @@ tcfail212.hs:13:7: error: ...@@ -16,25 +16,3 @@ tcfail212.hs:13:7: error:
tcfail212.hs:13:13: error: tcfail212.hs:13:13: error:
• Expecting a lifted type, but ‘Int#’ is unlifted • Expecting a lifted type, but ‘Int#’ is unlifted
• In the type signature: g :: (Int#, Int#) • In the type signature: g :: (Int#, Int#)
tcfail212.hs:14:6: error:
• Couldn't match a lifted type with an unlifted type
When matching types
a :: *
Int# :: TYPE 'IntRep
• In the expression: 1#
In the expression: (1#, 2#)
In an equation for ‘g’: g = (1#, 2#)
• Relevant bindings include
g :: (a, b) (bound at tcfail212.hs:14:1)
tcfail212.hs:14:10: error:
• Couldn't match a lifted type with an unlifted type
When matching types
b :: *
Int# :: TYPE 'IntRep
• In the expression: 2#
In the expression: (1#, 2#)
In an equation for ‘g’: g = (1#, 2#)
• Relevant bindings include
g :: (a, b) (bound at tcfail212.hs:14:1)
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