Commit 03541cba authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Be less picky about reporing inaccessible code

Triggered by the discussion on Trac #12466, this patch
makes GHC less aggressive about reporting an error when
there are insoluble Givens.

Being so agressive was making some libraries fail to
compile, and is arguably wrong in at least some cases.
See the discussion on the ticket.

Several test now pass when they failed before; see
the files-modified list for this patch.
parent 454033b5
......@@ -447,7 +447,7 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_insol = insols, wc_impl
-- type checking to get a Lint error later
report1 = [ ("custom_error", is_user_type_error,
True, mkUserTypeErrorReporter)
, ("insoluble1", is_given_eq, True, mkGroupReporter mkEqErr)
, ("insoluble1", is_given_eq, True, mkGivenErrorReporter)
, ("insoluble2", utterly_wrong, True, mkGroupReporter mkEqErr)
, ("skolem eq1", very_wrong, True, mkSkolReporter)
, ("skolem eq2", skolem_eq, True, mkSkolReporter)
......@@ -579,6 +579,77 @@ mkUserTypeError ctxt ct = mkErrorMsgFromCt ctxt ct
Nothing -> pprPanic "mkUserTypeError" (ppr ct)
mkGivenErrorReporter :: Reporter
-- See Note [Given errors]
mkGivenErrorReporter ctxt cts
| Just implic <- find_gadt_match (cec_encl ctxt)
= do { (ctxt, binds_msg, ct) <- relevantBindings True ctxt ct
; dflags <- getDynFlags
; let ct' = setCtLoc ct (setCtLocEnv (ctLoc ct) (ic_env implic))
-- For given constraints we overwrite the env (and hence src-loc)
-- with one from the implication. See Note [Inaccessible code]
inaccessible_msg = hang (text "Inaccessible code in")
2 (ppr (ic_info implic))
report = important inaccessible_msg `mappend`
relevant_bindings binds_msg
; err <- mkEqErr_help dflags ctxt report ct'
Nothing ty1 ty2
; traceTc "mkGivenErrorRporter" (ppr ct)
; maybeReportError ctxt err }
| otherwise -- Discard Given errors that don't come from
-- a pattern match; maybe we should warn instead?
= do { traceTc "mkGivenErrorRporter no" (ppr ct $$ ppr (cec_encl ctxt))
; return () }
where
(ct : _ ) = cts -- Never empty
(ty1, ty2) = getEqPredTys (ctPred ct)
find_gadt_match [] = Nothing
find_gadt_match (implic : implics)
| PatSkol {} <- ic_info implic
, not (ic_no_eqs implic)
= Just implic
| otherwise
= find_gadt_match implics
{- Note [Given errors]
~~~~~~~~~~~~~~~~~~~~~~
Given constaints reprsent things for which we have (or will have)
evidence, so they aren't errors. But if a Given constraint is
insoluble, this code is inaccessible, and we might want to at least
warn about that. A classic case is
data T a where
T1 :: T Int
T2 :: T a
T3 :: T Bool
f :: T Int -> Bool
f T1 = ...
f T2 = ...
f T3 = ... -- We want to report this case as inaccessible
We'd like to point out that the T3 match is inaccessible. It
will have a Given constraint [G] Int ~ Bool.
But we don't want to report ALL insoluble Given constraints. See Trac
#12466 for a long discussion on. For example, if we aren't careful
we'll complain about
f :: ((Int ~ Bool) => a -> a) -> Int
which arguably is OK. It's more debatable for
g :: (Int ~ Bool) => Int -> Int
but it's tricky to distinguish these cases to we don't report
either.
The bottom line is this: find_gadt_match looks for an encosing
pattern match which binds some equality constraints. If we
find one, we report the insoluble Given.
-}
mkGroupReporter :: (ReportErrCtxt -> [Ct] -> TcM ErrMsg)
-- Make error message for a group
-> Reporter -- Deal with lots of constraints
......@@ -1170,17 +1241,8 @@ mkEqErr ctxt (ct:_) = mkEqErr1 ctxt ct
mkEqErr _ [] = panic "mkEqErr"
mkEqErr1 :: ReportErrCtxt -> Ct -> TcM ErrMsg
mkEqErr1 ctxt ct
| arisesFromGivens ct
= do { (ctxt, binds_msg, ct) <- relevantBindings True ctxt ct
; let (given_loc, given_msg) = mk_given (ctLoc ct) (cec_encl ctxt)
; dflags <- getDynFlags
; let report = important given_msg `mappend` relevant_bindings binds_msg
; mkEqErr_help dflags ctxt report
(setCtLoc ct given_loc) -- Note [Inaccessible code]
Nothing ty1 ty2 }
| otherwise -- Wanted or derived
mkEqErr1 ctxt ct -- Wanted or derived;
-- givens handled in mkGivenErrorReporter
= do { (ctxt, binds_msg, ct) <- relevantBindings True ctxt ct
; rdr_env <- getGlobalRdrEnv
; fam_envs <- tcGetFamInstEnvs
......@@ -1200,14 +1262,6 @@ mkEqErr1 ctxt ct
where
(ty1, ty2) = getEqPredTys (ctPred ct)
mk_given :: CtLoc -> [Implication] -> (CtLoc, SDoc)
-- For given constraints we overwrite the env (and hence src-loc)
-- with one from the implication. See Note [Inaccessible code]
mk_given loc [] = (loc, empty)
mk_given loc (implic : _) = (setCtLocEnv loc (ic_env implic)
, hang (text "Inaccessible code in")
2 (ppr (ic_info implic)))
-- If the types in the error message are the same as the types
-- we are unifying, don't add the extra expected/actual message
mk_wanted_extra :: CtLoc -> Bool -> (Bool, Maybe SwapFlag, SDoc)
......
......@@ -1774,19 +1774,23 @@ isInInertEqs eqs tv rhs
, rhs `eqType` rhs2 = True
| otherwise = False
getNoGivenEqs :: TcLevel -- TcLevel of this implication
getNoGivenEqs :: TcLevel -- TcLevel of this implication
-> [TcTyVar] -- Skolems of this implication
-> Cts -- Given insolubles from solveGivens
-> TcS Bool -- True <=> definitely no residual given equalities
-- See Note [When does an implication have given equalities?]
getNoGivenEqs tclvl skol_tvs
= do { inerts@(IC { inert_eqs = ieqs, inert_irreds = iirreds, inert_funeqs = funeqs })
getNoGivenEqs tclvl skol_tvs given_insols
= do { inerts@(IC { inert_eqs = ieqs, inert_irreds = iirreds
, inert_funeqs = funeqs })
<- getInertCans
; let local_fsks = foldFunEqs add_fsk funeqs emptyVarSet
has_given_eqs = foldrBag ((||) . ev_given_here . ctEvidence) False iirreds
has_given_eqs = foldrBag ((||) . ev_given_here . ctEvidence) False
(iirreds `unionBags` given_insols)
|| anyDVarEnv (eqs_given_here local_fsks) ieqs
; traceTcS "getNoGivenEqs" (vcat [ppr has_given_eqs, ppr inerts])
; traceTcS "getNoGivenEqs" (vcat [ ppr has_given_eqs, ppr inerts
, ppr given_insols])
; return (not has_given_eqs) }
where
eqs_given_here :: VarSet -> EqualCtList -> Bool
......
......@@ -1254,7 +1254,7 @@ solveImplication imp@(Implic { ic_tclvl = tclvl
-- we want to retain derived equalities so we can float
-- them out in floatEqualities
; no_eqs <- getNoGivenEqs tclvl skols
; no_eqs <- getNoGivenEqs tclvl skols given_insols
-- Call getNoGivenEqs /after/ solveWanteds, because
-- solveWanteds can augment the givens, via expandSuperClasses,
-- to reveal given superclass equalities
......
-- Test -fwarn-type-errors
-- This test shows how each error is printed at runtime
-- Bizarrely Defer01.hs seems to be in typecheck/should_run
-- I can't see how ghci finds it!
:l Defer01
t5624
print a
......
......@@ -41,8 +41,7 @@ Defer01.hs:31:5: warning: [-Wdeferred-type-errors (in -Wdefault)]
but its type ‘Char’ has none
In the expression: e 'q'
In an equation for ‘f’: f = e 'q'
• Relevant bindings include
f :: t (bound at Defer01.hs:31:1)
• Relevant bindings include f :: t (bound at Defer01.hs:31:1)
Defer01.hs:34:8: warning: [-Wdeferred-type-errors (in -Wdefault)]
• Couldn't match expected type ‘Char’ with actual type ‘a’
......@@ -55,8 +54,7 @@ Defer01.hs:34:8: warning: [-Wdeferred-type-errors (in -Wdefault)]
In an equation for ‘h’: h x = (x, 'c')
• Relevant bindings include
x :: a (bound at Defer01.hs:34:3)
h :: a -> (Char, Char)
(bound at Defer01.hs:34:1)
h :: a -> (Char, Char) (bound at Defer01.hs:34:1)
Defer01.hs:39:17: warning: [-Wdeferred-type-errors (in -Wdefault)]
• Couldn't match expected type ‘Bool’ with actual type ‘T a’
......@@ -86,26 +84,11 @@ Defer01.hs:43:10: warning: [-Wdeferred-type-errors (in -Wdefault)]
In the expression: myOp 23
In an equation for ‘j’: j = myOp 23
Defer01.hs:45:1: warning: [-Wdeferred-type-errors (in -Wdefault)]
Couldn't match type ‘Int’ with ‘Bool’
Inaccessible code in
the type signature for:
k :: Int ~ Bool => Int -> Bool
Defer01.hs:45:6: warning: [-Wdeferred-type-errors (in -Wdefault)]
• Couldn't match type ‘Int’ with ‘Bool’
Inaccessible code in
the type signature for:
k :: Int ~ Bool => Int -> Bool
• In the ambiguity check for ‘k’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature: k :: (Int ~ Bool) => Int -> Bool
Defer01.hs:46:1: warning: [-Woverlapping-patterns (in -Wdefault)]
Defer01.hs:47:1: warning: [-Woverlapping-patterns (in -Wdefault)]
Pattern match is redundant
In an equation for ‘k’: k x = ...
Defer01.hs:49:5: warning: [-Wdeferred-type-errors (in -Wdefault)]
Defer01.hs:50:5: warning: [-Wdeferred-type-errors (in -Wdefault)]
• Couldn't match expected type ‘IO a0’
with actual type ‘Char -> IO ()’
• Probable cause: ‘putChar’ is applied to too few arguments
......@@ -131,7 +114,7 @@ Defer01.hs:49:5: warning: [-Wdeferred-type-errors (in -Wdefault)]
In an equation for ‘b’: b x = x == x
(deferred type error)
<interactive>:7:11: error:
<interactive>:10:11: error:
• Couldn't match type ‘Bool’ with ‘Int’
Expected type: C Int
Actual type: C Bool
......@@ -150,8 +133,7 @@ Defer01.hs:49:5: warning: [-Wdeferred-type-errors (in -Wdefault)]
but its type ‘Char’ has none
In the expression: e 'q'
In an equation for ‘f’: f = e 'q'
• Relevant bindings include
f :: t (bound at Defer01.hs:31:1)
• Relevant bindings include f :: t (bound at Defer01.hs:31:1)
(deferred type error)
*** Exception: Defer01.hs:34:8: error:
• Couldn't match expected type ‘Char’ with actual type ‘a’
......@@ -164,8 +146,7 @@ Defer01.hs:49:5: warning: [-Wdeferred-type-errors (in -Wdefault)]
In an equation for ‘h’: h x = (x, 'c')
• Relevant bindings include
x :: a (bound at Defer01.hs:34:3)
h :: a -> (Char, Char)
(bound at Defer01.hs:34:1)
h :: a -> (Char, Char) (bound at Defer01.hs:34:1)
(deferred type error)
*** Exception: Defer01.hs:39:17: error:
• Couldn't match expected type ‘Bool’ with actual type ‘T a’
......@@ -182,12 +163,12 @@ Defer01.hs:49:5: warning: [-Wdeferred-type-errors (in -Wdefault)]
In an equation for ‘j’: j = myOp 23
(deferred type error)
<interactive>:13:8: error:
<interactive>:16:8: error:
• Couldn't match type ‘Int’ with ‘Bool’ arising from a use of ‘k’
• In the first argument of ‘print’, namely ‘(k 2)’
In the expression: print (k 2)
In an equation for ‘it’: it = print (k 2)
*** Exception: Defer01.hs:49:5: error:
*** Exception: Defer01.hs:50:5: error:
• Couldn't match expected type ‘IO a0’
with actual type ‘Char -> IO ()’
• Probable cause: ‘putChar’ is applied to too few arguments
......
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
module T12466 where
class Foo a where
foo :: (a ~ Int => Int) -> a -> a
foo _ a2 = a2
instance Foo Char
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module T12466a where
import GHC.TypeLits (Nat)
import Unsafe.Coerce (unsafeCoerce)
data Dict a where
Dict :: a => Dict a
newtype a :- b = Sub (a => Dict b)
axiom :: forall a b. Dict (a ~ b)
axiom = unsafeCoerce (Dict :: Dict (a ~ a))
type Divides n m = n ~ Gcd n m
type family Gcd :: Nat -> Nat -> Nat where
dividesGcd :: forall a b c. (Divides a b, Divides a c) :- Divides a (Gcd b c)
dividesGcd = Sub axiom
......@@ -539,3 +539,5 @@ test('T12381', normal, compile, [''])
test('T12082', normal, compile, [''])
test('T10635', normal, compile, [''])
test('T12170b', normal, compile, [''])
test('T12466', normal, compile, [''])
test('T12466a', normal, compile, [''])
......@@ -6,6 +6,7 @@ class C a b | a -> b where
cop :: a -> b -> ()
{- Failing, as it righteously should! It's inaccessible code -}
-- But (c.f. test T5236) we no longer reject this (see Trac #12466)
g1 :: (C Char [a], C Char Bool) => a -> ()
g1 x = ()
FDsFromGivens.hs:9:7: error:
• Couldn't match type ‘[a]’ with ‘Bool’
arising from a functional dependency between constraints:
‘C Char Bool’
arising from the type signature for:
g1 :: (C Char [a], C Char Bool) => a -> ()
at FDsFromGivens.hs:9:7-42
‘C Char [a]’
arising from the type signature for:
g1 :: (C Char [a], C Char Bool) => a -> ()
at FDsFromGivens.hs:9:7-42
Inaccessible code in
the type signature for:
g1 :: (C Char [a], C Char Bool) => a -> ()
• In the ambiguity check for ‘g1’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature:
g1 :: (C Char [a], C Char Bool) => a -> ()
......@@ -6,5 +6,11 @@ import Data.Ord ( Down ) -- convenient newtype
data X a
-- See Trac #10715 for a long discussion about whether
-- this shoudl be accepted or not.
--
-- But in Trac #12466 we decided to accept contradictory
-- type signatures, so definition is now accepeted even
-- though you can never call it.
doCoerce :: Coercible a (X a) => a -> X a
doCoerce = coerce
T10715.hs:9:13: error:
• Couldn't match representation of type ‘a’ with that of ‘X a’
‘a’ is a rigid type variable bound by
the type signature for:
doCoerce :: forall a. Coercible a (X a) => a -> X a
at T10715.hs:9:13-41
Inaccessible code in
the type signature for:
doCoerce :: Coercible a (X a) => a -> X a
• In the ambiguity check for ‘doCoerce’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature: doCoerce :: Coercible a (X a) => a -> X a
......@@ -10,6 +10,9 @@ class Id a b | a -> b, b -> a
instance Id A A
instance Id B B
-- The fundeps mean that this type signature
-- has a (derived) insoluble Given, A~B, but
-- we now ignore that (Trac #12466)
loop :: Id A B => Bool
loop = True
......
T5236.hs:13:9: error:
• Couldn't match type ‘B’ with ‘A’
arising from a functional dependency between:
constraint ‘Id A B’
arising from the type signature for:
loop :: Id A B => Bool
instance ‘Id B B’ at T5236.hs:11:10-15
Inaccessible code in
the type signature for:
loop :: Id A B => Bool
• In the ambiguity check for ‘loop’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature:
loop :: Id A B => Bool
......@@ -2,6 +2,8 @@
module T8392a where
-- Should complain even with AllowAmbiguousTypes
--
-- But (Trac #12466) we now don't complain about
-- contradictory signatures
foo :: (Int ~ Bool) => a -> a
foo x = x
T8392a.hs:6:8: error:
• Couldn't match type ‘Int’ with ‘Bool’
Inaccessible code in
the type signature for:
foo :: Int ~ Bool => a -> a
• In the ambiguity check for ‘foo’
In the type signature:
foo :: (Int ~ Bool) => a -> a
......@@ -253,7 +253,7 @@ test('SilentParametersOverlapping', normal, compile, [''])
test('FailDueToGivenOverlapping', normal, compile_fail, [''])
test('LongWayOverlapping', normal, compile_fail, [''])
test('T5051', normal, compile, [''])
test('T5236',normal,compile_fail,[''])
test('T5236',normal,compile,[''])
test('T5246',normal,compile_fail,[''])
test('T5300',normal,compile_fail,[''])
test('T5095',normal,compile_fail,[''])
......@@ -287,7 +287,7 @@ test('T6018fail', extra_clean([ 'T6018fail.hi' , 'T6018fail.o'
test('T6018failclosed', normal, compile_fail, [''])
test('T6018failclosed2', normal, compile_fail, [''])
test('T6078', normal, compile_fail, [''])
test('FDsFromGivens', normal, compile_fail, [''])
test('FDsFromGivens', normal, compile, [''])
test('FDsFromGivens2', normal, compile_fail, [''])
test('T7019', normal, compile_fail,[''])
test('T7019a', normal, compile_fail,[''])
......@@ -335,7 +335,7 @@ test('TcCoercibleFail', [when(compiler_debugged(), skip)], compile_fail, [''])
test('TcCoercibleFail2', [], compile_fail, [''])
test('TcCoercibleFail3', [], compile_fail, [''])
test('T8306', normal, compile_fail, [''])
test('T8392a', normal, compile_fail, [''])
test('T8392a', normal, compile, [''])
test('T8428', normal, compile_fail, [''])
test('T8450', normal, compile_fail, [''])
test('T8514', normal, compile_fail, [''])
......@@ -389,7 +389,7 @@ test('ExpandSynsFail3', normal, compile_fail, ['-fprint-expanded-synonyms'])
test('ExpandSynsFail4', normal, compile_fail, ['-fprint-expanded-synonyms'])
test('T10698', expect_broken(10698), compile_fail, [''])
test('T10836', normal, compile_fail, [''])
test('T10715', normal, compile_fail, [''])
test('T10715', normal, compile, [''])
test('T10715b', normal, compile_fail, [''])
test('T10971b', normal, compile_fail, [''])
test('T10971d', extra_clean(['T10971c.hi', 'T10971c.o']), multimod_compile_fail, ['T10971d','-v0'])
......
......@@ -42,6 +42,7 @@ class MyClass a where myOp :: a -> String
j = myOp 23 -- Two errors, should not combine them
-- No longer reported as an error: Trac #12466
k :: (Int ~ Bool) => Int -> Bool
k x = x
......
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