diff options
| -rw-r--r-- | compiler/typecheck/TcType.hs | 72 | ||||
| -rw-r--r-- | compiler/typecheck/TcValidity.hs | 77 | ||||
| -rw-r--r-- | compiler/types/TyCoFVs.hs | 96 | ||||
| -rw-r--r-- | testsuite/tests/indexed-types/should_compile/T17008b.hs | 38 | ||||
| -rw-r--r-- | testsuite/tests/indexed-types/should_compile/all.T | 1 | ||||
| -rw-r--r-- | testsuite/tests/indexed-types/should_fail/T17008a.hs | 14 | ||||
| -rw-r--r-- | testsuite/tests/indexed-types/should_fail/T17008a.stderr | 7 | ||||
| -rw-r--r-- | testsuite/tests/indexed-types/should_fail/all.T | 1 |
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']) |