diff --git a/compiler/basicTypes/Var.hs b/compiler/basicTypes/Var.hs index c7a6bfe0cd1d8398c3146aacd73b7d2cd4529bb7..a231cf7db7d6b3c7b6d889a471c0606deee3afee 100644 --- a/compiler/basicTypes/Var.hs +++ b/compiler/basicTypes/Var.hs @@ -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 diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs index 276a6b820184c52ad5399cfdf71e7d808434ad82..a096db2635e3b78fb1aacf8690c3dea84382a0e8 100644 --- a/compiler/typecheck/TcErrors.hs +++ b/compiler/typecheck/TcErrors.hs @@ -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 diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs index e2644c537f45368cd79e1f40c43f5a01cbc695cf..0468b396f786be521d1002c2e362d7edf83a6d68 100644 --- a/compiler/typecheck/TcType.hs +++ b/compiler/typecheck/TcType.hs @@ -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,8 +1195,8 @@ isIndirect _ = False isRuntimeUnkSkol :: TyVar -> Bool -- Called only in TcErrors; see Note [Runtime skolems] there isRuntimeUnkSkol x - | isTcTyVar x, RuntimeUnk <- tcTyVarDetails x = True - | otherwise = False + | 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 diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs index 566594f40ba7a4d68fe012fac00408a50099bad9..12502c6f1a96055e2347314b15233a43124bce8e 100644 --- a/compiler/typecheck/TcUnify.hs +++ b/compiler/typecheck/TcUnify.hs @@ -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 diff --git a/compiler/types/InstEnv.hs b/compiler/types/InstEnv.hs index 61913c94e411efbeb2e945bc8b2495ce7ec597a7..e91e5b8b83b1d12e0d9bf87c7ebb06858098fa00 100644 --- a/compiler/types/InstEnv.hs +++ b/compiler/types/InstEnv.hs @@ -965,8 +965,8 @@ incoherent instances as long as there are others. -} instanceBindFun :: TyCoVar -> BindFlag -instanceBindFun tv | isTcTyVar tv && isOverlappableTyVar tv = Skolem - | otherwise = BindMe +instanceBindFun tv | isOverlappableTyVar tv = Skolem + | otherwise = BindMe -- Note [Binding when looking up instances] {- diff --git a/testsuite/tests/indexed-types/should_fail/all.T b/testsuite/tests/indexed-types/should_fail/all.T index 8403ea80cd9aa73691618bc9a82c8bc27f2bbb05..4b0e9946109c41d1b9a4b753cae75b1bf2bcb7c6 100644 --- a/testsuite/tests/indexed-types/should_fail/all.T +++ b/testsuite/tests/indexed-types/should_fail/all.T @@ -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, [''])