Fix generalisation for type constructors
authorSimon Peyton Jones <simonpj@microsoft.com>
Thu, 25 Oct 2018 14:16:19 +0000 (15:16 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Fri, 26 Oct 2018 11:05:43 +0000 (12:05 +0100)
Fixing the way that we close-over-kinds when taking the
free vars of a type revealed that the way we generalise
type constructors was a bit wrong.

This fixes it.  See TcTyClDecls
Note [Generalisation for type constructors]

compiler/typecheck/TcTyClsDecls.hs
compiler/typecheck/TcValidity.hs

index 20c79bd..49c6082 100644 (file)
@@ -398,8 +398,7 @@ like this:
   data T a k = MkT (Proxy (a :: k))
 
 Clearly, the k has to come first. Checking for this problem must come before
-kind generalisation, as described in Note [Bad telescopes] in
-TcValidity.
+kind generalisation, as described in Note [Generalisation for type constructors]
 
 However, we have to check again *after* kind generalisation, to catch something
 like this:
@@ -555,13 +554,16 @@ kcTyClGroup decls
            ; tc_res_kind <- zonkTcType (tyConResKind tc)
            ; let scoped_tvs  = tcTyConScopedTyVars tc
                  user_tyvars = tcTyConUserTyVars tc
+                 tc_tyvars   = binderVars tc_binders
 
               -- See Note [checkValidDependency]
            ; checkValidDependency tc_binders tc_res_kind
 
-               -- See Note [Bad telescopes] in TcValidity
-           ; checkValidTelescope tc_binders user_tyvars empty
-           ; kvs <- kindGeneralize (mkTyConKind tc_binders tc_res_kind)
+           -- See Note [Generalisation for type constructors]
+           ; let kvs_to_gen = tyCoVarsOfTypesDSet (tc_res_kind : map tyVarKind tc_tyvars)
+                              `delDVarSetList` tc_tyvars
+                 dvs = DV { dv_kvs = kvs_to_gen, dv_tvs = emptyDVarSet }
+           ; kvs <- quantifyTyVars emptyVarSet dvs
 
            -- See Note [Work out final tyConBinders]
            ; scoped_tvs' <- zonkTyVarTyVarPairs scoped_tvs
@@ -576,8 +578,7 @@ kcTyClGroup decls
            ; tc_res_kind'        <- zonkTcTypeToTypeX env tc_res_kind
 
              -- See Note [Check telescope again during generalisation]
-           ; let extra = text "NB: Implicitly declared variables come before others."
-           ; checkValidTelescope all_binders user_tyvars extra
+           ; checkValidTelescope all_binders user_tyvars
 
                       -- Make sure tc_kind' has the final, zonked kind variables
            ; traceTc "Generalise kind" $
@@ -590,6 +591,49 @@ kcTyClGroup decls
                                scoped_tvs'
                                (tyConFlavour tc)) }
 
+{- Note [Generalisation for type constructors]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider test T14066g:
+  data SameKind :: k -> k -> Type
+
+We find that the Specified variable has kind (c :: a). We always
+put Specified variables before Required ones, so we should reject.
+
+
+Now that we can mix type and kind variables, there are an awful lot of
+ways to shoot yourself in the foot. Here are some.
+
+data SameKind :: k -> k -> *   -- just to force unification
+
+1.  data T1 a k (b :: k) (x :: SameKind a b)
+
+    The problem here is that we discover that a and b should have the same
+    kind. But this kind mentions k, which is bound *after* a.
+    (Testcase: dependent/should_fail/BadTelescope)
+
+2.  data Q a (b :: a) (d :: SameKind c b)
+
+    Note that c is not bound; it is Specified, not Required.  Yet its
+    kind mentions a. Because we have a nice rule that all Specified
+    variables come before Required ones this is bogus. (We could
+    probably figure out to put c between a and b.  But I think this is
+    doing users a disservice, in the long run.)  (Testcase:
+    dependent/should_fail/BadTelescope4)
+
+    So, when finding the free vars to generalise, we should look at the
+    kinds of all Q's binders, plus its result kind, and delete Q's
+    binders, leaving just {c}.  We should NOT try to short-cut by taking
+    the free vars of the half-baked kind
+      (forall a. a -> SameKind c b -> *)
+    because since 'c' is free we also think 'a' (another 'a'!) is
+    free in that kind.
+
+To catch these dependency errors, we call checkValidTelescope during
+kind-checking datatype declarations.
+
+See Note [Keeping scoped variables in order: Explicit] for how this
+check works for `forall x y z.` written in a type.
+-}
 
 {- Note [Work out final tyConBinders]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
index 392c254..936eed8 100644 (file)
@@ -2062,38 +2062,6 @@ famPatErr fam_tc tvs pats
    Telescope checking
 *                                                                      *
 ************************************************************************
-
-Note [Bad telescopes]
-~~~~~~~~~~~~~~~~~~~~~
-Now that we can mix type and kind variables, there are an awful lot of
-ways to shoot yourself in the foot. Here are some.
-
-  data SameKind :: k -> k -> *   -- just to force unification
-
-1.  data T1 a k (b :: k) (x :: SameKind a b)
-
-The problem here is that we discover that a and b should have the same
-kind. But this kind mentions k, which is bound *after* a.
-(Testcase: dependent/should_fail/BadTelescope)
-
-2.  data T2 a (c :: Proxy b) (d :: Proxy a) (x :: SameKind b d)
-
-Note that b is not bound. Yet its kind mentions a. Because we have
-a nice rule that all implicitly bound variables come before others,
-this is bogus. (We could probably figure out to put b between a and c.
-But I think this is doing users a disservice, in the long run.)
-(Testcase: dependent/should_fail/BadTelescope4)
-
-To catch these errors, we call checkValidTelescope during kind-checking
-datatype declarations. This must be done *before* kind-generalization,
-because kind-generalization might observe, say, T1, see that k is free
-in a's kind, and generalize over it, producing nonsense. It also must
-be done *after* kind-generalization, in order to catch the T2 case, which
-becomes apparent only after generalizing.
-
-Note [Keeping scoped variables in order: Explicit] discusses how this
-check works for `forall x y z.` written in a type.
-
 -}
 
 -- | Check a list of binders to see if they make a valid telescope.
@@ -2104,35 +2072,45 @@ check works for `forall x y z.` written in a type.
 -- because k isn't in scope when a is bound. This check has to come before
 -- general validity checking, because once we kind-generalise, this sort
 -- of problem is harder to spot (as we'll generalise over the unbound
--- k in a's type.) See also Note [Bad telescopes].
+-- k in a's type.)
+--
+-- See Note [Generalisation for type constructors] in TcTyClsDecls for
+--     data type declarations
+-- and Note [Keeping scoped variables in order: Explicit] in TcHsType
+--     for foralls
 checkValidTelescope :: [TyConBinder]   -- explicit vars (zonked)
                     -> SDoc            -- original, user-written telescope
-                    -> SDoc            -- extra text to print
                     -> TcM ()
-checkValidTelescope tvbs user_tyvars extra
-  = do { let tvs      = binderVars tvbs
-
-             (_, sorted_tidied_tvs) = tidyVarBndrs emptyTidyEnv $
-                                      toposortTyVars tvs
-       ; unless (go [] emptyVarSet (binderVars tvbs)) $
-         addErr $
-         vcat [ hang (text "These kind and type variables:" <+> user_tyvars $$
-                      text "are out of dependency order. Perhaps try this ordering:")
-                   2 (pprTyVars sorted_tidied_tvs)
-              , extra ] }
-
+checkValidTelescope tvbs user_tyvars
+  = unless (null bad_tvbs) $ addErr $
+    vcat [ hang (text "These kind and type variables:" <+> user_tyvars $$
+                 text "are out of dependency order. Perhaps try this ordering:")
+              2 (pprTyVars sorted_tidied_tvs)
+         , extra ]
   where
-    go :: [TyVar]  -- misplaced variables
-       -> TyVarSet -> [TyVar] -> Bool
-    go errs in_scope [] = null (filter (`elemVarSet` in_scope) errs)
-        -- report an error only when the variable in the kind is brought
-        -- into scope later in the telescope. Otherwise, we'll just quantify
-        -- over it in kindGeneralize, as we should.
-
-    go errs in_scope  (tv:tvs)
-      = let bad_tvs = filterOut (`elemVarSet` in_scope) $
-                      tyCoVarsOfTypeList (tyVarKind tv)
-        in go (bad_tvs ++ errs) (in_scope `extendVarSet` tv) tvs
+    tvs = binderVars tvbs
+    (_, sorted_tidied_tvs) = tidyVarBndrs emptyTidyEnv (toposortTyVars tvs)
+
+    (_, bad_tvbs) = foldl add_one (mkVarSet tvs, []) tvbs
+
+    add_one :: (TyVarSet, [TyConBinder])
+            -> TyConBinder
+            -> (TyVarSet, [TyConBinder])
+    add_one (bad_bndrs, acc) tvb
+      | fkvs `intersectsVarSet` bad_bndrs
+      = (bad', tvb : acc)
+      | otherwise
+      = (bad', acc)
+      where
+        tv = binderVar tvb
+        fkvs = tyCoVarsOfType (tyVarKind tv)
+        bad' = bad_bndrs `delVarSet` tv
+
+    extra | all (isVisibleArgFlag . tyConBinderArgFlag) bad_tvbs
+          = empty
+          | otherwise
+          = text "NB: Implicitly declared variables come before others."
+
 
 {-
 ************************************************************************