Quantify unfixed kind variables in CUSKs
authorRichard Eisenberg <rae@cs.brynmawr.edu>
Thu, 14 Jun 2018 12:50:06 +0000 (08:50 -0400)
committerRichard Eisenberg <rae@cs.brynmawr.edu>
Sat, 16 Jun 2018 01:32:53 +0000 (21:32 -0400)
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

compiler/typecheck/TcHsType.hs
docs/users_guide/glasgow_exts.rst
testsuite/tests/indexed-types/should_compile/T13777.hs [moved from testsuite/tests/indexed-types/should_fail/T13777.hs with 80% similarity]
testsuite/tests/indexed-types/should_compile/all.T
testsuite/tests/indexed-types/should_fail/T13777.stderr [deleted file]
testsuite/tests/indexed-types/should_fail/all.T
testsuite/tests/polykinds/T11648b.stderr [deleted file]
testsuite/tests/polykinds/T6039.stderr [deleted file]
testsuite/tests/polykinds/all.T
testsuite/tests/typecheck/should_fail/T14904a.stderr

index f29dce9..0647ca4 100644 (file)
@@ -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
index 952b16c..466584a 100644 (file)
@@ -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!
index 5a6ae27..c58424f 100644 (file)
@@ -282,3 +282,4 @@ test('T14680', normal, compile, [''])
 test('T15057', normal, compile, [''])
 test('T15144', normal, compile, [''])
 test('T15122', normal, compile, [''])
+test('T13777', normal, compile, [''])
diff --git a/testsuite/tests/indexed-types/should_fail/T13777.stderr b/testsuite/tests/indexed-types/should_fail/T13777.stderr
deleted file mode 100644 (file)
index b920991..0000000
+++ /dev/null
@@ -1,20 +0,0 @@
-
-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 -> *
index f69bce8..ef5eee2 100644 (file)
@@ -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, [''])
diff --git a/testsuite/tests/polykinds/T11648b.stderr b/testsuite/tests/polykinds/T11648b.stderr
deleted file mode 100644 (file)
index cbe9263..0000000
+++ /dev/null
@@ -1,9 +0,0 @@
-
-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: *
diff --git a/testsuite/tests/polykinds/T6039.stderr b/testsuite/tests/polykinds/T6039.stderr
deleted file mode 100644 (file)
index bcaa2e1..0000000
+++ /dev/null
@@ -1,10 +0,0 @@
-
-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: *
index c3250b7..425e57a 100644 (file)
@@ -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, [''])
index 603ecb5..ea92de3 100644 (file)
@@ -1,13 +1,4 @@
 
-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)’