Commit 18d0bdd3 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Allow TyVars in TcTypes

Up to now we've had a rule that a TyVar can't apppear in a type
seen by the type checker; they should all be TcTyVars.  But:

a) With -XTypeInType it becomes much harder to exclude them;
   see Note [TcTyVars in the typechecker] in TcType.

b) It's unnecessary to exculde them; instead we can just treat
   a TyVar just like vanillaSkolemTv.

This is what was causing an ASSERT error in
indexed-types/should_fail/T12041, reported in Trac #12826.

That patch allows a TyVar in a TcType.  The most significant
change is to make Var.tcTyVarDetails return vanillaSkolemTv.
In fact it already did, but (a) it was not documented, and
(b) we never exploited it.  Now we rely on it.
parent 1eec1f21
......@@ -51,7 +51,7 @@ module Var (
setIdExported, setIdNotExported,
-- ** Predicates
isId, isTKVar, isTyVar, isTcTyVar,
isId, isTyVar, isTcTyVar,
isLocalVar, isLocalId, isCoVar, isNonCoVarId, isTyCoVar,
isGlobalId, isExportedId,
mustHaveLocalBinding,
......@@ -452,6 +452,7 @@ mkTcTyVar name kind details
}
tcTyVarDetails :: TyVar -> TcTyVarDetails
-- See Note [TcTyVars in the typechecker] in TcType
tcTyVarDetails (TcTyVar { tc_tv_details = details }) = details
tcTyVarDetails (TyVar {}) = vanillaSkolemTv
tcTyVarDetails var = pprPanic "tcTyVarDetails" (ppr var <+> dcolon <+> pprKind (tyVarKind var))
......@@ -563,15 +564,12 @@ setIdNotExported id = ASSERT( isLocalId id )
************************************************************************
-}
isTyVar :: Var -> Bool
isTyVar = isTKVar -- Historical
isTyVar :: Var -> Bool -- True of both TyVar and TcTyVar
isTyVar (TyVar {}) = True
isTyVar (TcTyVar {}) = True
isTyVar _ = False
isTKVar :: Var -> Bool -- True of both type and kind variables
isTKVar (TyVar {}) = True
isTKVar (TcTyVar {}) = True
isTKVar _ = False
isTcTyVar :: Var -> Bool
isTcTyVar :: Var -> Bool -- True of TcTyVar only
isTcTyVar (TcTyVar {}) = True
isTcTyVar _ = False
......
......@@ -1486,7 +1486,7 @@ mkTyVarEqErr dflags ctxt report ct oriented tv1 ty2
| (implic:_) <- cec_encl ctxt -- Get the innermost context
, Implic { ic_env = env, ic_given = given
, ic_tclvl = lvl, ic_info = skol_info } <- implic
= ASSERT2( isTcTyVar tv1 && not (isTouchableMetaTyVar lvl tv1)
= ASSERT2( not (isTouchableMetaTyVar lvl tv1)
, ppr tv1 ) -- See Note [Error messages for untouchables]
do { let msg = important $ misMatchMsg ct oriented ty1 ty2
tclvl_extra = important $
......@@ -1602,8 +1602,7 @@ extraTyVarInfo :: ReportErrCtxt -> TcTyVar -> TcType -> SDoc
-- Add on extra info about skolem constants
-- NB: The types themselves are already tidied
extraTyVarInfo ctxt tv1 ty2
= ASSERT2( isTcTyVar tv1, ppr tv1 )
tv_extra tv1 $$ ty_extra ty2
= tv_extra tv1 $$ ty_extra ty2
where
implics = cec_encl ctxt
ty_extra ty = case tcGetTyVar_maybe ty of
......
......@@ -260,8 +260,45 @@ tau ::= tyvar
-- In all cases, a (saturated) type synonym application is legal,
-- provided it expands to the required form.
Note [TcTyVars in the typechecker]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The typechecker uses a lot of type variables with special properties,
notably being a unification variable with a mutable reference. These
use the 'TcTyVar' variant of Var.Var.
However, the type checker and constraint solver can encounter type
variables that use the 'TyVar' variant of Var.Var, for a couple of
reasons:
- When unifying or flattening under (forall a. ty)
- When typechecking a class decl, say
class C (a :: k) where
foo :: T a -> Int
We have first kind-check the header; fix k and (a:k) to be
TyVars, bring 'k' and 'a' into scope, and kind check the
signature for 'foo'. In doing so we call solveEqualities to
solve any kind equalities in foo's signature. So the solver
may see free occurences of 'k'.
It's convenient to simply treat these TyVars as skolem constants,
which of course they are. So
* Var.tcTyVarDetails succeeds on a TyVar, returning
vanillaSkolemTv, as well as on a TcTyVar.
* tcIsTcTyVar returns True for both TyVar and TcTyVar variants
of Var.Var. The "tc" prefix means "a type variable that can be
encountered by the typechecker".
This is a bit of a change from an earlier era when we remoselessly
insisted on real TcTyVars in the type checker. But that seems
unnecessary (for skolems, TyVars are fine) and it's now very hard
to guarantee, with the advent of kind equalities.
-}
-- See Note [TcTyVars in the typechecker]
type TcTyVar = TyVar -- Used only during type inference
type TcCoVar = CoVar -- Used only during type inference
type TcType = Type -- A TcType can have mutable type variables
......@@ -701,7 +738,7 @@ checkTcLevelInvariant (TcLevel ctxt_tclvl) (TcLevel tv_tclvl)
tcTyVarLevel :: TcTyVar -> TcLevel
tcTyVarLevel tv
= ASSERT2( isTcTyVar tv, ppr tv )
= ASSERT2( tcIsTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
MetaTv { mtv_tclvl = tv_lvl } -> tv_lvl
SkolemTv tv_lvl _ -> tv_lvl
......@@ -840,6 +877,9 @@ rewritableTyVarsOfTypes :: [TcType] -> TcTyVarSet
rewritableTyVarsOfTypes tys = mapUnionVarSet rewritableTyVarsOfType tys
rewritableTyVarsOfType :: TcType -> TcTyVarSet
-- Used during kick-out from the inert set
-- Ignores coercions and casts, because rewriting those does
-- not help solving, and it's more efficient to ignore them
rewritableTyVarsOfType ty
= go ty
where
......@@ -1006,9 +1046,13 @@ splitDepVarsOfType = go
************************************************************************
-}
tcIsTcTyVar :: TcTyVar -> Bool
-- See Note [TcTyVars in the typechecker]
tcIsTcTyVar tv = isTyVar tv
isTouchableOrFmv :: TcLevel -> TcTyVar -> Bool
isTouchableOrFmv ctxt_tclvl tv
= ASSERT2( isTcTyVar tv, ppr tv )
= ASSERT2( tcIsTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
MetaTv { mtv_tclvl = tv_tclvl, mtv_info = info }
-> ASSERT2( checkTcLevelInvariant ctxt_tclvl tv_tclvl,
......@@ -1020,7 +1064,7 @@ isTouchableOrFmv ctxt_tclvl tv
isTouchableMetaTyVar :: TcLevel -> TcTyVar -> Bool
isTouchableMetaTyVar ctxt_tclvl tv
= ASSERT2( isTcTyVar tv, ppr tv )
= ASSERT2( tcIsTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
MetaTv { mtv_tclvl = tv_tclvl }
-> ASSERT2( checkTcLevelInvariant ctxt_tclvl tv_tclvl,
......@@ -1030,15 +1074,13 @@ isTouchableMetaTyVar ctxt_tclvl tv
isFloatedTouchableMetaTyVar :: TcLevel -> TcTyVar -> Bool
isFloatedTouchableMetaTyVar ctxt_tclvl tv
= ASSERT2( isTcTyVar tv, ppr tv )
= ASSERT2( tcIsTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
MetaTv { mtv_tclvl = tv_tclvl } -> tv_tclvl `strictlyDeeperThan` ctxt_tclvl
_ -> False
isImmutableTyVar :: TyVar -> Bool
isImmutableTyVar tv
| isTcTyVar tv = isSkolemTyVar tv
| otherwise = True
isImmutableTyVar tv = isSkolemTyVar tv
isTyConableTyVar, isSkolemTyVar, isOverlappableTyVar,
isMetaTyVar, isAmbiguousTyVar,
......@@ -1048,20 +1090,20 @@ isTyConableTyVar tv
-- True of a meta-type variable that can be filled in
-- with a type constructor application; in particular,
-- not a SigTv
= ASSERT2( isTcTyVar tv, ppr tv )
= ASSERT2( tcIsTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
MetaTv { mtv_info = SigTv } -> False
_ -> True
isFmvTyVar tv
= ASSERT2( isTcTyVar tv, ppr tv )
= ASSERT2( tcIsTcTyVar 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
= ASSERT2( isTcTyVar tv, ppr tv )
= ASSERT2( tcIsTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
FlatSkol {} -> True
MetaTv { mtv_info = FlatMetaTv } -> True
......@@ -1069,25 +1111,25 @@ isFlattenTyVar tv
-- | True of FlatSkol skolems only
isFskTyVar tv
= ASSERT2( isTcTyVar tv, ppr tv )
= ASSERT2( tcIsTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
FlatSkol {} -> True
_ -> False
isSkolemTyVar tv
= ASSERT2( isTcTyVar tv, ppr tv )
= ASSERT2( tcIsTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
MetaTv {} -> False
_other -> True
isOverlappableTyVar tv
= ASSERT2( isTcTyVar tv, ppr tv )
= ASSERT2( tcIsTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
SkolemTv _ overlappable -> overlappable
_ -> False
isMetaTyVar tv
= ASSERT2( isTcTyVar tv, ppr tv )
= ASSERT2( tcIsTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
MetaTv {} -> True
_ -> False
......@@ -1153,7 +1195,7 @@ isIndirect _ = False
isRuntimeUnkSkol :: TyVar -> Bool
-- Called only in TcErrors; see Note [Runtime skolems] there
isRuntimeUnkSkol x
| isTcTyVar x, RuntimeUnk <- tcTyVarDetails x = True
| RuntimeUnk <- tcTyVarDetails x = True
| otherwise = False
{-
......@@ -1958,7 +2000,7 @@ isRigidEqPred :: TcLevel -> PredTree -> Bool
-- * Meta-tv SigTv on LHS, tyvar on right
isRigidEqPred tc_lvl (EqPred NomEq ty1 _)
| Just tv1 <- tcGetTyVar_maybe ty1
= ASSERT2( isTcTyVar tv1, ppr tv1 )
= ASSERT2( tcIsTcTyVar tv1, ppr tv1 )
not (isMetaTyVar tv1) || isTouchableMetaTyVar tc_lvl tv1
| otherwise -- LHS is not a tyvar
......
......@@ -148,7 +148,7 @@ matchExpectedFunTys herald arity orig_ty thing_inside
, mkWpFun idHsWrapper wrap_res arg_ty res_ty ) }
go acc_arg_tys n ty@(TyVarTy tv)
| ASSERT( isTcTyVar tv) isMetaTyVar tv
| isMetaTyVar tv
= do { cts <- readMetaTyVar tv
; case cts of
Indirect ty' -> go acc_arg_tys n ty'
......@@ -275,7 +275,7 @@ matchActualFunTysPart herald ct_orig mb_thing arity orig_ty
, arg_ty : tys, ty_r ) }
go n acc_args ty@(TyVarTy tv)
| ASSERT( isTcTyVar tv) isMetaTyVar tv
| isMetaTyVar tv
= do { cts <- readMetaTyVar tv
; case cts of
Indirect ty' -> go n acc_args ty'
......@@ -372,7 +372,7 @@ matchExpectedTyConApp tc orig_ty
= return (mkTcNomReflCo ty, args)
go (TyVarTy tv)
| ASSERT( isTcTyVar tv) isMetaTyVar tv
| isMetaTyVar tv
= do { cts <- readMetaTyVar tv
; case cts of
Indirect ty -> go ty
......@@ -415,7 +415,7 @@ matchExpectedAppTy orig_ty
= return (mkTcNomReflCo orig_ty, (fun_ty, arg_ty))
go (TyVarTy tv)
| ASSERT( isTcTyVar tv) isMetaTyVar tv
| isMetaTyVar tv
= do { cts <- readMetaTyVar tv
; case cts of
Indirect ty -> go ty
......@@ -1121,8 +1121,7 @@ buildImplicationFor tclvl skol_info skol_tvs given wanted
= return (emptyBag, emptyTcEvBinds)
| otherwise
= ASSERT2( all isTcTyVar skol_tvs, ppr skol_tvs )
ASSERT2( all isSkolemTyVar skol_tvs, ppr skol_tvs )
= ASSERT2( all isSkolemTyVar skol_tvs, ppr skol_tvs )
do { ev_binds_var <- newTcEvBinds
; env <- getLclEnv
; let implic = Implic { ic_tclvl = tclvl
......
......@@ -965,7 +965,7 @@ incoherent instances as long as there are others.
-}
instanceBindFun :: TyCoVar -> BindFlag
instanceBindFun tv | isTcTyVar tv && isOverlappableTyVar tv = Skolem
instanceBindFun tv | isOverlappableTyVar tv = Skolem
| otherwise = BindMe
-- Note [Binding when looking up instances]
......
......@@ -137,6 +137,5 @@ test('T10899', normal, compile_fail, [''])
test('T11136', normal, compile_fail, [''])
test('T7788', normal, compile_fail, [''])
test('T11450', normal, compile_fail, [''])
test('T12041', when(compiler_debugged(), expect_broken(12826)),
compile_fail, [''])
test('T12041', normal, compile_fail, [''])
test('T12522a', normal, compile_fail, [''])
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