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.

5 files changed, 96 insertions, 34 deletions

diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs
index b1cc44975c..58bcafdda9 100644
--- a/compiler/typecheck/TcErrors.hs
+++ b/compiler/typecheck/TcErrors.hs
@@ -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.
 
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index 31eaeb0d5d..6a0daabe8a 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -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
diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index 972cbae749..73a46ae6c6 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -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
diff --git a/testsuite/tests/typecheck/should_compile/T11608.hs b/testsuite/tests/typecheck/should_compile/T11608.hs
new file mode 100644
index 0000000000..5627135b5b
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T11608.hs
@@ -0,0 +1,14 @@
+{-# 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
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 4310be440c..ca8cd0a28f 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -506,3 +506,4 @@ test('T11458', normal, compile, [''])
 test('T11524', normal, compile, [''])
 test('T11552', normal, compile, [''])
 test('T11246', normal, compile, [''])
+test('T11608', normal, compile, [''])