Representation of patterns in type family equations
Type patterns in type family equations
Type family equations are represented with the data type FamEqn
:
data FamEqn pass rhs
= FamEqn
{ feqn_ext :: XCFamEqn pass rhs
, feqn_tycon :: LIdP pass
, feqn_bndrs :: HsOuterFamEqnTyVarBndrs pass -- ^ Optional quantified type vars
, feqn_pats :: HsTyPats pass
, feqn_fixity :: LexicalFixity -- ^ Fixity used in the declaration
, feqn_rhs :: rhs
}
The feqn_pats
field represents the left-hand side of a type instance, its type HsTyPats
is defined as follows:
type HsTyPats pass = [LHsTypeArg pass]
type LHsTypeArg p = HsArg p (LHsType p) (LHsKind p)
data HsArg p tm ty
= HsValArg tm -- Argument is an ordinary expression (f arg)
| HsTypeArg !(LHsToken "@" p) ty -- Argument is a visible type application (f @ty)
| HsArgPar SrcSpan -- See Note [HsArgPar]
Example. Consider the type family instance type instance F2 @(j -> j) Int = Any :: j -> j
(taken from T23512b.hs
). Its type patterns are:
@(j -> j)
Int
We call those "type patterns" by analogy with term-level functions, where a function equation f p1 p2 = ...
has patterns p1
and p2
on the left-hand side.
Type patterns in constructor patterns
Now, a rather interesting development is that !10725 (merged) introduces a different notion of type patterns. It defines the following data type:
data HsTyPat pass
= HsTP { hstp_ext :: XHsTP pass -- ^ After renamer: 'HsTyPatRn'
, hstp_body :: LHsType pass -- ^ Main payload (the type itself)
}
| XHsTyPat !(XXHsTyPat pass)
type LHsTyPat pass = XRec pass (HsTyPat pass)
This data type is more analogous to HsPatSigType
, and it is used to represent type arguments in constructor patterns.
Example. Consider the function equation tyApp (Con @kx @ax (x :: Proxy ax)) = x :: Proxy (ax :: kx)
(taken from TyAppPat_KindDependency.hs
). The constructor pattern Con
has these arguments:
@kx
@ax
(x :: Proxy ax)
The first two of those (@kx
and @ax
) are type patterns, and the third one (x :: Proxy ax)
is a term/value pattern.
Problem
Both of these notions of a "type pattern" make sense on their own, but they are not the same. Any reasonable person would expect HsTyPats
to be a list of HsTyPat
, but that's not the case.
Solution 1: Change terminology
One way to look at this is that it's simply a naming issue. Just rename HsTyPats
to HsFamEqnPats
. This way we sidestep the problem by using different terminology for type patterns in type family instances and type patterns in constructor patterns.
Solution 2: Unify notions of type patterns
A more principled approach is to ask whether those two notions of type patterns are distinct for fundamental or historical reasons.
- if there are fundamental reasons to treat type patterns in type family instances and type patterns in constructor patterns differently, those reasons must be documented in a
Note
; - if those reasons are historical, we should simply refactor the code to use a single, unified notion of type patterns.
Such a refactoring would also allow us to move HsArg
from Language.Haskell.Syntax
to GHC.Hs
(@simonpj suggests this in !10725 (comment 512799)).
One immediate obstacle that comes to mind is that HsTyPats
tracks the presence or absence of @
for each pattern, whereas HsTyPat
assumes that it's already under @
. We could probably address this by pairing each HsTyPat
with a HsBndrVis
flag like this:
type HsTyPats pass = [(HsBndrVis pass, LHsTyPat pass)]
Another interesting question is how this relates to @a
-binders in lambdas (not implemented yet). What representation do we want for the patterns in f @a (x :: a) @b (y :: b) = ...
? Seems like we need to track @
there as well. Perhaps a wise thing to do would be to think ahead and come up with a representation of patterns that is suitable for both types and terms. Actually, HsArg
seems like it fits the bill, but I'm not entirely sure.
The bottom line is that it would be nice to clean up all of this, but it's not clear to me how exactly. Others might have opinions or suggestions.