summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorRyan Scott <ryan.gl.scott@gmail.com>2019-07-31 10:32:32 -0400
committerMarge Bot <ben+marge-bot@smart-cactus.org>2019-08-02 08:15:25 -0400
commit93bed40a0efdcb0ecea2406c22c402896e4ecfd8 (patch)
tree303dc3f6bca3a5663790acfabd3fd0f251136a9d
parent1b9d32b8b8d55335bed7fb3677054327c6072768 (diff)
downloadhaskell-93bed40a0efdcb0ecea2406c22c402896e4ecfd8.tar.gz
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.
-rw-r--r--compiler/typecheck/TcType.hs72
-rw-r--r--compiler/typecheck/TcValidity.hs77
-rw-r--r--compiler/types/TyCoFVs.hs96
-rw-r--r--testsuite/tests/indexed-types/should_compile/T17008b.hs38
-rw-r--r--testsuite/tests/indexed-types/should_compile/all.T1
-rw-r--r--testsuite/tests/indexed-types/should_fail/T17008a.hs14
-rw-r--r--testsuite/tests/indexed-types/should_fail/T17008a.stderr7
-rw-r--r--testsuite/tests/indexed-types/should_fail/all.T1
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'])