diff options
author | Ryan Scott <ryan.gl.scott@gmail.com> | 2019-02-01 19:10:55 -0500 |
---|---|---|
committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2019-02-01 19:10:55 -0500 |
commit | f0cd728fde9bb582930a616cff8d0c5a178c5e14 (patch) | |
tree | 2bbc4f5fcea598e13db934725ed470b489201b67 | |
parent | ef6b28339b18597a2df1ce39116f1d4e4533804c (diff) | |
download | haskell-f0cd728fde9bb582930a616cff8d0c5a178c5e14.tar.gz |
Reject oversaturated VKAs in type family equations
-rw-r--r-- | compiler/typecheck/TcTyClsDecls.hs | 3 | ||||
-rw-r--r-- | compiler/typecheck/TcValidity.hs | 68 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_compile/all.T | 1 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_fail/T15793.hs (renamed from testsuite/tests/typecheck/should_compile/T15793.hs) | 0 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_fail/T15793.stderr | 5 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_fail/T16255.hs | 21 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_fail/T16255.stderr | 10 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_fail/all.T | 2 |
8 files changed, 108 insertions, 2 deletions
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs index a3b7975b8e..7bf5e20431 100644 --- a/compiler/typecheck/TcTyClsDecls.hs +++ b/compiler/typecheck/TcTyClsDecls.hs @@ -3806,6 +3806,9 @@ wrongKindOfFamily family | isDataFamilyTyCon family = text "data family" | otherwise = pprPanic "wrongKindOfFamily" (ppr family) +-- | Produce an error for oversaturated type family equations with too many +-- required arguments. +-- See Note [Oversaturated type family equations] in TcValidity. wrongNumberOfParmsErr :: Arity -> SDoc wrongNumberOfParmsErr max_args = text "Number of parameters must match family declaration; expected" diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs index 3b88fe1c89..ca58877bcb 100644 --- a/compiler/typecheck/TcValidity.hs +++ b/compiler/typecheck/TcValidity.hs @@ -2056,7 +2056,17 @@ checkFamPatBinders fam_tc qtvs pats rhs -- data instance forall a. T Int = MkT Int -- See Note [Unused explicitly bound variables in a family pattern] ; check_tvs bad_qtvs (text "bound by a forall") - (text "used in") } + (text "used in") + + -- Check for oversaturated visible kind arguments in a type family + -- equation. + -- See Note [Oversaturated type family equations] + ; when (isTypeFamilyTyCon fam_tc) $ + case drop (tyConArity fam_tc) pats of + [] -> pure () + spec_arg:_ -> + addErr $ text "Illegal oversaturated visible kind argument:" + <+> quotes (char '@' <> pprParendType spec_arg) } where pat_tvs = tyCoVarsOfTypes pats exact_pat_tvs = exactTyCoVarsOfTypes pats @@ -2401,6 +2411,62 @@ type application, like @x \@Bool 1@. (Of course it does nothing, but it is permissible.) In the type family case, the only sensible explanation is that the user has made a mistake -- thus we throw an error. +Note [Oversaturated type family equations] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Type family tycons have very rigid arities. We want to reject something like +this: + + type family Foo :: Type -> Type where + Foo x = ... + +Because Foo has arity zero (i.e., it doesn't bind anything to the left of the +double colon), we want to disallow any equation for Foo that has more than zero +arguments, such as `Foo x = ...`. The algorithm here is pretty simple: if an +equation has more arguments than the arity of the type family, reject. + +Things get trickier when visible kind application enters the picture. Consider +the following example: + + type family Bar (x :: j) :: forall k. Either j k where + Bar 5 @Symbol = ... + +The arity of Bar is two, since it binds two variables, `j` and `x`. But even +though Bar's equation has two arguments, it's still invalid. Imagine the same +equation in Core: + + Bar Nat 5 Symbol = ... + +Here, it becomes apparent that Bar is actually taking /three/ arguments! So +we can't just rely on a simple counting argument to reject +`Bar 5 @Symbol = ...`, since it only has two user-written arguments. +Moreover, there's one explicit argument (5) and one visible kind argument +(@Symbol), which matches up perfectly with the fact that Bar has one required +binder (x) and one specified binder (j), so that's not a valid way to detect +oversaturation either. + +To solve this problem in a robust way, we do the following: + +1. When kind-checking, we count the number of user-written *required* + arguments and check if there is an equal number of required tycon binders. + If not, reject. (See `wrongNumberOfParmsErr` in TcTyClsDecls.) + + We perform this step during kind-checking, not during validity checking, + since we can give better error messages if we catch it early. +2. When validity checking, take all of the (Core) type patterns from on + equation, drop the first n of them (where n is the arity of the type family + tycon), and check if there are any types leftover. If so, reject. + + Why does this work? We know that after dropping the first n type patterns, + none of the leftover types can be required arguments, since step (1) would + have already caught that. Moreover, the only places where visible kind + applications should be allowed are in the first n types, since those are the + only arguments that can correspond to binding forms. Therefore, the + remaining arguments must correspond to oversaturated uses of visible kind + applications, which are precisely what we want to reject. + +Note that we only perform this check for type families, and not for data +families. This is because it is perfectly acceptable to oversaturate data +family instance equations: see Note [Arity of data families] in FamInstEnv. ************************************************************************ * * diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T index 5146dbc00e..7a08e21e23 100644 --- a/testsuite/tests/typecheck/should_compile/all.T +++ b/testsuite/tests/typecheck/should_compile/all.T @@ -629,7 +629,6 @@ test('T14735', normal, compile, ['']) test('T15180', normal, compile, ['']) test('T15232', normal, compile, ['']) test('T15788', normal, compile, ['']) -test('T15793', normal, compile, ['']) test('T15807a', normal, compile, ['']) test('T13833', normal, compile, ['']) test('T14185', expect_broken(14185), compile, ['']) diff --git a/testsuite/tests/typecheck/should_compile/T15793.hs b/testsuite/tests/typecheck/should_fail/T15793.hs index 4e96d83f10..4e96d83f10 100644 --- a/testsuite/tests/typecheck/should_compile/T15793.hs +++ b/testsuite/tests/typecheck/should_fail/T15793.hs diff --git a/testsuite/tests/typecheck/should_fail/T15793.stderr b/testsuite/tests/typecheck/should_fail/T15793.stderr new file mode 100644 index 0000000000..d160947e3b --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T15793.stderr @@ -0,0 +1,5 @@ + +T15793.hs:18:3: error: + • Illegal oversaturated visible kind argument: ‘@a’ + • In the equations for closed type family ‘F2’ + In the type family declaration for ‘F2’ diff --git a/testsuite/tests/typecheck/should_fail/T16255.hs b/testsuite/tests/typecheck/should_fail/T16255.hs new file mode 100644 index 0000000000..ef2f0a9cb6 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T16255.hs @@ -0,0 +1,21 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +module T16255 where + +import Data.Kind +import GHC.TypeLits + +data SBool :: Bool -> Type +type family F1 :: forall k. k -> Type where + F1 @Bool = SBool + +data family D1 :: forall k. k -> Type +-- Note that this similar-looking data family instance is OK, since data family +-- instances permit oversaturation in their equations. +data instance D1 @Bool :: Bool -> Type + +type family F2 (x :: j) :: forall k. Either j k where + F2 5 @Symbol = Left 4 diff --git a/testsuite/tests/typecheck/should_fail/T16255.stderr b/testsuite/tests/typecheck/should_fail/T16255.stderr new file mode 100644 index 0000000000..74379a316c --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T16255.stderr @@ -0,0 +1,10 @@ + +T16255.hs:13:3: error: + • Illegal oversaturated visible kind argument: ‘@Bool’ + • In the equations for closed type family ‘F1’ + In the type family declaration for ‘F1’ + +T16255.hs:21:3: error: + • Illegal oversaturated visible kind argument: ‘@Symbol’ + • In the equations for closed type family ‘F2’ + In the type family declaration for ‘F2’ diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T index 2b8561909f..a87c846c49 100644 --- a/testsuite/tests/typecheck/should_fail/all.T +++ b/testsuite/tests/typecheck/should_fail/all.T @@ -492,6 +492,7 @@ test('T15592a', normal, compile_fail, ['']) test('T15629', normal, compile_fail, ['']) test('T15767', normal, compile_fail, ['']) test('T15648', [extra_files(['T15648a.hs'])], multimod_compile_fail, ['T15648', '-v0 -fprint-equality-relations']) +test('T15793', normal, compile_fail, ['']) test('T15796', normal, compile_fail, ['']) test('T15807', normal, compile_fail, ['']) test('T15954', normal, compile_fail, ['']) @@ -508,3 +509,4 @@ test('T16059d', [extra_files(['T16059b.hs'])], multimod_compile_fail, ['T16059d', '-v0']) test('T16059e', [extra_files(['T16059b.hs'])], multimod_compile_fail, ['T16059e', '-v0']) +test('T16255', normal, compile_fail, ['']) |