Comments only

compiler/typecheck/TcTyClsDecls.hs

@@ -913,8 +913,8 @@ Then:
   * During TcHsType.tcTyVar we look in the *local* env, to get the
     fully-known, not knot-tied TcTyCon for T.
 
-  * Then, in TcHsSyn.zonkTcTypeToType (and zonkTcTyCon in particular) we look in
-    the *global* env to get the TyCon.
+  * Then, in TcHsSyn.zonkTcTypeToType (and zonkTcTyCon in particular)
+    we look in the *global* env to get the TyCon.
 
 This fancy footwork (with two bindings for T) is only necessary for the
 TyCons or Classes of this recursive group.  Earlier, finished groups,
@@ -929,19 +929,19 @@ is done by establishing an "initial kind", which is a rather uninformed
 guess at a tycon's kind (by counting arguments, mainly) and then
 using this initial kind for recursive occurrences.
 
-The initial kind is stored in exactly the same way during kind-checking
-as it is during type-checking (Note [Type checking recursive type and class
-declarations]): in the *local* environment, with ATcTyCon. But we still
-must store *something* in the *global* environment. Even though we
-discard the result of kind-checking, we sometimes need to produce error
-messages. These error messages will want to refer to the tycons being
-checked, except that they don't exist yet, and it would be Terribly
-Annoying to get the error messages to refer back to HsSyn. So we
-create a TcTyCon and put it in the global env. This tycon can
-print out its name and knows its kind,
-but any other action taken on it will panic. Note
-that TcTyCons are *not* knot-tied, unlike the rather valid but
-knot-tied ones that occur during type-checking.
+The initial kind is stored in exactly the same way during
+kind-checking as it is during type-checking (Note [Type checking
+recursive type and class declarations]): in the *local* environment,
+with ATcTyCon. But we still must store *something* in the *global*
+environment. Even though we discard the result of kind-checking, we
+sometimes need to produce error messages. These error messages will
+want to refer to the tycons being checked, except that they don't
+exist yet, and it would be Terribly Annoying to get the error messages
+to refer back to HsSyn. So we create a TcTyCon and put it in the
+global env. This tycon can print out its name and knows its kind, but
+any other action taken on it will panic. Note that TcTyCons are *not*
+knot-tied, unlike the rather valid but knot-tied ones that occur
+during type-checking.
 
 Note [Declarations for wired-in things]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1482,12 +1482,15 @@ tcTyFamInstEqn fam_tc mb_clsinfo
     tcFamTyPats fam_tc mb_clsinfo tv_names pats
                 (kcTyFamEqnRhs mb_clsinfo hs_ty) $
                     \tvs pats res_kind ->
-    do { rhs_ty <- solveEqualities $ tcCheckLHsType hs_ty res_kind
-
+    do { traceTc "tcTyFamInstEqn {" (ppr eqn_tc_name <+> ppr pats)
+       ; rhs_ty <- solveEqualities $ tcCheckLHsType hs_ty res_kind
+       ; traceTc "tcTyFamInstEqn 1" (ppr eqn_tc_name <+> ppr pats)
        ; (ze, tvs') <- zonkTyBndrsX emptyZonkEnv tvs
+       ; traceTc "tcTyFamInstEqn 2" (ppr eqn_tc_name <+> ppr pats)
        ; pats'      <- zonkTcTypeToTypes ze pats
+       ; traceTc "tcTyFamInstEqn 3" (ppr eqn_tc_name <+> ppr pats $$ ppr rhs_ty)
        ; rhs_ty'    <- zonkTcTypeToType ze rhs_ty
-       ; traceTc "tcTyFamInstEqn" (ppr fam_tc <+> pprTyVars tvs')
+       ; traceTc "tcTyFamInstEqn 4" (ppr fam_tc <+> pprTyVars tvs')
        ; return (mkCoAxBranch tvs' [] pats' rhs_ty'
                               (map (const Nominal) tvs')
                               loc) }

compiler/types/CoAxiom.hs

@@ -222,6 +222,8 @@ data CoAxBranch
                                     -- See Note [CoAxiom locations]
     , cab_tvs      :: [TyVar]       -- Bound type variables; not necessarily fresh
                                     -- See Note [CoAxBranch type variables]
+                                    -- May be eta-reduded; see FamInstEnv
+                                    -- Note [Eta reduction for data families]
     , cab_cvs      :: [CoVar]       -- Bound coercion variables
                                     -- Always empty, for now.
                                     -- See Note [Constraints in patterns]

compiler/types/FamInstEnv.hs

@@ -191,22 +191,31 @@ Solution: eta-reduce both axioms, thus:
 Now
    d' = d |> Monad (sym (ax2 ; ax1))
 
-This eta reduction happens for data instances as well as newtype
-instances. Here we want to eta-reduce the data family axiom.
-All this is done in TcInstDcls.tcDataFamInstDecl.
+----- Bottom line ------
 
-See also Note [Newtype eta] in TyCon.
+For a FamInst with fi_flavour = DataFamilyInst rep_tc,
+
+  - fi_tvs (and cab_tvs of its CoAxiom) may be shorter
+    than tyConTyVars of rep_tc.
 
-Bottom line:
-  For a FamInst with fi_flavour = DataFamilyInst rep_tc,
-  - fi_tvs may be shorter than tyConTyVars of rep_tc.
   - fi_tys may be shorter than tyConArity of the family tycon
        i.e. LHS is unsaturated
+
   - fi_rhs will be (rep_tc fi_tvs)
        i.e. RHS is un-saturated
 
-  But when fi_flavour = SynFamilyInst,
+  - This eta reduction happens for data instances as well
+    as newtype instances. Here we want to eta-reduce the data family axiom.
+
+  - This eta-reduction is done in TcInstDcls.tcDataFamInstDecl.
+
+But when fi_flavour = SynFamilyInst,
   - fi_tys has the exact arity of the family tycon
+
+
+(See also Note [Newtype eta] in TyCon.  This is notionally separate
+and deals with the axiom connecting a newtype with its representation
+type; but it too is eta-reduced.)
 -}
 
 -- Obtain the axiom of a family instance

compiler/types/TyCon.hs

@@ -1172,6 +1172,9 @@ so the coercion tycon CoT must have
         kind:    T ~ []
  and    arity:   0
 
+This eta-reduction is implemented in BuildTyCl.mkNewTyConRhs.
+
+
 ************************************************************************
 *                                                                      *
                  TyConRepName