Kind variables in RHS of an associated type instances should be bound on LHS
authorSimon Peyton Jones <simonpj@microsoft.com>
Fri, 28 Nov 2014 17:23:08 +0000 (17:23 +0000)
committerSimon Peyton Jones <simonpj@microsoft.com>
Fri, 28 Nov 2014 17:36:14 +0000 (17:36 +0000)
This patche fixes Trac #9574.

The previous Note [Renaming associated types] in RnTypes appears to me to be wrong;
it confused class and instance declarations.

I have:

 * Treated kind and type variables uniformly. Both must be bound on the LHS
   of an associated type instance.  Eg
       instance C ('KProxy :: KProxy o) where
          type F 'KProxy = NatTr (Proxy :: o -> *)
   is illegal because 'o' is not bound on the LHS of the instance.

 * Moved the Note to RnSource and fixed it up

This improves the error message from T7938. However it made the code in
T6118 incorrect. We had:
  instance SingE (a :: Maybe k) where
    type Demote a = Maybe (Demote (Any :: k))
and that is now rejected, rightly I think.

compiler/rename/RnSource.lhs
compiler/rename/RnTypes.lhs
compiler/typecheck/TcInstDcls.lhs
testsuite/tests/indexed-types/should_fail/T5515.stderr
testsuite/tests/indexed-types/should_fail/T7938.stderr
testsuite/tests/polykinds/T6118.hs
testsuite/tests/polykinds/T9574.hs [new file with mode: 0644]
testsuite/tests/polykinds/T9574.stderr [new file with mode: 0644]
testsuite/tests/polykinds/all.T

index 80db79a..5cf6b73 100644 (file)
@@ -545,10 +545,13 @@ rnFamInstDecl doc mb_cls tycon pats payload rnPayload
                     ; (payload', rhs_fvs) <- rnPayload doc payload
 
                          -- See Note [Renaming associated types]
-                    ; let bad_tvs = case mb_cls of
-                                      Nothing          -> []
-                                      Just (_,cls_tvs) -> filter is_bad cls_tvs
-                          is_bad tv = not (tv `elem` tv_names) && tv `elemNameSet` rhs_fvs
+                    ; let lhs_names = mkNameSet kv_names `unionNameSets` mkNameSet tv_names
+                          bad_tvs = case mb_cls of
+                                      Nothing           -> []
+                                      Just (_,cls_tkvs) -> filter is_bad cls_tkvs
+
+                          is_bad cls_tkv = cls_tkv `elemNameSet` rhs_fvs
+                                        && not (cls_tkv `elemNameSet` lhs_names)
 
                     ; unless (null bad_tvs) (badAssocRhs bad_tvs)
                     ; return ((pats', payload'), rhs_fvs `plusFV` pat_fvs) }
@@ -635,18 +638,45 @@ rnATInstDecls :: (Maybe (Name, [Name]) ->    -- The function that renames
 rnATInstDecls rnFun cls hs_tvs at_insts
   = rnList (rnFun (Just (cls, tv_ns))) at_insts
   where
-    tv_ns = hsLTyVarNames hs_tvs
-    -- Type variable binders (but NOT kind variables)
-    -- See Note [Renaming associated types] in RnTypes
+    tv_ns = hsLKiTyVarNames hs_tvs
+    -- See Note [Renaming associated types]
 \end{code}
 
-For the method bindings in class and instance decls, we extend the
-type variable environment iff -fglasgow-exts
+Note [Renaming associated types]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Check that the RHS of the decl mentions only type variables
+bound on the LHS.  For example, this is not ok
+   class C a b where
+      type F a x :: *
+   instance C (p,q) r where
+      type F (p,q) x = (x, r)   -- BAD: mentions 'r'
+c.f. Trac #5515
+
+The same thing applies to kind variables, of course (Trac #7938, #9574):
+   class Funct f where
+      type Codomain f :: *
+   instance Funct ('KProxy :: KProxy o) where
+      type Codomain 'KProxy = NatTr (Proxy :: o -> *)
+Here 'o' is mentioned on the RHS of the Codomain function, but
+not on the LHS.
+
+All this applies only for *instance* declarations.  In *class*
+declarations there is no RHS to worry about, and the class variables
+can all be in scope (Trac #5862):
+    class Category (x :: k -> k -> *) where
+      type Ob x :: k -> Constraint
+      id :: Ob x a => x a a
+      (.) :: (Ob x a, Ob x b, Ob x c) => x b c -> x a b -> x a c
+Here 'k' is in scope in the kind signature, just like 'x'.
+
 
 \begin{code}
 extendTyVarEnvForMethodBinds :: [Name]
                              -> RnM (LHsBinds Name, FreeVars)
                              -> RnM (LHsBinds Name, FreeVars)
+-- For the method bindings in class and instance decls, we extend
+-- the type variable environment iff -XScopedTypeVariables
+
 extendTyVarEnvForMethodBinds ktv_names thing_inside
   = do  { scoped_tvs <- xoptM Opt_ScopedTypeVariables
         ; if scoped_tvs then
@@ -991,7 +1021,7 @@ rnTyClDecl (ClassDecl {tcdCtxt = context, tcdLName = lcls,
              { (context', cxt_fvs) <- rnContext cls_doc context
              ; fds'  <- rnFds fds
                          -- The fundeps have no free variables
-             ; (ats',     fv_ats)     <- rnATDecls cls' ats
+             ; (ats',   fv_ats) <- rnATDecls cls' ats
              ; (sigs', sig_fvs) <- renameSigs (ClsDeclCtxt cls') sigs
              ; let fvs = cxt_fvs     `plusFV`
                          sig_fvs     `plusFV`
@@ -1260,8 +1290,7 @@ modules), we get better error messages, too.
 ---------------
 badAssocRhs :: [Name] -> RnM ()
 badAssocRhs ns
-  = addErr (hang (ptext (sLit "The RHS of an associated type declaration mentions type variable")
-                  <> plural ns
+  = addErr (hang (ptext (sLit "The RHS of an associated type declaration mentions")
                   <+> pprWithCommas (quotes . ppr) ns)
                2 (ptext (sLit "All such variables must be bound on the LHS")))
 
index c3692d3..e0df3ec 100644 (file)
@@ -504,31 +504,6 @@ dataKindsErr is_type thing
          | otherwise = ptext (sLit "kind")
 \end{code}
 
-Note [Renaming associated types]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Check that the RHS of the decl mentions only type variables
-bound on the LHS.  For example, this is not ok
-   class C a b where
-      type F a x :: *
-   instance C (p,q) r where
-      type F (p,q) x = (x, r)   -- BAD: mentions 'r'
-c.f. Trac #5515
-
-What makes it tricky is that the *kind* variable from the class *are*
-in scope (Trac #5862):
-    class Category (x :: k -> k -> *) where
-      type Ob x :: k -> Constraint
-      id :: Ob x a => x a a
-      (.) :: (Ob x a, Ob x b, Ob x c) => x b c -> x a b -> x a c
-Here 'k' is in scope in the kind signature even though it's not
-explicitly mentioned on the LHS of the type Ob declaration.
-
-We could force you to mention k explicitly, thus
-    class Category (x :: k -> k -> *) where
-      type Ob (x :: k -> k -> *) :: k -> Constraint
-but it seems tiresome to do so.
-
-
 %*********************************************************
 %*                                                      *
 \subsection{Contexts and predicates}
index 53411ce..abfe225 100644 (file)
@@ -525,8 +525,8 @@ tcClsInstDecl (L loc (ClsInstDecl { cid_poly_ty = poly_ty, cid_binds = binds
 
         -- Next, process any associated types.
         ; traceTc "tcLocalInstDecl" (ppr poly_ty)
-        ; tyfam_insts0 <- tcExtendTyVarEnv tyvars $
-                          mapAndRecoverM (tcAssocTyDecl clas mini_env) ats
+        ; tyfam_insts0  <- tcExtendTyVarEnv tyvars $
+                           mapAndRecoverM (tcTyFamInstDecl mb_info) ats
         ; datafam_insts <- tcExtendTyVarEnv tyvars $
                            mapAndRecoverM (tcDataFamInstDecl mb_info) adts
 
@@ -595,16 +595,6 @@ tcATDefault inst_subst defined_ats (ATI fam_tc defs)
       = (extendTvSubst subst tc_tv ty', ty')
       where
         ty' = mkTyVarTy (updateTyVarKind (substTy subst) tc_tv)
-
-
---------------
-tcAssocTyDecl :: Class                   -- Class of associated type
-              -> VarEnv Type             -- Instantiation of class TyVars
-              -> LTyFamInstDecl Name
-              -> TcM (FamInst)
-tcAssocTyDecl clas mini_env ldecl
-  = do { fam_inst <- tcTyFamInstDecl (Just (clas, mini_env)) ldecl
-       ; return fam_inst }
 \end{code}
 
 %************************************************************************
index 463a30b..25fbe9f 100644 (file)
@@ -1,8 +1,8 @@
 
 T5515.hs:9:3:
-    The RHS of an associated type declaration mentions type variable ‘a’
+    The RHS of an associated type declaration mentions ‘a’
       All such variables must be bound on the LHS
 
 T5515.hs:15:3:
-    The RHS of an associated type declaration mentions type variable ‘a’
+    The RHS of an associated type declaration mentions ‘a’
       All such variables must be bound on the LHS
index a6aeb8a..a9b5aef 100644 (file)
@@ -1,6 +1,4 @@
 
-T7938.hs:12:16:
-    Expected kind ‘*’, but ‘KP’ 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)’
+T7938.hs:12:3:
+    The RHS of an associated type declaration mentions ‘k2’
+      All such variables must be bound on the LHS
index df510ff..aaa78e7 100644 (file)
@@ -17,7 +17,7 @@ instance SingE (a :: Nat) where
   type Demote a = Nat
 
 instance SingE (a :: Maybe k) where
-  type Demote a = Maybe (Demote (Any :: k))
+  type Demote (a :: Maybe k) = Maybe (Demote (Any :: k))
 
 instance SingE (a :: List k) where
-  type Demote (a :: List k) = List (Demote (Any :: k))
\ No newline at end of file
+  type Demote (a :: List k) = List (Demote (Any :: k))
diff --git a/testsuite/tests/polykinds/T9574.hs b/testsuite/tests/polykinds/T9574.hs
new file mode 100644 (file)
index 0000000..e806e2a
--- /dev/null
@@ -0,0 +1,18 @@
+{-# LANGUAGE PolyKinds, DataKinds, TypeFamilies, ScopedTypeVariables, GADTs, RankNTypes #-}
+module T9574 where
+
+data KProxy (t :: *) = KProxy
+data Proxy p
+
+class Funct f where
+    type Codomain f :: *
+
+instance Funct ('KProxy :: KProxy o) where
+    type Codomain 'KProxy = NatTr (Proxy :: o -> *)
+
+data NatTr (c :: o -> *) where
+    M :: (forall (a :: o). Proxy a) -> NatTr (c :: o -> *)
+
+p :: forall (c :: o -> *). NatTr c
+p = M t where
+    M t = undefined :: Codomain ('KProxy :: KProxy o)
diff --git a/testsuite/tests/polykinds/T9574.stderr b/testsuite/tests/polykinds/T9574.stderr
new file mode 100644 (file)
index 0000000..50b42ad
--- /dev/null
@@ -0,0 +1,4 @@
+
+T9574.hs:11:5:
+    The RHS of an associated type declaration mentions ‘o’
+      All such variables must be bound on the LHS
index 3f17c68..19a194e 100644 (file)
@@ -111,3 +111,4 @@ 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, [''])