Two distinct Notes named "Eta reduction for data families"
I noticed recently that there are two places in the code base named Note [Eta reduction for data families]
, but with entirely different contents. One is in CoAxiom
:
Note [Eta reduction for data families]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this
data family T a b :: *
newtype instance T Int a = MkT (IO a) deriving( Monad )
We'd like this to work.
From the 'newtype instance' you might think we'd get:
newtype TInt a = MkT (IO a)
axiom ax1 a :: T Int a ~ TInt a -- The newtype-instance part
axiom ax2 a :: TInt a ~ IO a -- The newtype part
But now what can we do? We have this problem
Given: d :: Monad IO
Wanted: d' :: Monad (T Int) = d |> ????
What coercion can we use for the ???
Solution: eta-reduce both axioms, thus:
axiom ax1 :: T Int ~ TInt
axiom ax2 :: TInt ~ IO
Now
d' = d |> Monad (sym (ax2 ; ax1))
----- Bottom line ------
For a CoAxBranch for a data family instance with representation
TyCon rep_tc:
- cab_tvs (of its CoAxiom) may be shorter
than tyConTyVars of rep_tc.
- cab_lhs may be shorter than tyConArity of the family tycon
i.e. LHS is unsaturated
- cab_rhs will be (rep_tc cab_tvs)
i.e. RHS is un-saturated
- 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 for a /type/ family
- cab_lhs has the exact arity of the family tycon
There are certain situations (e.g., pretty-printing) where it is necessary to
deal with eta-expanded data family instances. For these situations, the
cab_eta_tvs field records the stuff that has been eta-reduced away.
So if we have
axiom forall a b. F [a->b] = D b a
and cab_eta_tvs is [p,q], then the original user-written definition
looked like
axiom forall a b p q. F [a->b] p q = D b a p q
(See #9692, #14179, and #15845 for examples of what can go wrong if
we don't eta-expand when showing things to the user.)
(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.)
And the other is in TcInstDcls
:
Note [Eta-reduction for data families]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
data D :: * -> * -> * -> * -> *
data instance D [(a,b)] p q :: * -> * where
D1 :: blah1
D2 :: blah2
Then we'll generate a representation data type
data Drep a b p q z where
D1 :: blah1
D2 :: blah2
and an axiom to connect them
axiom AxDrep forall a b p q z. D [(a,b]] p q z = Drep a b p q z
except that we'll eta-reduce the axiom to
axiom AxDrep forall a b. D [(a,b]] = Drep a b
There are several fiddly subtleties lurking here
* The representation tycon Drep is parameerised over the free
variables of the pattern, in no particular order. So there is no
guarantee that 'p' and 'q' will come last in Drep's parameters, and
in the right order. So, if the /patterns/ of the family insatance
are eta-redcible, we re-order Drep's parameters to put the
eta-reduced type variables last.
* Although we eta-reduce the axiom, we eta-/expand/ the representation
tycon Drep. The kind of D says it takses four arguments, but the
data instance header only supplies three. But the AlgTyCOn for Drep
itself must have enough TyConBinders so that its result kind is Type.
So, with etaExpandAlgTyCon we make up some extra TyConBinders
* The result kind in the instance might be a polykind, like this:
data family DP a :: forall k. k -> *
data instance DP [b] :: forall k1 k2. (k1,k2) -> *
So in type-checking the LHS (DP Int) we need to check that it is
more polymorphic than the signature. To do that we must skolemise
the siganture and istantiate the call of DP. So we end up with
data instance DP [b] @(k1,k2) (z :: (k1,k2)) where
Note that we must parameterise the representation tycon DPrep over
'k1' and 'k2', as well as 'b'.
The skolemise bit is done in tc_kind_sig, while the instantiate bit
is done by tcFamTyPats.
* Very fiddly point. When we eta-reduce to
axiom AxDrep forall a b. D [(a,b]] = Drep a b
we want the kind of (D [(a,b)]) to be the same as the kind of
(Drep a b). This ensures that applying the axiom doesn't change the
kind. Why is that hard? Because the kind of (Drep a b) depends on
the TyConBndrVis on Drep's arguments. In particular do we have
(forall (k::*). blah) or (* -> blah)?
We must match whatever D does! In #15817 we had
data family X a :: forall k. * -> * -- Note: a forall that is not used
data instance X Int b = MkX
So the data instance is really
data istance X Int @k b = MkX
The axiom will look like
axiom X Int = Xrep
and it's important that XRep :: forall k * -> *, following X.
To achieve this we get the TyConBndrVis flags from tcbVisibilities,
and use those flags for any eta-reduced arguments. Sigh.
* The final turn of the knife is that tcbVisibilities is itself
tricky to sort out. Consider
data family D k :: k
Then consider D (forall k2. k2 -> k2) Type Type
The visibilty flags on an application of D may affected by the arguments
themselves. Heavy sigh. But not truly hard; that's what tcbVisibilities
does.
This is rather confusing. I suggest that either:
- The two Notes be combined into one Note.
- The two Notes be given different names to set them apart.