diff options
author | Ryan Scott <ryan.gl.scott@gmail.com> | 2019-07-31 10:32:32 -0400 |
---|---|---|
committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2019-08-02 08:15:25 -0400 |
commit | 93bed40a0efdcb0ecea2406c22c402896e4ecfd8 (patch) | |
tree | 303dc3f6bca3a5663790acfabd3fd0f251136a9d /testsuite | |
parent | 1b9d32b8b8d55335bed7fb3677054327c6072768 (diff) | |
download | haskell-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.
Diffstat (limited to 'testsuite')
5 files changed, 61 insertions, 0 deletions
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']) |