Commit 02c1c573 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Use an Implication in 'deriving' error

Trac #11437 showed that erroneous constraints from a 'deriving'
clause need to be wrapped in an Implication to properly scope
their skolems.

The main change is in TcDeriv.simplifyDeriv; the call to
buildImplicationFor is new.
parent dc970966
......@@ -29,6 +29,7 @@ import FamInstEnv
import TcHsType
import TcMType
import TcSimplify
import TcUnify( buildImplicationFor )
import LoadIface( loadInterfaceForName )
import Module( getModule )
......@@ -1816,18 +1817,23 @@ simplifyDeriv pred tvs theta
-- We use *non-overlappable* (vanilla) skolems
-- See Note [Overlap and deriving]
; let skol_set = mkVarSet tvs_skols
; let skol_set = mkVarSet tvs_skols
skol_info = DerivSkol pred
doc = ptext (sLit "deriving") <+> parens (ppr pred)
mk_ct (PredOrigin t o t_or_k)
= newWanted o (Just t_or_k) (substTy skol_subst t)
; wanted <- mapM (\(PredOrigin t o t_or_k)
-> newWanted o (Just t_or_k) (substTy skol_subst t)) theta
; (wanted, tclvl) <- pushTcLevelM (mapM mk_ct theta)
; traceTc "simplifyDeriv" $
vcat [ pprTvBndrs tvs $$ ppr theta $$ ppr wanted, doc ]
; residual_wanted <- simplifyWantedsTcM wanted
-- Result is zonked
; let residual_simple = wc_simple residual_wanted
(good, bad) = partitionBagWith get_good residual_simple
unsolved = residual_wanted { wc_simple = bad }
; residual_simple <- zonkSimples (wc_simple residual_wanted)
; let (good, bad) = partitionBagWith get_good residual_simple
-- See Note [Exotic derived instance contexts]
get_good :: Ct -> Either PredType Ct
......@@ -1848,7 +1854,12 @@ simplifyDeriv pred tvs theta
-- constraints. They'll come up again when we typecheck the
-- generated instance declaration
; defer <- goptM Opt_DeferTypeErrors
; unless defer (reportAllUnsolved (residual_wanted { wc_simple = bad }))
; (implic, _) <- buildImplicationFor tclvl skol_info tvs_skols [] unsolved
-- The buildImplication is just to bind the skolems, in
-- case they are mentioned in error messages
-- See Trac #11347
; unless defer (reportAllUnsolved (mkImplicWC implic))
; let min_theta = mkMinimalBySCs (bagToList good)
subst_skol = zipTopTCvSubst tvs_skols $ mkTyVarTys tvs
......
......@@ -830,7 +830,7 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds })
, ic_skols = inst_tyvars
, ic_no_eqs = False
, ic_given = dfun_ev_vars
, ic_wanted = addImplics emptyWC sc_meth_implics
, ic_wanted = mkImplicWC sc_meth_implics
, ic_status = IC_Unsolved
, ic_binds = Just dfun_ev_binds_var
, ic_env = env
......
......@@ -257,7 +257,7 @@ tcCheckPatSynDecl PSB{ psb_id = lname@(L _ name), psb_args = details
-- Solve the constraints now, because we are about to make a PatSyn,
-- which should not contain unification variables and the like (Trac #10997)
-- Since all the inputs are implications the returned bindings will be empty
; _ <- simplifyTop (emptyWC `addImplics` implics)
; _ <- simplifyTop (mkImplicWC implics)
-- ToDo: in the bidirectional case, check that the ex_tvs' are all distinct
-- Otherwise we may get a type error when typechecking the builder,
......
......@@ -79,7 +79,8 @@ module TcRnTypes(
WantedConstraints(..), insolubleWC, emptyWC, isEmptyWC,
toDerivedWC,
andWC, unionsWC, addSimples, addImplics, mkSimpleWC, addInsols,
andWC, unionsWC, mkSimpleWC, mkImplicWC,
addInsols, addSimples, addImplics,
tyCoVarsOfWC, dropDerivedWC, dropDerivedSimples, dropDerivedInsols,
isDroppableDerivedLoc, insolubleImplic,
arisesFromGivens,
......@@ -1836,6 +1837,10 @@ mkSimpleWC cts
, wc_impl = emptyBag
, wc_insol = emptyBag }
mkImplicWC :: Bag Implication -> WantedConstraints
mkImplicWC implic
= WC { wc_simple = emptyBag, wc_impl = implic, wc_insol = emptyBag }
isEmptyWC :: WantedConstraints -> Bool
isEmptyWC (WC { wc_simple = f, wc_impl = i, wc_insol = n })
= isEmptyBag f && isEmptyBag i && isEmptyBag n
......@@ -2482,6 +2487,9 @@ data SkolemInfo
| ClsSkol Class -- Bound at a class decl
| DerivSkol Type -- Bound by a 'deriving' clause;
-- the type is the instance we are trying to derive
| InstSkol -- Bound at an instance decl
| InstSC TypeSize -- A "given" constraint obtained by superclass selection.
-- If (C ty1 .. tyn) is the largest class from
......@@ -2526,6 +2534,7 @@ pprSkolInfo (SigSkol ctxt ty) = pprSigSkolInfo ctxt ty
pprSkolInfo (IPSkol ips) = ptext (sLit "the implicit-parameter binding") <> plural ips <+> ptext (sLit "for")
<+> pprWithCommas ppr ips
pprSkolInfo (ClsSkol cls) = ptext (sLit "the class declaration for") <+> quotes (ppr cls)
pprSkolInfo (DerivSkol pred) = ptext (sLit "the deriving clause for") <+> quotes (ppr pred)
pprSkolInfo InstSkol = ptext (sLit "the instance declaration")
pprSkolInfo (InstSC n) = ptext (sLit "the instance declaration") <> ifPprDebug (parens (ppr n))
pprSkolInfo DataSkol = ptext (sLit "a data type declaration")
......
T10561.hs:10:52: error:
Couldn't match kind ‘k’ with ‘*’
arising from the first field of ‘Compose’ (type ‘f (g a)’)
When deriving the instance for (Functor (Compose f g))
• Couldn't match kind ‘k’ with ‘*’
arising from the first field of ‘Compose’ (type ‘f (g a)’)
‘k’ is a rigid type variable bound by
the deriving clause for ‘Functor (Compose f g)’ at T10561.hs:10:52
• When deriving the instance for (Functor (Compose f g))
T7148.hs:27:40: error:
Occurs check: cannot construct the infinite type: b ~ Tagged a b
arising from the coercion of the method ‘iso2’
from type ‘forall b. SameType b () -> SameType b b’
to type ‘forall b. SameType b () -> SameType b (Tagged a b)’
When deriving the instance for (IsoUnit (Tagged a b))
• Couldn't match type ‘b’ with ‘Tagged a b’
arising from the coercion of the method ‘iso2’
from type ‘forall b. SameType b () -> SameType b b’
to type ‘forall b. SameType b () -> SameType b (Tagged a b)’
‘b’ is a rigid type variable bound by
the deriving clause for ‘IsoUnit (Tagged a b)’ at T7148.hs:27:40
• When deriving the instance for (IsoUnit (Tagged a b))
T7148.hs:27:40: error:
Occurs check: cannot construct the infinite type: b ~ Tagged a b
arising from the coercion of the method ‘iso1’
from type ‘forall b. SameType () b -> SameType b b’
to type ‘forall b. SameType () b -> SameType (Tagged a b) b’
When deriving the instance for (IsoUnit (Tagged a b))
• Couldn't match type ‘b’ with ‘Tagged a b’
arising from the coercion of the method ‘iso1’
from type ‘forall b. SameType () b -> SameType b b’
to type ‘forall b. SameType () b -> SameType (Tagged a b) b’
‘b’ is a rigid type variable bound by
the deriving clause for ‘IsoUnit (Tagged a b)’ at T7148.hs:27:40
• When deriving the instance for (IsoUnit (Tagged a b))
dummy stderr:
here should be something about roles _not_ "No skolem info"
T11347.hs:6:41: error:
• Couldn't match representation of type ‘a’ with that of ‘b’
arising from the coercion of the method ‘unsafe’
from type ‘Id1 a -> Discern (Id1 a) b’
to type ‘Id2 a -> Discern (Id2 a) b’
‘a’ is a rigid type variable bound by
the deriving clause for ‘UnsafeCast b (Id2 a)’ at T11347.hs:6:41
‘b’ is a rigid type variable bound by
the deriving clause for ‘UnsafeCast b (Id2 a)’ at T11347.hs:6:41
• When deriving the instance for (UnsafeCast b (Id2 a))
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