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

[Richard Eisenberg]

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

> On Jun 2, 2017, at 9:34 AM, Anthony Clayden <anthony_clayden at clear.net.nz> 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