Commit f0cd728f authored by Ryan Scott's avatar Ryan Scott Committed by Marge Bot

Reject oversaturated VKAs in type family equations

parent ef6b2833
Pipeline #1742 passed with stages
in 381 minutes and 16 seconds
......@@ -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"
......@@ -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) }
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
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.
* *
......@@ -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, [''])
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’
{-# 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
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’
......@@ -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, [''])
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