Commit 93bed40a authored by Ryan Scott's avatar Ryan Scott Committed by Marge Bot

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.
parent 1b9d32b8
......@@ -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)
......
......@@ -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]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......
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
......
{-# 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
......@@ -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, [''])
{-# 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
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’
......@@ -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'])
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment