Use injectiveVarsOfType to catch dodgy type family instance binders (#17008)

Previously, we detected dodgy type family instances binders by
expanding type synonyms (via `exactTyCoVarsOfType`) and looking for
type variables on the RHS that weren't mentioned on the (expanded)
LHS. But this doesn't account for type families (like the example
in #17008), so we instead use `injectiveVarsOfType` to only count
LHS type variables that are in injective positions. That way, the `a`
in `type instance F (x :: T a) = a` will not count if `T` is a type
synonym _or_ a type family.

Along the way, I moved `exactTyCoVarsOfType` to `TyCoFVs` to live
alongside its sibling functions that also compute free variables.

Fixes #17008.

8 files changed, 216 insertions, 90 deletions

diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index c55d16ae9a..7fe947678a 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -957,78 +957,6 @@ isTyFamFree :: Type -> Bool
 -- ^ Check that a type does not contain any type family applications.
 isTyFamFree = null . tcTyFamInsts
 
-{-
-************************************************************************
-*                                                                      *
-          The "exact" free variables of a type
-*                                                                      *
-************************************************************************
-
-Note [Silly type synonym]
-~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider
-  type T a = Int
-What are the free tyvars of (T x)?  Empty, of course!
-
-exactTyCoVarsOfType is used by the type checker to figure out exactly
-which type variables are mentioned in a type.  It only matters
-occasionally -- see the calls to exactTyCoVarsOfType.
-
-Historical note: years and years ago this function was used during
-generalisation -- see #1813.  But that code has long since died.
--}
-
-exactTyCoVarsOfType :: Type -> TyCoVarSet
--- Find the free type variables (of any kind)
--- but *expand* type synonyms.  See Note [Silly type synonym] above.
-exactTyCoVarsOfType ty
-  = go ty
-  where
-    go ty | Just ty' <- tcView ty = go ty'  -- This is the key line
-    go (TyVarTy tv)         = goVar tv
-    go (TyConApp _ tys)     = exactTyCoVarsOfTypes tys
-    go (LitTy {})           = emptyVarSet
-    go (AppTy fun arg)      = go fun `unionVarSet` go arg
-    go (FunTy _ arg res)    = go arg `unionVarSet` go res
-    go (ForAllTy bndr ty)   = delBinderVar (go ty) bndr `unionVarSet` go (binderType bndr)
-    go (CastTy ty co)       = go ty `unionVarSet` goCo co
-    go (CoercionTy co)      = goCo co
-
-    goMCo MRefl    = emptyVarSet
-    goMCo (MCo co) = goCo co
-
-    goCo (Refl ty)            = go ty
-    goCo (GRefl _ ty mco)     = go ty `unionVarSet` goMCo mco
-    goCo (TyConAppCo _ _ args)= goCos args
-    goCo (AppCo co arg)     = goCo co `unionVarSet` goCo arg
-    goCo (ForAllCo tv k_co co)
-      = goCo co `delVarSet` tv `unionVarSet` goCo k_co
-    goCo (FunCo _ co1 co2)   = goCo co1 `unionVarSet` goCo co2
-    goCo (CoVarCo v)         = goVar v
-    goCo (HoleCo h)          = goVar (coHoleCoVar h)
-    goCo (AxiomInstCo _ _ args) = goCos args
-    goCo (UnivCo p _ t1 t2)  = goProv p `unionVarSet` go t1 `unionVarSet` go t2
-    goCo (SymCo co)          = goCo co
-    goCo (TransCo co1 co2)   = goCo co1 `unionVarSet` goCo co2
-    goCo (NthCo _ _ co)      = goCo co
-    goCo (LRCo _ co)         = goCo co
-    goCo (InstCo co arg)     = goCo co `unionVarSet` goCo arg
-    goCo (KindCo co)         = goCo co
-    goCo (SubCo co)          = goCo co
-    goCo (AxiomRuleCo _ c)   = goCos c
-
-    goCos cos = foldr (unionVarSet . goCo) emptyVarSet cos
-
-    goProv UnsafeCoerceProv     = emptyVarSet
-    goProv (PhantomProv kco)    = goCo kco
-    goProv (ProofIrrelProv kco) = goCo kco
-    goProv (PluginProv _)       = emptyVarSet
-
-    goVar v = unitVarSet v `unionVarSet` go (varType v)
-
-exactTyCoVarsOfTypes :: [Type] -> TyVarSet
-exactTyCoVarsOfTypes tys = mapUnionVarSet exactTyCoVarsOfType tys
-
 anyRewritableTyVar :: Bool    -- Ignore casts and coercions
                    -> EqRel   -- Ambient role
                    -> (EqRel -> TcTyVar -> Bool)
diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index 62ba9837d0..045f3c9f18 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/compiler/typecheck/TcValidity.hs
@@ -27,6 +27,7 @@ import Maybes
 import TcUnify    ( tcSubType_NC )
 import TcSimplify ( simplifyAmbiguityCheck )
 import ClsInst    ( matchGlobalInst, ClsInstResult(..), InstanceWhat(..), AssocInstInfo(..) )
+import TyCoFVs
 import TyCoRep
 import TcType hiding ( sizeType, sizeTypes )
 import TysWiredIn ( heqTyConName, eqTyConName, coercibleTyConName )
@@ -2141,7 +2142,7 @@ checkFamPatBinders fam_tc qtvs pats rhs
               , text "qtvs:" <+> ppr qtvs
               , text "rhs_tvs:" <+> ppr (fvVarSet rhs_fvs)
               , text "pat_tvs:" <+> ppr pat_tvs
-              , text "exact_pat_tvs:" <+> ppr exact_pat_tvs ]
+              , text "inj_pat_tvs:" <+> ppr inj_pat_tvs ]
 
          -- Check for implicitly-bound tyvars, mentioned on the
          -- RHS but not bound on the LHS
@@ -2161,15 +2162,21 @@ checkFamPatBinders fam_tc qtvs pats rhs
                             (text "used in")
        }
   where
-    pat_tvs       = tyCoVarsOfTypes pats
-    exact_pat_tvs = exactTyCoVarsOfTypes pats
-    rhs_fvs       = tyCoFVsOfType rhs
-    used_tvs      = pat_tvs `unionVarSet` fvVarSet rhs_fvs
-    bad_qtvs      = filterOut (`elemVarSet` used_tvs) qtvs
-                    -- Bound but not used at all
-    bad_rhs_tvs   = filterOut (`elemVarSet` exact_pat_tvs) (fvVarList rhs_fvs)
-                    -- Used on RHS but not bound on LHS
-    dodgy_tvs     = pat_tvs `minusVarSet` exact_pat_tvs
+    pat_tvs     = tyCoVarsOfTypes pats
+    inj_pat_tvs = fvVarSet $ injectiveVarsOfTypes pats
+      -- The type variables that are in injective positions.
+      -- See Note [Dodgy binding sites in type family instances]
+      --
+      -- NB: It's OK to use the nondeterministic `fvVarSet` function here,
+      -- since the order of `inj_pat_tvs` is never revealed in an error
+      -- message.
+    rhs_fvs     = tyCoFVsOfType rhs
+    used_tvs    = pat_tvs `unionVarSet` fvVarSet rhs_fvs
+    bad_qtvs    = filterOut (`elemVarSet` used_tvs) qtvs
+                  -- Bound but not used at all
+    bad_rhs_tvs = filterOut (`elemVarSet` inj_pat_tvs) (fvVarList rhs_fvs)
+                  -- Used on RHS but not bound on LHS
+    dodgy_tvs   = pat_tvs `minusVarSet` inj_pat_tvs
 
     check_tvs tvs what what2
       = unless (null tvs) $ addErrAt (getSrcSpan (head tvs)) $
@@ -2328,10 +2335,10 @@ checkFamPatBinders.  Here is an interesting example:
     type family   T :: k
     type instance T = (Nothing :: Maybe a)
 
-Upon a cursory glance, it may appear that the kind variable `a` is
-free-floating above, since there are no (visible) LHS patterns in
-`T`. However, there is an *invisible* pattern due to the return kind,
-so inside of GHC, the instance looks closer to this:
+Upon a cursory glance, it may appear that the kind variable `a` is unbound
+since there are no (visible) LHS patterns in `T`. However, there is an
+*invisible* pattern due to the return kind, so inside of GHC, the instance
+looks closer to this:
 
     type family T @k :: k
     type instance T @(Maybe a) = (Nothing :: Maybe a)
@@ -2346,7 +2353,7 @@ This would looks like this inside of GHC:
     type instance T @(*) = Proxy (Nothing :: Maybe a)
 
 So this time, `a` is neither bound by a visible nor invisible type pattern on
-the LHS, so it would be reported as free-floating.
+the LHS, so `a` would be reported as not in scope.
 
 Finally, here's one more brain-teaser (from #9574). In the example below:
 
@@ -2355,13 +2362,51 @@ Finally, here's one more brain-teaser (from #9574). In the example below:
     instance Funct ('KProxy :: KProxy o) where
       type Codomain 'KProxy = NatTr (Proxy :: o -> *)
 
-As it turns out, `o` is not free-floating in this example. That is because `o`
+As it turns out, `o` is in scope in this example. That is because `o` is
 bound by the kind signature of the LHS type pattern 'KProxy. To make this more
 obvious, one can also write the instance like so:
 
     instance Funct ('KProxy :: KProxy o) where
       type Codomain ('KProxy :: KProxy o) = NatTr (Proxy :: o -> *)
 
+Note [Dodgy binding sites in type family instances]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider the following example (from #7536):
+
+  type T a = Int
+  type instance F (T a) = a
+
+This `F` instance is extremely fishy, since the RHS, `a`, purports to be
+"bound" by the LHS pattern `T a`. "Bound" has scare quotes around it because
+`T a` expands to `Int`, which doesn't mention at all, so it's as if one had
+actually written:
+
+  type instance F Int = a
+
+That is clearly bogus, so to reject this, we check that every type variable
+that is mentioned on the RHS is /actually/ bound on the LHS. In other words,
+we need to do something slightly more sophisticated that just compute the free
+variables of the LHS patterns.
+
+It's tempting to just expand all type synonyms on the LHS and then compute
+their free variables, but even that isn't sophisticated enough. After all,
+an impish user could write the following (#17008):
+
+  type family ConstType (a :: Type) :: Type where
+    ConstType _ = Type
+
+  type family F (x :: ConstType a) :: Type where
+    F (x :: ConstType a) = a
+
+Just like in the previous example, the `a` on the RHS isn't actually bound
+on the LHS, but this time a type family is responsible for the deception, not
+a type synonym.
+
+We avoid both issues by requiring that all RHS type variables are mentioned
+in injective positions on the left-hand side (by way of
+`injectiveVarsOfTypes`). For instance, the `a` in `T a` is not in an injective
+position, as `T` is not an injective type constructor, so we do not count that.
+Similarly for the `a` in `ConstType a`.
 
 Note [Matching in the consistent-instantation check]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/types/TyCoFVs.hs b/compiler/types/TyCoFVs.hs
index 52dd945104..b8da86e36c 100644
--- a/compiler/types/TyCoFVs.hs
+++ b/compiler/types/TyCoFVs.hs
@@ -1,6 +1,7 @@
 module TyCoFVs
   (
         tyCoVarsOfType, tyCoVarsOfTypeDSet, tyCoVarsOfTypes, tyCoVarsOfTypesDSet,
+        exactTyCoVarsOfType, exactTyCoVarsOfTypes,
         tyCoFVsBndr, tyCoFVsVarBndr, tyCoFVsVarBndrs,
         tyCoFVsOfType, tyCoVarsOfTypeList,
         tyCoFVsOfTypes, tyCoVarsOfTypesList,
@@ -12,7 +13,7 @@ module TyCoFVs
         tyCoFVsOfCo, tyCoFVsOfCos,
         tyCoVarsOfCoList, tyCoVarsOfProv,
         almostDevoidCoVarOfCo,
-        injectiveVarsOfType,
+        injectiveVarsOfType, injectiveVarsOfTypes,
 
         noFreeVarsOfType, noFreeVarsOfTypes, noFreeVarsOfCo,
 
@@ -25,7 +26,7 @@ module TyCoFVs
 
 import GhcPrelude
 
-import {-# SOURCE #-} Type (coreView)
+import {-# SOURCE #-} Type (coreView, tcView)
 
 import TyCoRep
 import TyCon
@@ -299,6 +300,75 @@ tyCoVarsOfTypesList :: [Type] -> [TyCoVar]
 -- See Note [Free variables of types]
 tyCoVarsOfTypesList tys = fvVarList $ tyCoFVsOfTypes tys
 
+{-
+************************************************************************
+*                                                                      *
+          The "exact" free variables of a type
+*                                                                      *
+************************************************************************
+
+Note [Silly type synonym]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+  type T a = Int
+What are the free tyvars of (T x)?  Empty, of course!
+
+exactTyCoVarsOfType is used by the type checker to figure out exactly
+which type variables are mentioned in a type.  It only matters
+occasionally -- see the calls to exactTyCoVarsOfType.
+-}
+
+exactTyCoVarsOfType :: Type -> TyCoVarSet
+-- Find the free type variables (of any kind)
+-- but *expand* type synonyms.  See Note [Silly type synonym] above.
+exactTyCoVarsOfType ty
+  = go ty
+  where
+    go ty | Just ty' <- tcView ty = go ty'  -- This is the key line
+    go (TyVarTy tv)         = goVar tv
+    go (TyConApp _ tys)     = exactTyCoVarsOfTypes tys
+    go (LitTy {})           = emptyVarSet
+    go (AppTy fun arg)      = go fun `unionVarSet` go arg
+    go (FunTy _ arg res)    = go arg `unionVarSet` go res
+    go (ForAllTy bndr ty)   = delBinderVar (go ty) bndr `unionVarSet` go (binderType bndr)
+    go (CastTy ty co)       = go ty `unionVarSet` goCo co
+    go (CoercionTy co)      = goCo co
+
+    goMCo MRefl    = emptyVarSet
+    goMCo (MCo co) = goCo co
+
+    goCo (Refl ty)            = go ty
+    goCo (GRefl _ ty mco)     = go ty `unionVarSet` goMCo mco
+    goCo (TyConAppCo _ _ args)= goCos args
+    goCo (AppCo co arg)     = goCo co `unionVarSet` goCo arg
+    goCo (ForAllCo tv k_co co)
+      = goCo co `delVarSet` tv `unionVarSet` goCo k_co
+    goCo (FunCo _ co1 co2)   = goCo co1 `unionVarSet` goCo co2
+    goCo (CoVarCo v)         = goVar v
+    goCo (HoleCo h)          = goVar (coHoleCoVar h)
+    goCo (AxiomInstCo _ _ args) = goCos args
+    goCo (UnivCo p _ t1 t2)  = goProv p `unionVarSet` go t1 `unionVarSet` go t2
+    goCo (SymCo co)          = goCo co
+    goCo (TransCo co1 co2)   = goCo co1 `unionVarSet` goCo co2
+    goCo (NthCo _ _ co)      = goCo co
+    goCo (LRCo _ co)         = goCo co
+    goCo (InstCo co arg)     = goCo co `unionVarSet` goCo arg
+    goCo (KindCo co)         = goCo co
+    goCo (SubCo co)          = goCo co
+    goCo (AxiomRuleCo _ c)   = goCos c
+
+    goCos cos = foldr (unionVarSet . goCo) emptyVarSet cos
+
+    goProv UnsafeCoerceProv     = emptyVarSet
+    goProv (PhantomProv kco)    = goCo kco
+    goProv (ProofIrrelProv kco) = goCo kco
+    goProv (PluginProv _)       = emptyVarSet
+
+    goVar v = unitVarSet v `unionVarSet` go (varType v)
+
+exactTyCoVarsOfTypes :: [Type] -> TyVarSet
+exactTyCoVarsOfTypes tys = mapUnionVarSet exactTyCoVarsOfType tys
+
 -- | The worker for `tyCoFVsOfType` and `tyCoFVsOfTypeList`.
 -- The previous implementation used `unionVarSet` which is O(n+m) and can
 -- make the function quadratic.
@@ -536,6 +606,15 @@ almost_devoid_co_var_of_types (ty:tys) cv
 ------------- Injective free vars -----------------
 
 -- | Returns the free variables of a 'Type' that are in injective positions.
+-- Specifically, it finds the free variables while:
+--
+-- * Expanding type synonyms
+--
+-- * Ignoring the coercion in @(ty |> co)@
+--
+-- * Ignoring the non-injective fields of a 'TyConApp'
+--
+--
 -- For example, if @F@ is a non-injective type family, then:
 --
 -- @
@@ -570,6 +649,19 @@ injectiveVarsOfType = go
     go (CastTy ty _)     = go ty
     go CoercionTy{}      = emptyFV
 
+-- | Returns the free variables of a 'Type' that are in injective positions.
+-- Specifically, it finds the free variables while:
+--
+-- * Expanding type synonyms
+--
+-- * Ignoring the coercion in @(ty |> co)@
+--
+-- * Ignoring the non-injective fields of a 'TyConApp'
+--
+-- See @Note [When does a tycon application need an explicit kind signature?]@.
+injectiveVarsOfTypes :: [Type] -> FV
+injectiveVarsOfTypes tys = mapUnionFV injectiveVarsOfType tys
+
 ------------- No free vars -----------------
 
 -- | Returns True if this type has no free variables. Should be the same as
diff --git a/testsuite/tests/indexed-types/should_compile/T17008b.hs b/testsuite/tests/indexed-types/should_compile/T17008b.hs
new file mode 100644
index 0000000000..25763684e4
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T17008b.hs
@@ -0,0 +1,38 @@
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+module T17008b where
+
+import Data.Kind
+
+type family ConstType1 (a :: Type) :: Type where
+  ConstType1 _ = Type
+
+type family F1 (x :: ConstType1 a) :: Type where
+  F1 @a (x :: ConstType1 a) = a
+type family F2 (x :: ConstType1 a) :: ConstType1 a where
+  F2 @a (x :: ConstType1 a) = x :: ConstType1 a
+type F3 (x :: ConstType1 a) = a
+type F4 (x :: ConstType1 a) = x :: ConstType1 a
+
+type ConstType2 (a :: Type) = Type
+
+type family G1 (x :: ConstType2 a) :: Type where
+  G1 @a (x :: ConstType2 a) = a
+type family G2 (x :: ConstType2 a) :: ConstType2 a where
+  G2 @a (x :: ConstType2 a) = x :: ConstType1 a
+type G3 (x :: ConstType2 a) = a
+type G4 (x :: ConstType2 a) = x :: ConstType2 a
+
+type Id1 (a :: Type) = a
+
+type family H (a :: Type) :: Type where
+  H (Id1 a) = a
+type family I (x :: Id1 a) :: Type where
+  I (x :: Id1 a) = a
+
+type family Id2 (a :: Type) :: Type where
+  Id2 a = a
+
+type family J (x :: Id2 a) :: Type where
+  J (x :: Id2 a) = a
diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T
index f4ecabd83d..7eeeda6d59 100644
--- a/testsuite/tests/indexed-types/should_compile/all.T
+++ b/testsuite/tests/indexed-types/should_compile/all.T
@@ -291,3 +291,4 @@ test('T16356_Compile1', normal, compile, [''])
 test('T16356_Compile2', normal, compile, [''])
 test('T16632', normal, compile, ['-Wunused-type-patterns -fdiagnostics-show-caret'])
 test('T16828', normal, compile, [''])
+test('T17008b', normal, compile, [''])
diff --git a/testsuite/tests/indexed-types/should_fail/T17008a.hs b/testsuite/tests/indexed-types/should_fail/T17008a.hs
new file mode 100644
index 0000000000..53d7f7737c
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T17008a.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+module T17006 where
+
+import Data.Kind
+
+type family ConstType (a :: Type) :: Type where
+  ConstType _ = Type
+
+type family F (x :: ConstType a) :: Type where
+  F (x :: ConstType a) = a
+
+f :: F Int
+f = let x = x in x
diff --git a/testsuite/tests/indexed-types/should_fail/T17008a.stderr b/testsuite/tests/indexed-types/should_fail/T17008a.stderr
new file mode 100644
index 0000000000..8428a279b4
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T17008a.stderr
@@ -0,0 +1,7 @@
+
+T17008a.hs:11:21: error:
+    • Type variable ‘a1’ is mentioned in the RHS,
+        but not bound on the LHS of the family instance
+        The real LHS (expanding synonyms) is: F @a2 x
+    • In the equations for closed type family ‘F’
+      In the type family declaration for ‘F’
diff --git a/testsuite/tests/indexed-types/should_fail/all.T b/testsuite/tests/indexed-types/should_fail/all.T
index 1ad9aa2504..ca1781b8fd 100644
--- a/testsuite/tests/indexed-types/should_fail/all.T
+++ b/testsuite/tests/indexed-types/should_fail/all.T
@@ -159,3 +159,4 @@ test('T16110_Fail3', normal, compile_fail, [''])
 test('T16356_Fail1', normal, compile_fail, [''])
 test('T16356_Fail2', normal, compile_fail, [''])
 test('T16356_Fail3', normal, compile_fail, [''])
+test('T17008a', normal, compile_fail, ['-fprint-explicit-kinds'])