Commit 0829821a authored by Ryan Scott's avatar Ryan Scott

Implicitly bind kind variables in type family instance RHSes when it's sensible

Summary:
Before, there was a discrepancy in how GHC renamed type synonyms as
opposed to type family instances. That is, GHC would accept definitions like
this one:

```lang=haskell
type T = (Nothing :: Maybe a)
```

However, it would not accept a very similar type family instance:

```lang=haskell
type family   T :: Maybe a
type instance T = (Nothing :: Maybe a)
```

The primary goal of this patch is to bring the renaming of type family
instances up to par with that of type synonyms, causing the latter definition
to be accepted, and fixing #14131.

In particular, we now allow kind variables on the right-hand sides of type
(and data) family instances to be //implicitly// bound by LHS type (or kind)
patterns (as opposed to type variables, which must always be explicitly
bound by LHS type patterns only). As a consequence, this allows programs
reported in #7938 and #9574 to typecheck, whereas before they would
have been rejected.

Implementation-wise, there isn't much trickery involved in making this happen.
We simply need to bind additional kind variables from the RHS of a type family
in the right place (in particular, see `RnSource.rnFamInstEqn`, which has
undergone a minor facelift).

While doing this has the upside of fixing #14131, it also made it easier to
trigger #13985, so I decided to fix that while I was in town. This was
accomplished by a careful blast of `reportFloatingKvs` in `tcFamTyPats`.

Test Plan: ./validate

Reviewers: simonpj, goldfire, austin, bgamari

Reviewed By: simonpj

Subscribers: rwbarton, thomie

GHC Trac Issues: #13985, #14131

Differential Revision: https://phabricator.haskell.org/D3872
parent 24e50f98
This diff is collapsed.
......@@ -26,10 +26,12 @@ module RnTypes (
bindLHsTyVarBndr,
bindSigTyVarsFV, bindHsQTyVars, bindLRdrNames,
extractFilteredRdrTyVars, extractFilteredRdrTyVarsDups,
extractHsTyRdrTyVars, extractHsTyRdrTyVarsDups, extractHsTysRdrTyVars,
extractHsTyRdrTyVars, extractHsTyRdrTyVarsKindVars,
extractHsTyRdrTyVarsDups, extractHsTysRdrTyVars,
extractHsTysRdrTyVarsDups, rmDupsInRdrTyVars,
extractRdrKindSigVars, extractDataDefnKindVars,
freeKiTyVarsAllVars, freeKiTyVarsKindVars, freeKiTyVarsTypeVars
freeKiTyVarsAllVars, freeKiTyVarsKindVars, freeKiTyVarsTypeVars,
elemRdr
) where
import {-# SOURCE #-} RnSplice( rnSpliceType )
......@@ -1661,6 +1663,15 @@ extractHsTyRdrTyVarsDups :: LHsType GhcPs -> RnM FreeKiTyVarsWithDups
extractHsTyRdrTyVarsDups ty
= extract_lty TypeLevel ty emptyFKTV
-- | Extracts the free kind variables (but not the type variables) of an
-- 'HsType'. Does not return any wildcards.
-- When the same name occurs multiple times in the type, only the first
-- occurrence is returned.
-- See Note [Kind and type-variable binders]
extractHsTyRdrTyVarsKindVars :: LHsType GhcPs -> RnM [Located RdrName]
extractHsTyRdrTyVarsKindVars ty
= freeKiTyVarsKindVars <$> extractHsTyRdrTyVars ty
-- | Extracts free type and kind variables from types in a list.
-- When the same name occurs multiple times in the types, only the first
-- occurrence is returned and the rest is filtered out.
......
......@@ -38,6 +38,8 @@ module TcHsType (
kindGeneralize, checkExpectedKindX, instantiateTyUntilN,
reportFloatingKvs,
-- Sort-checking kinds
tcLHsKindSig,
......@@ -1744,6 +1746,46 @@ CUSK: When we determine the tycon's final, never-to-be-changed kind
in kcHsTyVarBndrs, we check to make sure all implicitly-bound kind
vars are indeed mentioned in a kind somewhere. If not, error.
We also perform free-floating kind var analysis for type family instances
(see #13985). 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:
type family T @k :: k
type instance T @(Maybe a) = (Nothing :: Maybe a)
Here, we can see that `a` really is bound by a LHS type pattern, so `a` is in
fact not free-floating. Contrast that with this example:
type instance T = Proxy (Nothing :: Maybe a)
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.
Finally, here's one more brain-teaser (from #9574). In the example below:
class Funct f where
type Codomain f :: *
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`
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 -> *)
-}
--------------------
......
......@@ -1380,7 +1380,9 @@ tc_fam_ty_pats :: FamTyConShape
-> [Name] -- Bound kind/type variable names
-> HsTyPats GhcRn -- Type patterns
-> (TcKind -> TcM r) -- Kind checker for RHS
-> TcM ([Type], r) -- Returns the type-checked patterns
-> TcM ( [TcTyVar] -- Returns the type-checked patterns,
, [TcType] -- the type variables that scope over
, r ) -- them, and the thing inside
-- Check the type patterns of a type or data family instance
-- type instance F <pat1> <pat2> = <type>
-- The 'tyvars' are the free type variables of pats
......@@ -1413,7 +1415,7 @@ tc_fam_ty_pats (FamTyConShape { fs_name = name, fs_arity = arity
-- Kind-check and quantify
-- See Note [Quantifying over family patterns]
; (_, result) <- tcImplicitTKBndrs tv_names $
; (arg_tvs, (args, stuff)) <- tcImplicitTKBndrs tv_names $
do { let loc = nameSrcSpan name
lhs_fun = L loc (HsTyVar NotPromoted (L loc name))
bogus_fun_ty = pprPanic "tc_fam_ty_pats" (ppr name $$ ppr arg_pats)
......@@ -1428,7 +1430,7 @@ tc_fam_ty_pats (FamTyConShape { fs_name = name, fs_arity = arity
; return ((args, stuff), emptyVarSet) }
; return result }
; return (arg_tvs, args, stuff) }
-- See Note [tc_fam_ty_pats vs tcFamTyPats]
tcFamTyPats :: FamTyConShape
......@@ -1443,9 +1445,9 @@ tcFamTyPats :: FamTyConShape
-> TcKind
-> TcM a) -- NB: You can use solveEqualities here.
-> TcM a
tcFamTyPats fam_shape@(FamTyConShape { fs_name = name }) mb_clsinfo
tv_names arg_pats kind_checker thing_inside
= do { (typats, (more_typats, res_kind))
tcFamTyPats fam_shape@(FamTyConShape { fs_name = name, fs_flavor = fam_flav })
mb_clsinfo tv_names arg_pats kind_checker thing_inside
= do { (fam_used_tvs, typats, (more_typats, res_kind))
<- solveEqualities $ -- See Note [Constraints in patterns]
tc_fam_ty_pats fam_shape mb_clsinfo
tv_names arg_pats kind_checker
......@@ -1481,7 +1483,21 @@ tcFamTyPats fam_shape@(FamTyConShape { fs_name = name }) mb_clsinfo
-- bit is cleverer.
; traceTc "tcFamTyPats" (ppr name $$ ppr all_pats $$ ppr qtkvs)
-- Don't print out too much, as we might be in the knot
-- Don't print out too much, as we might be in the knot
-- See Note [Free-floating kind vars] in TcHsType
; let tc_flav = case fam_flav of
TypeFam -> OpenTypeFamilyFlavour
DataFam -> DataFamilyFlavour
all_mentioned_tvs = mkVarSet qtkvs
-- qtkvs has all the tyvars bound by LHS
-- type patterns
unmentioned_tvs = filterOut (`elemVarSet` all_mentioned_tvs)
fam_used_tvs
-- If there are tyvars left over, we can
-- assume they're free-floating, since they
-- aren't bound by a type pattern
; checkNoErrs $ reportFloatingKvs name tc_flav qtkvs unmentioned_tvs
; tcExtendTyVarEnv qtkvs $
-- Extend envt with TcTyVars not TyVars, because the
......
......@@ -27,6 +27,24 @@ Language
wish to; this is quite like how regular datatypes with a kind signature can omit
some type variables.
- There are now fewer restrictions regarding whether kind variables can appear
on the right-hand sides of type and data family instances. Before, there was
a strict requirements that all kind variables on the RHS had to be explicitly
bound by type patterns on the LHS. Now, kind variables can be *implicitly*
bound, which allows constructions like these: ::
data family Nat :: k -> k -> *
-- k is implicitly bound by an invisible kind pattern
newtype instance Nat :: (k -> *) -> (k -> *) -> * where
Nat :: (forall xx. f xx -> g xx) -> Nat f g
class Funct f where
type Codomain f :: *
instance Funct ('KProxy :: KProxy o) where
-- o is implicitly bound by the kind signature
-- of the LHS type pattern ('KProxy)
type Codomain 'KProxy = NatTr (Proxy :: o -> *)
- Implicitly bidirectional pattern synonyms no longer allow bang patterns
(``!``) or irrefutable patterns (``~``) on the right-hand side. Previously,
this was allowed, although the bang patterns and irrefutable patterns would
......
......@@ -7659,8 +7659,23 @@ Note the following points:
instance declarations of the class in which the family was declared,
just as with the equations of the methods of a class.
- The variables on the right hand side of the type family equation
must, as usual, be bound on the left hand side.
- The type variables on the right hand side of the type family equation
must, as usual, be explicitly bound by the left hand side. This restriction
is relaxed for *kind* variables, however, as the right hand side is allowed
to mention kind variables that are implicitly bound. For example, these are
legitimate: ::
data family Nat :: k -> k -> *
-- k is implicitly bound by an invisible kind pattern
newtype instance Nat :: (k -> *) -> (k -> *) -> * where
Nat :: (forall xx. f xx -> g xx) -> Nat f g
class Funct f where
type Codomain f :: *
instance Funct ('KProxy :: KProxy o) where
-- o is implicitly bound by the kind signature
-- of the LHS type pattern ('KProxy)
type Codomain 'KProxy = NatTr (Proxy :: o -> *)
- The instance for an associated type can be omitted in class
instances. In that case, unless there is a default instance (see
......@@ -7715,15 +7730,18 @@ Note the following points:
- The default declaration must mention only type *variables* on the
left hand side, and the right hand side must mention only type
variables bound on the left hand side. However, unlike the associated
type family declaration itself, the type variables of the default
instance are independent of those of the parent class.
variables that are explicitly bound on the left hand side. This restriction
is relaxed for *kind* variables, however, as the right hand side is allowed
to mention kind variables that are implicitly bound on the left hand side.
- Unlike the associated type family declaration itself, the type variables of
the default instance are independent of those of the parent class.
Here are some examples:
::
class C a where
class C (a :: *) where
type F1 a :: *
type instance F1 a = [a] -- OK
type instance F1 a = a->a -- BAD; only one default instance is allowed
......@@ -7738,6 +7756,21 @@ Here are some examples:
type F4 a
type F4 b = a -- BAD; 'a' is not in scope in the RHS
type F5 a :: [k]
type F5 a = ('[] :: [x]) -- OK; the kind variable x is implicitly
bound by an invisible kind pattern
on the LHS
type F6 a
type F6 a =
Proxy ('[] :: [x]) -- BAD; the kind variable x is not bound,
even by an invisible kind pattern
type F7 (x :: a) :: [a]
type F7 x = ('[] :: [a]) -- OK; the kind variable a is implicitly
bound by the kind signature of the
LHS type pattern
.. _scoping-class-params:
Scoping of class parameters
......@@ -7760,6 +7793,33 @@ Here, the right-hand side of the data instance mentions the type
variable ``d`` that does not occur in its left-hand side. We cannot
admit such data instances as they would compromise type safety.
Bear in mind that it is also possible for the *right*-hand side of an
associated family instance to contain *kind* parameters (by using the
:ghc-flag:`-XPolyKinds` extension). For instance, this class and instance are
perfectly admissible: ::
class C k where
type T :: k
instance C (Maybe a) where
type T = (Nothing :: Maybe a)
Here, although the right-hand side ``(Nothing :: Maybe a)`` mentions a kind
variable ``a`` which does not occur on the left-hand side, this is acceptable,
because ``a`` is *implicitly* bound by ``T``'s kind pattern.
A kind variable can also be bound implicitly in a LHS type pattern, as in this
example: ::
class C a where
type T (x :: a) :: [a]
instance C (Maybe a) where
type T x = ('[] :: [Maybe a])
In ``('[] :: [Maybe a])``, the kind variable ``a`` is implicitly bound by the
kind signature of the LHS type pattern ``x``.
Instance contexts and associated type and data instances
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
module T14131 where
import Data.Kind
import Data.Proxy
data family Nat :: k -> k -> *
newtype instance Nat :: (k -> *) -> (k -> *) -> * where
Nat :: (forall xx. f xx -> g xx) -> Nat f g
type family F :: Maybe a
type instance F = (Nothing :: Maybe a)
class C k where
data CD :: k -> k -> *
type CT :: k
instance C (Maybe a) where
data CD :: Maybe a -> Maybe a -> * where
CD :: forall (m :: Maybe a) (n :: Maybe a). Proxy m -> Proxy n -> CD m n
type CT = (Nothing :: Maybe a)
class Z k where
type ZT :: Maybe k
type ZT = (Nothing :: Maybe k)
......@@ -267,3 +267,4 @@ test('T13662', normal, compile, [''])
test('T13705', normal, compile, [''])
test('T12369', normal, compile, [''])
test('T14045', normal, compile, [''])
test('T14131', normal, compile, [''])
T5515.hs:9:3:
The RHS of an associated type declaration mentions ‘a’
T5515.hs:9:3: error:
The RHS of an associated type declaration mentions out-of-scope variable ‘a’
All such variables must be bound on the LHS
T5515.hs:15:3:
The RHS of an associated type declaration mentions ‘a’
T5515.hs:15:3: error:
The RHS of an associated type declaration mentions out-of-scope variable ‘a’
All such variables must be bound on the LHS
T7938.hs:12:3:
The RHS of an associated type declaration mentions ‘k2’
All such variables must be bound on the LHS
T7938.hs:12:16: error:
• Expected a type, but ‘(KP :: KProxy k2)’ has kind ‘KProxy k2’
• In the type ‘(KP :: KProxy k2)’
In the type instance declaration for ‘Bar’
In the instance declaration for ‘Foo (a :: k1) (b :: k2)’
{-# LANGUAGE DataKinds, PolyKinds, TypeOperators, TypeFamilies #-}
{-# LANGUAGE DataKinds, GADTs, PolyKinds, RankNTypes, TypeOperators,
TypeFamilies #-}
module DumpRenamedAst where
......@@ -8,4 +9,10 @@ type family Length (as :: [k]) :: Peano where
Length (a : as) = Succ (Length as)
Length '[] = Zero
data family Nat :: k -> k -> *
-- Ensure that the `k` in the type pattern and `k` in the kind signature have
-- the same binding site.
newtype instance Nat (a :: k -> *) :: (k -> *) -> * where
Nat :: (forall xx. f xx -> g xx) -> Nat f g
main = putStrLn "hello"
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
module T13985 where
import Data.Kind
import Data.Proxy
data family Fam
data instance Fam = MkFam (forall (a :: k). Proxy a)
type family T
type instance T = Proxy (Nothing :: Maybe a)
class C k where
data CD :: k
type CT :: k
instance C Type where
data CD = forall (a :: k). CD (Proxy a)
type CT = Proxy (Nothing :: Maybe a)
class Z a where
type ZT a
type ZT a = Proxy (Nothing :: Maybe x)
T13985.hs:12:1: error:
• Kind variable ‘k’ is implicitly bound in data family
‘Fam’, but does not appear as the kind of any
of its type variables. Perhaps you meant
to bind it (with TypeInType) explicitly somewhere?
• In the data instance declaration for ‘Fam’
T13985.hs:15:15: error:
• Kind variable ‘a’ is implicitly bound in type family
‘T’, but does not appear as the kind of any
of its type variables. Perhaps you meant
to bind it (with TypeInType) explicitly somewhere?
• In the type instance declaration for ‘T’
T13985.hs:22:3: error:
• Kind variable ‘k’ is implicitly bound in data family
‘CD’, but does not appear as the kind of any
of its type variables. Perhaps you meant
to bind it (with TypeInType) explicitly somewhere?
• In the data instance declaration for ‘CD’
In the instance declaration for ‘C Type’
T13985.hs:23:8: error:
• Kind variable ‘a’ is implicitly bound in type family
‘CT’, but does not appear as the kind of any
of its type variables. Perhaps you meant
to bind it (with TypeInType) explicitly somewhere?
• In the type instance declaration for ‘CT’
In the instance declaration for ‘C Type’
T13985.hs:27:3: error:
• Kind variable ‘x’ is implicitly bound in type family
‘ZT’, but does not appear as the kind of any
of its type variables. Perhaps you meant
to bind it (with TypeInType) explicitly somewhere?
Type variables with inferred kinds: (k :: *) (a :: k)
• In the default type instance declaration for ‘ZT’
In the class declaration for ‘Z’
T9574.hs:11:5:
The RHS of an associated type declaration mentions ‘o’
All such variables must be bound on the LHS
......@@ -106,7 +106,7 @@ test('T9200b', normal, compile_fail, [''])
test('T9750', normal, compile, [''])
test('T9569', normal, compile, [''])
test('T9838', normal, multimod_compile, ['T9838.hs','-v0'])
test('T9574', normal, compile_fail, [''])
test('T9574', normal, compile, [''])
test('T9833', normal, compile, [''])
test('T7908', normal, compile, [''])
test('PolyInstances', normal, compile, [''])
......@@ -163,6 +163,7 @@ test('T13393', normal, compile_fail, [''])
test('T13555', normal, compile_fail, [''])
test('T13659', normal, compile_fail, [''])
test('T13625', normal, compile_fail, [''])
test('T13985', normal, compile_fail, [''])
test('T14110', normal, compile_fail, [''])
test('BadKindVar', normal, compile_fail, [''])
test('T13738', 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