Commit 12794287 authored by Richard Eisenberg's avatar Richard Eisenberg
Browse files

Quantify unfixed kind variables in CUSKs

This is a small change in user-facing behavior. When we
have a unification variable left over in a CUSK, we previously
would issue an error. But, we can just quantify. This also
teaches kcLHsQTyVars to use quantifyTyVars instead of its own,
ad-hoc quantification scheme.

Fixes #15273.

test case: polykinds/T11648b
parent fe770c21
......@@ -100,7 +100,7 @@ import PrelNames hiding ( wildCardName )
import qualified GHC.LanguageExtensions as LangExt
import Maybes
import Data.List ( partition, mapAccumR )
import Data.List ( mapAccumR )
import Control.Monad
{-
......@@ -1580,33 +1580,23 @@ kcLHsQTyVars name flav cusk
-- Now, because we're in a CUSK, quantify over the mentioned
-- kind vars, in dependency order.
; tc_tvs <- mapM zonkTcTyVarToTyVar tc_tvs
; res_kind <- zonkTcType res_kind
; let tc_binders_unzonked = zipWith mk_tc_binder hs_tvs tc_tvs
; dvs <- zonkTcTypeAndSplitDepVars (mkSpecForAllTys scoped_kvs $
mkTyConKind tc_binders_unzonked res_kind)
; qkvs <- quantifyTyVars emptyVarSet dvs
-- don't call tcGetGlobalTyCoVars. For associated types, it gets the
-- tyvars from the enclosing class -- but that's wrong. We *do* want
-- to quantify over those tyvars.
; scoped_kvs <- mapM zonkTcTyVarToTyVar scoped_kvs
; tc_tvs <- mapM zonkTcTyVarToTyVar tc_tvs
; res_kind <- zonkTcType res_kind
; let tc_binders = zipWith mk_tc_binder hs_tvs tc_tvs
qkvs = tyCoVarsOfTypeWellScoped (mkTyConKind tc_binders res_kind)
-- the visibility of tvs doesn't matter here; we just
-- want the free variables not to include the tvs
-- If there are any meta-tvs left, the user has
-- lied about having a CUSK. Error.
; let (meta_tvs, good_tvs) = partition isMetaTyVar qkvs
-- skip this check for associated types. Why?
-- Any variables mentioned in the definition will get defaulted,
-- except those that appear in the class head. Defaulted vars do
-- not concern us here (they are fully determined). Variables from
-- the class head will be fully determined whenever the class has
-- a CUSK, and an associated family has a CUSK only when the enclosing
-- class has one. So skipping is safe. But why is it necessary?
-- It's possible that a class variable has too low a TcLevel to have
-- fully settled down by this point, and so this check will get
-- a false positive.
; when (not_associated && not (null meta_tvs)) $
report_non_cusk_tvs (qkvs ++ tc_tvs) res_kind
-- If any of the scoped_kvs aren't actually mentioned in a binder's
-- kind (or the return kind), then we're in the CUSK case from
-- Note [Free-floating kind vars]
; let all_tc_tvs = good_tvs ++ tc_tvs
; let all_tc_tvs = scoped_kvs ++ tc_tvs
all_mentioned_tvs = mapUnionVarSet (tyCoVarsOfType . tyVarKind)
all_tc_tvs
`unionVarSet` tyCoVarsOfType res_kind
......@@ -1614,8 +1604,9 @@ kcLHsQTyVars name flav cusk
scoped_kvs
; reportFloatingKvs name flav all_tc_tvs unmentioned_kvs
; let final_binders = map (mkNamedTyConBinder Specified) good_tvs
++ tc_binders
; let final_binders = map (mkNamedTyConBinder Inferred) qkvs
++ map (mkNamedTyConBinder Specified) scoped_kvs
++ tc_binders
tycon = mkTcTyCon name (ppr user_tyvars) final_binders res_kind
(mkTyVarNamePairs (scoped_kvs ++ tc_tvs))
flav
......@@ -1627,7 +1618,7 @@ kcLHsQTyVars name flav cusk
; traceTc "kcLHsQTyVars: cusk" $
vcat [ ppr name, ppr kv_ns, ppr hs_tvs, ppr dep_names
, ppr tc_tvs, ppr (mkTyConKind final_binders res_kind)
, ppr qkvs, ppr meta_tvs, ppr good_tvs, ppr final_binders ]
, ppr qkvs, ppr final_binders ]
; return (tycon, stuff) }
......@@ -1651,11 +1642,6 @@ kcLHsQTyVars name flav cusk
; return (tycon, stuff) }
where
open_fam = tcFlavourIsOpen flav
not_associated = case flav of
DataFamilyFlavour assoc -> not assoc
OpenTypeFamilyFlavour assoc -> not assoc
_ -> True
skol_info = TyConSkol flav name
mk_tc_binder :: LHsTyVarBndr GhcRn -> TyVar -> TyConBinder
......@@ -1666,27 +1652,6 @@ kcLHsQTyVars name flav cusk
| otherwise
= mkAnonTyConBinder tv
report_non_cusk_tvs all_tvs res_kind
= do { all_tvs <- mapM zonkTyCoVarKind all_tvs
; let (_, tidy_tvs) = tidyOpenTyCoVars emptyTidyEnv all_tvs
(meta_tvs, other_tvs) = partition isMetaTyVar tidy_tvs
; addErr $
vcat [ text "You have written a *complete user-suppled kind signature*,"
, hang (text "but the following variable" <> plural meta_tvs <+>
isOrAre meta_tvs <+> text "undetermined:")
2 (vcat (map pp_tv meta_tvs))
, text "Perhaps add a kind signature."
, ppUnless (null other_tvs) $
hang (text "Inferred kinds of user-written variables:")
2 (vcat (map pp_tv other_tvs))
-- It's possible that the result kind contains
-- underdetermined, forall-bound variables which weren't
-- reported earier (see #13777).
, hang (text "Inferred result kind:")
2 (ppr res_kind) ] }
where
pp_tv tv = ppr tv <+> dcolon <+> ppr (tyVarKind tv)
kcLHsQTyVars _ _ _ (XLHsQTyVars _) _ = panic "kcLHsQTyVars"
kcLHsTyVarBndrs :: Bool -- True <=> bump the TcLevel when bringing vars into scope
......
......@@ -8893,14 +8893,8 @@ example, consider ::
data Proxy a -- Proxy :: forall k. k -> Type
data X (a :: Proxy k)
 
According to the rules above ``X`` has a CUSK. Yet, what is the kind of ``k``?
It is impossible to know. This code is thus rejected as masquerading as having
a CUSK, but not really. If you wish ``k`` to be polykinded, it is straightforward
to specify this: ::
data X (a :: Proxy (k1 :: k2))
The above definition is indeed fully fixed, with no masquerade.
According to the rules above ``X`` has a CUSK. Yet, the kind of ``k`` is undetermined.
It is thus quantified over, giving ``X`` the kind ``forall k1 (k :: k1). Proxy k -> Type``.
 
Kind inference in closed type families
--------------------------------------
......
......@@ -12,3 +12,5 @@ data S :: forall k. Proxy k -> Type where
data T (a :: b) :: forall c (d :: Type) e.
(forall f. Proxy f) -> Proxy c -> Proxy d -> Proxy e
-> Type where
-- NB: This was originally a failing test, but now that we have #15273, it works!
......@@ -282,3 +282,4 @@ test('T14680', normal, compile, [''])
test('T15057', normal, compile, [''])
test('T15144', normal, compile, [''])
test('T15122', normal, compile, [''])
test('T13777', normal, compile, [''])
T13777.hs:9:1: error:
You have written a *complete user-suppled kind signature*,
but the following variable is undetermined: k0 :: *
Perhaps add a kind signature.
Inferred result kind: forall (k :: k0). Proxy k -> *
T13777.hs:12:1: error:
You have written a *complete user-suppled kind signature*,
but the following variables are undetermined:
k0 :: *
k1 :: *
k2 :: *
Perhaps add a kind signature.
Inferred kinds of user-written variables:
b :: *
a :: b
Inferred result kind:
forall (c :: k2) d (e :: k1).
(forall (f :: k0). Proxy f) -> Proxy c -> Proxy d -> Proxy e -> *
......@@ -134,7 +134,6 @@ test('T7102', [ expect_broken(7102) ], ghci_script, ['T7102.script'])
test('T7102a', normal, ghci_script, ['T7102a.script'])
test('T13271', normal, compile_fail, [''])
test('T13674', normal, compile_fail, [''])
test('T13777', normal, compile_fail, [''])
test('T13784', normal, compile_fail, [''])
test('T13877', normal, compile_fail, [''])
test('T13972', normal, compile_fail, [''])
......
T11648b.hs:7:1: error:
You have written a *complete user-suppled kind signature*,
but the following variable is undetermined: k0 :: *
Perhaps add a kind signature.
Inferred kinds of user-written variables:
k :: k0
a :: Proxy k
Inferred result kind: *
T6039.hs:5:1: error:
You have written a *complete user-suppled kind signature*,
but the following variable is undetermined: k0 :: *
Perhaps add a kind signature.
Inferred kinds of user-written variables:
j :: k0 -> *
k :: k0
a :: j k
Inferred result kind: *
......@@ -37,7 +37,7 @@ test('T6035', normal, compile, [''])
test('T6036', normal, compile, [''])
test('T6025', normal, run_command, ['$MAKE -s --no-print-directory T6025'])
test('T6002', normal, compile, [''])
test('T6039', normal, compile_fail, [''])
test('T6039', normal, compile, [''])
test('T6021', normal, compile, [''])
test('T6020a', normal, compile, [''])
test('T6044', normal, compile, [''])
......@@ -143,7 +143,7 @@ test('T11399', normal, compile_fail, [''])
test('T11611', normal, compile_fail, [''])
test('T11616', normal, compile, [''])
test('T11648', normal, compile, [''])
test('T11648b', normal, compile_fail, [''])
test('T11648b', normal, compile, [''])
test('KindVType', normal, compile_fail, [''])
test('T11821', normal, compile, [''])
test('T11821a', normal, compile_fail, [''])
......
T14904a.hs:8:1: error:
You have written a *complete user-suppled kind signature*,
but the following variable is undetermined: k0 :: *
Perhaps add a kind signature.
Inferred kinds of user-written variables:
g :: k0 -> *
f :: forall (a :: k0). g a
Inferred result kind: *
T14904a.hs:9:6: error:
• Expected kind ‘forall (a :: k1). g a’, but ‘f’ has kind ‘k0’
• In the first argument of ‘F’, namely ‘(f :: forall a. g a)’
......
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