Re: [Haskell-cafe] [ghc-proposals/cafe] Partially applied type families

I'm going to respond just to the few points that concern me directly.

On Jun 2, 2017, at 9:34 AM, Anthony Clayden wrote:

...

...

There's a persistent problem for the compiler testing for type equality: the usage sites must have the types grounded. It's often more successful to prove disequality.

That's straight out of the HList paper [2], Section 9 "By chance or by design?". "We should point out however groundness issues. If TypeEq is to return HTrue, the types must be ground; TypeEq can return HFalse even for unground types, provided they are instantiated enough to determine that they are not equal."

While this may be true for HList's TypeEq, it is not true for closed type families. If we have

type family Equals a b where Equals a a = True Equals a b = False

then (Equals [a] [a]) will reduce to True, even if `a` is universally bound. Indeed, even (Equals a a) will reduce to True. So there is no groundness issue any more.

...

and also:

...

...

I suspect that for the compiler, Instance Chains will be as problematic for type inference as with Closed Type Families: CTFs have a lot of searching under the covers to 'look ahead' for equations that can safely match.

That's from Richard, particularly this comment [3]. The whole blog post is relevant here, I think.

I'm not sure where you're getting "look ahead" from. Closed type families -- and that post, as far as I can tell -- don't discuss looking ahead. Instead, closed type families are all about looking *behind*, considering previous equations (only) when working with a later one.

I think the situation has changed with the introduction of Type Families. They weren't applicable in 2010. So not relevant to the Instance Chains paper.

Type families were introduced in 2005, I believe. At least, that's when the papers were written. I don't know what version of GHC first included them, but I think it was before 2010.

"Look ahead" is exactly what Richard is describing in the bulk of that blog post.

I disagree here: that blog post was about what I now call compatibility, which is a property between equations, independent of a type that we're trying to reduce. There's no looking ahead. Richard