Tighten checking for associated type instances
authorSimon Peyton Jones <simonpj@microsoft.com>
Mon, 18 Apr 2016 14:14:40 +0000 (15:14 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Tue, 19 Apr 2016 07:38:47 +0000 (08:38 +0100)
This patch finishes off Trac #11450.  Following debate on that ticket,
the patch tightens up the rules for what the instances of an
associated type can look like.  Now they must match the instance
header exactly. Eg

   class C a b where
    type T a x b

With this class decl, if we have an instance decl
  instance C ty1 ty2 where ...
then the type instance must look like
     type T ty1 v ty2 = ...
with exactly
  - 'ty1' for 'a'
  -  'ty2' for 'b', and
  - a variable for 'x'

For example:

  instance C [p] Int
    type T [p] y Int = (p,y,y)

Previously we allowed multiple instance equations and now, in effect,
we don't since they would all overlap.  If you want multiple cases,
use an auxiliary type family.

This is consistent with the treatment of generic-default instances,
and the user manual always said "WARNING: this facility (multiple
instance equations may be withdrawn in the future".

I also improved error messages, and did other minor refactoring.

24 files changed:
compiler/rename/RnSource.hs
compiler/typecheck/TcDeriv.hs
compiler/typecheck/TcInstDcls.hs
compiler/typecheck/TcTyClsDecls.hs
compiler/typecheck/TcValidity.hs
compiler/types/Type.hs
docs/users_guide/glasgow_exts.rst
testsuite/tests/ghci/scripts/T4175.hs
testsuite/tests/ghci/scripts/T4175.stdout
testsuite/tests/ghci/scripts/T6018ghcifail.stderr
testsuite/tests/indexed-types/should_compile/T10931.hs
testsuite/tests/indexed-types/should_fail/SimpleFail10.hs
testsuite/tests/indexed-types/should_fail/SimpleFail10.stderr [new file with mode: 0644]
testsuite/tests/indexed-types/should_fail/SimpleFail9.hs
testsuite/tests/indexed-types/should_fail/SimpleFail9.stderr [new file with mode: 0644]
testsuite/tests/indexed-types/should_fail/T11450.hs [new file with mode: 0644]
testsuite/tests/indexed-types/should_fail/T11450.stderr [new file with mode: 0644]
testsuite/tests/indexed-types/should_fail/all.T
testsuite/tests/polykinds/T10570.stderr
testsuite/tests/th/T9692.hs
testsuite/tests/th/T9692.stderr
testsuite/tests/typecheck/should_fail/T6018fail.hs
testsuite/tests/typecheck/should_fail/T6018fail.stderr
testsuite/tests/typecheck/should_fail/T6018failclosed.stderr

index ea7d036..af60b7c 100644 (file)
@@ -709,7 +709,10 @@ rnClsInstDecl (ClsInstDecl { cid_poly_ty = inst_ty, cid_binds = mbinds
              --     to remove the context).
 
 rnFamInstDecl :: HsDocContext
-              -> Maybe (Name, [Name])
+              -> Maybe (Name, [Name])   -- Nothing => not associated
+                                        -- Just (cls,tvs) => associated,
+                                        --   and gives class and tyvars of the
+                                        --   parent instance delc
               -> Located RdrName
               -> HsTyPats RdrName
               -> rhs
@@ -743,10 +746,17 @@ rnFamInstDecl doc mb_cls tycon (HsIB { hsib_body = pats }) payload rnPayload
                                    freeKiTyVarsAllVars pat_kity_vars_with_dups
                     ; tv_nms_dups <- mapM (lookupOccRn . unLoc) $
                                      [ tv | (tv:_:_) <- groups ]
-                          -- Add to the used variables any variables that
-                          -- appear *more than once* on the LHS
-                          -- e.g.   F a Int a = Bool
-                    ; let tv_nms_used = extendNameSetList rhs_fvs tv_nms_dups
+                          -- Add to the used variables
+                          --  a) any variables that appear *more than once* on the LHS
+                          --     e.g.   F a Int a = Bool
+                          --  b) for associated instances, the variables
+                          --     of the instance decl.  See
+                          --     Note [Unused type variables in family instances]
+                    ; let tv_nms_used = extendNameSetList rhs_fvs $
+                                        inst_tvs ++ tv_nms_dups
+                          inst_tvs = case mb_cls of
+                                       Nothing            -> []
+                                       Just (_, inst_tvs) -> inst_tvs
                     ; warnUnusedTypePatterns var_names tv_nms_used
 
                          -- See Note [Renaming associated types]
@@ -757,8 +767,8 @@ rnFamInstDecl doc mb_cls tycon (HsIB { hsib_body = pats }) payload rnPayload
 
                           is_bad cls_tkv = cls_tkv `elemNameSet` rhs_fvs
                                         && not (cls_tkv `elemNameSet` var_name_set)
-
                     ; unless (null bad_tvs) (badAssocRhs bad_tvs)
+
                     ; return ((pats', payload'), rhs_fvs `plusFV` pat_fvs) }
 
        ; let anon_wcs = concatMap collectAnonWildCards pats'
@@ -872,15 +882,25 @@ fresh meta-variables whereas the former generate fresh skolems.
 
 Note [Unused type variables in family instances]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-When the flag -fwarn-unused-type-patterns is on, the compiler reports warnings
-about unused type variables. (rnFamInstDecl) A type variable is considered
-used
- * when it is either occurs on the RHS of the family instance, or
+When the flag -fwarn-unused-type-patterns is on, the compiler reports
+warnings about unused type variables in type-family instances. A
+tpye variable is considered used (i.e. cannot be turned into a wildcard)
+when
+
+ * it occurs on the RHS of the family instance
    e.g.   type instance F a b = a    -- a is used on the RHS
 
  * it occurs multiple times in the patterns on the LHS
    e.g.   type instance F a a = Int  -- a appears more than once on LHS
 
+ * it is one of the instance-decl variables, for associated types
+   e.g.   instance C (a,b) where
+            type T (a,b) = a
+   Here the type pattern in the type instance must be the same as that
+   for the class instance, so
+            type T (a,_) = a
+   would be rejected.  So we should not complain about an unused variable b
+
 As usual, the warnings are not reported for for type variables with names
 beginning with an underscore.
 
index d88686f..4d20a4a 100644 (file)
@@ -19,7 +19,7 @@ import DynFlags
 import TcRnMonad
 import FamInst
 import TcErrors( reportAllUnsolved )
-import TcValidity( validDerivPred )
+import TcValidity( validDerivPred, allDistinctTyVars )
 import TcClassDcl( tcATDefault, tcMkDeclCtxt )
 import TcEnv
 import TcGenDeriv                       -- Deriv stuff
@@ -639,11 +639,6 @@ deriveTyData tvs tc tc_args deriv_pred
               (tc_args_to_keep, args_to_drop)
                               = splitAt n_args_to_keep tc_args
               inst_ty_kind    = typeKind (mkTyConApp tc tc_args_to_keep)
-              -- Use exactTyCoVarsOfTypes, not tyCoVarsOfTypes, so that we
-              -- don't mistakenly grab a type variable mentioned in a type
-              -- synonym that drops it.
-              -- See Note [Eta-reducing type synonyms].
-              dropped_tvs     = exactTyCoVarsOfTypes args_to_drop
 
               -- Match up the kinds, and apply the resulting kind substitution
               -- to the types.  See Note [Unify kinds in deriving]
@@ -672,8 +667,7 @@ deriveTyData tvs tc tc_args deriv_pred
 
         ; traceTc "derivTyData2" (vcat [ ppr tkvs ])
 
-        ; checkTc (allDistinctTyVars args_to_drop &&              -- (a) and (b)
-                   not (any (`elemVarSet` dropped_tvs) tkvs))     -- (c)
+        ; checkTc (allDistinctTyVars (mkVarSet tkvs) args_to_drop)     -- (a, b, c)
                   (derivingEtaErr cls final_cls_tys (mkTyConApp tc final_tc_args))
                 -- Check that
                 --  (a) The args to drop are all type variables; eg reject:
@@ -822,6 +816,12 @@ where this was first noticed).
 For this reason, we call exactTyCoVarsOfTypes on the eta-reduced types so that
 we only consider the type variables that remain after expanding through type
 synonyms.
+
+              -- Use exactTyCoVarsOfTypes, not tyCoVarsOfTypes, so that we
+              -- don't mistakenly grab a type variable mentioned in a type
+              -- synonym that drops it.
+              -- See Note [Eta-reducing type synonyms].
+              dropped_tvs     = exactTyCoVarsOfTypes args_to_drop
 -}
 
 mkEqnHelp :: Maybe OverlapMode
index 1e34fc6..bd26e6e 100644 (file)
@@ -531,7 +531,7 @@ tcClsInstDecl (L loc (ClsInstDecl { cid_poly_ty = poly_ty, cid_binds = binds
         ; (tyvars, theta, clas, inst_tys) <- tcHsClsInstType InstDeclCtxt poly_ty
         ; let mini_env   = mkVarEnv (classTyVars clas `zip` inst_tys)
               mini_subst = mkTvSubst (mkInScopeSet (mkVarSet tyvars)) mini_env
-              mb_info    = Just (clas, mini_env)
+              mb_info    = Just (clas, tyvars, mini_env)
 
         -- Next, process any associated types.
         ; traceTc "tcLocalInstDecl" (ppr poly_ty)
@@ -582,7 +582,7 @@ lot of kinding and type checking code with ordinary algebraic data types (and
 GADTs).
 -}
 
-tcFamInstDeclCombined :: Maybe ClsInfo
+tcFamInstDeclCombined :: Maybe ClsInstInfo
                       -> Located Name -> TcM TyCon
 tcFamInstDeclCombined mb_clsinfo fam_tc_lname
   = do { -- Type family instances require -XTypeFamilies
@@ -602,7 +602,7 @@ tcFamInstDeclCombined mb_clsinfo fam_tc_lname
 
        ; return fam_tc }
 
-tcTyFamInstDecl :: Maybe ClsInfo
+tcTyFamInstDecl :: Maybe ClsInstInfo
                 -> LTyFamInstDecl Name -> TcM FamInst
   -- "type instance"
 tcTyFamInstDecl mb_clsinfo (L loc decl@(TyFamInstDecl { tfid_eqn = eqn }))
@@ -627,7 +627,7 @@ tcTyFamInstDecl mb_clsinfo (L loc decl@(TyFamInstDecl { tfid_eqn = eqn }))
        ; let axiom = mkUnbranchedCoAxiom rep_tc_name fam_tc co_ax_branch
        ; newFamInst SynFamilyInst axiom }
 
-tcDataFamInstDecl :: Maybe ClsInfo
+tcDataFamInstDecl :: Maybe ClsInstInfo
                   -> LDataFamInstDecl Name -> TcM (FamInst, Maybe DerivInfo)
   -- "newtype instance" and "data instance"
 tcDataFamInstDecl mb_clsinfo
index 1325966..4d664f4 100644 (file)
@@ -1081,7 +1081,7 @@ kcTyFamInstEqn fam_tc_shape@(fam_tc_name,_,_,_)
          tc_fam_ty_pats fam_tc_shape Nothing -- not an associated type
                         pats (discardResult . (tcCheckLHsType hs_ty)) }
 
-tcTyFamInstEqn :: FamTyConShape -> Maybe ClsInfo -> LTyFamInstEqn Name -> TcM CoAxBranch
+tcTyFamInstEqn :: FamTyConShape -> Maybe ClsInstInfo -> LTyFamInstEqn Name -> TcM CoAxBranch
 -- Needs to be here, not in TcInstDcls, because closed families
 -- (typechecked here) have TyFamInstEqns
 tcTyFamInstEqn fam_tc_shape@(fam_tc_name,_,_,_) mb_clsinfo
@@ -1171,7 +1171,7 @@ famTyConShape fam_tc
     , tyConResKind fam_tc )
 
 tc_fam_ty_pats :: FamTyConShape
-               -> Maybe ClsInfo
+               -> Maybe ClsInstInfo
                -> HsTyPats Name       -- Patterns
                -> (TcKind -> TcM ())  -- Kind checker for RHS
                                       -- result is ignored
@@ -1194,7 +1194,7 @@ tc_fam_ty_pats (name, _, binders, res_kind) mb_clsinfo
          -- See Note [Quantifying over family patterns]
          (_, (insted_res_kind, typats)) <- tcImplicitTKBndrs tv_names $
          do { (insting_subst, _leftover_binders, args, leftovers, n)
-                <- tcInferArgs name binders (snd <$> mb_clsinfo) arg_pats
+                <- tcInferArgs name binders (thdOf3 <$> mb_clsinfo) arg_pats
             ; case leftovers of
                 hs_ty:_ -> addErrTc $ too_many_args hs_ty n
                 _       -> return ()
@@ -1214,7 +1214,7 @@ tc_fam_ty_pats (name, _, binders, res_kind) mb_clsinfo
 
 -- See Note [tc_fam_ty_pats vs tcFamTyPats]
 tcFamTyPats :: FamTyConShape
-            -> Maybe ClsInfo
+            -> Maybe ClsInstInfo
             -> HsTyPats Name          -- patterns
             -> (TcKind -> TcM ())    -- kind-checker for RHS
             -> (   [TyVar]           -- Kind and type variables
@@ -2352,6 +2352,8 @@ checkValidClass cls
     cls_arity = length $ filterOutInvisibleTyVars (classTyCon cls) tyvars
        -- Ignore invisible variables
     cls_tv_set = mkVarSet tyvars
+    mini_env   = zipVarEnv tyvars (mkTyVarTys tyvars)
+    mb_cls     = Just (cls, tyvars, mini_env)
 
     check_op constrained_class_methods (sel_id, dm)
       = setSrcSpan (getSrcSpan sel_id) $
@@ -2394,11 +2396,10 @@ checkValidClass cls
 
              -- Check that any default declarations for associated types are valid
            ; whenIsJust m_dflt_rhs $ \ (rhs, loc) ->
-             checkValidTyFamEqn (Just (cls, mini_env)) fam_tc
+             checkValidTyFamEqn mb_cls fam_tc
                                 fam_tvs [] (mkTyVarTys fam_tvs) rhs loc }
         where
           fam_tvs = tyConTyVars fam_tc
-    mini_env = zipVarEnv tyvars (mkTyVarTys tyvars)
 
     check_dm :: UserTypeCtxt -> DefMethInfo -> TcM ()
     -- Check validity of the /top-level/ generic-default type
index 1d5799c..e710c6e 100644 (file)
@@ -11,14 +11,17 @@ module TcValidity (
   checkValidTheta, checkValidFamPats,
   checkValidInstance, validDerivPred,
   checkInstTermination,
-  ClsInfo, checkValidCoAxiom, checkValidCoAxBranch,
+  ClsInstInfo, checkValidCoAxiom, checkValidCoAxBranch,
   checkValidTyFamEqn,
   arityErr, badATErr,
-  checkValidTelescope, checkZonkValidTelescope, checkValidInferredKinds
+  checkValidTelescope, checkZonkValidTelescope, checkValidInferredKinds,
+  allDistinctTyVars
   ) where
 
 #include "HsVersions.h"
 
+import Maybes
+
 -- friends:
 import TcUnify    ( tcSubType_NC )
 import TcSimplify ( simplifyAmbiguityCheck )
@@ -28,7 +31,6 @@ import TcMType
 import PrelNames
 import Type
 import Coercion
-import Unify( tcMatchTyX )
 import Kind
 import CoAxiom
 import Class
@@ -45,6 +47,7 @@ import FamInst     ( makeInjectivityErrors )
 import Name
 import VarEnv
 import VarSet
+import Var         ( mkTyVar )
 import ErrUtils
 import DynFlags
 import Util
@@ -53,10 +56,10 @@ import SrcLoc
 import Outputable
 import BasicTypes
 import Module
+import Unique      ( mkAlphaTyVarUnique )
 import qualified GHC.LanguageExtensions as LangExt
 
 import Control.Monad
-import Data.Maybe
 import Data.List        ( (\\) )
 
 {-
@@ -1316,14 +1319,58 @@ for (T ty Int) elsewhere, because it's an *associated* type.
 
 Note [Checking consistent instantiation]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+See Trac #11450 for background discussion on this check.
+
   class C a b where
     type T a x b
 
+With this class decl, if we have an instance decl
+  instance C ty1 ty2 where ...
+then the type instance must look like
+     type T ty1 v ty2 = ...
+with exactly 'ty1' for 'a', 'ty2' for 'b', and a variable for 'x'.
+For example:
+
   instance C [p] Int
-    type T [p] y Int = (p,y,y)  -- Induces the family instance TyCon
-                                --    type TR p y = (p,y,y)
+    type T [p] y Int = (p,y,y)
+
+Note that
 
-So we
+* We used to allow completely different bound variables in the
+  associated type instance; e.g.
+    instance C [p] Int
+      type T [q] y Int = ...
+  But from GHC 8.2 onwards, we don't.  It's much simpler this way.
+  See Trac #11450.
+
+* When the class variable isn't used on the RHS of the type instance,
+  it's tempting to allow wildcards, thus
+    instance C [p] Int
+      type T [_] y Int = (y,y)
+  But it's awkward to do the test, and it doesn't work if the
+  variable is repeated:
+    instance C (p,p) Int
+      type T (_,_) y Int = (y,y)
+  Even though 'p' is not used on the RHS, we still need to use 'p'
+  on the LHS to establish the repeated pattern.  So to keep it simple
+  we just require equality.
+
+* We also check that any non-class-tyvars are instantiated with
+  distinct tyvars.  That rules out
+    instance C [p] Int where
+      type T [p] Bool Int = p  -- Note Bool
+      type T [p] Char Int = p  -- Note Char
+
+  and
+     instance C [p] Int where
+      type T [p] p Int = p     -- Note repeated 'p' on LHS
+  It's consistent to do this because we don't allow this kind of
+  instantiation for the class-tyvar arguments of the family.
+
+  Overall, we can have exactly one type instance for each
+  associated type.  If you wantmore, use an auxiliary family.
+
+Implementation
   * Form the mini-envt from the class type variables a,b
     to the instance decl types [p],Int:   [a->[p], b->Int]
 
@@ -1333,30 +1380,8 @@ So we
   * Apply the mini-evnt to them, and check that the result is
     consistent with the instance types [p] y Int
 
-We do *not* assume (at this point) the the bound variables of
-the associated type instance decl are the same as for the parent
-instance decl. So, for example,
-
-  instance C [p] Int
-    type T [q] y Int = ...
-
-would work equally well. Reason: making the *kind* variables line
-up is much harder. Example (Trac #7282):
-  class Foo (xs :: [k]) where
-     type Bar xs :: *
-
-   instance Foo '[] where
-     type Bar '[] = Int
-Here the instance decl really looks like
-   instance Foo k ('[] k) where
-     type Bar k ('[] k) = Int
-but the k's are not scoped, and hence won't match Uniques.
-
-So instead we just match structure, with tcMatchTyX, and check
-that distinct type variables match 1-1 with distinct type variables.
-
-HOWEVER, we *still* make the instance type variables scope over the
-type instances, to pick up non-obvious kinds.  Eg
+We make all the instance type variables scope over the
+type instances, of course, which picks up non-obvious kinds.  Eg
    class Foo (a :: k) where
       type F a
    instance Foo (b :: k -> k) where
@@ -1367,13 +1392,28 @@ But if the 'b' didn't scope, we would make F's instance too
 poly-kinded.
 -}
 
--- | Extra information needed when type-checking associated types. The 'Class' is
--- the enclosing class, and the @VarEnv Type@ maps class variables to their
--- instance types.
-type ClsInfo       = (Class, VarEnv Type)
+-- | Extra information about the parent instance declaration, needed
+-- when type-checking associated types. The 'Class' is the enclosing
+-- class, the [TyVar] are the type variable of the instance decl,
+-- and and the @VarEnv Type@ maps class variables to their instance
+-- types.
+type ClsInstInfo = (Class, [TyVar], VarEnv Type)
+
+type AssocInstArgShape = (Maybe Type, Type)
+  -- AssocInstArgShape is used only for associated family instances
+  --    (mb_exp, actual)
+  -- mb_exp = Just ty  => this arg corresponds to a class variable
+  --        = Nothing  => it doesn't correspond to a class variable
+  -- e.g.  class C b where
+  --          type F a b c
+  --       instance C [x] where
+  --          type F p [x] q
+  -- We get [AssocInstArgShape] = [ (Nothing,  p)
+  --                              , (Just [x], [x])
+  --                              , (Nothing,  q)]
 
 checkConsistentFamInst
-               :: Maybe ClsInfo
+               :: Maybe ClsInstInfo
                -> TyCon              -- ^ Family tycon
                -> [TyVar]            -- ^ Type variables of the family instance
                -> [Type]             -- ^ Type patterns from instance
@@ -1381,84 +1421,72 @@ checkConsistentFamInst
 -- See Note [Checking consistent instantiation]
 
 checkConsistentFamInst Nothing _ _ _ = return ()
-checkConsistentFamInst (Just (clas, mini_env)) fam_tc at_tvs at_tys
+checkConsistentFamInst (Just (clas, inst_tvs, mini_env)) fam_tc _at_tvs at_tys
   = do { -- Check that the associated type indeed comes from this class
          checkTc (Just clas == tyConAssoc_maybe fam_tc)
                  (badATErr (className clas) (tyConName fam_tc))
 
-         -- See Note [Checking consistent instantiation]
-         -- Check right to left, so that we spot type variable
-         -- inconsistencies before (more confusing) kind variables
-       ; checkTc (check_args emptyTCvSubst (fam_tc_tvs `zip` at_tys))
-                 (wrongATArgErr fam_tc expected_args at_tys) }
-  where
-    fam_tc_tvs  = tyConTyVars fam_tc
-    expected_args = zipWith pick fam_tc_tvs at_tys
-    pick fam_tc_tv at_ty = case lookupVarEnv mini_env fam_tc_tv of
-                              Just inst_ty -> inst_ty
-                              Nothing      -> at_ty
-
-    check_args :: TCvSubst -> [(TyVar,Type)] -> Bool
-    check_args subst ((fam_tc_tv, at_ty) : rest)
-      | Just inst_ty <- lookupVarEnv mini_env fam_tc_tv
-      = case tcMatchTyX subst at_ty inst_ty of
-           Just subst -> check_args subst rest
-           Nothing    -> False
+       -- Check type args first (more comprehensible)
+       ; checkTc (all check_arg type_shapes)   pp_wrong_at_arg
+       ; checkTc (check_poly_args type_shapes) pp_wrong_at_tyvars
 
-      | otherwise
-      = check_args subst rest
-
-    check_args subst []
-      = check_tvs subst [] at_tvs
-
-    check_tvs :: TCvSubst -> [TyVar] -> [TyVar] -> Bool
-    check_tvs _     _   [] = True   -- OK!!
-    check_tvs subst acc (tv:tvs)
-       | Just ty <- lookupTyVar subst tv
-       = case tcGetTyVar_maybe ty of
-           Nothing -> False
-           Just tv' | tv' `elem` acc -> False
-                    | otherwise      -> check_tvs subst (tv' : acc) tvs
-       | otherwise
-       = check_tvs subst acc tvs
+       -- And now kind args
+       ; checkTc (all check_arg kind_shapes)
+                 (pp_wrong_at_arg $$ ppSuggestExplicitKinds)
+       ; checkTc (check_poly_args kind_shapes)
+                 (pp_wrong_at_tyvars $$ ppSuggestExplicitKinds)
 
-{-
-    check_arg :: (TyVar, Type) -> TCvSubst -> TcM TCvSubst
-    check_arg (fam_tc_tv, at_ty) subst
-      | Just inst_ty <- lookupVarEnv mini_env fam_tc_tv
-      = case tcMatchTyX subst at_ty inst_ty of
-           Just subst -> return subst
-           Nothing    -> failWithTc $ wrongATArgErr at_ty inst_ty
-                -- No need to instantiate here, because the axiom
-                -- uses the same type variables as the assocated class
-      | otherwise
-      = return subst   -- Allow non-type-variable instantiation
-                       -- See Note [Associated type instances]
-
-    check_distinct :: TCvSubst -> TcM ()
-    -- True if all the variables mapped the substitution
-    -- map to *distinct* type *variables*
-    check_distinct subst = go [] at_tvs
-       where
-         go _   []       = return ()
-         go acc (tv:tvs) = case lookupTyVar subst tv of
-                             Nothing -> go acc tvs
-                             Just ty | Just tv' <- tcGetTyVar_maybe ty
-                                     , tv' `notElem` acc
-                                     -> go (tv' : acc) tvs
-                             _other -> addErrTc (dupTyVar tv)
--}
+       ; traceTc "cfi" (vcat [ ppr inst_tvs
+                             , ppr arg_shapes
+                             , ppr mini_env ]) }
+  where
+    arg_shapes :: [AssocInstArgShape]
+    arg_shapes = [ (lookupVarEnv mini_env fam_tc_tv, at_ty)
+                 | (fam_tc_tv, at_ty) <- tyConTyVars fam_tc `zip` at_tys ]
+
+    (kind_shapes, type_shapes) = partitionInvisibles fam_tc snd arg_shapes
+
+    check_arg :: AssocInstArgShape -> Bool
+    check_arg (Just exp_ty, at_ty) = exp_ty `tcEqType` at_ty
+    check_arg (Nothing,     _    ) = True -- Arg position does not correspond
+                                          -- to a class variable
+    check_poly_args :: [(Maybe Type,Type)] -> Bool
+    check_poly_args arg_shapes
+      = allDistinctTyVars (mkVarSet inst_tvs)
+                          [ at_ty | (Nothing, at_ty) <- arg_shapes ]
+
+    pp_wrong_at_arg
+      = vcat [ text "Type indexes must match class instance head"
+             , pp_exp_act ]
+
+    pp_wrong_at_tyvars
+      = vcat [ text "Polymorphic type indexes of associated type" <+> quotes (ppr fam_tc)
+             , nest 2 $ vcat [ text "(i.e. ones independent of the class type variables)"
+                             , text "must be distinct type variables" ]
+             , pp_exp_act ]
+
+    pp_exp_act
+      = vcat [ text "Expected:" <+> ppr (mkTyConApp fam_tc expected_args)
+             , text "  Actual:" <+> ppr (mkTyConApp fam_tc at_tys)
+             , sdocWithDynFlags $ \dflags ->
+               ppWhen (has_poly_args dflags) $
+               vcat [ text "where the `<tv>' arguments are type variables,"
+                    , text "distinct from each other and from the instance variables" ] ]
+
+    expected_args = [ exp_ty `orElse` mk_tv at_ty | (exp_ty, at_ty) <- arg_shapes ]
+    mk_tv at_ty   = mkTyVarTy (mkTyVar tv_name (typeKind at_ty))
+    tv_name = mkInternalName (mkAlphaTyVarUnique 1) (mkTyVarOcc "<tv>") noSrcSpan
+
+    has_poly_args dflags = any (isNothing . fst) shapes
+      where
+        shapes | gopt Opt_PrintExplicitKinds dflags = arg_shapes
+               | otherwise                          = type_shapes
 
 badATErr :: Name -> Name -> SDoc
 badATErr clas op
   = hsep [text "Class", quotes (ppr clas),
           text "does not have an associated type", quotes (ppr op)]
 
-wrongATArgErr :: TyCon -> [Type] -> [Type] -> SDoc
-wrongATArgErr fam_tc expected_args actual_args
-  = vcat [ text "Type indexes must match class instance head"
-         , text "Expected:" <+> ppr (mkTyConApp fam_tc expected_args)
-         , text "Actual:  " <+> ppr (mkTyConApp fam_tc actual_args) ]
 
 {-
 ************************************************************************
@@ -1523,7 +1551,7 @@ checkValidCoAxiom ax@(CoAxiom { co_ax_tc = fam_tc, co_ax_branches = branches })
 -- Check that a "type instance" is well-formed (which includes decidability
 -- unless -XUndecidableInstances is given).
 --
-checkValidCoAxBranch :: Maybe ClsInfo
+checkValidCoAxBranch :: Maybe ClsInstInfo
                      -> TyCon -> CoAxBranch -> TcM ()
 checkValidCoAxBranch mb_clsinfo fam_tc
                     (CoAxBranch { cab_tvs = tvs, cab_cvs = cvs
@@ -1534,7 +1562,7 @@ checkValidCoAxBranch mb_clsinfo fam_tc
 -- | Do validity checks on a type family equation, including consistency
 -- with any enclosing class instance head, termination, and lack of
 -- polytypes.
-checkValidTyFamEqn :: Maybe ClsInfo
+checkValidTyFamEqn :: Maybe ClsInstInfo
                    -> TyCon   -- ^ of the type family
                    -> [TyVar] -- ^ bound tyvars in the equation
                    -> [CoVar] -- ^ bound covars in the equation
@@ -1583,7 +1611,7 @@ checkFamInstRhs lhsTys famInsts
         what    = text "type family application" <+> quotes (pprType (TyConApp tc tys))
         bad_tvs = fvTypes tys \\ fvs
 
-checkValidFamPats :: Maybe ClsInfo -> TyCon -> [TyVar] -> [CoVar] -> [Type] -> TcM ()
+checkValidFamPats :: Maybe ClsInstInfo -> TyCon -> [TyVar] -> [CoVar] -> [Type] -> TcM ()
 -- Patterns in a 'type instance' or 'data instance' decl should
 -- a) contain no type family applications
 --    (vanilla synonyms are fine, though)
@@ -1887,3 +1915,16 @@ isTerminatingClass cls
 -- | Tidy before printing a type
 ppr_tidy :: TidyEnv -> Type -> SDoc
 ppr_tidy env ty = pprType (tidyType env ty)
+
+allDistinctTyVars :: TyVarSet -> [KindOrType] -> Bool
+-- (allDistinctTyVars tvs tys) returns True if tys are
+-- a) all tyvars
+-- b) all distinct
+-- c) disjoint from tvs
+allDistinctTyVars _    [] = True
+allDistinctTyVars tkvs (ty : tys)
+  = case getTyVar_maybe ty of
+      Nothing -> False
+      Just tv | tv `elemVarSet` tkvs -> False
+              | otherwise -> allDistinctTyVars (tkvs `extendVarSet` tv) tys
+
index 7ad2013..9559123 100644 (file)
@@ -95,7 +95,6 @@ module Type (
         funTyCon,
 
         -- ** Predicates on types
-        allDistinctTyVars,
         isTyVarTy, isFunTy, isDictTy, isPredTy, isVoidTy, isCoercionTy,
         isCoercionTy_maybe, isCoercionType, isForAllTy,
         isPiTy,
@@ -121,7 +120,6 @@ module Type (
         tyCoVarsOfTypeDSet,
         coVarsOfType,
         coVarsOfTypes, closeOverKinds,
-        splitDepVarsOfType, splitDepVarsOfTypes,
         splitVisVarsOfType, splitVisVarsOfTypes,
         expandTypeSynonyms,
         typeSize,
@@ -585,16 +583,6 @@ repGetTyVar_maybe :: Type -> Maybe TyVar
 repGetTyVar_maybe (TyVarTy tv) = Just tv
 repGetTyVar_maybe _            = Nothing
 
-allDistinctTyVars :: [KindOrType] -> Bool
-allDistinctTyVars tkvs = go emptyVarSet tkvs
-  where
-    go _      [] = True
-    go so_far (ty : tys)
-       = case getTyVar_maybe ty of
-             Nothing -> False
-             Just tv | tv `elemVarSet` so_far -> False
-                     | otherwise -> go (so_far `extendVarSet` tv) tys
-
 {-
 ---------------------------------------------------------------------
                                 AppTy
index 4d238a5..b88cf44 100644 (file)
@@ -6466,33 +6466,56 @@ keyword in the family instance: ::
       type Elem [e] = e
       ...
 
-Note the following points:
+The data or type family instance for an assocated type must follow
+the following two rules:
 
 -  The type indexes corresponding to class parameters must have
-   precisely the same shape the type given in the instance head. To have
-   the same "shape" means that the two types are identical modulo
-   renaming of type variables. For example: ::
+   precisely the same as type given in the instance head.
+   For example: ::
+
+       class Collects ce where
+         type Elem ce :: *
 
        instance Eq (Elem [e]) => Collects [e] where
          -- Choose one of the following alternatives:
          type Elem [e] = e       -- OK
-         type Elem [x] = x       -- OK
-         type Elem x   = x       -- BAD; shape of 'x' is different to '[e]'
-         type Elem [Maybe x] = x -- BAD: shape of '[Maybe x]' is different to '[e]'
+         type Elem [x] = x       -- BAD; '[x]' is differnet to '[e]' from head
+         type Elem x   = x       -- BAD; 'x' is different to '[e]'
+         type Elem [Maybe x] = x -- BAD: '[Maybe x]' is different to '[e]'
+
+-  The type indexes of the type family that do *not* correspond to
+   class parameters must be distinct type variables, not mentioned
+   in the instance head.  For example: ::
+
+       class C b x where
+          type F a b c :: *
+
+       instance C [v] [w] where
+         -- Choose one of the following alternatives:
+         type C a [v] c = a->c  -- OK; a,c are tyvars
+         type C x [v] y = y->x  -- OK; x,y are tyvars
+         type C x [v] x = x     -- BAD: x is repeated
+         type C x [v] w = x     -- BAD: w is mentioned in instance head
 
--  An instances for an associated family can only appear as part of an
+The effect of these two rules is that the type-family instance
+completely covers the cases covered by the instance head.
+
+-  An instance for an associated family can only appear as part of an
    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 instance for an associated type can be omitted in class
    instances. In that case, unless there is a default instance (see
    :ref:`assoc-decl-defs`), the corresponding instance type is not
    inhabited; i.e., only diverging expressions, such as ``undefined``,
    can assume the type.
 
--  Although it is unusual, there (currently) can be *multiple* instances
-   for an associated family in a single instance declaration. For
-   example, this is legitimate: ::
+-  A historical note.  In the past (but no longer), GHC allowed you to
+   write *multiple* type or data family instances for a single
+   asssociated type.  For example: ::
 
        instance GMapKey Flob where
          data GMap Flob [v] = G1 v
@@ -6501,10 +6524,23 @@ Note the following points:
 
    Here we give two data instance declarations, one in which the last
    parameter is ``[v]``, and one for which it is ``Int``. Since you
-   cannot give any *subsequent* instances for ``(GMap Flob ...)``, this
-   facility is most useful when the free indexed parameter is of a kind
-   with a finite number of alternatives (unlike ``*``). WARNING: this
-   facility may be withdrawn in the future.
+   cannot give any *subsequent* instances for ``(GMap Flob ...)``,
+   this facility was not very useful, except perhaps when the free
+   indexed parameter has a fixed number of alternatives
+   (e.g. ``Bool`). But in that case it is better to define an auxiliary
+   closed type function like this: ::
+
+       class C a where
+         type F a (b :: Bool) :: *
+
+       instance C Int where
+         type F Int b = FInt b
+
+       type family FInt a b where
+         FInt True  = Char
+         FInt False = Bool
+
+    Here the auxiliary type function is ``FInt``.
 
 .. _assoc-decl-defs:
 
index 0fc53e7..0b7b554 100644 (file)
@@ -16,10 +16,10 @@ class C a where
     type D a b
 
 instance C Int where
-    type D Int () = String
+    type D Int b = String
 
 instance C () where
-    type D () () = Bool
+    type D () a = Bool
 
 type family E a where
     E ()  = Bool
index e1ef925..d319bd6 100644 (file)
@@ -1,57 +1,56 @@
-type family A a b :: *         -- Defined at T4175.hs:7:1
-type instance A (B a) b = ()   -- Defined at T4175.hs:10:15
-type instance A (Maybe a) a = a        -- Defined at T4175.hs:9:15
-type instance A Int Int = ()   -- Defined at T4175.hs:8:15
-data family B a        -- Defined at T4175.hs:12:1
-instance G B -- Defined at T4175.hs:34:10
-data instance B () = MkB       -- Defined at T4175.hs:13:15
-type instance A (B a) b = ()   -- Defined at T4175.hs:10:15
-class C a where
-  type family D a b :: *
-       -- Defined at T4175.hs:16:5
-type instance D () () = Bool   -- Defined at T4175.hs:22:10
-type instance D Int () = String        -- Defined at T4175.hs:19:10
-type family E a :: *
-  where
-      E () = Bool
-      E Int = String
-       -- Defined at T4175.hs:24:1
-data () = ()   -- Defined in ‘GHC.Tuple’
-instance C () -- Defined at T4175.hs:21:10
-instance Bounded () -- Defined in ‘GHC.Enum’
-instance Enum () -- Defined in ‘GHC.Enum’
-instance Eq () -- Defined in ‘GHC.Classes’
-instance Ord () -- Defined in ‘GHC.Classes’
-instance Read () -- Defined in ‘GHC.Read’
-instance Show () -- Defined in ‘GHC.Show’
-instance Monoid () -- Defined in ‘GHC.Base’
-type instance D () () = Bool   -- Defined at T4175.hs:22:10
-type instance D Int () = String        -- Defined at T4175.hs:19:10
-data instance B () = MkB       -- Defined at T4175.hs:13:15
-data Maybe a = Nothing | Just a        -- Defined in ‘GHC.Base’
-instance Eq a => Eq (Maybe a) -- Defined in ‘GHC.Base’
-instance Monad Maybe -- Defined in ‘GHC.Base’
-instance Functor Maybe -- Defined in ‘GHC.Base’
-instance Ord a => Ord (Maybe a) -- Defined in ‘GHC.Base’
-instance Read a => Read (Maybe a) -- Defined in ‘GHC.Read’
-instance Show a => Show (Maybe a) -- Defined in ‘GHC.Show’
-instance Applicative Maybe -- Defined in ‘GHC.Base’
-instance Foldable Maybe -- Defined in ‘Data.Foldable’
-instance Traversable Maybe -- Defined in ‘Data.Traversable’
-instance Monoid a => Monoid (Maybe a) -- Defined in ‘GHC.Base’
-type instance A (Maybe a) a = a        -- Defined at T4175.hs:9:15
-data Int = I# Int#     -- Defined in ‘GHC.Types’
-instance C Int -- Defined at T4175.hs:18:10
-instance Bounded Int -- Defined in ‘GHC.Enum’
-instance Enum Int -- Defined in ‘GHC.Enum’
-instance Eq Int -- Defined in ‘GHC.Classes’
-instance Integral Int -- Defined in ‘GHC.Real’
-instance Num Int -- Defined in ‘GHC.Num’
-instance Ord Int -- Defined in ‘GHC.Classes’
-instance Read Int -- Defined in ‘GHC.Read’
-instance Real Int -- Defined in ‘GHC.Real’
-instance Show Int -- Defined in ‘GHC.Show’
-type instance D Int () = String        -- Defined at T4175.hs:19:10
-type instance A Int Int = ()   -- Defined at T4175.hs:8:15
-class Z a      -- Defined at T4175.hs:28:1
-instance F (Z a) -- Defined at T4175.hs:31:10
+type family A a b :: *         -- Defined at T4175.hs:7:1\r
+type instance A (B a) b = ()   -- Defined at T4175.hs:10:15\r
+type instance A (Maybe a) a = a        -- Defined at T4175.hs:9:15\r
+type instance A Int Int = ()   -- Defined at T4175.hs:8:15\r
+data family B a        -- Defined at T4175.hs:12:1\r
+instance G B -- Defined at T4175.hs:34:10\r
+data instance B () = MkB       -- Defined at T4175.hs:13:15\r
+type instance A (B a) b = ()   -- Defined at T4175.hs:10:15\r
+class C a where\r
+  type family D a b :: *\r
+       -- Defined at T4175.hs:16:5\r
+type instance D () a = Bool    -- Defined at T4175.hs:22:10\r
+type instance D Int b = String         -- Defined at T4175.hs:19:10\r
+type family E a :: *\r
+  where\r
+      E () = Bool\r
+      E Int = String\r
+       -- Defined at T4175.hs:24:1\r
+data () = ()   -- Defined in ‘GHC.Tuple’\r
+instance C () -- Defined at T4175.hs:21:10\r
+instance Bounded () -- Defined in ‘GHC.Enum’\r
+instance Enum () -- Defined in ‘GHC.Enum’\r
+instance Eq () -- Defined in ‘GHC.Classes’\r
+instance Ord () -- Defined in ‘GHC.Classes’\r
+instance Read () -- Defined in ‘GHC.Read’\r
+instance Show () -- Defined in ‘GHC.Show’\r
+instance Monoid () -- Defined in ‘GHC.Base’\r
+type instance D () a = Bool    -- Defined at T4175.hs:22:10\r
+data instance B () = MkB       -- Defined at T4175.hs:13:15\r
+data Maybe a = Nothing | Just a        -- Defined in ‘GHC.Base’\r
+instance Eq a => Eq (Maybe a) -- Defined in ‘GHC.Base’\r
+instance Monad Maybe -- Defined in ‘GHC.Base’\r
+instance Functor Maybe -- Defined in ‘GHC.Base’\r
+instance Ord a => Ord (Maybe a) -- Defined in ‘GHC.Base’\r
+instance Read a => Read (Maybe a) -- Defined in ‘GHC.Read’\r
+instance Show a => Show (Maybe a) -- Defined in ‘GHC.Show’\r
+instance Applicative Maybe -- Defined in ‘GHC.Base’\r
+instance Foldable Maybe -- Defined in ‘Data.Foldable’\r
+instance Traversable Maybe -- Defined in ‘Data.Traversable’\r
+instance Monoid a => Monoid (Maybe a) -- Defined in ‘GHC.Base’\r
+type instance A (Maybe a) a = a        -- Defined at T4175.hs:9:15\r
+data Int = I# Int#     -- Defined in ‘GHC.Types’\r
+instance C Int -- Defined at T4175.hs:18:10\r
+instance Bounded Int -- Defined in ‘GHC.Enum’\r
+instance Enum Int -- Defined in ‘GHC.Enum’\r
+instance Eq Int -- Defined in ‘GHC.Classes’\r
+instance Integral Int -- Defined in ‘GHC.Real’\r
+instance Num Int -- Defined in ‘GHC.Num’\r
+instance Ord Int -- Defined in ‘GHC.Classes’\r
+instance Read Int -- Defined in ‘GHC.Read’\r
+instance Real Int -- Defined in ‘GHC.Real’\r
+instance Show Int -- Defined in ‘GHC.Show’\r
+type instance D Int b = String         -- Defined at T4175.hs:19:10\r
+type instance A Int Int = ()   -- Defined at T4175.hs:8:15\r
+class Z a      -- Defined at T4175.hs:28:1\r
+instance F (Z a) -- Defined at T4175.hs:31:10\r
index c81c521..5964262 100644 (file)
       L a = MaybeSyn a -- Defined at <interactive>:49:15
 
 <interactive>:55:41: error:
-    Type family equation violates injectivity annotation.
-    Kind variable ‘k’ cannot be inferred from the right-hand side.
-    (enabling -fprint-explicit-kinds might help)
-    In the type family equation:
-      PolyKindVarsF '[] = '[] -- Defined at <interactive>:55:41
+    • Polymorphic type indexes of associated type ‘PolyKindVarsF’
+        (i.e. ones independent of the class type variables)
+        must be distinct type variables
+      Expected: PolyKindVarsF '[]
+      Actual:   PolyKindVarsF '[]
+      Use -fprint-explicit-kinds to see the kind arguments
+    • In the type instance declaration for ‘PolyKindVarsF’
+      In the instance declaration for ‘PolyKindVarsC '[]’
 
 <interactive>:60:15: error:
     Type family equation violates injectivity annotation.
index 44e5865..2c0ea20 100644 (file)
@@ -20,6 +20,6 @@ class ( m ~ Outer m (Inner m) ) => BugC (m :: * -> *) where
 
 instance BugC (IdT m) where
     type Inner (IdT m) = m
-    type Outer (IdT _) = IdT
+    type Outer (IdT m) = IdT
 
     bug f = IdC f
index 4bd7bde..57a9595 100644 (file)
@@ -8,6 +8,7 @@ class C8 a where
 instance C8 Int where
   data S8 Int a = S8Int a
 
--- Extra argument is not a variable; this is fine
+-- Extra argument is not a variable;
+-- this is now not allowed
 instance C8 Bool where
   data S8 Bool Char = S8Bool
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail10.stderr b/testsuite/tests/indexed-types/should_fail/SimpleFail10.stderr
new file mode 100644 (file)
index 0000000..9b99cd1
--- /dev/null
@@ -0,0 +1,11 @@
+
+SimpleFail10.hs:14:3: error:
+    • Polymorphic type indexes of associated type ‘S8’
+        (i.e. ones independent of the class type variables)
+        must be distinct type variables
+      Expected: S8 Bool <tv>
+      Actual:   S8 Bool Char
+      where the `<tv>' arguments are type variables,
+      distinct from each other and from the instance variables
+    • In the data instance declaration for ‘S8’
+      In the instance declaration for ‘C8 Bool’
index 927c60c..9c1c4a8 100644 (file)
@@ -8,8 +8,7 @@ class C7 a b where
 instance C7 Char (a, Bool) where
   data S7 (a, Bool) = S7_1
 
--- Used to fail, but now passes: 
--- type indexes don't match the instance types by name
--- but do by structure
+-- Fails because the arg to S7 should be the
+-- same as that to C7
 instance C7 Char (a, Int) where
   data S7 (b, Int) = S7_2
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail9.stderr b/testsuite/tests/indexed-types/should_fail/SimpleFail9.stderr
new file mode 100644 (file)
index 0000000..b0c421f
--- /dev/null
@@ -0,0 +1,7 @@
+
+SimpleFail9.hs:14:3: error:
+    • Type indexes must match class instance head
+      Expected: S7 (a, Int)
+      Actual:   S7 (b, Int)
+    • In the data instance declaration for ‘S7’
+      In the instance declaration for ‘C7 Char (a, Int)’
diff --git a/testsuite/tests/indexed-types/should_fail/T11450.hs b/testsuite/tests/indexed-types/should_fail/T11450.hs
new file mode 100644 (file)
index 0000000..59ef495
--- /dev/null
@@ -0,0 +1,9 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module T11450 where
+
+class C x where
+  type T x
+
+instance C (Either a b) where
+  type T (Either b a) = b -> a
diff --git a/testsuite/tests/indexed-types/should_fail/T11450.stderr b/testsuite/tests/indexed-types/should_fail/T11450.stderr
new file mode 100644 (file)
index 0000000..a6fe961
--- /dev/null
@@ -0,0 +1,7 @@
+
+T11450.hs:9:8: error:
+    • Type indexes must match class instance head
+      Expected: T (Either a b)
+      Actual:   T (Either b a)
+    • In the type instance declaration for ‘T’
+      In the instance declaration for ‘C (Either a b)’
index c6f29a4..dfc0326 100644 (file)
@@ -11,8 +11,8 @@ test('SimpleFail5b', normal, compile_fail, [''])
 test('SimpleFail6', normal, compile_fail, [''])
 test('SimpleFail7', normal, compile_fail, [''])
 test('SimpleFail8', normal, compile_fail, [''])
-test('SimpleFail9', normal, compile, [''])
-test('SimpleFail10', normal, compile, [''])
+test('SimpleFail9', normal, compile_fail, [''])
+test('SimpleFail10', normal, compile_fail, [''])
 test('SimpleFail11a', normal, compile_fail, [''])
 test('SimpleFail11b', normal, compile_fail, [''])
 test('SimpleFail11c', normal, compile_fail, [''])
@@ -139,3 +139,4 @@ test('T10817', normal, compile_fail, [''])
 test('T10899', normal, compile_fail, [''])
 test('T11136', normal, compile_fail, [''])
 test('T7788', normal, compile_fail, [''])
+test('T11450', normal, compile_fail, [''])
index f40ed10..3c91db5 100644 (file)
@@ -1,9 +1,9 @@
 
 T10570.hs:10:10: error:
-    Illegal instance declaration for ‘ConsByIdx2 Int a Proxy cls’
-      The coverage condition fails in class ‘ConsByIdx2’
-        for functional dependency: ‘x -> m’
-      Reason: lhs type ‘Int’ does not determine rhs type ‘Proxy’
-      Un-determined variable: k
-      (Use -fprint-explicit-kinds to see the kind variables in the types)
-    In the instance declaration for ‘ConsByIdx2 Int a Proxy cls’
+    • Illegal instance declaration for ‘ConsByIdx2 Int a Proxy cls’
+        The coverage condition fails in class ‘ConsByIdx2’
+          for functional dependency: ‘x -> m’
+        Reason: lhs type ‘Int’ does not determine rhs type ‘Proxy’
+        Un-determined variable: k
+        Use -fprint-explicit-kinds to see the kind arguments
+    • In the instance declaration for ‘ConsByIdx2 Int a Proxy cls’
index 770290d..3f67b0d 100644 (file)
@@ -8,7 +8,7 @@ import Language.Haskell.TH.Ppr
 import System.IO
 
 class C a where
-        data F a (b :: k) :: *
+        data F a b :: *
 
 instance C Int where
         data F Int x = FInt x
index ffa5536..f99d12b 100644 (file)
@@ -1,2 +1,2 @@
-data family T9692.F (a_0 :: k_1) (b_2 :: k_3) :: *
-data instance T9692.F GHC.Types.Int (x_4 :: *) = T9692.FInt x_4
+data family T9692.F (a_0 :: k_1) (b_2 :: *) :: *
+data instance T9692.F GHC.Types.Int x_3 = T9692.FInt x_3
index 44f5024..bb3c93c 100644 (file)
@@ -50,8 +50,8 @@ type MaybeSyn a = Id a
 type family L a = r | r -> a
 type instance L a = MaybeSyn a
 
--- These should fail because given the RHS kind there is no way to determine LHS
--- kind
+-- These should fail because given the RHS kind
+-- there is no way to determine LHS kind
 class PolyKindVarsC a where
     type PolyKindVarsF a = (r :: k) | r -> a
 
index 49e89af..95b9d1b 100644 (file)
@@ -58,11 +58,14 @@ T6018fail.hs:51:15: error:
       L a = MaybeSyn a -- Defined at T6018fail.hs:51:15
 
 T6018fail.hs:59:10: error:
-    Type family equation violates injectivity annotation.
-    Kind variable ‘k’ cannot be inferred from the right-hand side.
-    (enabling -fprint-explicit-kinds might help)
-    In the type family equation:
-      PolyKindVarsF '[] = '[] -- Defined at T6018fail.hs:59:10
+    • Polymorphic type indexes of associated type ‘PolyKindVarsF’
+        (i.e. ones independent of the class type variables)
+        must be distinct type variables
+      Expected: PolyKindVarsF '[]
+      Actual:   PolyKindVarsF '[]
+      Use -fprint-explicit-kinds to see the kind arguments
+    • In the type instance declaration for ‘PolyKindVarsF’
+      In the instance declaration for ‘PolyKindVarsC '[]’
 
 T6018fail.hs:62:15: error:
     Type family equation violates injectivity annotation.
index c151553..6cc0c37 100644 (file)
@@ -1,96 +1,96 @@
 
 T6018failclosed.hs:11:5: error:
-    Type family equation violates injectivity annotation.
-    RHS of injective type family equation cannot be a type family:
-      IdProxyClosed a = IdClosed a -- Defined at T6018failclosed.hs:11:5
-    In the equations for closed type family ‘IdProxyClosed’
-    In the type family declaration for ‘IdProxyClosed’
+    • Type family equation violates injectivity annotation.
+      RHS of injective type family equation cannot be a type family:
+        IdProxyClosed a = IdClosed a -- Defined at T6018failclosed.hs:11:5
+    • In the equations for closed type family ‘IdProxyClosed’
+      In the type family declaration for ‘IdProxyClosed’
 
 T6018failclosed.hs:19:5: error:
-    Type family equation violates injectivity annotation.
-    RHS of injective type family equation is a bare type variable
-    but these LHS type and kind patterns are not bare variables: ‘'Z’
-      PClosed 'Z m = m -- Defined at T6018failclosed.hs:19:5
-    In the equations for closed type family ‘PClosed’
-    In the type family declaration for ‘PClosed’
+    • Type family equation violates injectivity annotation.
+      RHS of injective type family equation is a bare type variable
+      but these LHS type and kind patterns are not bare variables: ‘'Z’
+        PClosed 'Z m = m -- Defined at T6018failclosed.hs:19:5
+    • In the equations for closed type family ‘PClosed’
+      In the type family declaration for ‘PClosed’
 
 T6018failclosed.hs:19:5: error:
-    Type family equations violate injectivity annotation:
-      PClosed 'Z m = m -- Defined at T6018failclosed.hs:19:5
-      PClosed ('S n) m = 'S (PClosed n m)
-        -- Defined at T6018failclosed.hs:20:5
-    In the equations for closed type family ‘PClosed’
-    In the type family declaration for ‘PClosed’
+    • Type family equations violate injectivity annotation:
+        PClosed 'Z m = m -- Defined at T6018failclosed.hs:19:5
+        PClosed ('S n) m = 'S (PClosed n m)
+          -- Defined at T6018failclosed.hs:20:5
+    • In the equations for closed type family ‘PClosed’
+      In the type family declaration for ‘PClosed’
 
 T6018failclosed.hs:25:5: error:
-    Type family equation violates injectivity annotation.
-    Type and kind variables ‘k’, ‘b’
-    cannot be inferred from the right-hand side.
-    (enabling -fprint-explicit-kinds might help)
-    In the type family equation:
-      forall k k1 (b :: k) (c :: k1).
-        JClosed Int b c = Char -- Defined at T6018failclosed.hs:25:5
-    In the equations for closed type family ‘JClosed’
-    In the type family declaration for ‘JClosed’
+    • Type family equation violates injectivity annotation.
+      Type and kind variables ‘k’, ‘b’
+      cannot be inferred from the right-hand side.
+      Use -fprint-explicit-kinds to see the kind arguments
+      In the type family equation:
+        forall k k1 (b :: k) (c :: k1).
+          JClosed Int b c = Char -- Defined at T6018failclosed.hs:25:5
+    • In the equations for closed type family ‘JClosed’
+      In the type family declaration for ‘JClosed’
 
 T6018failclosed.hs:30:5: error:
-    Type family equation violates injectivity annotation.
-    Type variable ‘n’ cannot be inferred from the right-hand side.
-    In the type family equation:
-      KClosed ('S n) m = 'S m -- Defined at T6018failclosed.hs:30:5
-    In the equations for closed type family ‘KClosed’
-    In the type family declaration for ‘KClosed’
+    • Type family equation violates injectivity annotation.
+      Type variable ‘n’ cannot be inferred from the right-hand side.
+      In the type family equation:
+        KClosed ('S n) m = 'S m -- Defined at T6018failclosed.hs:30:5
+    • In the equations for closed type family ‘KClosed’
+      In the type family declaration for ‘KClosed’
 
 T6018failclosed.hs:35:5: error:
-    Type family equation violates injectivity annotation.
-    RHS of injective type family equation cannot be a type family:
-      forall k (a :: k).
-        LClosed a = MaybeSynClosed a -- Defined at T6018failclosed.hs:35:5
-    In the equations for closed type family ‘LClosed’
-    In the type family declaration for ‘LClosed’
+    • Type family equation violates injectivity annotation.
+      RHS of injective type family equation cannot be a type family:
+        forall k (a :: k).
+          LClosed a = MaybeSynClosed a -- Defined at T6018failclosed.hs:35:5
+    • In the equations for closed type family ‘LClosed’
+      In the type family declaration for ‘LClosed’
 
 T6018failclosed.hs:39:5: error:
-    Type family equations violate injectivity annotation:
-      FClosed Char Bool Int = Int -- Defined at T6018failclosed.hs:39:5
-      FClosed Bool Int Char = Int -- Defined at T6018failclosed.hs:40:5
-    In the equations for closed type family ‘FClosed’
-    In the type family declaration for ‘FClosed’
+    • Type family equations violate injectivity annotation:
+        FClosed Char Bool Int = Int -- Defined at T6018failclosed.hs:39:5
+        FClosed Bool Int Char = Int -- Defined at T6018failclosed.hs:40:5
+    • In the equations for closed type family ‘FClosed’
+      In the type family declaration for ‘FClosed’
 
 T6018failclosed.hs:43:5: error:
-    Type family equations violate injectivity annotation:
-      IClosed Int Char Bool = Bool -- Defined at T6018failclosed.hs:43:5
-      IClosed Int Int Int = Bool -- Defined at T6018failclosed.hs:44:5
-    In the equations for closed type family ‘IClosed’
-    In the type family declaration for ‘IClosed’
+    • Type family equations violate injectivity annotation:
+        IClosed Int Char Bool = Bool -- Defined at T6018failclosed.hs:43:5
+        IClosed Int Int Int = Bool -- Defined at T6018failclosed.hs:44:5
+    • In the equations for closed type family ‘IClosed’
+      In the type family declaration for ‘IClosed’
 
 T6018failclosed.hs:49:3: error:
-    Type family equations violate injectivity annotation:
-      E2 'True = 'False -- Defined at T6018failclosed.hs:49:3
-      E2 a = 'False -- Defined at T6018failclosed.hs:50:3
-    In the equations for closed type family ‘E2’
-    In the type family declaration for ‘E2’
+    • Type family equations violate injectivity annotation:
+        E2 'True = 'False -- Defined at T6018failclosed.hs:49:3
+        E2 a = 'False -- Defined at T6018failclosed.hs:50:3
+    • In the equations for closed type family ‘E2’
+      In the type family declaration for ‘E2’
 
 T6018failclosed.hs:50:3: error:
-    Type family equation violates injectivity annotation.
-    Type variable ‘a’ cannot be inferred from the right-hand side.
-    In the type family equation:
-      E2 a = 'False -- Defined at T6018failclosed.hs:50:3
-    In the equations for closed type family ‘E2’
-    In the type family declaration for ‘E2’
+    • Type family equation violates injectivity annotation.
+      Type variable ‘a’ cannot be inferred from the right-hand side.
+      In the type family equation:
+        E2 a = 'False -- Defined at T6018failclosed.hs:50:3
+    • In the equations for closed type family ‘E2’
+      In the type family declaration for ‘E2’
 
 T6018failclosed.hs:61:3: error:
-    Type family equations violate injectivity annotation:
-      F a IO = IO a -- Defined at T6018failclosed.hs:61:3
-      F Char b = b Int -- Defined at T6018failclosed.hs:62:3
-    In the equations for closed type family ‘F’
-    In the type family declaration for ‘F’
+    • Type family equations violate injectivity annotation:
+        F a IO = IO a -- Defined at T6018failclosed.hs:61:3
+        F Char b = b Int -- Defined at T6018failclosed.hs:62:3
+    • In the equations for closed type family ‘F’
+      In the type family declaration for ‘F’
 
 T6018failclosed.hs:66:5: error:
-    Type family equation violates injectivity annotation.
-    Kind variable ‘k’ cannot be inferred from the right-hand side.
-    (enabling -fprint-explicit-kinds might help)
-    In the type family equation:
-      forall k (a :: k) (b :: k).
-        Gc a b = Int -- Defined at T6018failclosed.hs:66:5
-    In the equations for closed type family ‘Gc’
-    In the type family declaration for ‘Gc’
+    • Type family equation violates injectivity annotation.
+      Kind variable ‘k’ cannot be inferred from the right-hand side.
+      Use -fprint-explicit-kinds to see the kind arguments
+      In the type family equation:
+        forall k (a :: k) (b :: k).
+          Gc a b = Int -- Defined at T6018failclosed.hs:66:5
+    • In the equations for closed type family ‘Gc’
+      In the type family declaration for ‘Gc’