Allow TyVars in TcTypes
authorSimon Peyton Jones <simonpj@microsoft.com>
Wed, 23 Nov 2016 16:00:00 +0000 (16:00 +0000)
committerSimon Peyton Jones <simonpj@microsoft.com>
Fri, 25 Nov 2016 11:18:54 +0000 (11:18 +0000)
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.

compiler/basicTypes/Var.hs
compiler/typecheck/TcErrors.hs
compiler/typecheck/TcType.hs
compiler/typecheck/TcUnify.hs
compiler/types/InstEnv.hs
testsuite/tests/indexed-types/should_fail/all.T

index c7a6bfe..a231cf7 100644 (file)
@@ -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
 
index 276a6b8..a096db2 100644 (file)
@@ -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
index e2644c5..0468b39 100644 (file)
@@ -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
index 566594f..12502c6 100644 (file)
@@ -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
index 61913c9..e91e5b8 100644 (file)
@@ -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]
 
 {-
index 8403ea8..4b0e994 100644 (file)
@@ -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, [''])