Commit 7496be5c authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Exclude TyVars from the constraint solver

There is a general invariant that the constraint solver doesn't see
TyVars, only TcTyVars.  But when checking the generic-default
signature of a class, we called checkValidType on the generic-default
type, which had the class TyVar free. That in turn meant that it wasn't
considered during flattening, which led to the error reported in
Trac #11608.

The fix is simple: call checkValidType on the /closed/ type. Easy.

While I was at it, I added a bunch of ASSERTs about the TcTyVar
invariant.
parent 4ddfe135
......@@ -961,6 +961,20 @@ Here the second equation is unreachable. The original constraint
the *signature* (Trac #7293). So, for Given errors we replace the
env (and hence src-loc) on its CtLoc with that from the immediately
enclosing implication.
Note [Error messages for untouchables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider (Trac #9109)
data G a where { GBool :: G Bool }
foo x = case x of GBool -> True
Here we can't solve (t ~ Bool), where t is the untouchable result
meta-var 't', because of the (a ~ Bool) from the pattern match.
So we infer the type
f :: forall a t. G a -> t
making the meta-var 't' into a skolem. So when we come to report
the unsolved (t ~ Bool), t won't look like an untouchable meta-var
any more. So we don't assert that it is.
-}
mkEqErr :: ReportErrCtxt -> [Ct] -> TcM ErrMsg
......@@ -1212,9 +1226,13 @@ mkTyVarEqErr dflags ctxt report ct oriented tv1 ty2
; mkErrorMsgFromCt ctxt ct (mconcat [msg, tv_extra, report]) }
-- Nastiest case: attempt to unify an untouchable variable
-- See Note [Error messages for untouchables]
| (implic:_) <- cec_encl ctxt -- Get the innermost context
, Implic { ic_env = env, ic_given = given, ic_info = skol_info } <- implic
= do { let msg = important $ misMatchMsg ct oriented ty1 ty2
, Implic { ic_env = env, ic_given = given
, ic_tclvl = lvl, ic_info = skol_info } <- implic
= ASSERT2( isTcTyVar tv1 && not (isTouchableMetaTyVar lvl tv1)
, ppr tv1 ) -- See Note [Error messages for untouchables]
do { let msg = important $ misMatchMsg ct oriented ty1 ty2
tclvl_extra = important $
nest 2 $
sep [ quotes (ppr tv1) <+> text "is untouchable"
......@@ -1324,23 +1342,21 @@ extraTyVarInfo :: ReportErrCtxt -> TcTyVar -> TcType -> SDoc
-- Add on extra info about skolem constants
-- NB: The types themselves are already tidied
extraTyVarInfo ctxt tv1 ty2
= tv_extra tv1 $$ ty_extra ty2
= ASSERT2( isTcTyVar tv1, ppr tv1 )
tv_extra tv1 $$ ty_extra ty2
where
implics = cec_encl ctxt
ty_extra ty = case tcGetTyVar_maybe ty of
Just tv -> tv_extra tv
Nothing -> empty
tv_extra tv | isTcTyVar tv, isSkolemTyVar tv
, let pp_tv = quotes (ppr tv)
= case tcTyVarDetails tv of
SkolemTv {} -> pprSkol implics tv
FlatSkol {} -> pp_tv <+> text "is a flattening type variable"
RuntimeUnk {} -> pp_tv <+> text "is an interactive-debugger skolem"
MetaTv {} -> empty
| otherwise -- Normal case
= empty
tv_extra tv
| let pp_tv = quotes (ppr tv)
= case tcTyVarDetails tv of
SkolemTv {} -> pprSkol implics tv
FlatSkol {} -> pp_tv <+> text "is a flattening type variable"
RuntimeUnk {} -> pp_tv <+> text "is an interactive-debugger skolem"
MetaTv {} -> empty
suggestAddSig :: ReportErrCtxt -> TcType -> TcType -> SDoc
-- See Note [Suggest adding a type signature]
......@@ -1354,7 +1370,7 @@ suggestAddSig ctxt ty1 ty2
where
inferred_bndrs = nub (get_inf ty1 ++ get_inf ty2)
get_inf ty | Just tv <- tcGetTyVar_maybe ty
, isTcTyVar tv, isSkolemTyVar tv
, isSkolemTyVar tv
, (_, InferSkol prs) <- getSkolemInfo (cec_encl ctxt) tv
= map fst prs
| otherwise
......@@ -1711,8 +1727,9 @@ carry on. For example
f x = x:x
Here we will infer somethiing like
f :: forall a. a -> [a]
with a suspended error of (a ~ [a]). So 'a' is now a skolem, but not
one bound by the programmer! Here we really should report an occurs check.
with a deferred error of (a ~ [a]). So in the deferred unsolved constraint
'a' is now a skolem, but not one bound by the programmer in the context!
Here we really should report an occurs check.
So isUserSkolem distinguishes the two.
......
......@@ -2247,9 +2247,7 @@ checkValidClass cls
; unless constrained_class_methods $
mapM_ check_constraint (tail (theta1 ++ theta2))
; case dm of
Just (_, GenericDM ty) -> checkValidType ctxt ty
_ -> return ()
; check_dm ctxt dm
}
where
ctxt = FunSigCtxt op_name True -- Report redundant class constraints
......@@ -2279,6 +2277,18 @@ checkValidClass cls
fam_tvs = tyConTyVars fam_tc
mini_env = zipVarEnv tyvars (mkTyVarTys tyvars)
check_dm :: UserTypeCtxt -> DefMethInfo -> TcM ()
-- Check validity of the /top-level/ generic-default type
-- E.g for class C a where
-- default op :: forall b. (a~b) => blah
-- we do not want to do an ambiguity check on a type with
-- a free TyVar 'a' (Trac #11608). See TcType
-- Note [TyVars and TcTyVars during type checking]
-- Hence the mkSpecForAllTys to close the type.
check_dm ctxt (Just (_, GenericDM ty))
= checkValidType ctxt (mkSpecForAllTys tyvars ty)
check_dm _ _ = return ()
checkFamFlag :: Name -> TcM ()
-- Check that we don't use families without -XTypeFamilies
-- The parser won't even parse them, but I suppose a GHC API
......
......@@ -375,16 +375,26 @@ Similarly consider
When doing kind inference on {S,T} we don't want *skolems* for k1,k2,
because they end up unifying; we want those SigTvs again.
Note [TyVars and TcTyVars]
~~~~~~~~~~~~~~~~~~~~~~~~~~
Note [TyVars and TcTyVars during type checking]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The Var type has constructors TyVar and TcTyVar. They are used
as follows:
* TcTyVar: used only during type checking. Should never appear
* TcTyVar: used /only/ during type checking. Should never appear
afterwards. May contain a mutable field, in the MetaTv case.
* TyVar: can appear any time. During type checking they behave
precisely like (SkolemTv False) = vanillaSkolemTv
* TyVar: is never seen by the constraint solver, except locally
inside a type like (forall a. [a] ->[a]), where 'a' is a TyVar.
We instantiate these with TcTyVars before exposing the type
to the constraint solver.
I have swithered about the latter invariant, excluding TyVars from the
constraint solver. It's not strictly essential, and indeed
(historically but still there) Var.tcTyVarDetails returns
vanillaSkolemTv for a TyVar.
But ultimately I want to seeparate Type from TcType, and in that case
we would need to enforce the separation.
-}
-- A TyVarDetails is inside a TyVar
......@@ -838,7 +848,8 @@ allBoundVariabless = mapUnionVarSet allBoundVariables
isTouchableOrFmv :: TcLevel -> TcTyVar -> Bool
isTouchableOrFmv ctxt_tclvl tv
= case tcTyVarDetails tv of
= ASSERT2( isTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
MetaTv { mtv_tclvl = tv_tclvl, mtv_info = info }
-> ASSERT2( checkTcLevelInvariant ctxt_tclvl tv_tclvl,
ppr tv $$ ppr tv_tclvl $$ ppr ctxt_tclvl )
......@@ -850,7 +861,8 @@ isTouchableOrFmv ctxt_tclvl tv
isTouchableMetaTyVar :: TcLevel -> TcTyVar -> Bool
isTouchableMetaTyVar ctxt_tclvl tv
| isTyVar tv
= case tcTyVarDetails tv of
= ASSERT2( isTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
MetaTv { mtv_tclvl = tv_tclvl }
-> ASSERT2( checkTcLevelInvariant ctxt_tclvl tv_tclvl,
ppr tv $$ ppr tv_tclvl $$ ppr ctxt_tclvl )
......@@ -861,7 +873,8 @@ isTouchableMetaTyVar ctxt_tclvl tv
isFloatedTouchableMetaTyVar :: TcLevel -> TcTyVar -> Bool
isFloatedTouchableMetaTyVar ctxt_tclvl tv
| isTyVar tv
= case tcTyVarDetails tv of
= ASSERT2( isTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
MetaTv { mtv_tclvl = tv_tclvl } -> tv_tclvl `strictlyDeeperThan` ctxt_tclvl
_ -> False
| otherwise = False
......@@ -880,44 +893,51 @@ isTyConableTyVar tv
-- with a type constructor application; in particular,
-- not a SigTv
| isTyVar tv
= case tcTyVarDetails tv of
= ASSERT2( isTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
MetaTv { mtv_info = SigTv } -> False
_ -> True
| otherwise = True
isFmvTyVar tv
= case tcTyVarDetails tv of
= ASSERT2( isTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
MetaTv { mtv_info = FlatMetaTv } -> True
_ -> False
-- | True of both given and wanted flatten-skolems (fak and usk)
isFlattenTyVar tv
= case tcTyVarDetails tv of
= ASSERT2( isTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
FlatSkol {} -> True
MetaTv { mtv_info = FlatMetaTv } -> True
_ -> False
-- | True of FlatSkol skolems only
isFskTyVar tv
= case tcTyVarDetails tv of
= ASSERT2( isTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
FlatSkol {} -> True
_ -> False
isSkolemTyVar tv
= case tcTyVarDetails tv of
= ASSERT2( isTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
MetaTv {} -> False
_other -> True
isOverlappableTyVar tv
| isTyVar tv
= case tcTyVarDetails tv of
= ASSERT2( isTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
SkolemTv overlappable -> overlappable
_ -> False
| otherwise = False
isMetaTyVar tv
| isTyVar tv
= case tcTyVarDetails tv of
= ASSERT2( isTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
MetaTv {} -> True
_ -> False
| otherwise = False
......
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
module T11608 where
type Traversal s t a b = forall f. Applicative f => (a -> f b) -> s -> f t
class Each s t a b | s -> a, t -> b, s b -> t, t a -> s where
each :: Traversal s t a b
default each :: (Traversable g, s ~ g a, t ~ g b) => Traversal s t a b
each = traverse
......@@ -506,3 +506,4 @@ test('T11458', normal, compile, [''])
test('T11524', normal, compile, [''])
test('T11552', normal, compile, [''])
test('T11246', normal, compile, [''])
test('T11608', normal, compile, [''])
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