Opened 4 years ago

Last modified 3 days ago

#8177 new bug

Roles for type families

Reported by: simonpj Owned by: goldfire
Priority: normal Milestone:
Component: Compiler Version: 7.6.3
Keywords: TypeFamilies Cc: goldfire, int-index, hackage.haskell.org@…, ecrockett0@…, dmcclean, RyanGlScott
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s): Phab:D3662
Wiki Page:

Description

Now that we have roles, it might be helpful to be able to give a role signature for a data/type family.

At the moment, data/type family constructors have all parameters conservatively assigned to be role N. Thus

data family D a    -- Parameter conservatively assumed to be N

class C a where
  op :: D a -> a

instance C Int where ....

newtype N a = MkN a deriving( C )  -- Rejected

The generalised-newtype-deriving clause deriving( C ) is rejected because D might use its parameter at role N thus:

data instance D [b] = MkD (F b)   -- F is a type function

It would be strictly more expressive if we could

  • Declare the roles of D's arguments (as we can declare their kinds). E.g.
    data family D a@R
    
  • Check that each family instance obeys that role signature. E.g. given the preceding role signature, reject this instance:
    data instance D [b] = MkD (F b)   -- F is a type function
    

I think there is no technical difficulty here. Just a question of doing it.

Change History (41)

comment:1 Changed 4 years ago by goldfire

I would argue that, given the declaration for D above, the following instance should also be rejected:

data instance D (Maybe c) = MkD2 c

Why should that instance be rejected? Because it pattern-matches on its argument. Before thinking about implementing this (which I agree should be straightforward), we need to agree on the design. Here are a few questions to spur discussion:

  • What should the default role be for families? Is it different for data and for type families? (I would prefer N for both.)
  • Am I right that the instance above should be rejected?
  • Consider
    type family Flip x@R y@R
    type instance Flip x y = (y, x)
    

Is that accepted? I think "yes".

Here are some proposed rules:

  • If a parameter is at role N, its use is unrestricted in instances.
  • If a parameter is at role R, it cannot be matched against and it must only appear in R (or P) positions in the RHS of instances.
  • If a parameter is at role P, it cannot be matched against and it must only appear in P positions in the RHS of instances.

Thoughts? Let's have the conversation here, and I will put the resolution on the wiki along with writing the implementation.

comment:2 Changed 4 years ago by simonpj

Harump. You are right. type families are the very source of pattern matching so of course type families should have argument of role N.

You could argue that there might be a parameter of the family that is never matched. Thus:

type family F a@R b@N
type instance F a Int = a -> a
type instance F a Bool = (a,a)

But it's a bit marginal; in most cases you could re-order the args

type family F b@N :: * -> *

and similarly for the instances.

I think it's the same for data families. For example, it'd be utterly wrong to make a newtype coercion between (D Age) and (D Int); so D's parameter must clearly be role N.

In short, the main merit of this ticket would be to allow parametric (non-indexed) parameters to appear before index parameters. That seems a fairly marginal gain.

Simon

comment:3 Changed 4 years ago by goldfire

I'm not convinced that this is useless, actually. For example, I don't think Simon's last example F could be written without role annotations on type families, even if we switch the order of parameters. And, the kind signature trick doesn't work at all with data families:

data family Q1 :: * -> *

is equivalent to

data family Q2 a

In particular, under the current implementation, instances of Q1 can pattern-match on the parameter. Accordingly, Q1's parameter is currently given role N, just like Q2's.

So, I do think this idea would yield a real expressiveness gain, and I mused about it while implementing the main chunk of roles. Is it worth the extra complexity? Perhaps.

comment:4 Changed 3 years ago by goldfire

A post on #8672 seems more relevant here:

Simon PJ says: Richard, two questions. First (Q1), can't a data instance have a representational role inferred? Eg this ought to work. The definition of g is currently rejected.

data family T a
data instance T [b] = MkT b

newtype Age = MkAge Int

g :: T [Age] -> T [Int]
g x = coerce x

Second question (Q2). Are role annotations allowed on data family declarations, where they could indicate which parameters are the indices:

type role T representational nominal  -- Only second param can be an index
data family T a b

data instance T a Bool = ...   -- Allowed
data instance T Bool b = ...   -- Rejected

(And similarly for type families.)

Similarly are role annotations allowed on data instance declarations, where they would be useful in exactly the same way that they are on data decls

data family T a

type role T [a] (a:nominal)
data instance T [a] = MkT a

Here we are running out of syntax! This isn't supported now because I think all parameters are automatically nominal (see Q1 for why they shouldn't be).

Simon

comment:5 Changed 3 years ago by goldfire

Owner: set to goldfire

Q1: Yes, that's possible. I didn't do it mostly because my stomach lurched when thinking about parsing role annotation concrete syntax for data family instances -- I was going to wait until someone shouted. I considered having data instances go through role inference without allowing for role annotations, but that meant it would be impossible to create a properly abstract data family instance.

Q2: That's possible but currently unimplemented (see earlier posts to this bug report).

So, if we could just figure out a decent concrete syntax, I could make it all work. The hardest part will be updating the parser and HsSyn stuff. The role inference/checking should be almost no work at all.

As a strawman syntax, what about

type role instance T [nominal]

for the case above. Note the word instance to specify that we're talking about the roles on an instance, not on the family T. Then, role names would appear wherever type variables appear in the corresponding instance declaration. Underscores would be supported in these positions, as well (like normal role annotations). The corresponding data (or newtype) instance would have to be in the same module, as usual. The appearance of the word type (as opposed to data) in the role annotation syntax is regrettable, but it conforms to the universal use of the word type in all role annotations.

Though it makes me want to cry, I suppose we should allow associated role instance annotations, in class instance definitions alongside associated data/newtype instances.

Does anyone out there actually want to use this feature? Eager users would help motivate all this! :)

comment:6 Changed 3 years ago by carter

@goldfire, conflating list syntax seems red flaggy...

comment:7 Changed 3 years ago by carter

that said, having some way of describing these properties seems important, though i'm not sure if i'm sufficiently sophisticated a library author yet to see a use case for myself as yet

comment:8 Changed 3 years ago by goldfire

But that's the annotation for the instance

data instance T [a]

If we had an instance

data instance T (Int, Maybe a)

the role annotation would be

type role instance T (Int, Maybe representational)

for example. (Though, that particular annotation would be a no-op, as representational would be inferred.) I don't believe I'm conflating list syntax here...

comment:9 Changed 3 years ago by carter

you may be right! I'll reread this ticket when i'm a bit more awake :)

comment:10 Changed 3 years ago by simonpj

See also this thread on the GHC users list, which offers (I think) another example of the importance of this feature.

Simon

comment:11 Changed 3 years ago by jwlato

I agree that the vector issue is related to this feature. In summary, we would like the following to work (greatly simplified from vector WLOG):

class MVectorClass (v :: * -> * -> *) a where
    basicLength :: v s a -> Int

data family MVector s a

data instance MVector s Int -- implementation not important

newtype Age = Age Int deriving (MVectorClass MVector) -- rejected

The deriving is rejected because it generates

basicLength =
    coerce (basicLength :: MVector s Int -> Int) :: MVector s Age -> Int

If my understanding of role inference is correct, allowing

type role instance MVector nominal representational

would allow for this coerce to take place.

This means that we can't currently derive Unbox instances for vectors of newtypes (see https://github.com/haskell/vector/issues/16), which is rather unfortunate.

comment:12 Changed 3 years ago by jwlato

Priority: normalhigh

comment:13 Changed 3 years ago by liyang

Cc: hackage.haskell.org@… added

comment:14 Changed 3 years ago by goldfire

Priority: highnormal

Hmm... well, this just got a little more complicated. The full example John just posted would not be solved by fixing this ticket. That's because the data instance for MVector pattern-matches on Int. Currently in GHC, it would be sound to have both the instance given and a separate instance ending in Age, and have these instances be unrelated. Accordingly, if the MVector were declared to have a representational role for its last parameter, the instance given would be rejected for pattern-matching on a representational parameter.

What it seems John wants is something new -- a data family that does representational matching, not nominal matching. Such a beast would consider data instance MVector s Int and data instance MVector s Age to overlap. Along similar lines, if a MVector s Age were requested, GHC would serve up the instance for MVector s Int.

While I can imagine implementing such a feature (essentially by preventing newtypes from appearing in instance declarations, much like how type families can't appear in instance declarations today... and then normalizing with respect to newtypes at usage sites), the ramifications of the design are far from clear. In particular, what if the constructor of a newtype is not available? It would also mean, for example, that if a library exports a newtype Foo abstractly, a user wishing to have an MVector instance for Foo would need to know Foo's representation type, something that the library author thought was hidden from users. It's all a little murky.

So, I'm saying that John's use case does not qualify for this ticket, and I'll un-bump its priority. John, if in light of my analysis (and if you agree with it!) you still want this feature, create a new feature request with the priority you feel is appropriate. This seems related but quite separable to the features requested in this ticket.

comment:15 Changed 3 years ago by jwlato

It's only outside the scope of this request if you insist on the rule that parameters at role R can't be matched against. I think I agree with Richard's analysis that this would entail a data family that does representational matching.

I do think this is a valuable feature as ghc-7.8 broke code some code in the wild, so I'll make a new ticket.

comment:16 Changed 3 years ago by crockeea

Cc: ecrockett0@… added

comment:17 Changed 3 years ago by dmcclean

Cc: dmcclean added

comment:18 Changed 3 years ago by dmcclean

This would be helpful for one implementation that Bjorn Buckwalter and I are working on for the next generation version of the dimensional library.

comment:19 Changed 3 years ago by simonpj

dmcclean: can you say more precisely what "this" is? There are various designs floating about in this ticket, and comment:14 indicates that the one in the Ticket Description would not solve the problem identified in comment:11.

Better still, can you give a concrete, standalone example of what you want/need?

Simon

comment:20 Changed 3 years ago by dmcclean

Yes, my apologies Simon.

This is actually going to be an interesting example, perhaps, because I learned something about this since yesterday when I wrote that comment.

This example is slightly longer than I would like, I'm eliding a few things but I'm not sure exactly which details (e.g. the data family being associated) matter.

class KnownVariant (var :: Variant) where
  -- | A dimensional value, either a 'Quantity' or a 'Unit', parameterized by its 'Dimension' and representation.
  data Dimensional var :: Dimension -> * -> *
  -- elided: some functions to allow us to introduce and eliminate the quantities or units

instance KnownVariant DQuantity where
  newtype Dimensional DQuantity d v = Quantity' v
    deriving (Eq, Ord, Enum)
  -- elided: function implementations

instance KnownVariant (DUnit p) where
  data Dimensional (DUnit p) d v = Unit' UnitName v
  -- elided: function implementations

data Variant = DQuantity | DUnit Prefixability
type Quantity = Dimensional DQuantity
type Unit p = Dimensional (DUnit p)

So I set up all that machinery, and then I was curious whether we could coerce in and out of the Dimensional DQuantity d newtype. So I thought that the way to find out was by asking GHCi what the role of Dimensional was. In concept it's nominal phantom representational, but it would be extremely complicated for the compiler to see that because it would have to examine all the (both the) instances and so forth, so I didn't know what to expect.

Numeric.Units.Dimensional.DK> :i Dimensional
class KnownVariant (var :: Variant) where
  type role Dimensional nominal nominal nominal
  data family Dimensional (var :: Variant) ($a :: Dimension) $b
  ...

So I read that, and thought that it meant we were out of luck.

But, unexpectedly to me, but undoubtedly for a reason that is quite obvious to someone, and this is the part I only discovered last night:

> let x = 3.7 :: Double
> x
3.7
> let y = (coerce x) :: Mass Double
> y
3.7 kg
> let x' = (coerce y) :: Double
> x'
3.7

Somehow it even seems to be OK when you abstract over the dimension with RankNTypes, which isn't really a need but is just something I thought to investigate to see if that was the difference between my expectation of how this would work and how it in fact did work.

> let f = coerce :: (forall d.Double -> Quantity d Double)
> (f 3) :: Mass Double
3.0 kg

In conclusion, I now believe that I was too hasty yesterday, and that in fact this ticket doesn't impact me at all.

My sincere apologies to everyone copied on this ticket. If someone happened to have the time and knew the answer, it would be awesome if you you could help me fix my understanding about whether this should or shouldn't work and what the interplay with roles is, but otherwise I will merrily go about my business. :)

comment:21 Changed 3 years ago by goldfire

Roles for data families (associated or not) cannot be inferred, because they are open. But, theoretically, they can be declared and then checked. That is the subject of this ticket. So, it conceivable to give the roles you ask for.

But, you don't seem to need those roles, because you seem interested in coercing in and out of the newtype, not among different instantiations of the newtype. This is possible as long as the newtype constructor (Quantity') is in scope. Roles aren't a part of the story, in your case.

comment:22 Changed 3 years ago by dmcclean

Hmmm.

I was concerned there for a second, because actually Quantity' won't be in scope for my users. Its not exported from the module because you can use it to do nefarious things.

So I thought that my test in GHCi had been insufficiently thorough, because GHCi doesn't respect the export list and lets you get at unexported things for convenience.

So I made a new module to try it.

import Numeric.Units.Dimensional.DK.Prelude
import Data.Coerce

main = do
         let x = 3.7 :: Double
         let y = (coerce x) :: Mass Double
         putStrLn . show $ y
         -- putStrLn . show $ Quantity' x -- doesn't compile with this line here

It works just fine and prints "3.7 m". With the commented line it doesn't compile, complaining that Quantity' is (as I intended) not in scope. (If it had been in scope, it would still fail because the dimension is ambiguous, but that's not the point.)

So it seems that whether or not the newtype constructor is in scope is not the determining factor here. If it was intended to be, than this may be a bug?

comment:23 Changed 3 years ago by goldfire

That does look fishy, but I don't see a definition of Mass so I can be sure. Do you have a minimal test case, or a way I can check this myself? If so, please post that as a new ticket, as it's only very tangentially related to this one. Thanks!

comment:24 in reply to:  22 Changed 3 years ago by rwbarton

Replying to dmcclean:

Hmmm.

I was concerned there for a second, because actually Quantity' won't be in scope for my users. Its not exported from the module because you can use it to do nefarious things.

BTW I'm confused by this comment, because the things you can do with Quantity' are just the things you can do with coerce, no?

comment:25 Changed 3 years ago by dmcclean

Yes. I was badly confused when I wrote that comment, sorry.

See 9580 for where I broke this out as requested by goldfire. It turns out that the rule is indeed supposed to be that you can only do this coercion when Quantity' is in scope, which makes sense because that is when you could do it longhand, but that 7.8.3 currently implements a more lenient unintentional rule that also lets you do it (at least sometimes?) when you only have the data family in scope.

comment:26 Changed 3 years ago by goldfire

Milestone:

comment:27 Changed 3 years ago by goldfire

In trying to sweep up remaining tickets assigned to me before the feature freeze, I came across this one.

In comment:5, I ask for real users who want role annotations for type and/or data families (and/or their respective instances) to do real work -- preferably with an example of said real work. Though two people came out of the woodwork and tried to meet this need, neither one really qualifies:

  • The example from jwlato requires something fundamentally different from this ticket -- the ability to do representational matching on families. That, essentially, has been moved to #9112. The solution there may also require getting this ticket sorted out, but I don't think this ticket is the blocking issue.
  • The example from dmmclean is also, by dmmclean's own admission, not applicable here.

Fixing this would take several days worth of work, and days are precious. So I'm going to let this one slip unless convinced otherwise. Thanks!

comment:28 Changed 3 years ago by goldfire

Making a note here to look at :browse and :info in GHCi if/when we implement this. See also #8672.

comment:29 Changed 3 years ago by jwlato

Just a quick note to verify that goldfire is entirely correct WRT #9112; I agree that my example doesn't have much bearing on this ticket at this point.

comment:30 Changed 17 months ago by thomie

Keywords: TypeFamilies added

comment:31 Changed 11 months ago by RyanGlScott

Cc: RyanGlScott added

goldfire, I do have a need for this in order to do "real work"... at some point in the future after #9123 is fixed :)

My use case is laid out in this comment in #8516. I'm interested in using higher-kinded roles to increase the number of datatypes for which you can derive Generic1 instances by replacing Functor constraints with Representational constraints (where Representational is the typeclass proposed here). Unfortunately, at the moment, my proposed plan would actually decrease that number, because there are datatypes defined in terms of type families for which you can declare Functor instances. However, type families always default to nominal roles for its type arguments, which means they can't be Representational! Ack!

It definitely seems like some type families should be able to have Representational (or even Phantom!) roles for its arguments. A prime example is from this comment:

type family Id a where
  Id a = a

I have a strong hunch that a should be have a representational role. Unfortunately, I have no way to inform GHC of this.

comment:32 Changed 3 months ago by glguy

I'd like to share my usecase for wanting this feature

Given the following type:

-- | Family of N-ary operator types.
type family Op n a b where
  Op 'Z     a b = b
  Op ('S n) a b = a -> Op n a b

I'd love to be able to

coerce :: Coercible a b => Op n a c -> Op n b c

comment:33 Changed 3 months ago by int-index

I want this feature too. My use case is this:

data family EffDict (eff :: k) (m :: Type -> Type)

this data family represents effect methods for some monad m. Its data instances match on eff only, never on m. For example:

data StateEff s
data instance EffDict (StateEff s) m =
  StateDict
    { _state :: forall a . (s -> (a,s)) -> m a,
      _get :: m s,
      _put :: s -> m () }

Define a composition of monad transformers as follows:

newtype TComp t1 t2 m a = TComp (t1 (t2 m) a)

Then I want to be able to do this:

coerce :: Dict eff (t1 (t2 m)) -> Dict eff (TComp t1 t2 m)

comment:34 Changed 3 months ago by int-index

Cc: int-index added

comment:35 Changed 7 days ago by RyanGlScott

Differential Rev(s): Phab:D3662

I've uploaded a rough attempt at implementing support for roles for closed type families at Phab:D3662, although there are still some bugs to work out (for instance, the program in comment:32 doesn't typecheck yet, unfortunately).

comment:36 Changed 5 days ago by simonpj

I've uploaded a rough attempt at implementing support for roles for closed type families

Great work! But I really would prefer to see a specification first :-). There's a lot of discussion on this thread about what the specification should even be.

It's hard to review an implementation without a spec, covering

  • Syntax
  • Typing rules (at least in clear English)
  • Lots of examples

Of course, we'd ultimately like a proof of soundness of the rules, but the "Richard thinks this is right" tests is at least a start.

comment:37 Changed 3 days ago by RyanGlScott

Indeed, I will readily admit that I'm mostly parking this Diff here for Richard's sake (when he gets a chance to look at it). However, since you asked politely, I wrote up an (informal) specification of how I envision this would work here, based on the conversations I've had with Richard about this topic, as well as the commentary in this ticket.

comment:38 Changed 3 days ago by goldfire

I've commented on the wiki page (the specification) and on the diff.

comment:39 Changed 3 days ago by RyanGlScott

Thanks for replying, Richard! I'll respond to your comments here (since I don't like using wiki pages as a medium of conversation).

RAE: "feels"? Let's prove it! End RAE

Hoo boy, I was afraid you were going to demand a proof. I certainly don't have one at the moment.

RAE: There is a difference between roles for data families and data instances. And both might usefully have role annotations. For example:

data family DF a b
type role DF nominal representational

data instance DF Int b = MkDFInt b
 -- NB: No scrutinizing the second parameter.
 -- Also, b is not used in a nominal context

data instance DF [c] b = MkDFList c b
type role DF [nominal] representational

data instance DF (Maybe d) b = MkDFMaybe d b
type role DF (Maybe representational) representational

With this, we have Coercible (DF (Maybe Age) Int) (DF (Maybe Int) Age) but not Coercible (DF [Age] Int) (DF [Int] Age).

Ah, I think there's a bit of confusion regarding the extent of this design. To be clear, I am not proposing that we give users the power to specify roles the type variables in each equation, only the type variables of the parent type family itself. This is because:

  1. As your example hints at, we'd need to invent a new syntax for role annotations that match on particular types, and I don't feel anywhere near motivated enough to implement that.
  2. The current implementation of role inference does not lend itself well to this design. GHC assigns roles by using a map from TyCon names to roles, but type family equations have neither TyCons nor any kind of unique identifier from which we could look up its roles after inference.
  3. This kind of power isn't necessary for the kind of stuff I'd want to do anyways. All I really care about is that the second parameter is designated as representational. I don't really want the ability to coerce between DF (Maybe Age) Int and DF (Maybe Age) Int.

So in your above example:

data family DF a b
type role DF nominal representational
data instance DF [c] b = MkDFList c b
data instance DF (Maybe d) b = MkDFMaybe d b

I would propose that the tyvars in any type pattern which saturates a should inherit the role of a, so c and d would get role nominal in their respective equations. It's not as permissive as it could be, but for reasons that I explained above (and I'll make a note of this in the wiki).

I'm a bit worried about problems with what happens if a type constructor that appears as part of a type pattern for an instance is actually a newtype with a role annotation -- could we be breaking soundness with this? Need to think harder.

I don't understand this point.

RAE: This works well for closed type families, but is ineffective with open type/data families (associated or not). I propose that open families default to nominal roles. This is quite like how open families' type variables default to kind Type. Edit: I see this addressed below, but the opening paragraph for this section mentions inference for open families. End RAE

Yep, that's my bad. I'll update the intro so as not to mislead readers.

comment:40 in reply to:  39 ; Changed 3 days ago by goldfire

Replying to RyanGlScott:

Hoo boy, I was afraid you were going to demand a proof. I certainly don't have one at the moment.

"Demand"? No. But it would be nice if the design could at least update the various relevant judgments in the "Safe coercions" paper (use the JFP version). It shouldn't be terribly much work, and it's likely that the process of doing so will reveal any glaring problems. And once you have the updated judgments, it's also not terribly hard to follow along the JFP proof and see what lemmas have to be updated.

I'm always daunted by having to revisit the type safety proof. But every time I go through the process, my brain feels nice, limber, and at peace. It's all very much like a good yoga session: it's hard to find the time to do it, it involves painful contortions, and yet you feel quite good at the end.

Ah, I think there's a bit of confusion regarding the extent of this design. To be clear, I am not proposing that we give users the power to specify roles the type variables in each equation, only the type variables of the parent type family itself.

Note that instance-specific roles apply only to data families, not type families.

This is because:

  1. As your example hints at, we'd need to invent a new syntax for role annotations that match on particular types, and I don't feel anywhere near motivated enough to implement that.

And neither was I, as you'll see in my comment:5.

  1. The current implementation of role inference does not lend itself well to this design. GHC assigns roles by using a map from TyCon names to roles, but type family equations have neither TyCons nor any kind of unique identifier from which we could look up its roles after inference.

This isn't as bad as you say. Data family instances do have a TyCon. See the DataFamilyInst constructor of FamInstEnv.FamFlavor.

  1. This kind of power isn't necessary for the kind of stuff I'd want to do anyways. All I really care about is that the second parameter is designated as representational. I don't really want the ability to coerce between DF (Maybe Age) Int and DF (Maybe Age) Int.

So perhaps you want just roles for type families for now, not data families.

So in your above example:

data family DF a b
type role DF nominal representational
data instance DF [c] b = MkDFList c b
data instance DF (Maybe d) b = MkDFMaybe d b

I would propose that the tyvars in any type pattern which saturates a should inherit the role of a, so c and d would get role nominal in their respective equations. It's not as permissive as it could be, but for reasons that I explained above (and I'll make a note of this in the wiki).

But any time a pattern introduces a new tyvar (that's not just a renaming of the tycon tyvar), then the "parent" tyvar's role is always nominal (because you're doing pattern matching). As you note, this is not as permissive as possible. But, I would argue that if you were as permissive as possible, then you'd have no way of making a fully-abstract data family instance. So your design is self-consistent.

I'm a bit worried about problems with what happens if a type constructor that appears as part of a type pattern for an instance is actually a newtype with a role annotation -- could we be breaking soundness with this? Need to think harder.

I don't understand this point.

I was worried about something like this:

newtype Inty a = MkInty Int
type role Inty representational  -- just because I can

data family F a
type role F nominal

data instance F (Inty a) = MkF a
type role F (Inty nominal)

Is this a good idea? I don't know. Keep in mind that data families are injective.

comment:41 in reply to:  40 Changed 3 days ago by RyanGlScott

Replying to goldfire:

I'm always daunted by having to revisit the type safety proof.

It's doubly daunting for me because I wouldn't be revisiting the proof—I'd be trudging through it for the first time. :)

Not to say that I'm not willing to do this at some point, but it will take me a significant amount of time to invest in understanding the terminology (keep in mind I'm far from an expert on the intricacies of System FC), not to mention figuring out how to typeset all of those crazy typing judgments in TeX.

So perhaps you want just roles for type families for now, not data families.

Well, I do want to have roles for data families at some point (I started with closed type families since they're considerably easier to implement). I just don't want to worry about the additional baggage that per-data-instance role annotations would entail.

But any time a pattern introduces a new tyvar (that's not just a renaming of the tycon tyvar), then the "parent" tyvar's role is always nominal (because you're doing pattern matching). As you note, this is not as permissive as possible. But, I would argue that if you were as permissive as possible, then you'd have no way of making a fully-abstract data family instance. So your design is self-consistent.

Absolutely. I'm fine with making nominal roles be overly restrictive, since it dodges thorny issues like data abstraction...

I was worried about something like this:

newtype Inty a = MkInty Int
type role Inty representational  -- just because I can

data family F a
type role F nominal

data instance F (Inty a) = MkF a
type role F (Inty nominal)

Is this a good idea? I don't know. Keep in mind that data families are injective.

...and this sort of thing as well.

Note: See TracTickets for help on using tickets.