Perform a validity check on assoc type defaults.

This fixes #10817 and #10899. A knock-on effect is that we must
now remember locations of associated type defaults for error
messages during validity checking. This isn't too bad, but it
increases the size of the diff somewhat.

Test cases: indexed-types/should_fail/T108{17,99}

13 files changed, 82 insertions, 17 deletions

diff --git a/compiler/iface/MkIface.hs b/compiler/iface/MkIface.hs
index e8b37cea5e..0bbd907464 100644
--- a/compiler/iface/MkIface.hs
+++ b/compiler/iface/MkIface.hs
@@ -1763,7 +1763,7 @@ classToIfaceDecl env clas
 
     toIfaceAT :: ClassATItem -> IfaceAT
     toIfaceAT (ATI tc def)
-      = IfaceAT if_decl (fmap (tidyToIfaceType env2) def)
+      = IfaceAT if_decl (fmap (tidyToIfaceType env2 . fst) def)
       where
         (env2, if_decl) = tyConToIfaceDecl env1 tc
 
diff --git a/compiler/iface/TcIface.hs b/compiler/iface/TcIface.hs
index 5189b3c5a8..5462fa29c2 100644
--- a/compiler/iface/TcIface.hs
+++ b/compiler/iface/TcIface.hs
@@ -427,7 +427,7 @@ tc_iface_decl _parent ignore_prags
                       Just def -> forkM (mk_at_doc tc)                 $
                                   extendIfaceTyVarEnv (tyConTyVars tc) $
                                   do { tc_def <- tcIfaceType def
-                                     ; return (Just tc_def) }
+                                     ; return (Just (tc_def, noSrcSpan)) }
                   -- Must be done lazily in case the RHS of the defaults mention
                   -- the type constructor being defined here
                   -- e.g.   type AT a; type AT b = AT [b]   Trac #8002
diff --git a/compiler/typecheck/TcInstDcls.hs b/compiler/typecheck/TcInstDcls.hs
index a4b3870b2f..d31b7bf310 100644
--- a/compiler/typecheck/TcInstDcls.hs
+++ b/compiler/typecheck/TcInstDcls.hs
@@ -572,7 +572,7 @@ tcATDefault loc inst_subst defined_ats (ATI fam_tc defs)
    -- Example:   class C a where { type F a b :: *; type F a b = () }
    --            instance C [x]
    -- Then we want to generate the decl:   type F [x] b = ()
-  | Just rhs_ty <- defs
+  | Just (rhs_ty, _loc) <- defs
   = do { let (subst', pat_tys') = mapAccumL subst_tv inst_subst
                                             (tyConTyVars fam_tc)
              rhs'     = substTy subst' rhs_ty
@@ -580,6 +580,11 @@ tcATDefault loc inst_subst defined_ats (ATI fam_tc defs)
              tvs'     = varSetElemsKvsFirst tv_set'
        ; rep_tc_name <- newFamInstTyConName (L loc (tyConName fam_tc)) pat_tys'
        ; let axiom = mkSingleCoAxiom Nominal rep_tc_name tvs' fam_tc pat_tys' rhs'
+           -- NB: no validity check. We check validity of default instances
+           -- in the class definition. Because type instance arguments cannot
+           -- be type family applications and cannot be polytypes, the
+           -- validity check is redundant.
+
        ; traceTc "mk_deflt_at_instance" (vcat [ ppr fam_tc, ppr rhs_ty
                                               , pprCoAxiom axiom ])
        ; fam_inst <- ASSERT( tyVarsOfType rhs' `subVarSet` tv_set' )
diff --git a/compiler/typecheck/TcRnDriver.hs b/compiler/typecheck/TcRnDriver.hs
index 1128a44e5f..8b4747575c 100644
--- a/compiler/typecheck/TcRnDriver.hs
+++ b/compiler/typecheck/TcRnDriver.hs
@@ -939,8 +939,8 @@ checkBootTyCon tc1 tc2
                  (text "The associated type defaults differ")
 
        -- Ignore the location of the defaults
-       eqATDef Nothing    Nothing    = True
-       eqATDef (Just ty1) (Just ty2) = eqTypeX env ty1 ty2
+       eqATDef Nothing             Nothing             = True
+       eqATDef (Just (ty1, _loc1)) (Just (ty2, _loc2)) = eqTypeX env ty1 ty2
        eqATDef _ _ = False
 
        eqFD (as1,bs1) (as2,bs2) =
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index 516dca09b9..5c28b63c51 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -914,9 +914,9 @@ tcClassATs class_name parent ats at_defs
                   ; return (ATI fam_tc atd) }
 
 -------------------------
-tcDefaultAssocDecl :: TyCon                  -- ^ Family TyCon
-                   -> [LTyFamDefltEqn Name]  -- ^ Defaults
-                   -> TcM (Maybe Type)       -- ^ Type checked RHS
+tcDefaultAssocDecl :: TyCon                         -- ^ Family TyCon
+                   -> [LTyFamDefltEqn Name]         -- ^ Defaults
+                   -> TcM (Maybe (Type, SrcSpan))   -- ^ Type checked RHS
 tcDefaultAssocDecl _ []
   = return Nothing  -- No default declaration
 
@@ -941,7 +941,7 @@ tcDefaultAssocDecl fam_tc [L loc (TyFamEqn { tfe_tycon = L _ tc_name
        ; let fam_tc_tvs = tyConTyVars fam_tc
              subst = zipTopTvSubst tvs (mkTyVarTys fam_tc_tvs)
        ; return ( ASSERT( equalLength fam_tc_tvs tvs )
-                  Just (substTy subst rhs_ty) ) }
+                  Just (substTy subst rhs_ty, loc) ) }
     -- We check for well-formedness and validity later, in checkValidClass
 
 -------------------------
@@ -1821,13 +1821,19 @@ checkValidClass cls
             = when (tyVarsOfType pred `subVarSet` cls_tv_set)
                    (addErrTc (badMethPred sel_id pred))
 
-    check_at (ATI fam_tc _)
-      | cls_arity > 0   -- Check that the associated type mentions at least
+    check_at (ATI fam_tc m_dflt_rhs)
+      = do { checkTc (cls_arity == 0 || any (`elemVarSet` cls_tv_set) fam_tvs)
+                     (noClassTyVarErr cls fam_tc)
+                        -- Check that the associated type mentions at least
                         -- one of the class type variables
-      = checkTc (any (`elemVarSet` cls_tv_set) (tyConTyVars fam_tc))
-                (noClassTyVarErr cls fam_tc)
-      | otherwise       -- The check is disabled for nullary type classes,
-      = return ()       -- since there is no possible ambiguity (Trac #10020)
+                        -- The check is disabled for nullary type classes,
+                        -- since there is no possible ambiguity (Trac #10020)
+           ; whenIsJust m_dflt_rhs $ \ (rhs, loc) ->
+             checkValidTyFamEqn (Just (cls, mini_env)) fam_tc
+                                fam_tvs (mkTyVarTys fam_tvs) rhs loc }
+        where
+          fam_tvs = tyConTyVars fam_tc
+    mini_env = zipVarEnv tyvars (mkTyVarTys tyvars)
 
 checkFamFlag :: Name -> TcM ()
 -- Check that we don't use families without -XTypeFamilies
diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index 4f20a3d1d6..c21e683777 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/compiler/typecheck/TcValidity.hs
@@ -12,6 +12,7 @@ module TcValidity (
   checkValidInstance, validDerivPred,
   checkInstTermination,
   ClsInfo, checkValidCoAxiom, checkValidCoAxBranch,
+  checkValidTyFamEqn,
   checkConsistentFamInst,
   arityErr, badATErr
   ) where
@@ -1276,6 +1277,19 @@ checkValidCoAxBranch :: Maybe ClsInfo
 checkValidCoAxBranch mb_clsinfo fam_tc
                     (CoAxBranch { cab_tvs = tvs, cab_lhs = typats
                                 , cab_rhs = rhs, cab_loc = loc })
+  = checkValidTyFamEqn mb_clsinfo fam_tc tvs typats rhs loc
+
+-- | Do validity checks on a type family equation, including consistency
+-- with any enclosing class instance head, termination, and lack of
+-- polytypes.
+checkValidTyFamEqn :: Maybe ClsInfo
+                   -> TyCon   -- ^ of the type family
+                   -> [TyVar] -- ^ bound tyvars in the equation
+                   -> [Type]  -- ^ type patterns
+                   -> Type    -- ^ rhs
+                   -> SrcSpan
+                   -> TcM ()
+checkValidTyFamEqn mb_clsinfo fam_tc tvs typats rhs loc
   = setSrcSpan loc $
     do { checkValidFamPats fam_tc tvs typats
 
@@ -1329,7 +1343,8 @@ checkValidFamPats :: TyCon -> [TyVar] -> [Type] -> TcM ()
 --         type instance F (T a) = a
 -- c) Have the right number of patterns
 checkValidFamPats fam_tc tvs ty_pats
-  = ASSERT( length ty_pats == tyConArity fam_tc )
+  = ASSERT2( length ty_pats == tyConArity fam_tc
+           , ppr ty_pats $$ ppr fam_tc $$ ppr (tyConArity fam_tc) )
       -- A family instance must have exactly the same number of type
       -- parameters as the family declaration.  You can't write
       --     type family F a :: * -> *
diff --git a/compiler/types/Class.hs b/compiler/types/Class.hs
index 787ab6dad7..9daa3722b8 100644
--- a/compiler/types/Class.hs
+++ b/compiler/types/Class.hs
@@ -29,6 +29,7 @@ import Name
 import BasicTypes
 import Unique
 import Util
+import SrcLoc
 import Outputable
 import FastString
 import BooleanFormula (BooleanFormula)
@@ -100,7 +101,8 @@ data DefMeth = NoDefMeth                -- No default method
 
 data ClassATItem
   = ATI TyCon         -- See Note [Associated type tyvar names]
-        (Maybe Type)  -- Default associated type (if any) from this template
+        (Maybe (Type, SrcSpan))
+                      -- Default associated type (if any) from this template
                       -- Note [Associated type defaults]
 
 type ClassMinimalDef = BooleanFormula Name -- Required methods
@@ -147,6 +149,8 @@ Note that
    the default Type rhs
 
 The @mkClass@ function fills in the indirect superclasses.
+
+The SrcSpan is for the entire original declaration.
 -}
 
 mkClass :: [TyVar]
diff --git a/testsuite/tests/indexed-types/should_fail/T10817.hs b/testsuite/tests/indexed-types/should_fail/T10817.hs
new file mode 100644
index 0000000000..a9a12d0daa
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T10817.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module T10817 where
+
+import Data.Proxy
+
+class C a where
+  type F a
+  type F a = F a
+
+instance C Bool
+
+x :: Proxy (F Bool)
+x = Proxy
diff --git a/testsuite/tests/indexed-types/should_fail/T10817.stderr b/testsuite/tests/indexed-types/should_fail/T10817.stderr
new file mode 100644
index 0000000000..32c0e7f223
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T10817.stderr
@@ -0,0 +1,6 @@
+
+T10817.hs:9:3: error:
+    The type family application ‘F a’
+      is no smaller than the instance head
+    (Use UndecidableInstances to permit this)
+    In the class declaration for ‘C’
diff --git a/testsuite/tests/indexed-types/should_fail/T10899.hs b/testsuite/tests/indexed-types/should_fail/T10899.hs
new file mode 100644
index 0000000000..cacac4a2f7
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T10899.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE TypeFamilies, RankNTypes #-}
+
+module T10899 where
+
+class C a where
+  type F a
+  type F a = forall m. m a
diff --git a/testsuite/tests/indexed-types/should_fail/T10899.stderr b/testsuite/tests/indexed-types/should_fail/T10899.stderr
new file mode 100644
index 0000000000..e48274c466
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T10899.stderr
@@ -0,0 +1,4 @@
+
+T10899.hs:7:3: error:
+    Illegal polymorphic or qualified type: forall (m :: * -> *). m a
+    In the class declaration for ‘C’
diff --git a/testsuite/tests/indexed-types/should_fail/all.T b/testsuite/tests/indexed-types/should_fail/all.T
index a75dacd90e..722a4d3969 100644
--- a/testsuite/tests/indexed-types/should_fail/all.T
+++ b/testsuite/tests/indexed-types/should_fail/all.T
@@ -136,3 +136,5 @@ test('T7788', normal, compile_fail, [''])
 test('T8550', normal, compile_fail, [''])
 test('T9554', normal, compile_fail, [''])
 test('T10141', normal, compile_fail, [''])
+test('T10817', normal, compile_fail, [''])
+test('T10899', normal, compile_fail, [''])
diff --git a/testsuite/tests/typecheck/should_compile/tc253.hs b/testsuite/tests/typecheck/should_compile/tc253.hs
index 3ce439e4f2..2fd528b296 100644
--- a/testsuite/tests/typecheck/should_compile/tc253.hs
+++ b/testsuite/tests/typecheck/should_compile/tc253.hs
@@ -1,4 +1,6 @@
 {-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+  -- this is needed because |FamHelper a x| /< |Fam a x|
 module ShouldCompile where
 
 class Cls a where